From 3da95ea8b062c8b862a47ecdf4bcd637f44c7388 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Feb 2020 17:50:42 -0800
Subject: [PATCH] test: structure instance tests

---
 tests/lean/run/structInst2.lean | 46 +++++++++++++++++++++++++++++++--
 1 file changed, 44 insertions(+), 2 deletions(-)

diff --git a/tests/lean/run/structInst2.lean b/tests/lean/run/structInst2.lean
index 9ea2fa3e13..f7a7af4d71 100644
--- a/tests/lean/run/structInst2.lean
+++ b/tests/lean/run/structInst2.lean
@@ -1,11 +1,53 @@
 import Init.Control.Option
 
+universes u v
+
+def OptionT2 (m : Type u → Type v) (α : Type u) : Type v :=
+m (Option α)
+
+
+namespace OptionT2
+variables {m : Type u → Type v} [Monad m] {α β : Type u}
+
+@[inline] protected def bind (ma : OptionT2 m α) (f : α → OptionT2 m β) : OptionT2 m β :=
+(do {
+    a? ← ma;
+    match a? with
+    | some a => f a
+    | none   => pure none
+} : m (Option β))
+
+@[inline] protected def pure (a : α) : OptionT2 m α :=
+(pure (some a) : m (Option α))
+
+@[inline] protected def orelse (ma : OptionT2 m α) (mb : OptionT2 m α) : OptionT2 m α :=
+(do { a? ← ma;
+        match a? with
+        | some a => pure (some a)
+        | _      => mb } : m (Option α))
+
+@[inline] protected def fail : OptionT2 m α :=
+(pure none : m (Option α))
+
+end OptionT2
+
 new_frontend
 
-def optMonad {m} [Monad m] : Monad (OptionT m) :=
+instance optMonad1 {m} [Monad m] : Monad (OptionT2 m) :=
+{ pure := OptionT2.pure, bind := OptionT2.bind }
+
+def optMonad2 {m} [Monad m] : Monad (OptionT m) :=
 { pure := OptionT.pure, bind := OptionT.bind }
 
-def optAlt {m} [Monad m] : Alternative (OptionT m) :=
+def optAlt1 {m} [Monad m] : Alternative (OptionT m) :=
 { failure       := OptionT.fail,
   orelse        := OptionT.orelse,
   toApplicative := Monad.toApplicative (OptionT m) } -- TODO: check toApplicative binder annotations
+
+def optAlt2 {m} [Monad m] : Alternative (OptionT m) :=
+⟨OptionT.fail, OptionT.orelse⟩ -- it works because it treats `toApplicative` as an instance implicit argument
+
+def optAlt3 {m} [Monad m] : Alternative (OptionT2 m) :=
+{ failure       := OptionT2.fail,
+  orelse        := OptionT2.orelse,
+  toApplicative := Monad.toApplicative (OptionT2 m) }