Type variable in pattern binds invisible forall variable
Summary
Given A :: forall {k :: Type} (a :: k). A
, f (A @x) = ...
binds k
as x
, even though A @x
in an expression binds a
as x
.
Steps to reproduce
import Data.Proxy (Proxy (Proxy))
f :: Read a => Proxy a -> ()
f _ = ()
g :: Read a => Proxy a -> ()
g (Proxy @_ @a) = f (Proxy @a)
Expected behavior
This should err, and instead, g (Proxy @a) = f (Proxy @a)
should be correct.
Environment
- GHC version used: 9.2.4