The Coq mailing list

[forster AT ps.uni-saarland.de]

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