spurious "non-exhaustive" pattern warnings?

[Simon Peyton-Jones]

The overlap warning checker simply doesn't take account of GADTs.  There's a long-standing project suggestion to fix this:
http://hackage.haskell.org/trac/ghc/wiki/ProjectSuggestions

Perhaps a good GSoc project.

Simon

From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-bounces at haskell.org] On Behalf Of Conal Elliott
Sent: 31 March 2009 03:45
To: glasgow-haskell-users at haskell.org
Subject: spurious "non-exhaustive" pattern warnings?

-- Why do I get warnings about non-exhaustive pattern matches in the
-- following code?  Is the compiler just not clever enough to notice that
-- the uncovered cases are all type-incorrect?  (ghc 6.11.20090115)

{-# LANGUAGE TypeFamilies, EmptyDataDecls, TypeOperators
           , GADTs, KindSignatures
           , FlexibleInstances, FlexibleContexts
  #-}
{-# OPTIONS_GHC -Wall #-}

import Control.Applicative (Applicative(..))

data Z
data S n

infixr 1 :<

data Vec :: * -> * -> * where
  ZVec :: Vec Z a
  (:<) :: a -> Vec n a -> Vec (S n) a

-- todo: infix op for SVec

instance Functor (Vec n) where
  fmap _ ZVec     = ZVec
  fmap f (a :< u) = f a :< fmap f u

instance Applicative (Vec Z) where
  pure _        = ZVec
  ZVec <*> ZVec = ZVec

--     Warning: Pattern match(es) are non-exhaustive
--              In the definition of `<*>':
--                  Patterns not matched:
--                      (_ :< _) _
--                      ZVec (_ :< _)

instance Applicative (Vec n) => Applicative (Vec (S n)) where
  pure a                  = a :< pure a
  (f :< fs) <*> (x :< xs) = f x :< (fs <*> xs)

--     Warning: Pattern match(es) are non-exhaustive
--              In the definition of `<*>':
--                  Patterns not matched:
--                      ZVec _
--                      (_ :< _) ZVec

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20090331/0eb975b1/attachment.htm