Hello Greg, It seems that I am late for the party but we used a "GADT parser" in the tool we built for our "Generating Generic Functions" paper[1]. It so happens that I made slides for this material so, if you're interested you can have a look at [2]. The motivation for doing this was that we needed to check whether a simply typed lambda calculus term satisfies a property or not. The road we took was software testing, but for that we needed evaluation and hence the GADT stuff. You might like the fact that these well-typed terms include binding constructs such as lambda abstractions and variables. The code uses some tricks that I borrowed from Conor McBride and company :). Cheers, Alexey [1] http://www.cs.uu.nl/wiki/Alexey/GeneratingGenericFunctions [2] http://abaris.zoo.cs.uu.nl:8080/wiki/pub/Alexey/GeneratingGenericFunctions/C...