GADTSyntax and ExistentialQuantification is enough to define GADT
{-# LANGUAGE GADTSyntax, ExistentialQuantification #-}
data Tag i where
TagInt :: Int -> Tag Int
TagBool :: Bool -> Tag Bool
Is accepted with all GHCs knowing about GADTSyntax
(i.e. starting from GHC-7.2.2 to GHC-9.4.2).
But I find it surprising. That is GADT, and pattern matching on the values of that type require GADTs
, e.g. to define
fromTag :: Tag i -> i
fromTag (TagInt x) = x
fromTag (TagBool x) = x
we need to enable GADTs
.
I don't think that Tag
can be defined using ExistentialQuantification
syntax, can it?
EDIT: I think this is important to address as GHC2021
enables GADTSyntax
and ExistialQuantification
but doesn't enable GADTs
, leaving weird inconsistency in that you can define a thing which you cannot use properly.