On Mon, Oct 30, 2017 at 5:14 AM, Gabor Greif
My original question, though, is not answered yet, namely why not to detect that we are about to pattern match on a GADT constructor and allow the programmer to capture the *refined* type with her type annotation. Sure this would necessitate a change to the type checker, but would also increase the expressive power a bit.
Is there some fundamental problem with this? Or simply nobody wanted to do this yet? Would it be hard to implement type checking *after* refinement on GADT(-like) patterns?
I wouldn't be surprised if type checking is precisely what enables refinement, making this a bit chicken-and-egg. -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net