diff --git a/tests/lean/lazySeq.lean b/tests/lean/lazySeq.lean
new file mode 100644
index 0000000000..98ba052ed0
--- /dev/null
+++ b/tests/lean/lazySeq.lean
@@ -0,0 +1,14 @@
+partial def loop (x : Nat) : Nat :=
+  dbg_trace x
+  loop (x+1) + 1
+
+def act1 : IO Unit :=
+  throw (IO.userError "act1 failed")
+
+def act2 : IO Unit :=
+  act1 *> IO.println (loop 0) -- `loop 0` should not be executed
+
+def act3 : IO Unit :=
+  try act2 catch ex => IO.println s!"error: {ex}"
+
+#eval act3
diff --git a/tests/lean/lazySeq.lean.expected.out b/tests/lean/lazySeq.lean.expected.out
new file mode 100644
index 0000000000..97e8eb474b
--- /dev/null
+++ b/tests/lean/lazySeq.lean.expected.out
@@ -0,0 +1 @@
+error: act1 failed
diff --git a/tests/lean/run/struct3.lean b/tests/lean/run/struct3.lean
index f3d08cfff0..fd219bbf46 100644
--- a/tests/lean/run/struct3.lean
+++ b/tests/lean/run/struct3.lean
@@ -5,18 +5,18 @@ class Bind2 (m : Type u → Type v) where
 
 class Monad2 (m : Type u → Type v) extends Applicative m, Bind2 m : Type (max (u+1) v) where
   map      := fun f x => Bind2.bind x (pure ∘ f)
-  seq      := fun f x => Bind2.bind f fun y => Functor.map y x
-  seqLeft  := fun x y => Bind2.bind x fun a => Bind2.bind y fun _ => pure a
-  seqRight := @fun α β x y => Bind2.bind x fun _ => y -- Recall that `@` disables implicit lambda support
+  seq      := fun f x => Bind2.bind f fun y => Functor.map y (x ())
+  seqLeft  := fun x y => Bind2.bind x fun a => Bind2.bind (y ()) fun _ => pure a
+  seqRight := @fun α β x y => Bind2.bind x fun _ => y () -- Recall that `@` disables implicit lambda support
 
 class Monad3 (m : Type u → Type v) extends Applicative m, Bind2 m : Type (max (u+1) v) where
   map (f x)      := Bind2.bind x (pure ∘ f)
-  seq (f x)      := Bind2.bind f fun y => Functor.map y x
-  seqLeft (x y)  := Bind2.bind x fun a => Bind2.bind y fun _ => pure a
-  seqRight (x y) := Bind2.bind x fun _ => y
+  seq (f x)      := Bind2.bind f fun y => Functor.map y (x ())
+  seqLeft (x y)  := Bind2.bind x fun a => Bind2.bind (y ()) fun _ => pure a
+  seqRight (x y) := Bind2.bind x fun _ => y ()
 
 class Monad4 (m : Type u → Type v) extends Applicative m, Bind2 m : Type (max (u+1) v) where
   map f x      := Bind2.bind x (pure ∘ f)
-  seq f x      := Bind2.bind f fun y => Functor.map y x
-  seqLeft x y  := Bind2.bind x fun a => Bind2.bind y fun _ => pure a
-  seqRight x y := Bind2.bind x fun _ => y
+  seq f x      := Bind2.bind f fun y => Functor.map y (x ())
+  seqLeft x y  := Bind2.bind x fun a => Bind2.bind (y ()) fun _ => pure a
+  seqRight x y := Bind2.bind x fun _ => y ()