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.