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.
Edited by Oleg Grenrus