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