GHC 9.2/9.4 -Wincomplete-patterns regression with GADTs

Summary

Totality checker seemingly regressed from 9.0 to GHC 9.2 and 9.4, specifically with GADTs and type families.

Consider this code.

{-# LANGUAGE DataKinds, TypeFamilies, GADTs #-}
{-# OPTIONS_GHC -Wincomplete-patterns -Werror #-}

module Bug where

data T = Z | S

data ST n where
  SZ :: ST Z
  SS :: ST S

type family F n where
  F Z = Z
  F S = Z

f :: F m ~ n => ST m -> ST n -> ()
f _ SZ = ()

(I tried to cut this down as much as possible, in the original context this happened with typelevel Peano arithmetic with singleton proofs)

Now, reasonably speaking, these patterns are complete, n must be Z due to the constraint, regardless of what m is, hence the value can only be SZ, and GHC 9.0.2 is indeed able to infer that. GHC 9.2.5 and 9.4.3, however, fail to, reporting missing patterns:

$ ghc-9.0 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

$ ghc-9.2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:17:1: error: [-Wincomplete-patterns, -Werror=incomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘f’:
        Patterns of type ‘ST m’, ‘ST n’ not matched: _ SS
   |
17 | f _ SZ = ()
   | ^^^^^^^^^^^

$ ghc-9.4 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

-- same as above

I can silence this by adding f x SS = case x of, but that's pretty ugly.

Does not reproduce if type family is trivial (i.e. only has one case, or is reduced to one case by GHC). Does reproduce regardless whether the type family is open or closed.

Steps to reproduce

ghc-9.2 Bug.hs

Expected behavior

Not produce redundant pattern warnings.

Environment

• GHC version used: reproduces on 9.2.5, 9.4.3

---

Additional information

There is another example I found where GHC 9.2 finds incomplete patterns when GHC 9.0 doesn't, but it seems it's rather a bug in GHC 9.0! Still, for the sake of thoroughness:

{-# LANGUAGE DataKinds, TypeFamilies, GADTs #-}
{-# OPTIONS_GHC -Wincomplete-patterns -Werror #-}

module OldBug where

data T = TInt | TVoid

data AST t where
  VInt :: Int -> AST TInt

data ST t where
  STInt :: ST TInt
  STVoid :: ST TVoid

f :: ST t -> AST t -> ()
f STInt _ = ()

Note that this pattern is not, in fact, complete: f STVoid undefined will lead to "incomplete patterns" error at runtime. I would argue we want to keep the current 9.2/9.4 behaviour for this case.

$ ghc-9.0 OldBug.hs
[1 of 1] Compiling OldBug              ( OldBug.hs, OldBug.o )

$ ghc-9.2 OldBug.hs
[1 of 1] Compiling OldBug              ( OldBug.hs, OldBug.o )

OldBug.hs:16:1: error: [-Wincomplete-patterns, -Werror=incomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘f’:
        Patterns of type ‘ST t’, ‘AST t’ not matched: STVoid _
   |
16 | f STInt _ = ()
   | ^^^^^^^^^^^^^^

$ ghc-9.4 OldBug.hs

-- same as above