[Haskell-cafe] Type equality with "forall"

[Oleg]

There are no problems in the code you have posted so far: it works
exactly as it is supposed to. Overlapping instances worked as
designed. It seems the problem is not in Haskell but in your
expectations of existentials. Existentials are a means of abstraction,
that is, deliberately forgetting details. In our case, forgetting all
the details about the type. Consider the following code

data W where
  Wrap :: a -> W


test1 = case Wrap True of
          Wrap x -> not x

It does not type-check. The variable x in test1 has the type which is
different from any other existing type. Therefore, you cannot do
anything sensible with it -- in particular, you cannot apply 'not',
which works only for Booleans. Can't GHC just see that ``x is Bool''
-- just look at the line above!? No, by using the existential you
specifically told GHC to forget all it knows about the type of the
Wrapped value.

If you want to remember some information about the existential type,
you have to do it explicitly. For example, you can use Typeable
and cast

data W where
  Wrap :: Typeable a => a -> W


test1 = case Wrap True of
          Wrap x' | Just x <- cast x' -> not x
          Wrap _ -> error "not a Bool"

or build your own Universe (if you know in advance all the types you
will be working with)

data TypeRep a where
  TInt  :: TypeRep Int
  TBool :: TypeRep Bool
  TArr  :: TypeRep a -> TypeRep b -> TypeRep (a -> b)
  

data W where
  Wrap :: TypeRep a -> a -> W


test1 :: Bool
test1 = case Wrap TBool True of
          Wrap TBool x -> not x
          Wrap _ _ -> error "not a Bool"


In the latter case, the type signature is required. Basically, you
have to write signature for every function that pattern-matches on the
real GADTs (sometimes you can get away; but oftentimes you'll get a
really cryptic error message instead). The latter pattern, using
TypeRep, is the foundation of basically all generic programming out
there.