Sometimes, universe polymorphic definitions aren't polymorphic enough (but making them more polymorphic might break other things) (polyproj)

[JasonGross]

Behold another issue with Set. In this case, the problem is that the theorem that Contr (Unit : Set) doesn't also prove Contr (Unit : Type) for other universes, even though its proof term does.

Perhaps the problem is that sometimes I use Set to mean Type > Prop, and, much more rarely, I use it to mean Type <= Type_0, but Coq doesn't give me a way to distinguish these. Perhaps I want a way to declare an inductive type

Inductive unit : Type := tt.

which will not land in Prop, but won't land in Set either, i.e., so that all three Checks in the following code work:

Set Universe Polymorphism.
Set Printing Universes.
Section u.
  Let U := Type.
  Inductive unit : U := tt.
End u.
Print unit. (* Inductive unit : Type (* Top.35 *) :=
    tt : unit (* Top.35 *)
             (* Top.35 |= Prop <= Top.35
             *) *)
Check unit. (* unit
(* Prop *)
     : Prop *)
Definition same_univ : $(let U := constr:(Type) in exact (U -> U -> True))$
  := fun _ _ => I.

Definition foo := same_univ unit.
Check unit : Set.
Check foo nat.
Check foo Set.

(It might be nice if Check unit : Prop. also works, in addition to the ones above.)

Here's some more code that breaks:

(* File reduced by coq-bug-finder from original input, then from 4171 lines to 78 lines, then from 88 lines to 53 lines *)

Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.
Arguments idpath {A a} , [A] a.
Notation "x = y" := (@paths _ x y) : type_scope.

Class Contr_internal (A : Type) := BuildContr {
  center : A ;
  contr : (forall y : A, center = y)
}.

Inductive Unit : Set := tt.

Instance contr_unit : Contr_internal Unit | 0 := let x := {|
  center := tt;
  contr := fun t : Unit => match t with tt => idpath end
|} in x.

Section local.
  Let type_cast_up_type : Type.
  Proof.
    let U0 := constr:(Type) in
    let U1 := constr:(Type) in
    let unif := constr:(U0 : U1) in
    exact (U0 -> U1).
  Defined.
  Definition Lift : type_cast_up_type
    := fun T => T.
End local.

Record hProp := hp { hproptype :> Type ; isp : Contr_internal hproptype}.

Set Printing All.

Definition foo : hProp.
  exact (hp (Lift Unit) (BuildContr Unit tt (fun t => match t as t0 return (@paths Unit tt t0) with
                                                        | tt => idpath
                                                      end))).
  Undo.
  Set Printing Universes.
  exact (hp (Lift Unit) (contr_unit)).
  (* Toplevel input, characters 23-33:
Error:
The term "contr_unit" has type "Contr_internal (* Set *) Unit"
while it is expected to have type
 "Contr_internal (* Top.50 *) (Lift (* Top.51 Top.52 Top.53 Top.54 *) Unit)"
(Universe inconsistency: Cannot enforce Top.50 = Set because Set <= Top.54
< Top.51 <= Top.50)). *)