Abstracting out pattern into a pattern synonym fails with scary error
This works
{-# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #-}
import Data.Kind
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(a -> as)
data ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where
AO :: a -> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) ctx
-> ApplyT(k -> ks) f (a:&:ctx)
foo :: ApplyT(Type -> Type -> Type) Either a -> ()
foo (ASSO (Left a)) = ()
pattern ASSO a = AS (AS (AO a))but then you might think, let's give a name (pattern synonym) to ASSO (Left a)
This fails
{-# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #-}
import Data.Kind
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(a -> as)
data ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where
AO :: a -> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) ctx
-> ApplyT(k -> ks) f (a:&:ctx)
pattern ASSO a = AS (AS (AO a))
pattern ASSOLeft a = ASSO (Left a)$ ghci -ignore-dot-ghci 464.hs
GHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/464.hs, interpreted )
hs/464.hs:16:22: error:
• Couldn't match type ‘k1’ with ‘*’
‘k1’ is a rigid type variable bound by
the signature for pattern synonym ‘ASSOLeft’
at hs/464.hs:16:1-34
Expected type: ApplyT kind a b
Actual type: ApplyT (* -> * -> *) Either (a1 ':&: (a20 ':&: 'E))
• In the expression: ASSO (Left a)
In an equation for ‘ASSOLeft’: ASSOLeft a = ASSO (Left a)
|
16 | pattern ASSOLeft a = ASSO (Left a)
| ^^^^^^^^^^^^^
hs/464.hs:16:28: error:
• Could not deduce: k1 ~ *
from the context: (kind ~ (k -> ks), a ~~ f, b ~~ (a2 ':&: ctx),
ks ~ (k1 -> ks1), f a2 ~~ f1, ctx ~~ (a3 ':&: ctx1), ks1 ~ *,
f1 a3 ~~ a4, ctx1 ~~ 'E)
bound by a pattern with pattern synonym:
ASSO :: forall kind (a :: kind) (b :: Ctx kind).
() =>
forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx
ks) ks1 k1 (f1 :: k1
-> ks1) (a2 :: k1) (ctx1 :: Ctx
ks1) a3.
(kind ~ (k -> ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 -> ks1),
f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,
ctx1 ~~ 'E) =>
a3 -> ApplyT kind a b,
in a pattern synonym declaration
at hs/464.hs:16:22-34
‘k1’ is a rigid type variable bound by
a pattern with pattern synonym:
ASSO :: forall kind (a :: kind) (b :: Ctx kind).
() =>
forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx
ks) ks1 k1 (f1 :: k1
-> ks1) (a2 :: k1) (ctx1 :: Ctx
ks1) a3.
(kind ~ (k -> ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 -> ks1),
f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,
ctx1 ~~ 'E) =>
a3 -> ApplyT kind a b,
in a pattern synonym declaration
at hs/464.hs:16:22-34
When matching types
a3 :: k1
b0 :: *
Expected type: a4
Actual type: Either a1 b0
• In the pattern: Left a
In the pattern: ASSO (Left a)
In the declaration for pattern synonym ‘ASSOLeft’
|
16 | pattern ASSOLeft a = ASSO (Left a)
| ^^^^^^
Failed, no modules loaded.
Prelude> Can I, as a user, assume that any valid pattern foo (ASSO (Left a)) = ... can be abstracted into a pattern synonym? There error message is too scary for me to sensibly know what to expect
Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |