Annotating Pattern Synonym Breaks Typechecking
Consider this module:
{-# LANGUAGE TypeFamilies
, TypeFamilyDependencies
, DataKinds
, TypeOperators
, GADTs
, FlexibleContexts
, PatternSynonyms
#-}
module Strange where
data Expr a where
Tuple :: NTup ts -> Expr (Flatten ts)
data NTup (ts :: [*]) where
Unit :: NTup '[]
Pair :: Expr a -> NTup ts -> NTup (a ': ts)
type family Flatten ts = r | r -> ts where
Flatten '[] = ()
Flatten '[a, b] = (a, b)
pattern P a b = Pair a (Pair b Unit)
fstExpr :: Expr (a, b) -> (Expr a, Expr b)
fstExpr (Tuple (P x y)) = (x, y)
GHC 8.6.4 accepts this program and infers the type Expr a -> Expr a1 -> NTup '[a, a1]
for P
. Annotating P
with this type like so:
pattern P :: Expr a -> Expr b -> NTup '[a, b]
pattern P a b = Pair a (Pair b Unit)
Causes the program to be rejected with:
Strange.hs:26:17: error:
• Could not deduce: ts ~ '[a, b]
from the context: (a, b) ~ Flatten ts
bound by a pattern with constructor:
Tuple :: forall (ts :: [*]). NTup ts -> Expr (Flatten ts),
in an equation for ‘fstExpr’
at Strange.hs:26:10-22
‘ts’ is a rigid type variable bound by
a pattern with constructor:
Tuple :: forall (ts :: [*]). NTup ts -> Expr (Flatten ts),
in an equation for ‘fstExpr’
at Strange.hs:26:10-22
Expected type: NTup ts
Actual type: NTup '[a, b]
• In the pattern: P x y
In the pattern: Tuple (P x y)
In an equation for ‘fstExpr’: fstExpr (Tuple (P x y)) = (x, y)
• Relevant bindings include
fstExpr :: Expr (a, b) -> (Expr a, Expr b)
(bound at Strange.hs:26:1)
|
26 | fstExpr (Tuple (P x y)) = (x, y)
| ^^^^^