Inconsistent pattern-match warnings when using guards versus case expressions

Consider the following code (apologies for the rather non-minimal example):

{-# 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.

Trac metadata

Trac field	Value
Version	8.6.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture