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 likef2
, 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 |