The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Yes it is a strange bug of (e)apply. [refine (trivial1 _)] works.

On Fri, Oct 21, 2016 at 5:18 PM Maxime Dénès <mail AT maximedenes.fr> wrote:

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 *)
>
>
>