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

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.

But someone would need to write down a type system.

I agree here. I think we'd need more Medium Thought (not quite Hard Thought) before committing to this plan, but it still seems plausible. Richard