Anomaly "in build_signature: not enough products." during `rewrite` with dependent occurrences

[vfukala]

Description of the problem

$ rocq c -bt ./Bug.v
File "./Bug.v", line 19, characters 2-20:
Error: Anomaly "in build_signature: not enough products."
Please report at http://rocq-prover.org/bugs/.
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Rewrite.GlobalBindings.build_signature.aux in file "tactics/rewrite.ml", line 300, characters 42-79
Called from Rewrite.GlobalBindings.build_signature.aux in file "tactics/rewrite.ml", line 308, characters 14-68
Called from Rewrite.GlobalBindings.build_signature.aux in file "tactics/rewrite.ml", line 308, characters 14-68
Called from Rewrite.resolve_morphism in file "tactics/rewrite.ml", line 797, characters 16-72
Called from Rewrite.subterm.aux.rewrite_args in file "tactics/rewrite.ml", line 1026, characters 22-76
Called from Rewrite.general_s_rewrite.(fun) in file "tactics/rewrite.ml", line 1929, characters 20-95
Called from Rewrite.apply_strategy in file "tactics/rewrite.ml", lines 1514-1516, characters 15-62
Called from Rewrite.cl_rewrite_clause_aux in file "tactics/rewrite.ml", line 1556, characters 11-58
Called from Rewrite.cl_rewrite_clause_newtac.(fun) in file "tactics/rewrite.ml", line 1657, characters 8-73
Called from Proofview.Goal.enter.f in file "engine/proofview.ml", line 1183, characters 40-46
Called from Proofview.Goal.enter.(fun) in file "engine/proofview.ml", line 1188, characters 10-34
Called from Logic_monad.BackState.(>>=).(fun) in file "engine/logic_monad.ml", line 194, characters 38-43
Called from Logic_monad.BackState.split.(fun) in file "engine/logic_monad.ml", line 263, characters 6-27
Called from Logic_monad.NonLogical.run in file "engine/logic_monad.ml", line 117, characters 8-12
Called from Proofview.apply.(fun) in file "engine/proofview.ml", line 250, characters 12-42
Called from Proof.run_tactic in file "proofs/proof.ml", line 321, characters 4-49
Called from Proof.solve in file "proofs/proof.ml", line 459, characters 36-57
Called from ComTactic.solve_core.(fun) in file "vernac/comTactic.ml", line 49, characters 23-59
Called from Declare.Proof.map_fold_endline in file "vernac/declare.ml", line 1785, characters 20-33
Called from ComTactic.solve_core in file "vernac/comTactic.ml", lines 46-53, characters 23-22
Called from Vernactypes.vtmodifyproof.(fun) in file "vernac/vernactypes.ml", line 185, characters 32-47
Called from Vernactypes.typed_vernac.(fun) in file "vernac/vernactypes.ml", line 170, characters 65-71
Called from Vernactypes.run.(fun) in file "vernac/vernactypes.ml", line 164, characters 15-32
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", line 126, characters 16-23
Called from Vernactypes.OpaqueAccess.runner.(fun) in file "vernac/vernactypes.ml", line 114, characters 30-34
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", lines 125-127, characters 14-41
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", line 126, characters 16-23
Called from Vernactypes.Proof.runner.(fun) in file "vernac/vernactypes.ml", line 72, characters 19-22
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", lines 125-127, characters 14-41
Called from Vernactypes.Prog.runner.(fun) in file "vernac/vernactypes.ml", line 27, characters 30-34
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", lines 124-128, characters 12-39
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", lines 124-128, characters 12-39
Called from Vernactypes.run in file "vernac/vernactypes.ml", lines 163-164, characters 14-47
Called from Vernacinterp.interp_expr_core in file "vernac/vernacinterp.ml", lines 80-84, characters 60-7
Called from Vernacinterp.interp_expr in file "vernac/vernacinterp.ml", lines 49-50, characters 19-47
Called from VernacControl.under_control in file "vernac/vernacControl.ml", line 203, characters 14-18
Called from Vernacinterp.interp_control_gen in file "vernac/vernacinterp.ml", lines 36-40, characters 4-7
Called from Util.try_finally in file "lib/util.ml", line 133, characters 16-19
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Util.try_finally in file "lib/util.ml", line 137, characters 6-32
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 151, characters 16-41
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp in file "vernac/vernacinterp.ml", line 165, characters 15-115
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2025, characters 20-47
Called from Stm.Reach.known_state.resilient_tactic in file "stm/stm.ml", line 1964, characters 10-14
Called from Stm.State.define in file "stm/stm.ml", line 963, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", lines 2203-2204, characters 4-74
Called from Stm.observe in file "stm/stm.ml", line 2295, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.interp_vernac in file "toplevel/vernac.ml", line 83, characters 29-50
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Util.try_finally in file "lib/util.ml", line 133, characters 16-19
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Util.try_finally in file "lib/util.ml", line 137, characters 6-32
Called from Vernac.load_vernac_core.loop in file "toplevel/vernac.ml", lines 127-145, characters 8-12
Called from Vernac.load_vernac_core in file "toplevel/vernac.ml", line 150, characters 6-19
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.load_vernac in file "toplevel/vernac.ml", line 227, characters 30-83
Called from Ccompile.compile in file "toplevel/ccompile.ml", line 68, characters 18-78
Called from Ccompile.compile in file "toplevel/ccompile.ml" (inlined), line 107, characters 2-59
Called from Ccompile.compile_file in file "toplevel/ccompile.ml", line 116, characters 4-61
Called from Coqc.coqc_main in file "toplevel/coqc.ml", lines 38-39, characters 2-56
Called from Coqc.coqc_run in file "toplevel/coqc.ml", line 54, characters 4-36

Changing the Q true in the example to nat -> Prop changes the error to build_signature: no constraint can apply on a dependent argument.

Small Rocq / Coq file to reproduce the bug

(* Bug.v *)

From Stdlib Require Import Setoid.

Example bug
  (cond : bool)
  (Hceq : cond = true)
  (P : forall (x : bool) (Q : bool -> Type), x = true -> Q true)
  :
  P
     cond
     (fun _ => nat -> Prop)
     (match Hceq in (_ = b) return (cond = b) with
      | eq_refl => eq_refl
      end)
     0
  .
Proof.
  rewrite Hceq at 2.
Abort.

Version of Rocq / Coq where this bug occurs

9.1.1,9.1.0,9.0.0

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response