## Stream: Equations devs & users

### Topic: Derive EqDec for parametrised types

#### James Wood (Jul 12 2022 at 15:53):

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 parameters and supposing any primitive inductive
type used in the definition also has decidable equality.

What's the mismatch here?

#### Paolo Giarrusso (Jul 13 2022 at 13:39):

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 ?

#### Matthieu Sozeau (Jul 13 2022 at 14:01):

I think it works if you define box in a section, adding the EqDec A instance yourself before the Derive.

#### James Wood (Jul 13 2022 at 15:11):

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}".
*)


#### James Wood (Jul 13 2022 at 15:52):

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.

#### Paolo Giarrusso (Jul 13 2022 at 16:36):

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

#### James Wood (Jul 14 2022 at 08:14):

Yeah. I can add a Universe u. declaration in the section, and have A : Type@{u} &c, then scratch.75 becomes u`.

#### Matthieu Sozeau (Jul 22 2022 at 23:04):

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

#### James Wood (Jul 23 2022 at 14:09):

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

#### Matthieu Sozeau (Jul 26 2022 at 08:46):

Thanks, I fixed it

Last updated: Jan 29 2023 at 15:02 UTC