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 Eisenberg <r...@cs.brynmawr.edu> wrote: > 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 <ggr...@gmail.com> 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