Pattern matching on GADT pattern synonyms
If I define a GADT
{-# LANGUAGE PatternSynonyms, GADTs #-}
module X where
data T a b where
MkT :: T a a
pattern MkT2 = MkT
GHC requires an extension to pattern match on the constructor MkT
:
f :: T a b -> a -> b
f MkT x = x
• A pattern match on a GADT requires the GADTs or TypeFamilies language extension
• In the pattern: MkT
In an equation for ‘f’: f MkT x = x
but not on the pattern synonym MkT2
:
g :: T a b -> a -> b
g MkT2 x = x
I think pattern synonyms shouldn't be special in this regard - we should either remove the requirement for normal data constructors or enforce it for pattern synonyms.
Related: #18469