diff --git a/theories/Data/Monads/EitherMonad.v b/theories/Data/Monads/EitherMonad.v index 8c9a53b..8c50460 100644 --- a/theories/Data/Monads/EitherMonad.v +++ b/theories/Data/Monads/EitherMonad.v @@ -90,12 +90,12 @@ Section except. | (inl l, _) => ret (inl l) | (inr a, t) => ret (inr (a, t)) end) - ; pass := fun _ c => mkEitherT ( + ; pass := fun _ c => mkEitherT (pass ( x <- unEitherT c ;; match x with - | inl s => ret (inl s) - | inr (a,f) => pass (ret (inr a, f)) - end) + | inl s => ret (inl s, fun x => x) + | inr (a, f) => ret (inr a, f) + end)) }. Global Instance MonadFix_eitherT (MF : MonadFix m) : MonadFix eitherT := diff --git a/theories/Data/Monads/StateMonad.v b/theories/Data/Monads/StateMonad.v index 2448584..73130bb 100644 --- a/theories/Data/Monads/StateMonad.v +++ b/theories/Data/Monads/StateMonad.v @@ -79,8 +79,8 @@ Section StateType. ; listen := fun _ c => mkStateT (fun s => bind (listen (runStateT c s)) (fun x => let '(a,s,t) := x in ret (a,t,s))) - ; pass := fun _ c => mkStateT (fun s => bind (runStateT c s) (fun x => - let '(a,t,s) := x in pass (ret ((a,s),t)))) + ; pass := fun _ c => mkStateT (fun s => pass (bind (runStateT c s) (fun x => + let '(a,t,s) := x in ret ((a,s),t)))) }. Global Instance Exc_stateT T (MR : MonadExc T m) : MonadExc T stateT :=