Types in GADT pattern match

[Gabor Greif]

On 10/30/17, Simon Peyton Jones <simonpj at microsoft.com> wrote:
> foo b@(Bar :: Foo [a]) = quux b
> The pattern (p :: ty) checks that the thing being matched has type ‘ty’ and
> THEN matches ‘p’.  You expected it to FIRST match ‘p’, and THEN check that
> the thing being matched has type ‘ty’.  But that’s not the way it works.

Yep. Understood. I was just hoping that one could annotate the
"insider view" of GADT pattern matches (considering the equality
constraints of the constructor) as well as the "outsider view", namely
'foo's external signature.

>
> e.g what about this
>
>             rats ([Just (Bar, True)] :: [Maybe (Foo [a], Bool)]) = …
>
> Here the pattern to be matched is deep, with the Bar part deep inside.  Do
> you still expect it to work?

Well, it reflects a truth, so I'd expect it to work, yes :-)

>
> This would be hard to change.  And I’m not sure it’d be an improvement.

Hmmm, sure. There are probably better areas to invest effort into.

Thanks,

    Gabor

>
> Simon
>
> From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Gabor
> Greif
> Sent: 29 October 2017 17:43
> To: ghc-devs <ghc-devs at haskell.org>
> Subject: 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 at 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
>