Incorrect Exhaustivity Checking

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.

Trac metadata

Trac field	Value
Version	8.0.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture