Q: Types in GADT pattern match

Mon Oct 30 12:39:39 UTC 2017

Right, but I think Gabor's suggestion here is for type checking of the pattern to be done first, and then capturing the coercions
that were brought into scope by the pattern match.

data Foo a where
  Bar :: Foo [a]

foo :: Foo a -> ()
foo Bar = <body> -- we know (a ~ [b]) here, for some b

The pattern match on Bar in foo gives us the equality assumption on the right hand side, but
we don't have an easy way of capturing 'b' - which we might want to do for, say, visible type application inside <body>.

foo' :: Foo a -> ()
foo' (Bar :: Foo a) = <body>

of course works, but it only gives us access to 'a' in <body>.

foo'' :: Foo a -> ()
foo'' (Bar :: Foo [c]) = <body>

This would mean that in addition to (a ~ [b]), for some b, we would get (a ~ [c]), for our new c. This then gives (b ~ c),
essentially giving us access to the existential b. Of course we would need to check that our scoped type signature
doesn't introduce bogus coercions, like

foo''' :: Foo a -> ()
foo''' (Bar :: Foo [[c]]) = <body>

is clearly invalid, because (a ~ [b]) and (a ~ [[c]]) would need (b ~ [c]), which we can't prove from the given assumptions.

Cheers,
Csongor

On 30 Oct 2017, 12:13 +0000, Brandon Allbery <allbery.b at gmail.com>, wrote:
> > 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
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20171030/5184d07a/attachment.html>