Typecheck TypeAbstractions lambda expressions without explicit type ascriptions
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:
{-# 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:
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. 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, 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.