#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 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).
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3927#comment:7>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
