Stack overflow with UIP

[laMudri]

I was minifying some code to debug an error Equations was giving me, and instead found a bug. Incidentally, I believe this should be possible without a global UIP, because everything in sight is a set, but I couldn't get it to work.

From Equations Require Import Equations.
Set Equations With UIP.

Variant ty : Type :=
| val (A : nat).
Derive NoConfusion EqDec for ty.

Variant Node : ty -> ty -> Type :=
| bar {A} : Node A A.
Derive NoConfusion for Node.

Variant Is_bar : forall {Ga De}, Node Ga De -> Type :=
| bar_is_bar {A} : Is_bar (@bar A).

Equations Is_bar_prop {Ga De n} (x y : @Is_bar Ga De n) : x = y :=
| bar_is_bar, bar_is_bar => eq_refl.

Result of checking the last definition:

Error: Stack overflow.

ocaml version 4.13.1; coq version 8.15.1; coq-equations version 1.3+8.15

[laMudri]

If, instead of Derive NoConfusion for Node., I do Derive Signature NoConfusionHom for Node., I get a different error at the last definition:

Anomaly
"Uncaught exception Failure("Could not generate a permutation: irreducible inaccessible")."
Please report at http://coq.inria.fr/bugs/.

[mattam82]

Interesting errors :) I'll have a look.