GitLab

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.