Q: Types in GADT pattern match

[Richard Eisenberg]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20171029/6a41f081/attachment.html>