Q: Types in GADT pattern match

[Oleg Grenrus]

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 at 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 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 --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20171029/ba0258d8/attachment.sig>