<div dir="ltr"><font face="monospace">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.</font><div><font face="monospace"><br></font></div><div><font face="monospace">There's a different use case (which is I suspect what was in mind for DatatypeContexts), with characteristics for each data constructor:</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">* the constraints are the same for all the type's parameters;</font></div><div><font face="monospace">* the return type is bare `T a`</font></div><div><font face="monospace">* any recursion is also to bare `T a`</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">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):</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">    {-# LANGUAGE  GADTs    #-}</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">    data SetG a  where<br>      NilSetG  :: Eq a => SetG a<br>      ConsSetG :: Eq a => a -> SetG a -> SetG a<br></font></div><div><font face="monospace"><br></font></div><div><font face="monospace">    sillySetG = undefined :: SetG (Int -> Int)           -- accepted, but useless<br>--     sillySetG = NilSetG :: SetG (Int -> Int)            -- rejected no Eq instance<br></font></div><div><font face="monospace"><br></font></div><div><font face="monospace">(DatatypeContext's equiv with NilSet constructor at `(Int -> Int)` is accepted, so some improvement.)</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">    elemSG x NilSetG                     = False<br>    elemSG x (ConsSetG y ys) | x == y    = True<br>                             | otherwise = elemSG x ys<br></font></div><div><font face="monospace">      -- ===> elemSG :: a -> SetG a -> Bool                           -- no Eq a inferred<br></font></div><div><font face="monospace"><br></font></div><div><font face="monospace">The elem pattern matching test makes use of ConsSetG's Eq instance, but doesn't expose that in the inferred type. Whereas:</font></div><div><font face="monospace"><br></font></div><font face="monospace">    headS (ConsSetG x _) = x                             -- hide the pattern match<br>    tailS (ConsSetG _ xs) = xs<br></font><div><font face="monospace"><br></font></div><div><font face="monospace">    elemSh x NilSetG                     = False<br>    elemSh x yss        | x == headS yss = True<br>                        | otherwise      = elemSG x $ tailS yss<br></font></div><div><font face="monospace">      -- ==> elemSh :: Eq a => a -> SetG a -> Bool                   -- Eq a inferred<br></font></div><div><font face="monospace"><br></font></div><div><font face="monospace">A 'morally equivalent' elem test but with a different inferred type, exposing the `Eq a` constraint.</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">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.</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">I'm concluding that for this use case, a GADT doesn't 'fix' all of the stupidness with stupid theta.</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">AntC</font></div></div>