RE: GHC type-checker bug

| The following program:
| 
|  > f :: (forall a. Eq a => [a]) -> Bool
|  > f xs@(x:_)  = x
|  >
|  > main = main
| 
| Causes ghc to report the following:
| 
| ghc-6.2.1: panic! (the `impossible' happened, GHC version 6.2.1):
|         cgPanic

This is certainly a bug.  The original idea is that subsumption for
higher-rank types works in pattern-matching as well as in function
applications.  In principle, it's reasonable to say
        f ::(forall a. a->a) -> ...
        f (x::Int->Int) = ...

But as you have discovered (and I did not know this) I didn't get it
right, at least for qualified types.

As it happens, in the GADT version of GHC I have already disabled this
feature -- pattern matching is complicated enough, and the feature was
not at all useful in practice.  So your three examples consistently give
the error:

tcfail124.hs:6:7:
    Couldn't match `forall a. (Eq a) => [a]' against `[a]'
    In the definition of `f1': f1 (xs@(x : _)) = x


I've added all three variants of your example to the test suite
(tcfail124).  I'm lazily disinclined to fix 6.2.2, because it'll take me
a while to page it all in again, and (as you say) it's a very dark
corner.

Thanks for pointing it out.

Simon