Incorrect inaccessibility warnings with impredicative types and GADTs
Consider this code:
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE GADTs #-}
data AB a where
A :: (x ~ (forall a b. a -> b -> b)) => x -> AB x
B :: (x ~ (forall p. p -> forall q. q -> q)) => x -> AB x
data SomeAB = forall x. SomeAB (AB x)
showAB :: SomeAB -> String
showAB (SomeAB A{}) = "A"
showAB (SomeAB B{}) = "B"
main = putStrLn (showAB (SomeAB (A @(forall a b. a -> b -> b) (\_ x -> x))))
Gives the warnings:
S.hs:15:1: warning: [GHC-94210] [-Woverlapping-patterns]
Pattern match has inaccessible right hand side
In an equation for ‘showAB’: showAB (SomeAB A {}) = ...
|
15 | showAB (SomeAB A{}) = "A"
| ^^^^^^^^^^^^^^^^^^^^^^^^^
S.hs:15:16: warning: [GHC-40564] [-Winaccessible-code]
• Inaccessible code in
a pattern with constructor:
A :: forall x. (x ~ (forall a b. a -> b -> b)) => x -> AB x,
in an equation for ‘showAB’
Couldn't match type ‘x’ with ‘forall a b. a -> b -> b’
Cannot equate type variable ‘x’
with a type involving polytypes: forall a b. a -> b -> b
‘x’ is a rigid type variable bound by
a pattern with constructor: SomeAB :: forall x. AB x -> SomeAB,
in an equation for ‘showAB’
at S.hs:15:9-18
• In the pattern: A {}
In the pattern: SomeAB A {}
In an equation for ‘showAB’: showAB (SomeAB A {}) = "A"
|
15 | showAB (SomeAB A{}) = "A"
| ^^^
S.hs:16:1: warning: [GHC-53633] [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘showAB’: showAB (SomeAB B {}) = ...
|
16 | showAB (SomeAB B{}) = "B"
| ^^^^^^^^^^^^^^^^^^^^^^^^^
S.hs:16:16: warning: [GHC-40564] [-Winaccessible-code]
• Inaccessible code in
a pattern with constructor:
B :: forall x.
(x ~ (forall p. p -> forall q. q -> q)) =>
x -> AB x,
in an equation for ‘showAB’
Couldn't match type ‘x’ with ‘forall p. p -> forall q. q -> q’
Cannot equate type variable ‘x’
with a type involving polytypes: forall p. p -> forall q. q -> q
‘x’ is a rigid type variable bound by
a pattern with constructor: SomeAB :: forall x. AB x -> SomeAB,
in an equation for ‘showAB’
at S.hs:16:9-18
• In the pattern: B {}
In the pattern: SomeAB B {}
In an equation for ‘showAB’: showAB (SomeAB B {}) = "B"
|
16 | showAB (SomeAB B{}) = "B"
| ^^^
But it runs just fine and prints:
A
Expected behavior
No warnings.
Environment
- GHC version used: GHC 9.2.6 and GHC 9.6.1