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? I suppose you could say (forall b. (forall a. b -> b)), but presumably it could equally well have the type (forall a. a->a). I think I can see an algorithm. But someone would need to write down a type system. (I think I was probably was wrong to mutter about impredicativity.) Simon From: ghc-steering-committee <ghc-steering-committee-bounces@haskell.org> On Behalf Of Richard Eisenberg Sent: 05 March 2019 03:06 To: Eric Seidel <eric@seidel.io> Cc: ghc-steering-committee@haskell.org Subject: Re: [ghc-steering-committee] Discussion on #155 Type Variable in Labmdas On Mar 3, 2019, at 8:44 PM, Eric Seidel <eric@seidel.io<mailto:eric@seidel.io>> wrote: Why not say that `\ @a -> body` infers the type `forall a. ty` where `body :: ty`, and let unification handle the rest? That's intriguingly simple. I haven't thought through the consequences of this fully, but it does seem plausible. I'm not ready to commit to that, but after a few minutes' focused thought, I can't see any problems with it. In any case, the proposal as written is forward-compatible with such a change, as doing what you say will allow only more programs: ones accepted by the proposal will remain accepted and with the same meanings. Richard