From b8aefe3a3723b8ca7d15e06f4fd1c3b4c4a00233 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 22 Aug 2024 16:20:25 +0200
Subject: [PATCH] fix: improper handling of strict-implicit section variables
 (#5138)

This was actually broken even before `include`

(cherry picked from commit 33d24c3bcab0cb18a26b1f817ef2f0b2299f1e95)
---
 src/Lean/Elab/BuiltinCommand.lean |  4 ++--
 src/Lean/Elab/Command.lean        | 26 ++++++++++++++------------
 2 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 6558fa6fb625..f4d352eec856 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -235,7 +235,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
       let binders ← replaceBinderAnnotation binder
       -- Remark: if we want to produce error messages when variables shadow existing ones, here is the place to do it.
       for binder in binders do
-        let varUIds ← getBracketedBinderIds binder |>.mapM (withFreshMacroScope ∘ MonadQuotation.addMacroScope)
+        let varUIds ← (← getBracketedBinderIds binder) |>.mapM (withFreshMacroScope ∘ MonadQuotation.addMacroScope)
         modifyScope fun scope => { scope with varDecls := scope.varDecls.push binder, varUIds := scope.varUIds ++ varUIds }
   | _ => throwUnsupportedSyntax
 
@@ -505,7 +505,7 @@ def elabRunMeta : CommandElab := fun stx =>
 @[builtin_command_elab Lean.Parser.Command.include] def elabInclude : CommandElab
   | `(Lean.Parser.Command.include| include $ids*) => do
     let sc ← getScope
-    let vars := sc.varDecls.concatMap getBracketedBinderIds
+    let vars ← sc.varDecls.concatMapM getBracketedBinderIds
     let mut uids := #[]
     for id in ids do
       if let some idx := vars.findIdx? (· == id.getId) then
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 3b81cc026807..5ca2f406be66 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -553,19 +553,21 @@ private def mkMetaContext : Meta.Context := {
 
 open Lean.Parser.Term in
 /-- Return identifier names in the given bracketed binder. -/
-def getBracketedBinderIds : Syntax → Array Name
-  | `(bracketedBinderF|($ids* $[: $ty?]? $(_annot?)?)) => ids.map Syntax.getId
-  | `(bracketedBinderF|{$ids* $[: $ty?]?})             => ids.map Syntax.getId
-  | `(bracketedBinderF|[$id : $_])                     => #[id.getId]
-  | `(bracketedBinderF|[$_])                           => #[Name.anonymous]
-  | _                                                 => #[]
-
-private def mkTermContext (ctx : Context) (s : State) : Term.Context := Id.run do
+def getBracketedBinderIds : Syntax → CommandElabM (Array Name)
+  | `(bracketedBinderF|($ids* $[: $ty?]? $(_annot?)?)) => return ids.map Syntax.getId
+  | `(bracketedBinderF|{$ids* $[: $ty?]?})             => return ids.map Syntax.getId
+  | `(bracketedBinderF|⦃$ids* : $_⦄)                   => return ids.map Syntax.getId
+  | `(bracketedBinderF|[$id : $_])                     => return #[id.getId]
+  | `(bracketedBinderF|[$_])                           => return #[Name.anonymous]
+  | _                                                  => throwUnsupportedSyntax
+
+private def mkTermContext (ctx : Context) (s : State) : CommandElabM Term.Context := do
   let scope      := s.scopes.head!
   let mut sectionVars := {}
-  for id in scope.varDecls.concatMap getBracketedBinderIds, uid in scope.varUIds do
+  for id in (← scope.varDecls.concatMapM getBracketedBinderIds), uid in scope.varUIds do
     sectionVars := sectionVars.insert id uid
-  { macroStack             := ctx.macroStack
+  return {
+    macroStack             := ctx.macroStack
     sectionVars            := sectionVars
     isNoncomputableSection := scope.isNoncomputable
     tacticCache?           := ctx.tacticCache? }
@@ -605,7 +607,7 @@ def liftTermElabM (x : TermElabM α) : CommandElabM α := do
   -- make sure `observing` below also catches runtime exceptions (like we do by default in
   -- `CommandElabM`)
   let _ := MonadAlwaysExcept.except (m := TermElabM)
-  let x : MetaM _ := (observing (try x finally Meta.reportDiag)).run (mkTermContext ctx s) { levelNames := scope.levelNames }
+  let x : MetaM _ := (observing (try x finally Meta.reportDiag)).run (← mkTermContext ctx s) { levelNames := scope.levelNames }
   let x : CoreM _ := x.run mkMetaContext {}
   let ((ea, _), _) ← runCore x
   MonadExcept.ofExcept ea
@@ -702,7 +704,7 @@ def expandDeclId (declId : Syntax) (modifiers : Modifiers) : CommandElabM Expand
   let currNamespace ← getCurrNamespace
   let currLevelNames ← getLevelNames
   let r ← Elab.expandDeclId currNamespace currLevelNames declId modifiers
-  for id in (← getScope).varDecls.concatMap getBracketedBinderIds do
+  for id in (← (← getScope).varDecls.concatMapM getBracketedBinderIds) do
     if id == r.shortName then
       throwError "invalid declaration name '{r.shortName}', there is a section variable with the same name"
   return r