zify: anomaly when adding a parameterized InjTyp instance

[samuelgruetter]

By adapting the code from this Coq-club email by @fajb, I was able to instrument zify so that it adds bounds for injections of my custom data type tuple byte 4 into Z:

Require Import Coq.ZArith.ZArith. Open Scope Z_scope.
Require Coq.Init.Byte Coq.Strings.Byte.
Require Import Coq.micromega.ZifyClasses Coq.micromega.Lia.

Notation byte := Coq.Init.Byte.byte.

Module byte.
  Definition unsigned(b: byte): Z := Z.of_N (Byte.to_N b).
End byte.

Section WithA.
  Context (A: Type).
  Fixpoint tuple(n: nat): Type :=
    match n with
    | O => unit
    | S m => A * tuple m
    end.
End WithA.

Module LittleEndian.
  Fixpoint combine (n : nat) : forall (bs : tuple byte n), Z :=
    match n with
    | O => fun _ => 0
    | S n => fun bs => Z.lor (byte.unsigned (fst bs))
                             (Z.shiftl (combine n (snd bs)) 8)
    end.
  Lemma combine_bound: forall {n: nat} (t: tuple byte n),
      0 <= LittleEndian.combine n t < 2 ^ (8 * Z.of_nat n).
  Admitted.
End LittleEndian.

Instance InjByteTuple4: InjTyp (tuple byte 4) Z := {|
  inj := LittleEndian.combine 4;
  pred x := 0 <= x < 2 ^ 32;
  cstr := @LittleEndian.combine_bound 4;
|}.
Add Zify InjTyp InjByteTuple4.

Program Instance Op_combine4 : UnOp (LittleEndian.combine 4) :=
  {| TUOp := fun x  => x ;  |}.
Add Zify UnOp Op_combine4.

Goal forall w: tuple byte 4,
    LittleEndian.combine 4 w mod 2 ^ 32 = LittleEndian.combine 4 w.
Proof.
  intros.
  zify.
  Z.to_euclidean_division_equations.
  lia.
Qed.

However, if I generalize my solution to tuples of any size n,

Instance InjByteTuple{n: nat}: InjTyp (tuple byte n) Z := {|
  inj := LittleEndian.combine n;
  pred x := 0 <= x < 2 ^ (8 * Z.of_nat n);
  cstr := @LittleEndian.combine_bound n;
|}.
Add Zify InjTyp InjByteTuple.

I get

Error: Anomaly "in econstr: grounding a non evar-free term" Please report at http://coq.inria.fr/bugs/.

Coq version: 8.13.0 and master are affected.

Might be a duplicate of #13242, but with a less artificial (though less minimal) example.

[fajb]

Hi @samuelgruetter ,

Don't expect zify to work with parameterized instances. Some error checking is missing but the error message should be something like "Dependent types are not allowed".
This is a strong restriction of the implementation that is hardwired very deep. Sorry.

If possible the solution would be to instantiate with the ns of interest.

PS: It may be possible to implement a more expressive zify like tactic in pure Ltac using typeclasse inference.

[samuelgruetter]

Thanks for the information, and yes in my case I can just instantiate n with 1,2,4 and 8, that's all I need.