The sweet spot for GADTs is representing ASTs for EDSLs typefully. The characteristics of those use cases is that each data constructor: carries different constraints; returns a more specific type than `T a`; similarly recursion may be to a more specific type. There's a different use case (which is I suspect what was in mind for DatatypeContexts), with characteristics for each data constructor: * the constraints are the same for all the type's parameters; * the return type is bare `T a` * any recursion is also to bare `T a` So it's the same type `a` all the way down, and therefore the same instance for the constraint(s). Consider (adapted from the H98 Report for DatatypeContexts): {-# LANGUAGE GADTs #-} data SetG a where NilSetG :: Eq a => SetG a ConsSetG :: Eq a => a -> SetG a -> SetG a sillySetG = undefined :: SetG (Int -> Int) -- accepted, but useless -- sillySetG = NilSetG :: SetG (Int -> Int) -- rejected no Eq instance (DatatypeContext's equiv with NilSet constructor at `(Int -> Int)` is accepted, so some improvement.) elemSG x NilSetG = False elemSG x (ConsSetG y ys) | x == y = True | otherwise = elemSG x ys -- ===> elemSG :: a -> SetG a -> Bool -- no Eq a inferred The elem pattern matching test makes use of ConsSetG's Eq instance, but doesn't expose that in the inferred type. Whereas: headS (ConsSetG x _) = x -- hide the pattern match tailS (ConsSetG _ xs) = xs elemSh x NilSetG = False elemSh x yss | x == headS yss = True | otherwise = elemSG x $ tailS yss -- ==> elemSh :: Eq a => a -> SetG a -> Bool -- Eq a inferred A 'morally equivalent' elem test but with a different inferred type, exposing the `Eq a` constraint. If you give an explicit signature for `elemSh`, you must specify `Eq a` -- which is annoying same as with DatatypeContexts; an explicit signature for elemSG needn't -- which gives a more annoying imprecise type that'll get reported at some usage site. I'm concluding that for this use case, a GADT doesn't 'fix' all of the stupidness with stupid theta. AntC