Type application in patterns ignores inferredness of type variables
Summary
When a constructor has inferred arguments, like k
in Proxy :: forall {k} (t :: k). Proxy t
, type application in patterns (!2464 (closed)) treats the k
as though it were not inferred.
Steps to reproduce
import Data.Kind
data Proxy t where
Proxy :: forall {k} (t :: k) . Proxy t
a :: () -> Proxy Int
-- a = Proxy @Type @Int -- This would, rightfully, not compile
a () = Proxy @Int
b :: Proxy Int -> ()
b (Proxy @Type @Int) = () -- This compiles, but shouldn't
b (Proxy @Int) = () -- This should compile, but doesn't
{--
TypeAppBug.hs:13:4: error:
* Expected a type, but found something with kind `Int'
* In the pattern: Proxy @Int
In an equation for `b': b (Proxy @Int) = ()
|
13 | b (Proxy @Int) = () -- This should compile, but doesn't
| ^^^^^^^^^^
--}
Expected behavior
Accept and reject the same type applications in patterns as in expressions
Environment
- GHC version used: 9.3.20210925
Optional:
- Operating System: Arch
- System Architecture: x86_64