Rank-2 polymorphism and pattern matching

[Daniil Elovkov]

Hello

On Sat, 29 Dec 2007 10:59:19 +0300, Jim Apple  
<jbapple+ghc-users at gmail.com> wrote:

> The following won't compile for me
>
> isnull :: (forall a . [a]) -> Bool
> isnull ([] :: forall b . [b]) = True
>
>    Couldn't match expected type `forall b. [b]'
>            against inferred type `[a]'
>     In the pattern: []
>
> Wrapping it in a constructor doesn't help, though I can define a "null":
>
> data NullList = NullList (forall a . [a])
> null = NullList []
>
> isnull2 :: NullList -> Bool
> isnull2 (NullList []) = True
>
> Why?



Well, the wise people shall tell you precisely why.

I think, it's because you cannot pattern match the existentials in a way  
that lets escape something out of (forall) context. Of course, in this  
particular case the pattern [] doesn't bind anything, so definitely  
nothing can escape. But it seems like ghc doesn't track this special case.

Of course,

isnull :: (forall a . [a] -> Bool)
isnull ([] :: forall b . [b]) = True

will work.

Consider this

-- inferred type is forall a. ([a] -> Bool)
isn [] = True -- usual function

isnull :: (forall a . [a]) -> Bool
isnull x = isn x

it works because you apply a function isn, which has (implicitly) Bool  
inside the forall context to a forall value.

--
Daniil Elovkov