Hi, I met with a very strange GHC behaviour concerning type inference of patterns. Consider the following gist:
Here I create an existential type for
Expr a with a dictionary for
ToType typeclass. I want to create a bidirectional pattern that will bind both the expression and its type. Here something strange happens.
- If I uncomment the type signature for
(:::), the GHC will say it can’t unify the type variable
a1hidden existentially in the constructor with a variable
abound by a pattern. Sounds at least probable, however this is the exact same signature that gets inferred when I load it to repl and type
- If I change
test, the GHC will complain about refutable pattern although the
(:::)is marked with a
How to get around this? I’m ok with not specifying the pattern’s type, but
MonadFail is a no-go for me.
EDIT: I’m using ghc 8.10.7
EDIT 2: If I specify the signature to:
pattern (:::) :: () => ToType a => Expr a -> Type a -> SomeExpr
(note the empty constraint
()), it suddenly compiles. This is in line with https://mpickering.github.io/papers/pattern-synonyms.pdf section 6.1: “if there is a provided context but no required one, you must write () for the required one”. So indeed the
() => is necessary to differentiate between provided and required contexts. Still it doesn’t explain why the pattern is failable.