<span style="font-family: courier new,monospace;">-- Why do I get warnings about non-exhaustive pattern matches in the</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- following code? Is the compiler just not clever enough to notice that</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">-- the uncovered cases are all type-incorrect?</span> (ghc 6.11.20090115)<br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">{-# LANGUAGE TypeFamilies, EmptyDataDecls, TypeOperators</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;"> , GADTs, KindSignatures</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;"> , FlexibleInstances, FlexibleContexts</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;"> #-}</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">{-# OPTIONS_GHC -Wall #-}</span><br style="font-family: courier new,monospace;">
<br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">import Control.Applicative (Applicative(..))</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">data Z</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">data S n</span><br style="font-family: courier new,monospace;">
<br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">infixr 1 :<</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">data Vec :: * -> * -> * where</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;"> ZVec :: Vec Z a</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;"> (:<) :: a -> Vec n a -> Vec (S n) a</span><br style="font-family: courier new,monospace;">
<br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- todo: infix op for SVec</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">instance Functor (Vec n) where</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;"> fmap _ ZVec = ZVec</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;"> fmap f (a :< u) = f a :< fmap f u</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">instance Applicative (Vec Z) where</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;"> pure _ = ZVec</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;"> ZVec <*> ZVec = ZVec</span><br style="font-family: courier new,monospace;">
<br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- Warning: Pattern match(es) are non-exhaustive</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- In the definition of `<*>':</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">-- Patterns not matched:</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- (_ :< _) _</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">-- ZVec (_ :< _)</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">instance Applicative (Vec n) => Applicative (Vec (S n)) where</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;"> pure a = a :< pure a</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;"> (f :< fs) <*> (x :< xs) = f x :< (fs <*> xs)</span><br style="font-family: courier new,monospace;">
<br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- Warning: Pattern match(es) are non-exhaustive</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- In the definition of `<*>':</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">-- Patterns not matched:</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- ZVec _</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">-- (_ :< _) ZVec</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;">