The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Robert Dockins wrote:

> If I understand the situation correctly, there isn't any way at all  
> to define a function with this type if Term is in sort Type.   
> Actually, you could replace Term with _any_ definition in sort Type  
> and this would still be impossible.  It is also my understanding that  
> if I could magically make Coq accept the Term definition in sort Set  
> that these problems would go away.  Is all that right?
That's correct, with the right magic.  The bit of magic that you're 
looking for is the "-impredicative-set" command-line flag.  With it, you 
can replace all instances of Type with Set in your example (and add type 
annotations on a few forall's, since Type is chosen by default for any 
variable that is used as a type) and it should work swimmingly.

The big gotcha is that your main types are "large," so you won't be able 
to eliminate their values to form others in sort Type.  I haven't tried 
your whole example to see if that would cause problems.  The other 
gotcha is that some people are uncomfortable with the idea of 
impredicativity and will question the validity of any results you 
derive, but I've found impredicativity to be so useful for formalizing 
programming languages that I ignore this last point. :)