What GADTs aren't useful for

[AntC2]

@romes

In fact, (one of) the most canonical example of GADTs (Vec) doesn’t use type class constraints at all, and actually, the other common example, creating an AST for expressions using GADTs doesn’t either.

I think you’ll find there are constraints built into the constructors under the hood:

data Term a where
    Lit    :: !Int -> Term Int

-- ===> Lit :: a ~ Int => a -> Term a

So the ~ constraint gets exposed on a pattern match on Lit x.

(Vec appears to be a data family these days, BTW.)