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