Type application in pattern does not substitute correctly
See also
Inspired by @Icelandjack's #19691 (comment 352594), I typed in
pattern Is :: forall (b :: Type) (a :: Type). Typeable b => (a ~ b) => TypeRep a
pattern Is < (eqTypeRep (typeRep @b) > Just HRefl)
where Is = typeRep
def :: TypeRep a > a
def = \case
Is @Int > 10
Is @Bool > False
which looks pretty sensible to me. HEAD tells me
Scratch.hs:40:3: error:
• No instance for (Typeable b0) arising from a use of ‘Is’
• In the pattern: Is @Int
In a case alternative: Is @Int > 10
In the expression:
\case
Is @Int > 10
Is @Bool > False

40  Is @Int > 10
 ^^^^^^^
Scratch.hs:40:3: error:
• Could not deduce: a ~ Int
from the context: a ~ b0
bound by a pattern with pattern synonym:
Is :: forall b a. Typeable b => (a ~ b) => TypeRep a,
in a case alternative
at Scratch.hs:40:39
Expected: b0
Actual: Int
‘a’ is a rigid type variable bound by
the type signature for:
def :: forall a. TypeRep a > a
at Scratch.hs:38:121
• In the pattern: Is @Int
In a case alternative: Is @Int > 10
In the expression:
\case
Is @Int > 10
Is @Bool > False
• Relevant bindings include
def :: TypeRep a > a (bound at Scratch.hs:39:1)

40  Is @Int > 10
 ^^^^^^^
Scratch.hs:41:3: error:
• No instance for (Typeable b1) arising from a use of ‘Is’
• In the pattern: Is @Bool
In a case alternative: Is @Bool > False
In the expression:
\case
Is @Int > 10
Is @Bool > False

41  Is @Bool > False
 ^^^^^^^^
Scratch.hs:41:15: error:
• Could not deduce: a ~ Bool
from the context: a ~ b1
bound by a pattern with pattern synonym:
Is :: forall b a. Typeable b => (a ~ b) => TypeRep a,
in a case alternative
at Scratch.hs:41:310
‘a’ is a rigid type variable bound by
the type signature for:
def :: forall a. TypeRep a > a
at Scratch.hs:38:121
• In the expression: False
In a case alternative: Is @Bool > False
In the expression:
\case
Is @Int > 10
Is @Bool > False
• Relevant bindings include
def :: TypeRep a > a (bound at Scratch.hs:39:1)

41  Is @Bool > False

But that looks wrong: it shouldn't be looking for Typeable b0
or Typeable b1
, it should be looking for Typeable Int
or Typeable Bool
. While I have not investigated further, this smells like a missing application of a substitution somewhere.