#3927: Incomplete/overlapped pattern warnings + GADTs = inadequate
---------------------------------+------------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 6.12.1
Keywords: | Difficulty:
Os: Unknown/Multiple | Testcase:
Architecture: Unknown/Multiple | Failure: None/Unknown
---------------------------------+------------------------------------------
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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3927>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
