[GHC] #15753: Inconsistent pattern-match warnings when using guards versus case expressions

[GHC]

#15753: Inconsistent pattern-match warnings when using guards versus case
expressions
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.8.1
          Component:  Compiler       |           Version:  8.6.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  PatternMatchWarnings               |
       Architecture:                 |   Type of failure:  Incorrect
  Unknown/Multiple                   |  error/warning at compile-time
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the following code (apologies for the rather non-minimal
 example):

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wall -Wno-unticked-promoted-constructors #-}
 module Bug where

 import Data.Kind
 import Data.Type.Bool
 import Data.Type.Equality ((:~:)(..))
 import Data.Void

 data family Sing :: forall k. k -> Type
 data instance Sing :: Bool -> Type where
   SFalse :: Sing False
   STrue  :: Sing True
 data instance Sing :: forall a. [a] -> Type where
   SNil  :: Sing '[]
   SCons :: Sing x -> Sing xs -> Sing (x:xs)
 data instance Sing :: forall a b. (a, b) -> Type where
   STuple2 :: Sing x -> Sing y -> Sing '(x, y)
 newtype instance Sing (f :: k1 ~> k2) =
   SLambda { (@@) :: forall t. Sing t -> Sing (f @@ t) }

 data TyFun :: Type -> Type -> Type
 type a ~> b = TyFun a b -> Type
 infixr 0 ~>
 type family (f :: k1 ~> k2) @@ (x :: k1) :: k2
 infixl 9 @@

 newtype Map k v = MkMap [(k, v)]
 data instance Sing :: forall k v. Map k v -> Type where
   SMkMap :: Sing x -> Sing (MkMap x)

 type family MapEmpty :: Map k v where
   MapEmpty = MkMap '[]

 type family MapInsertWith (f :: v ~> v ~> v) (new_k :: k) (new_v :: v) (m
 :: Map k v) :: Map k v where
   MapInsertWith _ new_k new_v (MkMap '[]) = MkMap '[ '(new_k, new_v)]
   MapInsertWith f new_k new_v (MkMap ('(old_k,old_v):old_kvs)) =
     If (old_k == new_k)
        (MkMap ('(new_k,f @@ new_v @@ old_v):old_kvs))
        (Case (MapInsertWith f new_k new_v (MkMap old_kvs)) old_k old_v)

 type family Case (m :: Map k v) (old_k :: k) (old_v :: v) :: Map k v where
   Case (MkMap kvs) old_k old_v = MkMap ('(old_k,old_v) : kvs)

 sMapInsertWith :: forall k v (f :: v ~> v ~> v) (new_k :: k) (new_v :: v)
 (m :: Map k v).
                   SEq k
                => Sing f -> Sing new_k -> Sing new_v -> Sing m
                -> Sing (MapInsertWith f new_k new_v m)
 sMapInsertWith _  snew_k snew_v (SMkMap SNil) = SMkMap (STuple2 snew_k
 snew_v `SCons` SNil)
 sMapInsertWith sf snew_k snew_v (SMkMap (STuple2 sold_k sold_v `SCons`
 sold_kvs)) =
   case sold_k %== snew_k of
     STrue -> SMkMap (STuple2 snew_k (sf @@ snew_v @@ sold_v) `SCons`
 sold_kvs)
     SFalse ->
       case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of
         SMkMap skvs -> SMkMap (STuple2 sold_k sold_v `SCons` skvs)

 class PEq a where
   type (x :: a) == (y :: a) :: Bool
 class SEq a where
   (%==) :: forall (x :: a) (y :: a).
            Sing x -> Sing y -> Sing (x == y)

 mapInsertWithNonEmpty1 :: forall k v (f :: v ~> v ~> v) (old_k :: k)
 (old_v :: v) (old_kvs :: [(k,v)])
                                      (new_k :: k) (new_v :: v) (m :: Map k
 v).
                           SEq k
                        => Sing f -> Sing new_k -> Sing new_v -> Sing m
                        -> m :~: MkMap ('(old_k,old_v) : old_kvs)
                        -> MapInsertWith f new_k new_v m :~: MapEmpty
                        -> Void
 mapInsertWithNonEmpty1 sf snew_k snew_v (SMkMap sm) Refl Refl
   | STuple2 sold_k _ `SCons` sold_kvs <- sm
   , SFalse <- sold_k %== snew_k
   = case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of {}

 mapInsertWithNonEmpty2 :: forall k v (f :: v ~> v ~> v) (old_k :: k)
 (old_v :: v) (old_kvs :: [(k,v)])
                                      (new_k :: k) (new_v :: v) (m :: Map k
 v).
                           SEq k
                        => Sing f -> Sing new_k -> Sing new_v -> Sing m
                        -> m :~: MkMap ('(old_k,old_v) : old_kvs)
                        -> MapInsertWith f new_k new_v m :~: MapEmpty
                        -> Void
 mapInsertWithNonEmpty2 sf snew_k snew_v (SMkMap sm) Refl Refl
   | STuple2 sold_k _ `SCons` sold_kvs <- sm
   = case sold_k %== snew_k of
       SFalse ->
         case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of {}
 }}}

 If you compile this with GHC 8.6.1 or later, you'll notice something
 interesting happening with the pattern-match coverage checker warnings:

 {{{
 $ /opt/ghc/8.6.1/bin/ghci Bug.hs
 GHCi, version 8.6.1: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:78:1: warning: [-Wincomplete-patterns]
     Pattern match(es) are non-exhaustive
     In an equation for ‘mapInsertWithNonEmpty1’:
         Patterns not matched: _ _ _ (SMkMap _) Refl Refl
    |
 78 | mapInsertWithNonEmpty1 sf snew_k snew_v (SMkMap sm) Refl Refl
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
 Ok, one module loaded.
 }}}

 `mapInsertWithNonEmpty1` is deemed non-exhaustive, but
 `mapInsertWithNonEmpty2` is deemed exhaustive. However, the code for the
 two functions are functionally identical—the only difference is that
 `mapInsertWithNonEmpty1` uses one more pattern guard than
 `mapInsertWithNonEmpty2` does.

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