From 164b26bf019fe8e7f6312111c8fcd1bea1fa6751 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 4 May 2021 19:27:36 -0700
Subject: [PATCH] fix: make sure the resulting array size is equal to the
 number of binders

The following code relies on this property
```lean
       for uid in scope.varUIds, x in xs do
          sectionFVars := sectionFVars.insert uid x
```
---
 src/Lean/Elab/Command.lean    | 2 +-
 tests/lean/run/secVarBug.lean | 8 ++++++++
 2 files changed, 9 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/secVarBug.lean

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index d7ceacfd73..0dbd036a4e 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -306,7 +306,7 @@ def getBracketedBinderIds : Syntax → Array Name
   | `(bracketedBinder|($ids* $[: $ty?]? $(annot?)?)) => ids.map Syntax.getId
   | `(bracketedBinder|{$ids* $[: $ty?]?})            => ids.map Syntax.getId
   | `(bracketedBinder|[$id : $ty])                   => #[id.getId]
-  | `(bracketedBinder|[$ty])                         => #[]
+  | `(bracketedBinder|[$ty])                         => #[Name.anonymous]
   | _                                                => #[]
 
 private def mkTermContext (ctx : Context) (s : State) (declName? : Option Name) : Term.Context := do
diff --git a/tests/lean/run/secVarBug.lean b/tests/lean/run/secVarBug.lean
new file mode 100644
index 0000000000..f25b33f5b9
--- /dev/null
+++ b/tests/lean/run/secVarBug.lean
@@ -0,0 +1,8 @@
+variable {α} [ToString α] (n : Nat)
+
+local macro "foo" : term => `(n)
+
+def f :=
+  foo
+
+#check f 10