Reordering alternatives in case expression causes exhaustive function to become non-exhaustive
The following code emits no pattern-match coverage warnings on GHC HEAD, as I would expect:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
module Bug where
import Data.Kind
import Data.Void
type SFalse = SBool 'False
type STrue = SBool 'True
data SBool :: Bool -> Type where
SFalse :: SFalse
STrue :: STrue
type family F (b :: Bool) :: Type where
F 'False = Void
F 'True = ()
data T (b :: Bool)
= MkT1
| MkT2 !(F b)
ex :: SBool b -> T b -> ()
ex sb t =
case t of
MkT1 -> ()
MkT2 f ->
case sb of
STrue -> f
However, if you reorder the alternatives in the case
expression in ex
:
ex :: SBool b -> T b -> ()
ex sb t =
case t of
MkT2 f ->
case sb of
STrue -> f
MkT1 -> ()
Then GHC HEAD will emit a spurious warning:
GHCi, version 8.11.0.20200526: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:30:7: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: SFalse
|
30 | case sb of
| ^^^^^^^^^^...
To the best of my knowledge, the order of alternatives should not affect exhaustivity in this example.
I originally discovered this in the wild while writing some TTG-heavy code in !3337 (closed). Thankfully, this bug has a workaround (just reorder the alternatives), so this isn't actively blocking !3337 (closed). But it would still be interesting to figure out why this is happening.
cc @sgraf812