feat: support for unboundImplicitLocals at variable and variables commands

They are morally part of the header.

cc @Kha

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

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

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