GADTs but not existential quantification

Question

The following code containing existential types does not compile

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
module TestGadt () where

-- |Symbol only for arithmetic
data ArithSym = AInt Int | ASym String
-- |Symbol for arithmetic or strings or anything else
data GSym x = GInt Int | GStr String | GOther x
data Expr x = EAdd (Expr x) (Expr x) | E0 x deriving Functor
-- |Concatenate the string literals
concatStrings :: Expr (GSym x)  -> Expr (GSym x)
concatStrings = undefined
-- |Add the integer literals
addInts :: Expr (GSym x)  -> Expr (GSym x)
addInts = undefined
-- |Do some transform according to the sizes
otherOpt :: (e -> Int) -> Expr e  -> Expr e
otherOpt symSize = undefined


-- |Configuration to optimize an expression with symbols of type e.
data OptConfig e = OptConfig {
  ocSymSize :: e -> Int,
  ocGSymIso :: forall e0 . (e -> GSym e0,GSym e0 -> e)
  -- ^ this should be existential
  }

-- |Optimize given the configuration
opt :: OptConfig e -> Expr e -> Expr e
opt oc =
  otherOpt (ocSymSize oc)
  . fmap (snd $ ocGSymIso oc)
  . addInts
  . concatStrings
  . fmap (fst $ ocGSymIso oc)


arithConfig32 :: OptConfig ArithSym
arithConfig32 = OptConfig {
  ocSymSize=const 4,
  ocGSymIso=(\case{AInt i -> GInt i;ASym s -> GOther s},
             \case {GInt i -> AInt i;GOther a -> ASym a;_-> error "unreachable"})
  -- XXX: ^ ""Couldn't match type ‘e0’ with ‘String’"" even though e0
  -- should be existential!
  }

arithOpt :: Expr ArithSym -> Expr ArithSym
arithOpt = opt arithConfig32

But if I change the existential into a GADT it does:

{-# LANGUAGE GADTs #-}
[...]

-- |Configuration to optimize an expression with symbols of type e.
data OptConfig e = OptConfig {
  ocSymSize :: e -> Int,
  ocGSymIso0 :: GIso e
  -- ^ this should be existential
  }
data GIso e where
  GIso :: (e -> GSym e0,GSym e0 -> e) -> GIso e

-- |Optimize given the configuration
opt :: OptConfig e -> Expr e -> Expr e
opt oc = case ocGSymIso0 oc of
  GIso (fromE,toE) ->
    otherOpt (ocSymSize oc)
    . fmap toE
    . addInts
    . concatStrings
    . fmap fromE


arithConfig32 :: OptConfig ArithSym
arithConfig32 = OptConfig {
  ocSymSize=const 4,
  ocGSymIso0=GIso
    (\case{AInt i -> GInt i;ASym s -> GOther s},
     \case {GInt i -> AInt i;GOther a -> ASym a;_-> error "unreachable"})
  -- XXX: It works now?
  }

[...]

Can someone explain to me why one typechecks but not the other

Answer 1

The latter is an existential, but the former is not: it is an universal quantification, instead.

Note the types of the constructor:

-- first definition
OptConfig :: forall e. (e -> Int) -> (forall e0 . (e -> GSym e0,GSym e0 -> e))
          -> OptConfig e
-- second definition
OptConfig :: forall e e0. (e -> Int) -> (e -> GSym e0,GSym e0 -> e)
          -> OptConfig e

The position of the forall e0 differs, changing the the effective meaning of the quantifier, from universal to existential.

Try this notation, instead, if you do not want to use GADT syntax (which I would prefer):

-- |Configuration to optimize an expression with symbols of type e.
data OptConfig e = forall e0 . OptConfig {
  ocSymSize :: e -> Int,
  ocGSymIso :: (e -> GSym e0,GSym e0 -> e)
  -- ^ this should be existential
  }