Just want to point out that GADTs are not just about having data type constructors with constraints (and thus have them store dictionaries), but rather about introducing local equality constraints that further allow you to use types to express invariants and such.
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’m on the phone so I’ll pass on writing down the examples. Also, there are comprehensive write ups that do great explanations (if someone wants to link to them, could be useful).
(As I’m afraid someone might read that and take away GADTs=adding type class constraints/runtime dicts to datatypes)