The following code produces the following unsolved obligation:

```
From Equations Require Import Equations.
Inductive box {A : Type} : Type :=
| pack : A -> box.
Arguments box A : clear implicits.
Derive NoConfusion EqDec for box.
(* ...
Obligation 1 fo box_eqdec: (forall (A : Type) (x y : box A), dec_eq x y).
*)
```

However, from the documentation, I expected it to be a bit cleverer about the parameter `A`

, and produce (and solve) a sensible obligation. Emphasis mine:

This derives a decidable equality on $C$,

assuming decidable equal-

ity instances for the parametersand supposing any primitive inductive

type used in the definition also has decidable equality.

What's the mismatch here?

That seems a good question — I got the same results, even with `Derive NoConfusion EqDec for list`

, and supporting decidable equality on containers seems a desirable feature. WDYT @Matthieu Sozeau ?

I think it works if you define `box`

in a section, adding the `EqDec A`

instance yourself before the `Derive`

.

That sounded believable, but when I try it I get an odd universe-related error when using `Type`

rather than `Set`

(which I need in my use case):

```
From Equations Require Import Equations.
Section box.
Context {A : Type} `(EA : EqDec A).
Inductive box : Type :=
| pack : A -> box.
Derive NoConfusion for box.
Fail Derive EqDec for box.
End box.
(*
box_eqdec has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
Unable to compute diffs: Input string is not lexable
The command has indeed failed with message:
Illegal application:
The term "@dec_eq" of type "forall A : Type, A -> A -> Set"
cannot be applied to the terms
"box" : "Type"
"x" : "box"
"y" : "box"
The 1st term has type "Type@{scratch.75}" which should be coercible to
"Type@{dec_eq.u0}".
*)
```

It seems to be because `dec_eq`

is not universe polymorphic, but I don't really understand why that should be (just through not really understanding universe polymorphism). It looks like some things in stdlib are template polymorphic, and other things aren't.

Hmm where does scratch.75 come from, this must be in scratch.v right?

Yeah. I can add a `Universe u.`

declaration in the section, and have `A : Type@{u}`

&c, then `scratch.75`

becomes `u`

.

Sounds like a universe bug on Equations side, can you please report it?

Someone reported a very similar-looking issue just a few days ago, so I'm going to add to that.

Thanks, I fixed it

Last updated: May 25 2024 at 20:01 UTC