Is this use of GADTs fully equivalent to existential types?

Question

Existentially quantified data constructors like

data Foo = forall a. MkFoo a (a -> Bool)
         | Nil

can be easily translated to GADTs:

data Foo where 
    MkFoo :: a -> (a -> Bool) -> Foo
    Nil :: Foo

Are there any differences between them: code which compiles with one but not another, or gives different results?

Answer 1

They are nearly equivalent, albeit not completely so, depending on which extensions you turn on.

First of all, note that you don't need to enable the GADTs extension to use the data .. where syntax for existential types. It suffices to enable the following lesser extensions.

{-# LANGUAGE GADTSyntax #-}
{-# LANGUAGE ExistentialQuantification #-}

With these extensions, you can compile

data U where
    U :: a -> (a -> String) -> U

foo :: U -> String
foo (U x f) = f x

g x = let h y = const y x
      in  (h True, h 'a')

The above code also compiles if we replace the extensions and the type definition with

{-# LANGUAGE ExistentialQuantification #-}
data U = forall a . U a (a -> String)

The above code, however, does not compile with the GADTs extension turned on! This is because GADTs also turns on the MonoLocalBinds extension, which prevents the above definition of g to compile. This is because the latter extension prevents h to receive a polymorphic type.