Superclass constraints are ignored in instances

[garyb]

-- With this class definition:

class (Monad m) <= MonadError e m where
  throwError :: forall a. e -> m a
  catchError :: forall a. m a -> (e -> m a) -> m a

-- This instance doesn't work:

instance monadErrorMaybeT :: (MonadError e m) => MonadError e (MaybeT m) where
  throwError e = lift (throwError e)
  catchError = liftCatchMaybe catchError

-- You have to add another `Monad m` constraint:

instance monadErrorMaybeT :: (Monad m, MonadError e m) => MonadError e (MaybeT m) where
  throwError e = lift (throwError e)
  catchError = liftCatchMaybe catchError

[paf31]

I took a look at this, and it's going to need more work, but I at least know what's wrong.

We can find a Monad m instance if we have a MonadError e m instance, but the issue is that Monad m does not determine e.

[garyb]

Isn't that the wrong way around though? It's Monad m that we're "missing" in the case that fails, no e involved... or is that the problem, that it's "Monad m for all e" (if you see what I mean) that we can't represent right now?

[garyb]

I'm not sure that makes it any clearer actually ;)

I thought this would "just" need fixing by doing something like pulling through the superclass constraints and then applying the current substitution to them when constructing the constraint context. I don't know if that makes sense in the PS typechecker (I'm not sure I've ever looked into the typeclass machinery much), but I was doing something like that in the language I was working on previously.

[paf31]

@garyb To find the instance for Monad m, the only way is to use the instance for MonadError e m which contains Monad m as a superclass. Which means we need an instance for MonadError e? m, but what is e?? Really it doesn't matter. From a unification perspective, it can be a fresh variable. But the type checker doesn't work that way right now, so it looks for MonadError e <skolemized m> and only finds MonadError <skolemized e> <skolemized m>.

[garyb]

Got it 💡

I wasn't actually seeing the right problem, which didn't help! After playing around with some test cases I see where this arises now.