Universe constraints collapsed too eagerly (polyproj)

[JasonGross]

Set Printing Universes.
Polymorphic Axiom opaque_type_cast_down : forall (T : Type), { T' : Type & T' = T }.
Print opaque_type_cast_down.
(* *** [ opaque_type_cast_down :
forall T : Type (* Top.1272 *), {T' : Type (* Top.1275 *) | T' = T} ]
(* Top.1272
   Top.1275
   Top.1276 |= Top.1275 < Top.1276
                Top.1272 <= Top.1275
                 *) *)
Eval compute in opaque_type_cast_down.
(*      = opaque_type_cast_down (* Top.1277 Top.1277
Top.1279 *)
     : forall T : Type (* Top.1277 *), {T' : Type (* Top.1277 *) | T' = T} *)

Perhaps this is not a bug, though, and I just need a better way to cast things across universes.

[JasonGross]

Actually, I take that back. I think it is very much a bug, or at least a feature that should be disableable:

Inductive type_paths (A : Type) : Type -> Type
  := idtypepath : type_paths A A.
Eval compute in type_paths.
(*      = type_paths (* Top.1012
Top.1012 *)
     : Type (* Top.1012 *) -> Type (* Top.1012 *) -> Type (* Top.1012+1 *) *)
(* This is terrible. *)

Inductive type_paths' (A : Type) : Type -> Type
  := idtypepath' : type_paths' A A
   | other_type_path : forall B : Type, type_paths' A B.
Eval compute in type_paths'.
(*     = type_paths' (* Top.1029 Top.1030
Top.1031 *)
     : Type (* Top.1029 *) -> Type (* Top.1030 *) -> Type (* Top.1030+1 *)*)

[JasonGross]

Is there any (easy to write) code that will distinguish between U0 -> U1 -> suc(U1) and U0 -> U0 -> suc(U0)?

[JasonGross]

Here's a test case:

Set Universe Polymorphism.
Set Printing Universes.

Inductive type_paths (A : Type) : Type -> Prop
  := idtypepath : type_paths A A.
Monomorphic Definition comp_type_paths := Eval compute in type_paths.
Check comp_type_paths.
(* comp_type_paths
     : Type (* Top.12 *) -> Type (* Top.12 *) -> Prop *)
(* This is terrible. *)

Inductive type_paths' (A : Type) : Type -> Prop
  := idtypepath' : type_paths' A A
   | other_type_path : False -> forall B : Set, type_paths' A B.
Monomorphic Definition comp_type_paths' := Eval compute in type_paths'.
Check comp_type_paths'.
(* comp_type_paths'
     : Type (* Top.24 *) -> Type (* Top.23 *) -> Prop *)
(* Ok, then ... *)

(** Fail if it's [U0 -> U0 -> _], but not on [U0 -> U1 -> _]. *)
Goal Type.
Proof.
  match type of comp_type_paths' with
    | ?U0 -> ?U1 -> ?R
      => exact (@comp_type_paths' nat U0)
  end.
Defined.

Goal Type.
Proof.
  match type of comp_type_paths with
    | ?U0 -> ?U1 -> ?R
      => exact (@comp_type_paths nat U0)
      => exact (@comp_type_paths nat U0)
  end.
  (* Toplevel input, characters 110-112:
Error:
The term "Type (* Top.51 *)" has type "Type (* Top.51+1 *)"
while it is expected to have type "Type (* Top.51 *)"
(Universe inconsistency: Cannot enforce Top.51 < Top.51 because Top.51
= Top.51)). *)
Defined.

[mattam82]

It's not a bug, but indeed, you need to be explicit if you want to avoid an early collapse like this. Typically, the following works now. Monomorphic Definition comp_type_paths := Eval compute in type_paths@{Type Type}. This just makes the parameter Type level smaller or equal to the index Type level.