Unexpected "Inaccessible RHS" in pattern matching with kind parameters
Summary
I've been trying to adapt my library to GHC 8.10+ and got a great deal of warnings. Most of them complain about the redundant pattern matches, which is awesome (thank you guys!). However, I've stumbled upon this Pattern match has inaccessible right hand side
.
Here is my attempt to reduce the code to the exemplary minimum:
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE ViewPatterns #}
module Lib where
import Data.Kind (Type)
data A
data B
data ElemKind k where
ElemKindA :: ElemKind A
ElemKindB :: ElemKind B
class KnownElemKind (xs :: [k]) where
getKind :: TypedList f xs > ElemKind k
data TypedList (f :: (k > Type)) (xs :: [k]) where
Nil :: TypedList f '[]
Cons :: f x > TypedList f xs > TypedList f (x ': xs)
data Dim (x :: k)
pattern DimA :: forall k (xs :: [k]) . KnownElemKind xs => (k ~ A) => TypedList Dim xs
pattern DimA < (getKind > ElemKindA)
{# COMPLETE DimA #}
{# COMPLETE Nil, Cons #}
f :: forall (xns :: [B]) . TypedList Dim xns > TypedList Dim xns > Bool
f Nil Nil = True
f (Cons _ _) (Cons _ _) = True
g :: forall (xns :: [B]) . TypedList Dim xns > Bool
g Nil = True
g (Cons _ _) = True
h :: forall (xns :: [A]) . TypedList Dim xns > Bool
h Nil = True
h (Cons _ _) = True
i :: forall (xns :: [A]) . TypedList Dim xns > TypedList Dim xns > Bool
i Nil Nil = True
i (Cons _ _) (Cons _ _) = True
j :: forall k (xns :: [k]) . TypedList Dim xns > TypedList Dim xns > Bool
j Nil Nil = True
j (Cons _ _) (Cons _ _) = True
l :: forall (xns :: [A]) . KnownElemKind xns => TypedList Dim xns > Bool
l DimA = True
Here is the full (unexpected) output:
Lib.hs:35:1: warning: [Woverlappingpatterns]
Pattern match has inaccessible right hand side
In an equation for ‘f’: f Nil Nil = ...

35  f Nil Nil = True
 ^^^^^^^^^^^^^^^^
Lib.hs:36:1: warning: [Woverlappingpatterns]
Pattern match is redundant
In an equation for ‘f’: f (Cons _ _) (Cons _ _) = ...

36  f (Cons _ _) (Cons _ _) = True
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Lib.hs:40:1: warning: [Woverlappingpatterns]
Pattern match is redundant
In an equation for ‘g’: g (Cons _ _) = ...

40  g (Cons _ _) = True
 ^^^^^^^^^^^^^^^^^^^
I am not 100% sure, what happens here. It looks like the complete set checker tries to match DimA
, but fails due to the wrong element kind. Then, for some reason, it still sticks to that complete set and thinks another constructor is impossible there.
Steps to reproduce
Compile the code above with GHC 8.10+, observe the warnings.
Furthermore, the "Pattern match has inaccessible right hand side" vanishes if I remove either of:

(k ~ A)
on line 28 
{# COMPLETE DimA #}
on line 31  Second argument of
f
(seeg
)
Expected behavior
With GHC 8.4.4, 8.6.5, 8.8.4 the code produces no warnings. I expect the warnings to not happen or be more consistent across functions f, g, h, i, l.
Environment
 GHC version used: 8.10.4, 9.0.1
Optional:
 Operating System: Ubuntu 20.04
 System Architecture: x64