The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hello,

It looks like a bug.

The canonical structure inference probably forgets a universe
constraint. I wouldn't be surprised if it is related to the insertion of
the coercion to Type.

Can you submit a bug report at : https://coq.inria.fr/bugs/ ?

Thanks!

Maxime.

On 10/21/16 16:56, 
forster AT ps.uni-saarland.de
 wrote:
> Dear coq-club,
> 
> while playing around with Canonical Structures (mainly to find out if we
> want to use eqTypes in our lecture and the accompanying exercises) I am
> running into weird universe inconsistencies.
> 
> I condensed the issue to a minimal example (which looks a bit unnatural,
> but it's just to produce the error). Assume I have a structure that has a
> type enclosed, plus usually some additional stuff (for instance the fact
> that equality on this type is decidable if we're talking about eqTypes)
> and a straightforward Canonical Structure for it.
> 
> Structure wrap :=
>   Wrap {
>       type :> Type;
>       (* here's normally a typeclass with function type, so this has to be
> a structure *)
>   }.
> Canonical Structure do_wrap (X : Type) := Wrap X.
> 
> I'll use the following two lemmas to make the problem clear:
> 
> Lemma trivial1 (X: wrap) (x : X) : True.
> Proof.
>   tauto.
> Qed.
> 
> Lemma trivial2 (X: Type) (x : X) : True.
> Proof.
>   tauto.
> Qed.
> 
> And now the following explains the problem:
> 
> Lemma should_be_trivial (X : wrap) : forall (x : list X), True.
> Proof.
>   eapply trivial1.
>   Show Proof.
>   Fail Qed.
> (* The command has indeed failed with message: *)
> (* Illegal application:  *)
> (* The term "do_wrap" of type "forall _ : Type@{Top.35}, wrap" *)
> (* cannot be applied to the term *)
> (*  "list (eqType_X X)" : "Type@{max(Set, Top.34)}" *)
> (* This term has type "Type@{max(Set, Top.34)}" which should be coercible
> to "Type@{Top.35}". *)
> Restart.
>   eapply trivial2.
>   Fail Fail Qed. (* this is universe consistent, Qed would work! *)
> Restart.
>   eapply trivial1 with (X := Wrap (list X)).
>   Fail Fail Qed. (* Qed would work here, which is not surprising *)
> Restart.
>   eapply trivial1 with (X := do_wrap (list X)).
> Qed. (* Qed works. This looks surprising to me *)
> 
> For some reason, the implicit use of the canonical structure when applying
> trivial1 introduces a universe inconsistency. Not using the canonical
> structure at all works flawlessly.
> 
> Also not very surprising, if I apply trivial1 and do the work of the Can.
> Structure by hand, it works. So I thought, ok, maybe the Canonical
> Structure (Wrap in this case) is not Template Universe polymorphic (it's
> really not) and that's why this doesn't work.
> 
> However, if I apply the Structure by hand, unfolded, it also works. So
> somewhere during finding out which Canonical Structure to use, there's a
> universe inconsistency introduced.
> 
> Is this a bug, or somehow intended behaviour?
> 
> Many thanks in advance
> Yannick
> 
> PS: Here the complete source code of the example, if you want to try it:
> 
> 
> Structure wrap :=
>   Wrap {
>       type :> Type;
>       (* here's normally a typeclass with function type, so this has to be
> a structure *)
>   }.
> 
> Canonical Structure do_wrap (X : Type) := Wrap X.
> 
> Universe Polymorphic do_wrap. (* this does nothing *)
> 
> Lemma trivial1 (X: wrap) (x : X) : True.
> Proof.
>   tauto.
> Qed.
> 
> Lemma trivial2 (X: Type) (x : X) : True.
> Proof.
>   tauto.
> Qed.
> 
> Set Printing Universes.
> Set Printing All.
> 
> Lemma should_be_trivial (X : wrap) : forall (x : list X), True.
> Proof.
>   eapply trivial1.
>   Show Proof.
>   Fail Qed.
> (* The command has indeed failed with message: *)
> (* Illegal application:  *)
> (* The term "do_wrap" of type "forall _ : Type@{Top.35}, wrap" *)
> (* cannot be applied to the term *)
> (*  "list (eqType_X X)" : "Type@{max(Set, Top.34)}" *)
> (* This term has type "Type@{max(Set, Top.34)}" which should be coercible
> to "Type@{Top.35}". *)
> Restart.
>   eapply trivial2.
>   Fail Fail Qed. (* this is universe consistent, Qed would work! *)
> Restart.
>   eapply trivial1 with (X := Wrap (list X)).
>   Fail Fail Qed. (* Qed would work here, which is not surprising *)
> Restart.
>   eapply trivial1 with (X := do_wrap (list X)).
> Qed. (* Qed works. This looks surprising to me *)
> 
> 
>