test: scoped and local instances

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

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"