diff --git a/tests/lean/run/structInst2.lean b/tests/lean/run/structInst2.lean
new file mode 100644
index 0000000000..9ea2fa3e13
--- /dev/null
+++ b/tests/lean/run/structInst2.lean
@@ -0,0 +1,11 @@
+import Init.Control.Option
+
+new_frontend
+
+def optMonad {m} [Monad m] : Monad (OptionT m) :=
+{ pure := OptionT.pure, bind := OptionT.bind }
+
+def optAlt {m} [Monad m] : Alternative (OptionT m) :=
+{ failure       := OptionT.fail,
+  orelse        := OptionT.orelse,
+  toApplicative := Monad.toApplicative (OptionT m) } -- TODO: check toApplicative binder annotations