Strictness of pattern synonym matches and pattern-match checking
Sound handling of pattern synonym strictness in the pattern-match checker is quite tricky. Consider the following module:
{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE BangPatterns #-}
module Lib where
import Data.Void
strictConst :: a -> b -> a
strictConst a b = seq b a
pattern F <- (const False -> True)
pattern SF <- (strictConst False -> True)
-- | The second clause is redundant, really, because (the matcher of) 'F' is
-- not strict in its argument. As a result, the third clause is *not*
-- redundant, but inaccessible RHS! Deleting the third clause would be unsound.
-- This is bad, especially because this outcome depends entirely on the
-- strictness of 'F's matcher.
f :: Bool -> Bool -> ()
f _ True = ()
f F True = ()
f !_ True = ()
f _ _ = ()
-- | In this example, the second clause really is inaccessible RHS (because SF
-- is a strict match). And as a result, the third clause *is* redundant.
f2 :: Bool -> Bool -> ()
f2 _ True = ()
f2 SF True = ()
f2 !_ True = ()
f2 _ _ = ()
-- The following is related to the same issue:
pattern T <- (const True -> True)
{-# COMPLETE T, F :: Void #-}
-- | The following function definition is exhaustive.
-- Its clauses are *not* inaccessible RHS, because neither
-- pattern synonym is strict.
g :: Void -> ()
g F = ()
g T = ()
Current warning output:
PatSynsLazy.hs:22:1: warning: [-Woverlapping-patterns]
Pattern match has inaccessible right hand side
In an equation for ‘f’: f F True = ...
|
22 | f F True = ()
| ^^^^^^^^^^^^^^^^
PatSynsLazy.hs:23:1: warning: [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘f’: f !_ True = ...
|
23 | f !_ True = ()
| ^^^^^^^^^^^^^^^^
PatSynsLazy.hs:30:1: warning: [-Woverlapping-patterns]
Pattern match has inaccessible right hand side
In an equation for ‘f2’: f2 SF True = ...
|
30 | f2 SF True = ()
| ^^^^^^^^^^^^^^^^^
PatSynsLazy.hs:31:1: warning: [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘f2’: f2 !_ True = ...
|
31 | f2 !_ True = ()
| ^^^^^^^^^^^^^^^^^
PatSynsLazy.hs:44:1: warning: [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘g’: g T = ...
|
44 | g T = ()
| ^^^^^^^^
Comments explain the purpose of each function. Note that f
and f2
mean that we are necessarily unsound by assuming that all pattern synonyms are lazy (in which case we mark the second clause of f2
as redundant, which is unsound). But the same is true if we assume that all pattern synonym matches are strict (in which case we mark the third clause of f
as redundant, which is unsound).
The warnings for g
are entirely unsound and have the same root issue.