Q: Types in GADT pattern match

[Gabor Greif]

Hi Oleg, Richard,

thanks for your answers! Seems like my original diagnosis is correct and
GADT type refinement is done *after* the checking of the pattern type signature.

My workaround

  >  foo b at Bar | (c :: Foo [x]) <- b = ... @x ...

works perfectly well and is essentially the same what Richard
suggests, while being
a little less gross.

My original question, though, is not answered yet, namely why not to
detect that we are about to pattern match on a GADT constructor and
allow the programmer to capture the *refined* type with her type
annotation. Sure this would necessitate a change to the type checker,
but would also increase the expressive power a bit.

Is there some fundamental problem with this? Or simply nobody wanted
to do this yet? Would it be hard to implement type checking *after*
refinement on GADT(-like) patterns?

Cheers and thanks,

    Gabor


On 10/30/17, Richard Eisenberg <rae at cs.brynmawr.edu> wrote:
> 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
>
>