Incomplete/overlapped pattern warnings + GADTs = inadequate

[simonpj]

Consider these defintions

data T a where
  T1 :: T Int
  T2 :: T Bool

-- f1 should be exhaustive
f1 :: T a -> T a -> Bool
f1 T1 T1 = True
f1 T2 T2 = False

-- f2 is exhaustive too, even more obviously
f2 :: T a -> T a -> Bool
f2 T1 (T1 :: T Int) = True
f2 T2 (T2 :: T Bool) = False

-- f3's first equation is unreachable
f3 :: T a -> T a -> Bool
f3 T2 T1 = False
f3 _  _  = True 

With HEAD (GHC 6.13) we get

G1.hs:11:1:
    Warning: Pattern match(es) are non-exhaustive
             In the definition of `f1':
                 Patterns not matched:
                     T1 T2
                     T2 T1

This is wrong.

• f1 should behave like f2, and be accepted without warning.
• f3 has an inaccessible branch that is not reported.

The type checker accepts just the right programs, but the rather simple-minded approach to overlap warnings isn't doing the right thing.

Note to self: the reason is that tcPat does not insert a coercion on the second arg to narrow the type, because there's no type reason to do so. So for f1 we get

f1 a (x:T a) (y:T a)
  = case x of { T1 (cox:a~Int) ->
      case y of { T1 (coy:a~Int) -> ... }

In the inner case it's not obvious that T2 is inaccessible. If we refined eagerly we might get

f1 a (x:T a) (y:T a)
  = case x of { T1 (cox:a~Int) ->
      case (y |> T cox) of { T1 (coy:Int~Int) -> ... }

and now the scrutinee of the inner case has type (T Int) and the T2 constructor obviously can't occur.

Fix this with the new inference engine.

[igloo]

See #4139 for a tricker case of the same problem.

Simon, I'm assigning the ticket to you as I think you're working on the inference engine at the moment.

Incidentally, in 6.13.20100617 this fails with:

    Pattern signature must exactly match: T a
    In the pattern: T1 :: T Int
    In the definition of `f2': f2 T1 (T1 :: T Int) = True

[pumpkin]

Mostly just adding myself to the CC list here, but I figured I'd attach the test code that made me interested in this ticket in the first place, in case you wanted a more tangible example of why some people might want this.

