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 <[email protected]> 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 > [email protected] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
