Q: Types in GADT pattern match

[Brandon Allbery]

On Mon, Oct 30, 2017 at 5:14 AM, Gabor Greif <ggreif at 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
allbery.b at gmail.com                                  ballbery at sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20171030/49622156/attachment-0001.html>