The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Gert Smolka wrote:
> Am 05.05.2011 18:01, schrieb Adam Chlipala:
> > Gert Smolka wrote:
> > > So far I thought that "Type" is a placeholder
> > > for a universe different from "Set" and "Prop".
> > > But it turns out that
> > >
> > > Check (fun X : Type => X) : Set -> Type.
> > >
> > > is successful.  In fact, Coq replaces the left Type
> > > with Set.  What is the motivation behind
> > > this behavior?
> >
> > I think this is standard contravariant subtyping for function types, 
> > since [Set] is a subtype of [Type] (for any universe index attached 
> > to the latter).
>
> I don't think so.  Coq really changes the term on the left to
> "fun X : Set => X" in the output.  Incidentally, the check
>
> Check (fun X : Type => X) : Set -> Set.
>
> fails as I would expect.

It looks like something interesting is going on in Coq lately.  I tried 
your original command in Coq 8.2 and got a type error.  Perhaps [Set] is 
truly changed to a synonym for [Type] level 0 in 8.3 and later.