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 a1 hidden existentially in the constructor with a variable a bound 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 :t (:::)
If I change MonadFail constraint to Monad in test, the GHC will complain about refutable pattern although the (:::) is marked with a COMPLETE pragma.
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.
I suspect that this example is an extract from a larger program where my proposal won’t work, but I figured I’d post it anyway in case it’s helpful. I don’t know why the pattern is marked refutable.
What about replacing the ::: pattern with a datatype that works the same way as your pattern synonym, and a convenience function that uses the class to construct it? In particular, this code seems to do everything you’re wanting on my machine, but without the complications due to pattern synonyms:
data SomeExpr' where
(:::) :: Expr a -> Type a -> SomeExpr'
typed :: ToType a => Expr a -> SomeExpr'
typed e = e ::: toType
test :: Monad m => m String
test = do
_e ::: t <- pure $ typed EInt
case t of
TInt -> pure "int"
Basically, instead of hauling a dictionary around, it hauls around a runtime representative of the expression’s type as a plain GADT constructor. This kind of design also makes GADT pattern matching easy if you need to take advantage of the hidden type later.
Thanks for your reply. That’s almost exactly what I had previously: I had a type
data SomeExpr where
(:::) :: ToType a => Expr a -> Type a -> SomeExpr
So here we have a duplication: a runtime representative (Type a) and a dictionary (ToType a). However it is redundant (either of them suffice), but useful (after deconstruction I have a dictionary already in hand when I need it, and I can specify the type of Expr during construction). So in order not to have a duplication, I got rid of the Type a element, but wanted to keep the pattern so that the change is localized and I don’t rewrite the whole typechecker.