#3927: Incomplete/overlapped pattern warnings + GADTs = inadequate
---------------------------------+------------------------------------------
Reporter: simonpj | Owner: simonpj
Type: bug | Status: new
Priority: high | Milestone: 6.14.1
Component: Compiler | Version: 6.12.1
Keywords: | Testcase:
Blockedby: 4232 | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
---------------------------------+------------------------------------------
Changes (by pumpkin):
* cc: pumpkin...@… (added)
Comment:
Mostly just adding myself to the CC list here, but I figured I'd attach
the test code that made me interested in this ticket in the first place,
in case you wanted a more tangible example of why some people might want
this.
{{{
{-# OPTIONS_GHC -Wall #-}
{-# Language GADTs #-}
data Nz = Nz
newtype Ns n = Ns n
data Fin n where
Fz :: Fin (Ns n)
Fs :: Fin n -> Fin (Ns n)
data Vec n a where
Nil :: Vec Nz a
Cons :: a -> Vec n a -> Vec (Ns n) a
-- This works nicely!
test :: Fin Nz -> a
test _ = undefined
-- test Fz = undefined -- Rightfully rejected by GHC
-- test (Fs n) = undefined -- Rightfully rejected by GHC
-- Here, "knowledge" acquired by patern matching on one parameter refines
the type of the other, and in the Nil case,
-- refines the second parameter to Fin Nz, which contains nothing and thus
I cannot provide a meaningful pattern.
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
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3927#comment:5>
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
