I'm curious: is there any real-world use of GADTs, other than in PL
itself?  I mean, writing interpreters, compilers, and such?  Any non-PL use?

Again, not trying to start a flame-war -- just *curious*.