I’m confused about the behavior of GHC in regards to coverage checking of pattern matches. According to the GHC source code, it’s based on the Lower Your Guards (LYG) paper. That paper, as well as the Note [Determining inaccessible clauses] in the source code, indicate that a pattern match will be reported as “redundant” if removing it will have no effect on the result. But there are cases where a pattern match cannot apply, yet removing it would still alter the result - these are reported as “inaccessible”.
Yet the following code segment reports both “inaccessible” and “redundant” warnings for the same pattern match: on f (GBool _) and f (GGreat _). However, f (GGood _) is only reported as redundant. For reference, I was using GHC 9.6.4.
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
import Data.Kind
import GHC.TypeError
data G a where
GShow :: Show a => a -> G a
GBool :: Bool -> G Bool
GGood :: Good a => a -> G a
GGreat :: Great a ~ True => a -> G a
type family Good a :: Constraint where
Good Bool = ()
Good Int = TypeError (Text "Int is not good")
Good _ = TypeError (Text "That is not good")
type family Great a :: Bool where
Great Bool = True
Great Int = False
Great _ = False
f :: G Int -> Char
f (GShow _) = 's'
f (GBool _) = 'b'
f (GGood _) = 'g'
f (GGreat _) = 'r'
g :: G (Int -> Int) -> Char
g (GShow _) = 's'
gadt_type_error_2.hs:27:1: warning: [GHC-53633] [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘f’: f (GBool _) = ...
|
27 | f (GBool _) = 'b'
| ^^^^^^^^^^^^^^^^^
gadt_type_error_2.hs:27:4: warning: [GHC-40564] [-Winaccessible-code]
• Inaccessible code in
a pattern with constructor: GBool :: Bool -> G Bool,
in an equation for ‘f’
Couldn't match type ‘Int’ with ‘Bool’
• In the pattern: GBool _
In an equation for ‘f’: f (GBool _) = 'b'
|
27 | f (GBool _) = 'b'
| ^^^^^^^
gadt_type_error_2.hs:28:1: warning: [GHC-53633] [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘f’: f (GGood _) = ...
|
28 | f (GGood _) = 'g'
| ^^^^^^^^^^^^^^^^^
gadt_type_error_2.hs:29:1: warning: [GHC-53633] [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘f’: f (GGreat _) = ...
|
29 | f (GGreat _) = 'r'
| ^^^^^^^^^^^^^^^^^^
gadt_type_error_2.hs:29:4: warning: [GHC-40564] [-Winaccessible-code]
• Inaccessible code in
a pattern with constructor:
GGreat :: forall a. (Great a ~ True) => a -> G a,
in an equation for ‘f’
Couldn't match type ‘False’ with ‘True’
• In the pattern: GGreat _
In an equation for ‘f’: f (GGreat _) = 'r'
|
29 | f (GGreat _) = 'r'
| ^^^^^^^^
It’s fantastic that LYG can figure out that those GRHSs (guarded right-hand sides) can’t be reached. It’s also great that, if I leave out constructors that can be matched, it lists those as missing from the cases.
The example of g (GShow _) is to show that LYG can’t figure out that the type class-constrained constructor can’t be matched. That makes to me since type classes are open - some other module could yet provide an instance for Int -> Int. I would imagine the same issue holds with open type families.
I wish that the f cases with GBool, GGood and GGreat would all report type errors instead of just coverage warnings, since technically they don’t match the type of the scrutinee. Is type checking for GADT pattern matches just handled a bit more loosely?
I wonder why GGood doesn’t get an “inaccessible” warning, but GGreat does. And it’s a shame we can’t have the custom type error for GGood show up. Instead, for GGreat we get an “inaccessible” warning, but it talks about True not matching False, which is not as helpful. (I suppose I could make a custom type instead of using Bool, that would have some more descriptive name, like GoodNotAllowed.)
