diff --git a/tests/lean/sec2.lean b/tests/lean/sec2.lean
new file mode 100644
index 000000000..efae2f972
--- /dev/null
+++ b/tests/lean/sec2.lean
@@ -0,0 +1,24 @@
+structure A : Type := mk
+structure B : Type := mk
+constant f : A → B
+constant g : B → B
+constant a : A
+
+namespace foo
+  coercion f
+  print coercions
+  check g a
+end foo
+
+check g a -- Error
+
+section boo
+  coercion f
+  print coercions
+  check g a
+end boo
+-- The metaobjects defined in the section persist to the outer level.
+-- This is not a bug. The idea is: we can use the scope to define
+-- auxiliary variables that are then used to define classes/instances/etc.
+-- That is, the whole point of the scope is to define these metaobjects.
+check g a -- Ok
diff --git a/tests/lean/sec2.lean.expected.out b/tests/lean/sec2.lean.expected.out
new file mode 100644
index 000000000..f5e465157
--- /dev/null
+++ b/tests/lean/sec2.lean.expected.out
@@ -0,0 +1,13 @@
+A ↣ B : f
+g a : B
+sec2.lean:13:6: error: type mismatch at application
+  g a
+term
+  a
+has type
+  A
+but is expected to have type
+  B
+A ↣ B : f
+g a : B
+g a : B