Re: Q: Types in GADT pattern match
On 10/30/17, Csongor Kisswrote: > 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 = -- 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 . 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) = > > of course works, but it only gives us access to 'a' in . > > foo'' :: Foo a -> () > foo'' (Bar :: Foo [c]) = > > 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]]) = > > 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 +, Brandon Allbery , wrote: >> > On Mon, Oct 30, 2017 at 5:14 AM, Gabor Greif 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
Re: Q: Types in GADT pattern match
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 = -- 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 . foo' :: Foo a -> () foo' (Bar :: Foo a) = of course works, but it only gives us access to 'a' in . foo'' :: Foo a -> () foo'' (Bar :: Foo [c]) = 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]]) = 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 +, Brandon Allbery, wrote: > > On Mon, Oct 30, 2017 at 5:14 AM, Gabor Greif 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
Re: Q: Types in GADT pattern match
On Mon, Oct 30, 2017 at 5:14 AM, Gabor Greifwrote: > 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, xmonadhttp://sinenomine.net ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Q: Types in GADT pattern match
Hi Oleg, Richard, thanks for your answers! Seems like my original diagnosis is correct and GADT type refinement is done *after* the checking of the pattern type signature. My workaround > foo b@Bar | (c :: Foo [x]) <- b = ... @x ... works perfectly well and is essentially the same what Richard suggests, while being a little less gross. 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? Cheers and thanks, Gabor On 10/30/17, Richard Eisenbergwrote: > Hi Gabor, > > Oleg is right that the re-use of type variables obscures the error, but it's > not quite a scoping error under the hood. The problem is that GHC > type-checks type signatures on patterns *before* type-checking the pattern > itself. That means that when GHC checks your `Foo [a]` type signature, we > haven't yet learned that `a1` (the type variable used in the type signature > of foo) equals `[a]`. This makes it hard to bind a variable to `a`. Here's > what I've done: > >> foo :: Foo a -> () >> foo b@Bar = case b of >> (_ :: Foo [c]) -> quux b >> where >> quux :: Foo [c] -> () >> quux Bar = () > > It's gross, but it works, and I don't think there's a better way at the > moment. A collaborator of mine is working on a proposal (and implementation) > of binding existentials in patterns (using similar syntax to visible type > application), but that's still a few months off, at best. > > Richard > >> On Oct 29, 2017, at 1:42 PM, Gabor Greif wrote: >> >> Hi Devs! >> >> I encountered a curious restriction with type signatures (tyvar bindings) >> in GADT pattern matches. >> >> GHC won't let me directly capture the refined type structure of GADT >> constructors like this: >> >> >> {-# Language GADTs, ScopedTypeVariables #-} >> >> data Foo a where >> Bar :: Foo [a] >> >> foo :: Foo a -> () >> foo b@(Bar :: Foo [a]) = quux b >> where quux :: Foo [b] -> () >> quux Bar = () >> >> >> I get: >> >> >> test.hs:7:8: error: >> • Couldn't match type ‘a1’ with ‘[a]’ >> ‘a1’ is a rigid type variable bound by >> the type signature for: >> foo :: forall a1. Foo a1 -> () >> at test.hs:6:1-18 >> Expected type: Foo a1 >> Actual type: Foo [a] >> >> >> To me it appears that the type refinement established by the GADT pattern >> match is not accounted for. >> >> Of course I can write: >> >> foo :: Foo a -> () >> foo b@Bar | (c :: Foo [a]) <- b = quux c >> where quux :: Foo [b] -> () >> quux Bar = () >> >> but it feels like a complicated way to do it... >> >> My question is whether this is generally seen as the way to go or whether >> ScopedTypeVariables coming from a GADT pattern match should be able to >> capture the refined type. To me the latter seems more useful. >> >> Just wanted to feel the waters before writing a ticket about this. >> >> Cheers and thanks, >> >> Gabor >> ___ >> 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
Re: Q: Types in GADT pattern match
Hi Gabor, Oleg is right that the re-use of type variables obscures the error, but it's not quite a scoping error under the hood. The problem is that GHC type-checks type signatures on patterns *before* type-checking the pattern itself. That means that when GHC checks your `Foo [a]` type signature, we haven't yet learned that `a1` (the type variable used in the type signature of foo) equals `[a]`. This makes it hard to bind a variable to `a`. Here's what I've done: > foo :: Foo a -> () > foo b@Bar = case b of > (_ :: Foo [c]) -> quux b > where > quux :: Foo [c] -> () > quux Bar = () It's gross, but it works, and I don't think there's a better way at the moment. A collaborator of mine is working on a proposal (and implementation) of binding existentials in patterns (using similar syntax to visible type application), but that's still a few months off, at best. Richard > On Oct 29, 2017, at 1:42 PM, Gabor Greifwrote: > > Hi Devs! > > I encountered a curious restriction with type signatures (tyvar bindings) in > GADT pattern matches. > > GHC won't let me directly capture the refined type structure of GADT > constructors like this: > > > {-# Language GADTs, ScopedTypeVariables #-} > > data Foo a where > Bar :: Foo [a] > > foo :: Foo a -> () > foo b@(Bar :: Foo [a]) = quux b > where quux :: Foo [b] -> () > quux Bar = () > > > I get: > > > test.hs:7:8: error: > • Couldn't match type ‘a1’ with ‘[a]’ > ‘a1’ is a rigid type variable bound by > the type signature for: > foo :: forall a1. Foo a1 -> () > at test.hs:6:1-18 > Expected type: Foo a1 > Actual type: Foo [a] > > > To me it appears that the type refinement established by the GADT pattern > match is not accounted for. > > Of course I can write: > > foo :: Foo a -> () > foo b@Bar | (c :: Foo [a]) <- b = quux c > where quux :: Foo [b] -> () > quux Bar = () > > but it feels like a complicated way to do it... > > My question is whether this is generally seen as the way to go or whether > ScopedTypeVariables coming from a GADT pattern match should be able to > capture the refined type. To me the latter seems more useful. > > Just wanted to feel the waters before writing a ticket about this. > > Cheers and thanks, > > Gabor > ___ > 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
Re: Q: Types in GADT pattern match
The problem is scoping. The problem is more obvious if you don't reuse type-variables: {-# Language GADTs, ScopedTypeVariables #-} data Foo a where Bar :: Foo [x] foo :: Foo a -> () foo b@(Bar :: Foo [c]) = quux b where quux :: Foo [b] -> () quux Bar = () Then you'll get an: Couldn't match type ‘a’ with ‘[c]’ error. I.e. GHC tries to match `foo`s type signatures, with annotation on variable `b`. But you don't need it. If you remove it, everything works fine: {-# Language GADTs, ScopedTypeVariables #-} data Foo a where Bar :: Foo [x] foo :: Foo a -> () foo b@Bar = quux b where quux :: Foo [b] -> () quux Bar = () Cheers, Oleg. On 29.10.2017 19:42, Gabor Greif wrote: > Hi Devs! > > I encountered a curious restriction with type signatures (tyvar > bindings) in GADT pattern matches. > > GHC won't let me directly capture the refined type structure of GADT > constructors like this: > > > {-# Language GADTs, ScopedTypeVariables #-} > > data Foo a where > Bar :: Foo [a] > > foo :: Foo a -> () > foo b@(Bar :: Foo [a]) = quux b > where quux :: Foo [b] -> () > quux Bar = () > > > I get: > > > *test.hs:7:8: **error:* > > * • Couldn't match type ‘a1’ with ‘[a]’* > > * ‘a1’ is a rigid type variable bound by* > > * the type signature for:* > > * foo :: forall a1. Foo a1 -> ()* > > * at test.hs:6:1-18* > > * Expected type: Foo a1* > > * Actual type: Foo [a]* > > * > * > > To me it appears that the type refinement established by the GADT > pattern match is not accounted for. > > Of course I can write: > > foo :: Foo a -> () > foo b@Bar | (c :: Foo [a]) <- b = quux c > where quux :: Foo [b] -> () > quux Bar = () > > but it feels like a complicated way to do it... > > My question is whether this is generally seen as the way to go or > whether ScopedTypeVariables coming from a GADT pattern match should be > able to capture the refined type. To me the latter seems more useful. > > Just wanted to feel the waters before writing a ticket about this. > > Cheers and thanks, > > Gabor > > > ___ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs signature.asc Description: OpenPGP digital signature ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Q: Types in GADT pattern match
Hi Devs! I encountered a curious restriction with type signatures (tyvar bindings) in GADT pattern matches. GHC won't let me directly capture the refined type structure of GADT constructors like this: {-# Language GADTs, ScopedTypeVariables #-} data Foo a where Bar :: Foo [a] foo :: Foo a -> () foo b@(Bar :: Foo [a]) = quux b where quux :: Foo [b] -> () quux Bar = () I get: *test.hs:7:8: **error:* *• Couldn't match type ‘a1’ with ‘[a]’* * ‘a1’ is a rigid type variable bound by* *the type signature for:* * foo :: forall a1. Foo a1 -> ()* *at test.hs:6:1-18* * Expected type: Foo a1* *Actual type: Foo [a]* To me it appears that the type refinement established by the GADT pattern match is not accounted for. Of course I can write: foo :: Foo a -> () foo b@Bar | (c :: Foo [a]) <- b = quux c where quux :: Foo [b] -> () quux Bar = () but it feels like a complicated way to do it... My question is whether this is generally seen as the way to go or whether ScopedTypeVariables coming from a GADT pattern match should be able to capture the refined type. To me the latter seems more useful. Just wanted to feel the waters before writing a ticket about this. Cheers and thanks, Gabor ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs