diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index 67da75e979..5e48c348ea 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -26,7 +26,7 @@ pure "hello"
 #eval run "#check id $ Nat.succ one"
 #eval run "#check HasAdd.add one two"
 #eval run "#check one + two > one ∧ True"
--- #eval run "#check act1 >>= IO.println"
+#eval run "#check act1 >>= IO.println"
 
 #eval run
 "universe u universe v
diff --git a/tests/lean/run/synth1.lean b/tests/lean/run/synth1.lean
index 0a91dfa379..fbc4e063ea 100644
--- a/tests/lean/run/synth1.lean
+++ b/tests/lean/run/synth1.lean
@@ -35,3 +35,15 @@ do inst ← mkAppM `HasCoerce #[mkConst `Nat, mkSort levelZero];
    print r
 
 #eval tst1
+
+def tst2 : MetaM Unit :=
+do inst ← mkAppM `HasBind #[mkConst `IO];
+   -- globalInstances ← getGlobalInstances;
+   -- print (format globalInstances);
+   -- result ← globalInstances.getUnify inst;
+   -- print result;
+   r ← synthInstance inst;
+   print r;
+   pure ()
+
+#eval tst2