The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

On 01/21/2017 06:03 PM, Jason Gross wrote:
> If you write
>   (fun x : Set => (x : Prop))
> Coq will currently reject that.  If you relax Prop < Set to Prop ≤ Set, Coq 
> will add the global constraint that Set ≤ Prop and hence that Prop = Set, 
> just as when you write

I wasn't able to reproduce what you say. In my branch where I relaxed Prop < 
Set to Prop ≤ Set, this is what I see:

    Welcome to Coq trunk (January 2017)

    Coq < Print Universes.
    Prop <= Set

    Coq < Set Printing Universes.

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

which totally makes sense. The term:

  fun x : Set => (x : Prop)

is not well-typed because Set is not a subtype of Prop.
(this is not the case of neither in the official Coq branches, neither in my 
experiment).

Relaxing Prop < Set to Prop ≤ Set does not imply Set suddenly becomes a 
subtype of Prop.

> (fun x : Type@{i} => (x : Type@{j}))
> Coq adds the constraint that i ≤ j.

It may. I fail to see how it is a problem (wrt what I asked).

> 
> It might also be the case that you'd get this constraint in more subtle 
> situations, such as if you write
>   Inductive inhabited (X : Set) : Prop := inhabits (_ : X).
> or if you write
>   (forall X : Set, X) : Set

    Welcome to Coq trunk (January 2017)

    Coq < Print Universes.
    Prop <= Set


    Coq < Inductive inhabited (X : Set) : Prop := inhabits (_ : X).
    inhabited is defined
    inhabited_ind is defined

    Coq < Print Universes.
    Prop <= Set

> 
> Does this answer your question?

Unfortunatelly, not. But think you (all) for the answers!

However, independently from your concrete arguments, which I wasn't able to 
reproduce, there is more simple way to see that something is wrong after 
these changes:

    
https://github.com/matej-kosik/coq/commit/2fcbb0ced3bc32210ae9fbf4acc40804841c9200

this:

    Welcome to Coq trunk (January 2017)

    Coq < Print Universes.
    Prop <= Set


    Coq < Print Sorted Universes.
    Prop = Set

shows that Coq, somehow really decides (why?) infers that "Prop = Set"
(regardless whether we add inhabitants to Set or not).

I wonder why Coq infers that.

This is consistent with what Hugo said.

Hm, I guess that the only way to find out is to look at the implementation ...

> 
> 
> On Sat, Jan 21, 2017, 11:27 AM Matej Kosik 
> <5764c029b688c1c0d24a2e97cd764f AT gmail.com
>  
> <mailto:5764c029b688c1c0d24a2e97cd764f AT gmail.com>>
>  wrote:
> 
>     Hi Hugo,
> 
>     For me, the most surprising parts of you reply are:
> 
>     On 01/19/2017 11:58 PM, Hugo Herbelin wrote:
>     >
>     > The "Prop < Set" is technical: the universe-acyclicity algorithm
>     > internally needs to consider Prop <> Set to ensure that Prop is not
>     > accidentally equated to Set (*). Matthieu, who introduced this for the
>     > polymorphism of universes, confirmed.
> 
>     ...
> 
>     > (*) In particular, changing the line "enforce_univ_lt Level.prop
>     > Level.set empty" into "enforce_univ_le Level.prop Level.set empty"
>     > would be incorrect, unless other means are used to ensure that the
>     > algorithm does not eventually incorrectly conclude that Prop = Set is
>     > part of the logic.
> 
>     I wouldn't be surprised if Coq concluded that:
> 
>       X ≤ Z      (* all inhabitants of X are also inhabitants of Z *)
> 
>     from the following two universe constraints:
> 
>       X ≤ Y      (* all inhabitants of X are also inhabitants of Y *)
> 
>       Y ≤ Z      (* all inhabitants of Y are also inhabitants of Z *)
> 
> 
>     Similarly, no surprise when it concludes:
> 
>       X = Y      (* X and Y have the same inhabitants *)
> 
>     from these constraints:
> 
>       X ≤ Y      (* all inhabitants of X are also inhabitants of Y *)
> 
>       Y ≤ X      (* all inhabitants of Y are also inhabitants of X *)
> 
> 
>     However, when you claim that Coq can conclude
> 
>       Prop = Set   (* Prop and Set have the same inhabitants *)
> 
>     from, and solely from:
> 
>       Prop ≤ Set   (* all inhabitants of Prop are also inhabitants of Set *)
> 
>     isn't that counterintuitive for the user?
> 
>     Did I understand you correctly when you said that this could really 
> happen (if we imagine that "Prop < Set" was relaxed to "Prop ≤ Set") ?
> 
>     Would Coq do this only in case of Prop and Set or in general for any 
> two universes?
> 


-- 
Matej Košík