Anomaly "decompose_lambda_n_decls: not enough declarations." with Ltac2

[TDiazT]

Description of the problem

I'm trying to build a very basic discriminate tactic using Ltac2 but I'm getting the following error with backtrace:

Anomaly "decompose_lambda_n_decls: not enough declarations."
Please report at http://rocq-prover.org/bugs/.
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Inductive.contract_case.map in file "kernel/inductive.ml", line 545, characters 20-80
Called from Stdlib__Array.mapi in file "array.ml", line 136, characters 21-43
Called from Inductive.contract_case in file "kernel/inductive.ml", line 549, characters 25-42
Called from EConstr.contract_case in file "engine/eConstr.ml", line 653, characters 35-85
Called from Ltac2_plugin__Tac2core.(fun) in file "plugins/ltac2/tac2core.ml", line 650, characters 19-71
Called from Ltac2_plugin__Tac2externals.interp_spec.(fun) in file "plugins/ltac2/tac2externals.ml", line 67, characters 68-75

As far as I've seen it comes from when I try to build a case programmatically (calling Unsafe.make case_kind).

I tried it and it works with true = false but not with S O = O.

I imagine since it's Unsafe that it might be ok for it to fail but I guess not with an Anomaly?

Small Rocq / Coq file to reproduce the bug

From Ltac2 Require Import Ltac2 Printf Constr.
Import Unsafe.

Ltac2 destConstructor (t : constr) : (constructor * instance) option  :=
  match kind t with
  | Constructor cstr i => Some (cstr, i)
  | _ => None
  end.

Ltac2 build_predicate (ind_type : inductive)  (index_false : int) :=
  let case_info := case ind_type  in
  let indt := Env.instantiate (Std.IndRef ind_type) in
  let x := Unsafe.make (Rel 1) in
  let inner_pred := ('(fun _ : $indt => Prop), Relevance.relevant) in
  let d := Ind.data ind_type in
  let n := Ind.nconstructors d in
  let branches := Array.init n (fun i => if Int.equal i index_false then 'False else 'True) in
  let case_kind := Case case_info inner_pred NoInvert x branches in
  let case_constr := Unsafe.make case_kind in
  let innerbind := match kind '(fun b : $indt => b) with Lambda b _ => b | _ => Control.throw Not_found end in
  Unsafe.make (Lambda innerbind case_constr).

Ltac2 discriminate_base () :=
lazy_match! goal with
| [ heq : ?x = ?y |- _] =>
    let (hx, _) := Constr.decompose_app x in
    let (hy, _) := Constr.decompose_app y in
    match destConstructor hx with
    | None => fail
    | Some (cstr_x, _) =>
        match destConstructor hy with
        | None => fail
        | Some (cstr_y, _) =>
            if Constructor.equal cstr_x cstr_y then
              fail
            else
            let predicate := build_predicate (Constructor.inductive cstr_x) (Constructor.index cstr_y) in
            let heq := Control.hyp heq in
            let eq_ind := '(eq_ind $x $predicate I $y $heq) in
            let false_ind := '(False_ind False $eq_ind) in
            exact $false_ind
        end
    end
 end.

Goal  true = false -> False.
intros H.
discriminate_base (). (* ok *)
Show Proof.
Abort.

Goal S O = O -> False.
intro H.
Set Debug "backtrace".
discriminate_base (). (* Anomaly *)

Version of Rocq / Coq where this bug occurs

master

Interface of Rocq / Coq where this bug occurs

No response

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

No response

[SkySkimmer]

It's OK for Unsafe to cause anomalies.
For this specific one we might want to implement a better error though as it seems likely people will keep hitting it.