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 <allber...@gmail.com>, wrote: > > 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
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
