Strange pattern type inference & refutability

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.

  1. 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 (:::)
  2. 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 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.

I’ve used a more general version with a lot of success in the past.

Hi David,

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.

However perhaps going your way (removing the constraint) will be simpler.

Depending on the structure of your actual Expr type, it might also be enough to write something like:

getType :: Expr a -> Type a
getType EInt = TInt

test :: Monad m => m String
test = do
  e <- pure EInt
  case getType e of
    TInt -> pure "int"

because Expr already contains all the information that would have been in Type's constructors.