Pattern match warning emitted twice
Consider
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
module G2 where
data T a where
A :: T True
B :: T False
g :: ()
g | B <- A = ()
This will generate the following compilation warnings:
G2.hs:11:1: warning: [-Woverlapping-patterns]
Pattern match has inaccessible right hand side
In a pattern binding in
a pattern guard for
an equation for ‘g’:
B <- ...
|
11 | g | B <- A = ()
| ^^^^^^^^^^^^^^^
G2.hs:11:5: warning: [-Winaccessible-code]
• Couldn't match type ‘'True’ with ‘'False’
Inaccessible code in
a pattern with constructor: B :: T 'False,
in a pattern binding in
a pattern guard for
an equation for ‘g’
• In the pattern: B
In a stmt of a pattern guard for
an equation for ‘g’:
B <- A
In an equation for ‘g’: g | B <- A = ()
|
11 | g | B <- A = ()
| ^
G2.hs:11:5: warning: [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘g’: g | B <- A = ...
|
11 | g | B <- A = ()
| ^^^^^^
Note how the same redundancy warning was emitted twice.
Solution
The problem is that we currently call checkSingle
in a pattern guard context, in addition to calling checkMatches
on the individual clauses. We should only really checkSingle
when we are in a context where exhaustiveness warnings are interesting (so, not inside a pattern guard or list comprehension), because in the other cases we will generate redundancy warnings through checkMatches
. Also it's totally redundant.
Side note: We need GADTs because prior to calling checkSingle
we represent the RHS of the binding (A
) by a fresh variable. Without type info this can never result in a redundant match.