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 |