From dcf5f855ddd71dfc8e73c599834d3e361b816a3b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 5 Dec 2020 16:10:27 -0800
Subject: [PATCH] test: scoped and local instances

---
 tests/lean/scopedLocalInsts.lean              | 36 +++++++++++++++++++
 tests/lean/scopedLocalInsts.lean.expected.out | 15 ++++++++
 2 files changed, 51 insertions(+)
 create mode 100644 tests/lean/scopedLocalInsts.lean
 create mode 100644 tests/lean/scopedLocalInsts.lean.expected.out

diff --git a/tests/lean/scopedLocalInsts.lean b/tests/lean/scopedLocalInsts.lean
new file mode 100644
index 0000000000..4d32100cb8
--- /dev/null
+++ b/tests/lean/scopedLocalInsts.lean
@@ -0,0 +1,36 @@
+structure A where
+  x : Nat
+  y : Nat
+
+namespace Foo
+
+scoped instance : ToString A where
+  toString a := s!"A.mk {a.x} {a.y}"
+
+end Foo
+
+#eval toString { x := 10, y := 20 : A } -- Error: failed to synthesize `ToString A`
+
+section Sec1
+open Foo
+
+#eval toString { x := 10, y := 20 : A } -- works
+
+end Sec1 -- scoped instance `ToString A` is not available anymore
+
+#eval toString { x := 10, y := 20 : A } -- Error
+
+section Sec2
+
+local instance : ToString A where
+  toString a := s!"\{ x := {a.x}, y := {a.y} }"
+
+#eval toString { x := 10, y := 20 : A } -- works, using local instance
+
+end Sec2 -- local instance `ToString A` is not available anymore
+
+#eval toString { x := 10, y := 20 : A } -- Error
+
+open Foo
+
+#eval toString { x := 10, y := 20 : A } -- works
diff --git a/tests/lean/scopedLocalInsts.lean.expected.out b/tests/lean/scopedLocalInsts.lean.expected.out
new file mode 100644
index 0000000000..f315078da2
--- /dev/null
+++ b/tests/lean/scopedLocalInsts.lean.expected.out
@@ -0,0 +1,15 @@
+scopedLocalInsts.lean:12:6: error: failed to synthesize instance
+  ToString A
+scopedLocalInsts.lean:12:0: error: failed to synthesize
+  Lean.Eval ?m
+"A.mk 10 20"
+scopedLocalInsts.lean:21:6: error: failed to synthesize instance
+  ToString A
+scopedLocalInsts.lean:21:0: error: failed to synthesize
+  Lean.Eval ?m
+"{ x := 10, y := 20 }"
+scopedLocalInsts.lean:32:6: error: failed to synthesize instance
+  ToString A
+scopedLocalInsts.lean:32:0: error: failed to synthesize
+  Lean.Eval ?m
+"A.mk 10 20"