<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 :&lt;</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">data Vec :: * -&gt; * -&gt; * 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;">  (:&lt;) :: a -&gt; Vec n a -&gt; 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 :&lt; u) = f a :&lt; 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 &lt;*&gt; 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 `&lt;*&gt;&#39;:</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;">--                      (_ :&lt; _) _</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">--                      ZVec (_ :&lt; _)</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) =&gt; Applicative (Vec (S n)) where</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">  pure a                  = a :&lt; pure a</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">  (f :&lt; fs) &lt;*&gt; (x :&lt; xs) = f x :&lt; (fs &lt;*&gt; 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 `&lt;*&gt;&#39;:</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;">--                      (_ :&lt; _) ZVec</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;">