The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 13 oct. 09 à 13:49, Vladimir Voevodsky a écrit :

> In the following sequence of instructions:
>
> Axiom f5 : Set -> nat .
>
> Axiom P0 : Prop .
>
> Axiom S0 : Set .
>
> Check f5 P0 .
>
> Check eq P0 S0 .
>
> The last two produce the following reactions:
>
> f5 P0
>     : nat
>
> and
>
> Error: The term "S0" has type "Set" while it is expected to have  
> type "Prop".
>
> respectively.
>
> Why does f5 treat Prop as a subtype of Set but eq does not?

It's because eq's arguments type is fixed by the type of its first  
argument.
One could say it's somewhat premature, there exists some systems
using unification with subtyping that can handle this case.
In short, [Check @eq Set P0 S0.] works, as does [Check eq S0 P0] :).

-- Matthieu