[GHC] #12949: Pattern coverage mistake

8 Dec 2016

      #12949: Pattern coverage mistake
-------------------------------------+-------------------------------------
           Reporter:  dfeuer         |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Incorrect
  Unknown/Multiple                   |  error/warning at compile-time
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

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