New subject: Types in GADT pattern match

29 Oct 2017

      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

Q: Types in GADT pattern match

Gabor Greif

Oleg Grenrus

Richard Eisenberg

Gabor Greif

Brandon Allbery

Csongor Kiss

Gabor Greif

Simon Peyton Jones

Gabor Greif

tags

participants (6)