The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Vladimir Voevodsky wrote:
> But that should not be a problem here. Isn't "Set" a particular instance of 
> "Type"?

Yes, it is, but I don't see why that implies the below problem shouldn't 
show up.  Coq doesn't claim to provide _complete_ type inference.

> On Apr 20, 2012, at 6:08 PM, Adam Chlipala wrote:
>
> > On 04/20/2012 05:08 PM, Thomas Braibant wrote:
> > > I encountered the following behavior, which I find strange....
> > >
> > > Inductive b : Type := t1 | t2.
> > > Inductive I : list Type ->   Type ->   Type :=
> > > | C : I (b :: b :: nil) unit.
> > >
> > > The term "I" of type "list Type ->   Type ->   Type"
> > > cannot be applied to the terms
> > >   "b :: b :: nil" : "list Set"
> > >   "b" : "Set"
> > > The 1st term has type "list Set" which should be coercible to "list Type".
> > >
> > > Could someone explain me what's happening ?
> > So you expect [list] to be recognized as covariant in its parameter, 
> > subtyping-wise?  That would be an interesting feature which I can believe 
> > could be justified semantically, but I don't think it's in today's Coq.  It 
> > would certainly complicate the metatheory, and probably wouldn't apply very 
> > often.
> >
> > In your specific case, you can just replace the second definition with:
> >     Inductive I : list Type ->  Type ->  Type :=
> >     | C : I ((b : Type) :: (b : Type) :: nil) unit.
> >
> > ...or use some other method for forcing the implicit parameters of [cons] to 
> > be different.
> >
> > It's an interesting coincidence that you bring this issue up so soon after 
> > the previous question relating to fake universe polymorphism in Coq!  The 
> > specific consequence of such polymorphism here is that the type [b] is 
> > interpreted as being at the lowest possible universe level, [Set].