Confusion around visible type application in pattern synonym pattern
See also #19847 (closed)
Sometimes, I like to declare
import Data.Kind
import Type.Reflection
pattern TypeApp ::
forall {k1} {k2} (f :: k1 -> k2) (result :: k2).
Typeable f =>
forall (arg :: k1).
result ~ f arg =>
TypeRep arg ->
TypeRep result
pattern TypeApp arg_rep <- App (eqTypeRep (typeRep @f) -> Just HRefl) arg_rep
This pattern synonym allows me to match on a TypeRep
to see whether its an application of some known type constructor, like List
or Maybe
.
GHC accepts this declaration, as it should.
But using causes chaos:
f :: TypeRep a -> String
f (TypeApp @[] rep) = show rep
produces
Bug.hs:18:4: error:
• No instance for (Typeable f0) arising from a use of ‘TypeApp’
• In the pattern: TypeApp @[] rep
In an equation for ‘f’: f (TypeApp @[] rep) = show rep
|
18 | f (TypeApp @[] rep) = show rep
| ^^^^^^^^^^^^^^^
Bug.hs:18:4: error:
• Could not deduce (k1 ~ *)
from the context: a ~ f0 arg
bound by a pattern with pattern synonym:
TypeApp :: forall {k1} {k2} (f :: k1 -> k2) (result :: k2).
Typeable f =>
forall (arg :: k1).
(result ~ f arg) =>
TypeRep arg -> TypeRep result,
in an equation for ‘f’
at Bug.hs:18:4-18
‘k1’ is a rigid type variable bound by
the type signature for:
f :: forall {k1} (a :: k1). TypeRep a -> String
at Bug.hs:17:1-24
• In the pattern: TypeApp @[] rep
In an equation for ‘f’: f (TypeApp @[] rep) = show rep
• Relevant bindings include
f :: TypeRep a -> String (bound at Bug.hs:18:1)
|
18 | f (TypeApp @[] rep) = show rep
| ^^^^^^^^^^^^^^^
I have no clue what GHC is thinking here. Even when I try making k1
and k2
specified (in parens, not braces) and stating @Type @Type
, GHC is no better off, producing roughly the same messages.
For the record, this was encountered while I was writing a library that is intended to be useful in the Real World.