Rank-2 polymorphism and pattern matching

[Simon Peyton-Jones]

| > 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: []

This is a pretty strange thing to do, to match a polymorphic argument against a data constructor.  I guess you'd expect this to work too, perhaps?

f :: forall a.  (forall b. Either a b) -> a
f (Left x) = x

I grant that arguably these should work, but I think it'd be quite tricky to make it do so, because it'd involve re-generalising in the pattern.  Furthermore, I can't see any use for it.  Just remove the type signature from the pattern.

One could argue that it's a bad sign that the pattern typechecker should have difficulty with this.  But until it turns out to be important I'm not going to lose sleep over it!

Interesting example though.  Perhaps the error message should be better.

Simon