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

[Xuanrui Qi]

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