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

[Eric Seidel]

On Tue, Mar 5, 2019, at 16:19, Richard Eisenberg wrote:
> 
> 
> > On Mar 5, 2019, at 11:34 AM, Simon Peyton Jones <simonpj at microsoft.com> 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.