[GHC] #13484: Incorrect Exhaustivity Checking

25 Mar 2017

      #13484: Incorrect Exhaustivity Checking
-------------------------------------+-------------------------------------
           Reporter:  andrewthad     |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Small example:

 {{{
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE DataKinds #-}

 {-# OPTIONS_GHC -Werror -fwarn-incomplete-patterns #-}

 data Chunk (f :: k -> *) (xs :: [k]) where
   ChunkCons :: f a -> f b -> f c -> f d -> Chunk f xs -> Chunk f (a ': b
 ': c ': d ': xs)
   ChunkNil :: Chunk f '[]

 impossibleChunk01 :: Chunk f as -> Chunk f (a ': as) -> b
 impossibleChunk01 (ChunkCons _ _ _ _ c1) (ChunkCons _ _ _ _ c2) =
 impossibleChunk01 c1 c2

 }}}

 This fails with:

 {{{
 fast_records.hs:32:1: warning: [-Wincomplete-patterns]
     Pattern match(es) are non-exhaustive
     In an equation for ‘impossibleChunk01’:
         Patterns not matched: ChunkNil _
 }}}

 Obviously a Chunk and a Chunk that's one element bigger cannot both exist.
 They must each be a multiple of 4. The impossibleChunk01 function is
 supposed to prove this. However, GHC doesn't currently figure out that
 neither data constructor can pair up with ChunkNil.

 This may be a moot point. The EmptyCase extension is currently sort of
 broken (because it currently never warns), but in GHC 8.2, it does some
 exhaustivity checking to ensure that you aren't shooting yourself in the
 foot. So, I might be able to write:

 {{{
 impossibleChunk01 :: Chunk f as -> Chunk f (a ': as) -> b
 impossibleChunk01 (ChunkCons _ _ _ _ c1) (ChunkCons _ _ _ _ c2) =
 impossibleChunk01 c1 c2
 impossibleChunk01 ChunkNill x = case x of {}
 }}}

 If that's the case (no pun intended), then I don't mind having to manually
 help out the exhaustivity checker in that way.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13484
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler