I am using GHC 9.10.1-alpha3, which debuts support for `TypeAbstractions` in lambda positions. Or rather, it debuts _partial_ support. I was surprised to discover that the following example does not typecheck: ```hs {-# LANGUAGE GHC2024 #-} {-# LANGUAGE TypeAbstractions #-} module Foo where doesn'tWork :: forall a. Maybe a doesn'tWork = \ @a -> Nothing @a ``` ``` $ ghc-9.10.0.20240413 Foo.hs [1 of 1] Compiling Foo ( Foo.hs, Foo.o ) Foo.hs:6:18: error: [GHC-14964] • Invisible type pattern a has no associated forall • In the expression: \ @a -> Nothing @a In an equation for ‘doesn'tWork’: doesn'tWork = \ @a -> Nothing @a | 6 | doesn'tWork = \ @a -> Nothing @a | ^ ``` But the following example _does_ typecheck: ```hs doesWork = (\ @a -> Nothing @a) :: forall a. Maybe a ``` At first, I believed this to be a bug, but upon a closer look in the GHC User's Guide, this behavior is actually documented [here](https://gitlab.haskell.org/ghc/ghc/-/blob/e1cf8dc2c941d36dc92139faa07ee6baf2599e38/docs/users_guide/exts/type_abstractions.rst#L168-178). My `doesn'tWork` example is a simpler version of `f2` in the User's Guide, and my `doesWork` example is a simpler version of `f3` in the User's Guide. My question is: is there a technical reason why we can't make both styles of examples typecheck? To my (untrained) eye, they appear to have exactly the same amount of type information available. I tried reading the [corresponding GHC proposal](https://github.com/ghc-proposals/ghc-proposals/blob/a8ea5cc8f4fe24d2885d5d0fb4b61a865e5a5f1b/proposals/0155-type-lambda.rst), but I couldn't find explicit mention of this limitation anywhere, so I'm unclear what the challenges are. My hope is that this is not a fundamental limitation of `TypeAbstractions` but rather an implementation challenge. If so, I'd like to dedicate this issue to the task of implementing full support for examples like `doesn'tWork` above.