The Coq mailing list

[Matej Košík <universe.inconsistency AT gmail.com>]

Hi Jason,

On 01/21/2017 07:59 PM, Jason Gross wrote:
> Matej,
> 
> With your branch of Coq:
> 
> Set Universe Polymorphism.
> Definition foo@{i j} (x : Type@{i}) := x : Type@{j}.
> Set Printing Universes.
> Section foo.
>   Universe i.
>   Constraint i = Prop. (* works fine in your branch, fails in standard Coq 
> with Error: Universe inconsistency. Cannot enforce i = Prop because Prop < 
> Set <= i. *)
>   Definition bar := foo@{Set i}.
> End foo.
> Eval compute in bar nat. (* = nat : Prop *)
> Definition natP : Prop.
> Proof.
>   let v := (eval compute in (bar nat)) in exact v.
> Defined.
> Print natP. (* natP = nat
>      : Prop
> (*  |= Prop = Set
>         *) *)
> 
> I had to jump through some hoops to work around other ad-hoc restrictions 
> that prevent collapsing things to Prop (polymorphic universes can't 
> normally be instantiated with [Prop], even when you relax
> Prop < Set; monomorphic universes are always strictly greater than Set, the 
> subtyping relation must special-case Prop and Set in some places, rather 
> than going through the generic universe comparison
> algorithm.)

Wouldn't the following example (in my branch):

  Constraint Set <= Prop.

  Check nat : Prop. (* does not fail --- unsurprisingly *)

achieve the same?

(* so far, I wasn't aware that there is this "Constraint" command so I did 
not know that this kind of thing is possible *)

I guess that there is nothing to be gain (?) by letting the user to do that 
(or is there?).

Can that be the reason why we absolutely must insist on "Prop < Set" instead 
of just on "Prop ≤ Set"?

> 
> Regarding your question
>> I wonder why Coq infers that.
> The command [Print Sorted Universes] collapses all universes to the minimal 
> universe they can inhabit.

Why?

> If you include the prelude and [Print Sorted Universes], all of the 
> universes in the prelude get
> collapsed to Type.0.  So since you don't have Prop < Set, Coq infers that 
> Set can be collapsed to Prop.

That statement is not consistent with my experiments.

  Coq < Print Sorted Universes.
  Coq.Init.Logic_Type.6 = Type.0
  Coq.Init.Logic_Type.5 = Type.0
  Coq.Init.Logic_Type.4 = Type.0

  <snip>

  Coq.Init.Wf.3 = Type.0
  Coq.Init.Wf.2 = Type.0
  Coq.Init.Wf.1 = Type.0
  Set < Type.0
  Prop = Set

The surprising behavior (of Coq in my branch) is, I believe, this:

  Welcome to Coq trunk (January 2017)

  Coq < Print Sorted Universes.
  Prop = Set

  (* I still do not understand how could "Prop = Set" follow from "Prop ≤ 
Set". *)

  (* Fortunatelly, even though Coq prints "Prop = Set", it does not really 
mean it ... *)

  Coq < Check fun A:Set => (A:Prop).
  Toplevel input, characters 20-21:
  > Check fun A:Set => (A:Prop).
  >                     ^
  Error:
  In environment
  A : Set
  The term "A" has type "Set" while it is expected to have type
  "Prop" (universe inconsistency).

  (* ... so we are safe. Just that the output of "Print Sorted Universes." 
cannot be take literally :-/. *)

  (* Now, after I do ... *)

  Coq < Constraint Prop = Set.

  Coq < Print Sorted Universes.
  Prop = Set

  (* ... I get the same output of the "Print Sorted Universes." command as 
before; but *this time* Coq really means it: *)

  Coq < Check fun A:Set => (A:Prop).
  fun A : Set => A : Prop
       : forall _ : Set, Prop