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