On 10/30/17, Csongor Kiss <kiss.csongor.k...@gmail.com> wrote: > 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>.
Yep. Visible type application on the RHS is what I am after. It is just user-unfriendly that one has to doubly pattern match on the same object in order to bring the GADT constructor's type equality into play. Thanks Csongor for the expanded reasoning! Gabor > > 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