This post so far the best example of GADTs I have found. Most just go about “here is an AST type for our compiler” which is certainly useful for compiler writers but making a case for it in other areas was tricky for me. What I especially like here is the “disadvantages” section, which discusses what the drawbacks are (aka not “magic unicorn dust”).
I’ve used GADTs for the first time in a project recently. It’s a “fetch” function that returns a different type based on the input arguments. It all typechecks without having to wrap the output in a variant and do pattern matching every time I have to handle the returned value from that function. It’s amazing.