{-# OPTIONS_GHC -Wall #-}
{-# Language GADTs #-}

data Nz = Nz
newtype Ns n = Ns n

data Fin n where
  Fz :: Fin (Ns n)
  Fs :: Fin n -> Fin (Ns n)
  
data Vec n a where
  Nil  :: Vec Nz a
  Cons :: a -> Vec n a -> Vec (Ns n) a

-- This works nicely!
test :: Fin Nz -> a
test _ = undefined
-- test Fz = undefined -- Rightfully rejected by GHC
-- test (Fs n) = undefined -- Rightfully rejected by GHC

-- Here, "knowledge" acquired by patern matching on one parameter refines the type of the other, and in the Nil case,
-- refines the second parameter to Fin Nz, which contains nothing and thus I cannot provide a meaningful pattern.
index :: Vec n a -> Fin n -> a
index Nil Fz = error "GHC shouldn't even let me write this combination of patterns, but the coverage checker tells me my pattern is non-exhaustive if I don't write it"
index Nil (Fs _) = error "Ditto"
index (Cons x _) Fz = x
index (Cons _ xs) (Fs n) = index xs n

[simonpj]

Pumpkin, GHC is quite correct in its warnings about your code. If you put in the "error" lines in your code above, then GHC correctly warns that those branches are inaccessible:

T3927b.hs:26:11:
    Inaccessible code in
      a pattern with constructor `Fz', in an equation for `index'
    Couldn't match type `Nz' with `Ns n'
    In the pattern: Fz
    In an equation for `index':
        index Nil Fz
          = error
              "GHC shouldn't even let me write this combination of ..."

If you comment out both those lines you get the non-exhaustive warning:

T3927b.hs:28:1:
    Warning: Pattern match(es) are non-exhaustive
             In an equation for `index': Patterns not matched: Nil _

And that is right too! For example consider the call:

index Nil (undefined :: Fin Nz)

If you don't have an equation for Nil the pattern match indeed is not exhaustive. So you need an equation

index Nil _ = error "index called with Nil argument"

However, my original bug report remains valid

Simon

[pumpkin]

I understand that you can provide bottoms for Fin Nz, but the issue is that in the code I submitted, the pattern match itself is badly typed. The warning alludes to it, but the fact remains that for my index function, Nil and Fz or Fs cannot "coexist" within a pattern and have consistent types. I see that the warning spots that, but I'd expect it to be an error instead of a warning, a bit like the test function above, since the constructors in the pattern are impossible to type correctly.

Just to clarify, I'm advocating that

index :: Vec n a -> Fin n -> a
index Nil Fz = error "GHC shouldn't even let me write this combination of patterns, but the coverage checker tells me my pattern is non-exhaustive if I don't write it"
index Nil (Fs _) = error "Ditto"
index (Cons x _) Fz = x
index (Cons _ xs) (Fs n) = index xs n

be rejected, and

index :: Vec n a -> Fin n -> a
index Nil _ = error "damn!"
index (Cons x _) Fz = x
index (Cons _ xs) (Fs n) = index xs n

be accepted (that is, for a Nil in the Vec position, the only valid pattern for the Fin should be _ or a variable).

[simonpj]

Ok so you are saying that GHC is giving correct messages, but you'd like to see the warning become an error.

I don't think we'll do this:

• Technically dead GADT case alternatives are not ill-typed. (Just look at any GADT paper.)
• More pragmatically, GHC can spot some dead code, but not all dead code. Eg

   f x y | x > y  = ...
         | x <= y = ....
         | otherwise = ...dead code...
  

  Even thinking only of type equalities, the solver cannot guarantee to find all unsatisfiable contexts. So it'd be tricky to pin down exactly which programs were errors (and hence would not even compile) and which were only warnings (and hence would run).

All in all, I think it's best as it is. That said, the original bug report of this ticket still stands.

[pumpkin]

Oh! I see the difference now!

Matching on a GADT constructor introduces a type equality context on the matched variables, but doesn't refine them explicitly, as far as I can tell.

To test this, in addition to the

test :: Fin Nz -> a
test _ = undefined
-- test Fz = undefined -- Rightfully rejected by GHC
-- test (Fs n) = undefined -- Rightfully rejected by GHC

example above, I wrote the following:

test' :: (n ~ Nz) => Fin n -> a
test' Fz = undefined
test' (Fs n) = undefined

It seems like roughly the same thing as test, but GHC happily accepts the Fz and Fs constructors. I see now that that is what matching on Nil does in my original index function, so that is why the seemingly incompatible Fin constructors are accepted!

Anyway, I promise I'll shut up about this now! It had just misunderstood how GADT matching actually refined the types. I'm putting this up here for the benefit of anyone else who might be interested and have the same confusion (a couple of people in the Haskell IRC channel expressed interest in my example). Sorry for the noise :)

[Saizan]

Replying to simonpj:

Pumpkin, GHC is quite correct in its warnings about your code. If you put in the "error" lines in your code above, then GHC correctly warns that those branches are inaccessible: {{{ T3927b.hs:26:11: Inaccessible code in a pattern with constructor Fz', in an equation for index' Couldn't match type Nz' with Ns n' In the pattern: Fz In an equation for `index': index Nil Fz = error "GHC shouldn't even let me write this combination of ..." }}}

but with the latest GHC HEAD that's an error not just a warning (ghci refuses to load the module, at least), so it actually implements what pumpkin is advocating in comment #7

[simonpj]

Ha ha, how true! Well, I could revert it to a warning, but its somethign of a moot point anyway, and I'm inclined to leave it as it is.

S

[simonpj]

There is still improvement to be had here, and I want to get to it, but it's not critical for 7.0.

Simon

[conal]

Here is another example of this problem, which arose in the blog post  Fixing lists. This example doesn't appear to be handled correctly in ghc 7.0.1 either. Moreover, I don't think SPJ's "quite correct" remark above (to pumpkin) applies in this case.

{-# LANGUAGE GADTs, KindSignatures, EmptyDataDecls #-}
{-# OPTIONS_GHC -Wall #-}

module Test where

data Z
data S n

infixr 5 :<
data Vec :: * -> * -> * where
  ZVec :: Vec Z a
  (:<) :: a -> Vec n a -> Vec (S n) a

applyV :: Vec n (a -> b) -> Vec n a -> Vec n b
ZVec      `applyV` ZVec      = ZVec
(f :< fs) `applyV` (x :< xs) = f x :< (fs `applyV` xs)

-- GHC 6.12.3 gives me a warning (with -Wall)

--     Warning: Pattern match(es) are non-exhaustive
--              In the definition of `<*>':
--                  Patterns not matched:
--                      ZVec (_ :< _)
--                      (_ :< _) ZVec

-- Adding the following cases silences the compiler.

-- ZVec `applyV` (_ :< _) = undefined
-- (_ :< _) `applyV` ZVec = undefined

-- However, benmachine found that GHC 7.0.1 balks at these definitions as ill-typed,
-- but also warns of non-exhaustive patterns when the lines are removed.

[simonpj]

Yes, this is another example of f1 above. And since GHC now rejects inacccessible case branches, you can't even put in the missing cases. Well you can say

_ `applyV` _ = undefined

to suppress the warning.

I wish this was easier to fix. The difficulty is that the type inference engine (which has a sophisticated constraint solver) only sees one equation at a time, and hence can't check exhaustiveness). But the overlap checker (which sees all the equations at once) does not have a sophisticated solver.

Obviously this is fixable with enough work. But annoyingly it needs real work. For example the desugarer could collect constraints, and call the solver to make the check.

To be honest I keep putting this off because it doesn't seem that important, and there are always more important things to do. So keep adding examples to this ticket if you come across them, and adding yourself to the cc list. The more complaints the more likely I am to put off other things to do this one!

[sjoerd_visscher]

So keep adding examples to this ticket if you come across them, and adding yourself to the cc list.

In the data-category package I constantly run into this. See for example  https://github.com/sjoerdvisscher/data-category/blob/master/Data/Category/Boolean.hs

[sjoerd_visscher]

Here's another case in code from Edward Kmett:  https://github.com/ekmett/semigroupoid-extras/blob/master/Data/Semigroupoid/Coproduct.hs#L17

[simonpj]

Punting to 7.6; sorry.