The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi John,

I don't know if anyone answered to you before.
This clearly looks like a bug to me: there should never be such errors at Defined time when you are using "safe" tactics like "apply". There must be a problem in collecting and threading the universe constraints generated during the proof.

So yes, please do open a bug report about this.

Théo

Le ven. 18 mai 2018 à 02:33, John Wiegley <johnw AT newartisans.com> a écrit :

Hi,

The code below (or something like it) occurs in several places in one of my
projects. This works fine with Coq 8.5, 8.6, and 8.7. But with 8.8, I'm now
getting universe errors I don't quite understand on the final line:

  File "./Bug.v", line 39, characters 0-8:
  Error:
  Illegal application:
  The term "list_equivalence_obligation_1" of type
   "forall (A : Type) (H : Setoid A), Reflexive list_equiv"
  cannot be applied to the terms
   "A" : "Type"
   "H" : "Setoid A"
  The 1st term has type "Type@{Bug.181}" which should be coercible to
   "Type@{Bug.196}".

Note that if I explicitly type the parameter {A : Type}, the error changes to
complain about the 2nd term.

I'd like to know if this is a bug to be reported, or if not, what the nature
of the problem is so I can fix it in a way that's compatible with at least
8.6-8.8.

Thanks,
  John

--8<---------------cut here---------------start------------->8---
Require Import Coq.Classes.CMorphisms.

Set Universe Polymorphism.

Class Setoid A := {
  equiv : crelation A;
  setoid_equiv :> Equivalence equiv
}.

Generalizable All Variables.

Fixpoint list_equiv `{Setoid A} (xs ys : list A) : Type :=
  match xs, ys with
  | nil, nil => True
  | cons x xs, cons y ys => prod (equiv x y) (list_equiv xs ys)
  | _, _ => False
  end.

Axiom admit : forall A : Type, A.

Program Instance list_equivalence `{Setoid A} : Equivalence list_equiv.
Next Obligation.
  repeat intro.
  induction x; simpl; split; auto.
  apply reflexivity.
Qed.
Next Obligation.
  repeat intro.
  generalize dependent y.
  induction x, y; simpl in *; intros; auto.
  destruct X.
  split; [now apply symmetry|now apply IHx].
Qed.
Next Obligation.
apply admit.
Defined.
--8<---------------cut here---------------end--------------->8---

--
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2