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