On Mon, Oct 30, 2017 at 5:14 AM, Gabor Greif <ggr...@gmail.com> wrote:
> 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 allber...@gmail.com ballb...@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
