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 |