GHC complains about non-exhaustive patterns that are enforced by the type checker

Question

I have the following code

{-# LANGUAGE DataKinds, GADTs, TypeOperators #-}

data Vect v a where
    Nil :: Vect '[] a
    Vec :: a -> Vect v a -> Vect (() ': v) a 

instance Eq a => Eq (Vect v a) where
    (==) Nil Nil               = True
    (Vec e0 v0) == (Vec e1 v1) = e0 == e1 && v0 == v1

When compiling or interpreting with -Wall the following warning is given:

Pattern match(es) are non-exhaustive
In an equation for `==':
    Patterns not matched:
        Nil (Vec _ _)
        (Vec _ _) Nil

Normally this is to be expected. Normally, even if I can reason that my patterns will cover all possible cases, there is no way for the compiler to know that without running the code. However, the exhaustiveness of the provided patterns are enforced by the type checker, which runs at compile time. Adding the patterns suggested by GHC gives a compile time time error:

Couldn't match type '[] * with `(':) * () v1'

So my question is this: do GHC warnings just not play well with GHC extensions? Are they supposed to be aware of each other? Is this functionality (warnings taking into account extensions) slated for a future release, or is there some technical limitation to implementing this feature?

It seems that the solution is simple; the compiler can try adding the supposedly unmatched pattern to the function, and asking the type checker again if the suggested pattern is well typed. If it is, then it can indeed be reported to the user as a missing pattern.

Answer 1

This looks like a bug -- here's a slightly simpler version:

data Foo :: Bool -> * where
    A :: Foo False
    B :: Foo True

hmm :: Foo b -> Foo b -> Bool
hmm A A = False
hmm B B = True

It also looks like it's a known bug, or part of a family of known bugs -- the closest I could find in a few minutes of looking was #3927.