[Haskell-cafe] A Specification for GADTs in Haskell?

Hello all, I recently came a cross a comment by Richard Eisenberg that there's actually no specification for GADTs and creating one would be a major research project (in a GHC proposal somewhere, I recall, but I don't remember exactly where). I was wondering what exactly does Richard's comment mean. What constitutes a specification for GADTs in Haskell? I suppose typing rules and semantics are necessary; what are the major roadblocks hindering the creation of a formal specification for GADTs in Haskell? Thanks! Xuanrui -- Xuanrui Qi Graduate School of Mathematics, Nagoya University https://www.xuanruiqi.com