#3927: Incomplete/overlapped pattern warnings + GADTs = inadequate
---------------------------------+------------------------------------------
Reporter: simonpj | Owner: simonpj
Type: bug | Status: new
Priority: high | Milestone: 7.0.1
Component: Compiler | Version: 6.12.1
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
---------------------------------+------------------------------------------
Comment(by 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
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3927#comment:6>
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
