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:3-9
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:1-21
• 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:3-10
‘a’ is a rigid type variable bound by
the type signature for:
def :: forall a. TypeRep a -> a
at Scratch.hs:38:1-21
• 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.