VerifiedMonad instance for an error monad

Question

I'm trying to complete the monadLeftIdentity proof for the following data type:

data ErrorM : (a : Type) -> Type where
  AllGood : a -> ErrorM a
  Error : String -> ErrorM a

instance Monad ErrorM where
  (AllGood x) >>= f = f x
  (Error err) >>= f = Error err

instance VerifiedMonad ErrorM where
  monadApplicative (AllGood f) (AllGood x) = Refl
  monadApplicative (Error err) (AllGood x) = Refl
  monadApplicative (AllGood f) (Error err) = Refl
  monadApplicative (Error er1) (Error er2) = Refl
  monadLeftIdentity x f = ?z

I've left out the instances for Functor, Applicative and their Verified counterparts, as they're quite verbose and trivial. Do let me know, can paste them all here.

I've tried to rewrite return x as pure x or AllGood x, but have been unsuccessful in doing so (the rewrite does nothing to the proof state).

I've also tried to refine return x like so:

  monadLeftIdentity x f with (return x)
    monadLeftIdentity x' f | AllGood x' = ?z

but I get the following err msg:

 `-- Error.idr line 51 col 22:
     When elaborating left hand side of with block in Prelude.Monad.Astra.Error.ErrorM instance of Prelude.Monad.VerifiedMonad, method monadLeftIdentity:
     Can't match on with block in Prelude.Monad.Astra.Error.ErrorM instance of Prelude.Monad.VerifiedMonad, method monadLeftIdentity a (AllGood x') x' b f return

How does one go about this?

Answer 1

This seems like a bug in the Idris typechecker that doesn't resolve overloaded functions even when they are completely determined by the type.

To witness, I can make a proof like this:

myLeftIdentity : (x : a) -> (f : a -> ErrorM b) -> return x >>= f = f x
myLeftIdentity x f = Refl

and it typechecks just fine, but it can't be used as a witness in the instance:

instance VerifiedMonad ErrorM where
  monadApplicative (AllGood _) (AllGood _) = Refl
  monadApplicative (Error _) _ = Refl
  monadApplicative (AllGood _) (Error _) = Refl

  monadLeftIdentity = myLeftIdentity

results in

 Can't unify
         (x : a) -> (f : a -> ErrorM b) -> return x >>= f = f x
 with
         (x : a) -> (f : a -> ErrorM b) -> Main.ErrorM instance of Prelude.Monad.Monad, method >>= (return x) f = f x

even though the two >>= should be one and the same.

Interestingly, I was able to work around this by defining my own version of the Monad and VerifiedMonad classes:

infixl 5 >>=>

class Applicative m => Monad' (m : Type -> Type) where
  (>>=>) : m a -> (a -> m b) -> m b

return' : Monad' m => a -> m a
return' = pure

instance Monad' ErrorM where
  (AllGood x) >>=> f = f x
  (Error err) >>=> f = Error err

class (Monad' m, VerifiedApplicative m) => VerifiedMonad' (m : Type -> Type) where
  monadLeftIdentity : (x : a) -> (f : a -> m b) -> return' x >>=> f = f x

instance VerifiedMonad' ErrorM where
  monadLeftIdentity x f = Refl