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