Coq: [ssr] Definition unfolding leads to universe anomaly with Set Universe Polymophism

[anton-trunov]

Version

Coq: 8.8.2, 8.10+alpha (7f2e50319d77d09ecc9fdbd6695dd9c92f8389d0)

Operating system

macOS 10.14.2

Description of the problem

This snippet

From Coq Require Import ssreflect ssrbool.

Set Universe Polymorphism.

Structure type := Pack {sort; op : rel sort}.

Lemma refl (T : type) (x : sort T) : op T x x.
Proof.
Fail rewrite /op.

generates the following anomaly:

Error: Anomaly "Uncaught exception "Anomaly: Universe foo.1293 undefined."." Please report at http://coq.inria.fr/bugs/.

• Btw, unfold op. works and
• in Coq 8.7.2 there is no anomaly, but rewrite /op does nothing.

[gares]

The problem is in the matching routine that compare terms discarding universes, but then calls unfold on the pattern term (op{fresh} here) an obtains the body instantiated on fresh.

I've been planning to clean up the code of ssrmatching, but don't hold your breath.

[arthuraa]

I ran into the same issue, and it seems that it can be mitigated by explicitly declaring the universe level:

From Coq Require Import ssreflect ssrbool.

Set Universe Polymorphism.

Section Foo.

Universe i.

Structure type := Pack {sort : Type@{i}; op : rel sort}.

Lemma refl (T : type) (x : sort T) : op T x x.
Proof.
rewrite /op.
Abort.

End Foo.

[kyoDralliam]

I have a similar problem but Primitive Projections seem to also influence the results. Here are my experiences so far (with coq version 8.10+alpha e9c2bc9a) :

From Coq Require Import ssreflect.

Set Primitive Projections. (* without this both tests fail = throw an aomaly *)
(* 1 *) (* Set Universe Polymorphism. *)


Section MapBug.
  Record Monad : Type :=
    mkMonad
      { monad_tyop :> Type -> Type
      ; monad_ret  : forall A, A -> monad_tyop A
      ; monad_bind : forall A B,
          monad_tyop A -> (A -> monad_tyop B) -> monad_tyop B
      }.

  (* 2 *) Set Universe Polymorphism.

  Definition map {M:Monad} {A B} (f : A -> B) (m : M A) : M B :=
    monad_bind _ _ _ m (fun x => monad_ret M _ (f x)).

  (* test 1 : works independently of universe polymorphism *)
  Goal forall (M:Monad) A B (f : A -> M B) (m: M A) , map f m = map f m.
  Proof. rewrite /map //. Qed.

  Definition ret {M : Monad} {A} := @monad_ret M A.
  Definition bind {M : Monad} {A} {B} := @monad_bind M A B.
  Definition map' {M:Monad} {A B} (f : A -> B) (m : M A) : M B :=
    bind m (fun x => ret (f x)).

  (* test 2 *)
  (* Without universe polymorphism, does not fail *)
  Goal forall (M:Monad) A B (f : A -> M B) (m: M A) , map' f m = map' f m.
  Proof. Fail rewrite /map'. 

  (* With 1 uncommented gives : *)

  (* The command has indeed failed with message: *)
  (* Conversion test raised an anomaly: *)
  (* Anomaly "Universe Mon.sprop.test.441 undefined." *)
  (* Please report at http://coq.inria.fr/bugs/. *)


  (* With 1 commented and 2 uncommented, gives : *)
  (* Error: *)
  (* Anomaly *)
  (* "Uncaught exception "Anomaly: Universe Mon.sprop.test.1054 undefined."." *)
  (* Please report at http://coq.inria.fr/bugs/. *)

End MapBug.

I also tried @arthuraa solution but the second test keep throwing an anomaly (that fail cannot catch).

[andreaslyn]

Hi @gares, Maybe the workaround in the following link can help https://github.com/coq/coq/compare/master...andreaslyn:issue-9336-poly-ssr-unfold.

[gares]

It can't hurt, but Im not sure it fixes all the bugs here. Could you please open a pr, possibly with a test case in test-suite/ssr?

[andreaslyn]

It can't hurt, but Im not sure it fixes all the bugs here. Could you please open a pr, possibly with a test case in test-suite/ssr?

Indeed, there are more bugs. I will spend a bit more time on this before opening the PR+test.