Thanks, and true. GADTs are weird creatures when you first see them. I originally thought it was entirely a syntactic thing! As weird as it is, I always recomm

Thanks, and true. GADTs are weird creatures when you first see them. I originally thought it was entirely a syntactic thing! As weird as it is, I always recommend Agda/Coq for learning GADTs. It feels like overkill, but Haskell's DT stuff is really wonky, so it's nice to see GADTs expressed in a clean manner before trying them out in Haskell.