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.

Handhold

Why can't you just add (==) _ _ = False? – Nellanellda

@Satvik: That's not really the point -- it's an impossible case, and in some cases you wouldn't be able to produce a value out of nowhere (and you shouldn't really have to come up with one anyway). – Telic

@Telic You are trying to say that only value of type Vector '[] a is Nil? What about undefined? – Nellanellda

What does undefined have to do with exhaustivity checking? not :: Bool -> Bool; not False = True; not True = False doesn't need an _ case, and neither should this. – Telic

No. That's the point of the GADT: If v is [], then the only possible constructor is Nil; if v is _ : _, then the only possible constructor is Vec. Since the two types match, their constructors must also match (and GHC "knows" that, which is why it gives an error when you try to match on two different constructors). – Telic

@Telic thanks. I understand the point now. – Nellanellda

@Nellanellda The type of == is Eq a => a -> a -> Bool or instantiated with Vect v a, Vect v a -> Vect v a -> Bool. The type of Nil is Vect '[] a and the type of Vec undefined Nil (for example) is Vect (() ': '[]) a. Those two values can't be arguments to the == function because their types differ. – Handhold

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.

Telic

I thought it was an issue with DataKinds. Looks like you don't even need DataKinds to have this problem, it is caused solely by GADTs. – Handhold

Yep, it's a much more general issue. – Telic

I believe that ghc.haskell.org/trac/ghc/ticket/595 is the primary ticket for this. – Lucilucia