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: May 28 2023 at 18:29 UTC