Pattern synonym implicit existential quantification
This code typechecks when k
is brought into scope explicitly, but not implicitly (code example courtesy of RyanGlScott):
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
import Data.Kind
import Data.Proxy
data T = forall k (a :: k). MkT (Proxy a)
-- Uncomment `k` and it typechecks
pattern P :: forall. () => forall {-k-} (a :: k). Proxy a -> T
pattern P x = MkT (x :: Proxy (a :: k))
I discovered this because I was implementing https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst and had to explicitly quantify some definitions in the test suite. Then the test case for #14498 (closed) stopped producing the error that it should.
It seems indicative of an issue in typechecking pattern synonyms: I would expect equal treatment for implicit and explicit type/kind variables.
Trac metadata
Trac field | Value |
---|---|
Version | 8.6.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | RyanGlScott |
Operating system | |
Architecture |