Incomplete/overlapped pattern warnings + GADTs = inadequate

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.

Trac metadata

Trac field	Value
Version	6.12.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture