Strange pattern type inference & refutability

Learn
#1

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 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.

#2

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.

#3

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.

#4

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

#5

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.