Pattern coverage checker ignores dictionary arguments
I disabled syntax highlighting below; the bugs highlighting single quotes made the code unreadable.
{-# LANGUAGE DataKinds, TypeFamilies, GADTs, TypeOperators, ScopedTypeVariables, ConstraintKinds, StandaloneDeriving #-}
{-# OPTIONS_GHC -Wall #-}
import Data.Constraint
import Data.Type.Bool
-- Bool singletons
data Boolly b where
Falsey :: Boolly 'False
Truey :: Boolly 'True
deriving instance Show (Boolly b)
class KnownBool b where
knownBool :: Boolly b
instance KnownBool 'False where
knownBool = Falsey
instance KnownBool 'True where
knownBool = Truey
-- OrRel a b r expresses all the usual implications inherent
-- in the statement that r ~ (a || b).
type OrRel (a :: Bool) (b :: Bool) (r :: Bool) :: Constraint =
(r ~ (a || b),
If r
(If (Not a) (b ~ 'True) (() :: Constraint),
If (Not b) (a ~ 'True) (() :: Constraint))
(a ~ 'False, b ~ 'False))
-- Given known Bools, their disjunction is also known
abr :: forall a b r p1 p2 . (OrRel a b r, KnownBool a, KnownBool b) => p1 a -> p2 b -> Dict (KnownBool r)
abr _ _ = case knownBool :: Boolly a of
Truey -> Dict
Falsey -> case knownBool :: Boolly b of
Truey -> Dict -- Problematic match
Falsey -> Dict
The trouble is that GHC warns that the problematic match is redundant, which it is not. If I remove it, GHC fails to warn that the patterns are incomplete, which they are.
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |