[isabelle-dev] Additional type variable(s) in specification

[Makarius]

On Thu, 2 Dec 2010, Brian Huffman wrote:

> But if we had something like a "fixes" clause for types, it would look 
> nicer and indicate the intention unambiguously, making a warning message 
> unnecessary:
>
> locale count = fixes_type 'a assumes ex_inj: "EX f::'a => nat. inj f"

This would be a substantial change in the way "polymorhphism" works in the 
system.  IIRC, Moscow ML introduced such an extension to Hindley-Milner 
typing and consequently caused some serious breakdown.


 	Makarius