The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

And indeed there is special code for Prop </<=/= Set that was already present before my changes that can prevent Set <= Prop (see check_leq_sort in closure.ml IIRC)

On Mon, Jan 23, 2017 at 8:30 AM Théo Zimmermann <theo.zimmi AT gmail.com> wrote:

Matej, you disabled one of the various checks which make Prop not be collapsed to Set but there are others. Your branch is not in a consistent state (by that I don't mean that the logic is inconsistent). Jason had to work around those inconsistencies to find an example where your check alone would be enough to collapse Prop to Set but you can't use the statement further because of these other checks.

Anyway, I think your questions got fully answered: (Hugo said) there is nothing preventing to relax the constraint in the logic but (as I said, Hugo and Matthieu confirmed and Jason further exemplified) the universe constraint solving algorithm is dependent on this constraint being here.
The reason you can had constraints is that normally there are used only for Types.
There would be other ways to ensure that Prop and Set are not collapsed, without listing Prop < Set as a constraint, and this is what Hugo suggested.

Théo

Le dim. 22 janv. 2017 17:54, Matej Košík <universe.inconsistency AT gmail.com> a écrit :

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