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