Runaway universe

[Lysxia]

Description of the problem

The following lemma fails to typecheck on coq.dev (it passes on 8.9):

Set Universe Polymorphism.

Lemma eq_list_eq@{u}
: forall (a : Type@{u}) (pf : a = a) (xs : list a),
    match pf in _ = c return list c with
    | eq_refl => xs
    end
  = xs.
Abort.

with the error message (where A.v is the name of the file)

Error: Universe {A.2} is unbound.

Coq Version

coq.dev

[JasonGross]

In 8.9, a = a turns into @eq Type@{u} a a. In master, it turns into @eq Type@{A.2} a a. Since mentioning some but not all universes in the universe list is an error (there's a setting to make it not an error, I think, but I don't recall which one it is), this results in an error in master. I'm not sure why the universes end up being different, though... cc @mattam82 ?

[Lysxia]

Thanks! What about this other case, which complains about a missing third universe?

Set Universe Polymorphism.

Lemma eq_list_eq@{u v}
: forall (T : Type@{u}) (F : T -> Type@{v}) (a : T) (pf : a = a) (xs : list (F a)),
    match pf in _ = c return list (F c) with
    | eq_refl => xs
    end
  = xs.
Abort.

[JasonGross]

Running

Set Universe Polymorphism.
Set Printing All.
Set Printing Universes.

Section foo.
  Universes u v.

  Lemma eq_list_eq
    : forall (T : Type@{u}) (F : T -> Type@{v}) (a : T) (pf : a = a) (xs : list (F a)),
      match pf in _ = c return list (F c) with
      | eq_refl => xs
      end
      = xs.
  Admitted.
  Print eq_list_eq.
  (* *** [ eq_list_eq@{Crypto.foo.17} :
forall (T : Type@{u}) (F : forall _ : T, Type@{v}) (a : T)
  (pf : @eq T a a) (xs : list (F a)),
@eq (list (F a)) match pf in (eq _ c) return (list (F c)) with
                 | eq_refl => xs
                 end xs ]
(* Crypto.foo.17 |= Set <= Crypto.foo.17
                    u <= eq.u0
                    v <= eq.u0
                    v <= list.u0
                    v <= Crypto.foo.17 *)

Argument scopes are [type_scope function_scope _ _ list_scope]
*)

It seems that this is another instance of universe minimization failure, but this time the universe doesn't even appear anywhere in the term.

[SkySkimmer]

Might be a Lemma issue, if you use Axiom instead there's no extra universe.