Re: [ghc-steering-committee] Discussion on #155 Type Variable in Labmdas

On Tue, Mar 5, 2019, at 16:19, Richard Eisenberg wrote:

...

On Mar 5, 2019, at 11:34 AM, Simon Peyton Jones wrote:

I haven't thought through the consequences of this fully, but it does seem plausible. It says we must generalise over some ‘a’, but *which* ‘a’? What type does (\@a (\x. x)) have?

My understanding of Eric's idea is that GHC would give (\x.x) the type (alpha -> alpha), as usual. Then (\ @a (\x.x)) gets the type forall a. alpha -> alpha. Later, we might solve for alpha or generalize over it, perhaps leading a type like forall b a. b -> b.

Yep, that's precisely what I would expect. It doesn't need to happen for this proposal, but it would make a very nice addition assuming the theory works out.