Comment by nathanrf

GADTs let you do similar things in the simplest cases, they just don't work as well for complex constraints.

Like, append: Vector n t -> Vector m t -> Vector (n+m) t. With GADTs you need to manually lift (+) to work on the types, and then provide proofs that it's compatible with the value-level.

Then you often need singletons for the cases that are more complex- if I have a set of integers, and an int x, and I want to constrain that the item is in the set and is also even, the GADT approach looks like:

doThing :: Singleton Int x -> Singleton (Set Int) s -> IsInSet x s -> IsEven x -> SomeOutput

Which looks reasonable, until you remember that the Singleton type has to have a representation which is convenient to prove things about, not a representation that is convenient/efficient to operate on, which means your proofs will be annoying or your function itself will hardly resemble a "naive" untyped implementation.

Dependent types fix this because your values are "just" values, so it would be something like

doThing :: (x : int) -> (s : set int) -> so (is_in s x) -> so (even x) -> SomeOutput

Here, x and s are just plain values, not a weird wrapper, and is_in and event are ordinary (and arbitrary) library functions.