From 72032980ffca584a3dadca42306e9a430794ec91 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Nov 2020 12:32:32 -0800
Subject: [PATCH] feat: support for `unboundImplicitLocals` at `variable` and
 `variables` commands

They are morally part of the header.

cc @Kha
---
 src/Lean/Elab/Command.lean                        | 11 +++++++----
 tests/lean/unboundImplicitLocals.lean             | 15 +++++++++++++++
 .../lean/unboundImplicitLocals.lean.expected.out  |  3 +++
 3 files changed, 25 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 100b8347ab..98a344ca47 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -296,10 +296,13 @@ def liftTermElabM {α} (declName? : Option Name) (x : TermElabM α) : CommandEla
 
 @[inline] def runTermElabM {α} (declName? : Option Name) (elabFn : Array Expr → TermElabM α) : CommandElabM α := do
   let s ← get
-  liftTermElabM declName?
+  liftTermElabM declName? <|
     -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
     -- So, we use `Term.resetMessageLog`.
-    (Term.elabBinders (getVarDecls s) (fun xs => do Term.resetMessageLog; elabFn xs))
+    Term.withUnboundImplicitLocal <|
+      Term.elabBinders (getVarDecls s) fun xs => do
+        Term.resetMessageLog
+        Term.withUnboundImplicitLocal (flag := false) <| elabFn xs
 
 @[inline] def catchExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit := fun ctx ref =>
   EIO.catchExceptions (withLogging x ctx ref) (fun _ => pure ())
@@ -504,14 +507,14 @@ def elabOpenRenaming (n : SyntaxNode) : CommandElabM Unit := do
   -- `variable` bracketedBinder
   let binder := n[1]
   -- Try to elaborate `binder` for sanity checking
-  runTermElabM none fun _ => Term.elabBinder binder fun _ => pure ()
+  runTermElabM none fun _ => Term.withUnboundImplicitLocal <| Term.elabBinder binder fun _ => pure ()
   modifyScope fun scope => { scope with varDecls := scope.varDecls.push binder }
 
 @[builtinCommandElab «variables»] def elabVariables : CommandElab := fun n => do
   -- `variables` bracketedBinder+
   let binders := n[1].getArgs
   -- Try to elaborate `binders` for sanity checking
-  runTermElabM none fun _ => Term.elabBinders binders $ fun _ => pure ()
+  runTermElabM none fun _ => Term.withUnboundImplicitLocal <| Term.elabBinders binders $ fun _ => pure ()
   modifyScope fun scope => { scope with varDecls := scope.varDecls ++ binders }
 
 open Meta
diff --git a/tests/lean/unboundImplicitLocals.lean b/tests/lean/unboundImplicitLocals.lean
index 3a4cd078b4..63a78218e0 100644
--- a/tests/lean/unboundImplicitLocals.lean
+++ b/tests/lean/unboundImplicitLocals.lean
@@ -25,3 +25,18 @@ def Vec.map3 (xs : Vec α n) (f : α → β) : Vec α β := -- Errors, unknown i
   ⟨ xs.val.map f, sorry ⟩
 
 def double [Add α] (a : α) := a + a
+
+variables (xs : Vec α n) -- works
+
+def f := xs
+
+#check @f
+
+#check f mkVec
+
+#check f (α := Nat) mkVec
+
+def g (a : α) := xs.val.push a
+
+theorem ex3 : g ⟨#[0], rfl⟩ 1 = #[0, 1] :=
+  rfl
diff --git a/tests/lean/unboundImplicitLocals.lean.expected.out b/tests/lean/unboundImplicitLocals.lean.expected.out
index 024486c3c2..fe1d580652 100644
--- a/tests/lean/unboundImplicitLocals.lean.expected.out
+++ b/tests/lean/unboundImplicitLocals.lean.expected.out
@@ -7,3 +7,6 @@ unboundImplicitLocals.lean:24:33: error: unknown identifier 'α'
 unboundImplicitLocals.lean:24:37: error: unknown identifier 'β'
 unboundImplicitLocals.lean:24:46: error: unknown identifier 'α'
 unboundImplicitLocals.lean:24:48: error: unknown identifier 'β'
+f : {α_1 : Type} → {n_1 : Nat} → Vec α_1 n_1 → Vec α_1 n_1
+f mkVec : Vec ?m 0
+f mkVec : Vec Nat 0