Skip to content

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information