fix: remove hacky addAutoBoundImplicitsOld

src/Lean/Elab/Command.lean

@@ -395,7 +395,8 @@ def liftTermElabM {α} (declName? : Option Name) (x : TermElabM α) : CommandEla
           -- 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.resetMessageLog
-          Term.addAutoBoundImplicitsOld xs fun xs =>
+          let someType := mkSort levelZero
+          Term.addAutoBoundImplicits' xs someType fun xs _ =>
             Term.withoutAutoBoundImplicit <| elabFn xs
 
 @[inline] def catchExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit := fun ctx ref =>

src/Lean/Elab/Term.lean

@@ -1311,86 +1311,6 @@ partial def withAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
 def withoutAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
   withReader (fun ctx => { ctx with autoBoundImplicit := false, autoBoundImplicits := {} }) k
 
-private def mvarsToParamsCore (type : Expr) (init : Array Expr) (k : Array Expr → TermElabM α) : TermElabM α := do
-  let mvarIds ← getMVars type
-  if mvarIds.isEmpty then
-    k init
-  else
-    let hugeFuel := 10000000
-    go hugeFuel mvarIds.toList init
-where
-  go (fuel : Nat) (mvarIds : List MVarId) (params : Array Expr) : TermElabM α :=
-    match fuel with
-    | 0 => throwError "too many parameters"
-    | fuel+1 =>
-      match mvarIds with
-      | [] => k params
-      | mvarId :: mvarIds => do
-        if (← isExprMVarAssigned mvarId) then
-          go fuel mvarIds params
-        else
-          let mvarType := (← getMVarDecl mvarId).type
-          let mvarIdsNew ← getMVars mvarType
-          if mvarIdsNew.isEmpty then
-            withLocalDecl (← mkFreshUserName `a) BinderInfo.implicit mvarType fun newParam => do
-              /-
-                HACK: The following assingment is a bit hackish since `newParam` is not in the scope
-                of the metavariable. We claim this ok because we fully instantiate thes metavariables before executing the
-                continuation `k`.
-                Remark: yes, the resulting term is correct, but the `InfoTree` remains littered with invalid terms.
-                This must be fixed in the future. Otherwise, users will fin `_uniq.????` unknown free variables in the `InfoView`.
-               -/
-              assignExprMVar mvarId newParam
-              go fuel mvarIds (params.push newParam)
-          else
-            go fuel (mvarIdsNew.toList ++ mvarId :: mvarIds) params
-
-/--
-   Helper function for converting metavariables occurring in `type` into new parameters.
--/
-def mvarsToParams (type : Expr) (k : Array Expr → Expr → TermElabM α) (init : Array Expr := #[]) : TermElabM α :=
-  mvarsToParamsCore type init fun newParams => do
-    if newParams.isEmpty then
-      k newParams type
-    else
-      -- If new parameters were created for metavariables, we fully instantiate all metavariables in the current
-      -- local context befor invoking `k`. See hack above.
-      let (lctx, mctx) := (← getMCtx).instantiateLCtxMVars (← getLCtx)
-      setMCtx mctx
-      withLCtx lctx (← getLocalInstances) (k newParams (← instantiateMVars type))
-
-/--
-  Return `k (autoBoundImplicits ++ xs)`
-  This methoid throws an error if a variable in `autoBoundImplicits` depends on some `x` in `xs`.
-
-  Remark: this method corrupts the `InfoTree` when metavariables are converted into fresh free variables.
-  See "HACK" comment `mvarsToParamsCore.go`.
--/
-def addAutoBoundImplicitsOld (xs : Array Expr) (k : Array Expr → TermElabM α) : TermElabM α := do
-  let autos := (← read).autoBoundImplicits
-  go autos.toList #[]
-where
-  go (todo : List Expr) (autos : Array Expr) : TermElabM α := do
-    match todo with
-    | [] =>
-      for auto in autos do
-        let localDecl ← getLocalDecl auto.fvarId!
-        trace[Meta.debug] "auto bound implicit: {localDecl.userName} : {localDecl.type}"
-        for x in xs do
-          if (← getMCtx).localDeclDependsOn localDecl x.fvarId! then
-            throwError "invalid auto implicit argument '{auto}', it depends on explicitly provided argument '{x}'"
-      if autos.size != (← read).autoBoundImplicits.size then
-        -- If new auto locals were created for metavariables, we fully instantiate all metavariables in the current
-        -- local context befor invoking `k`. See hack above.
-        let (lctx, mctx) := (← getMCtx).instantiateLCtxMVars (← getLCtx)
-        setMCtx mctx
-        withLCtx lctx (← getLocalInstances) do
-          k (autos ++ xs)
-      else
-        k (autos ++ xs)
-    | auto :: todo =>
-      mvarsToParamsCore (← inferType auto) (init := autos) (fun autos => go todo (autos.push auto))
-
 /--
   Collect unassigned metavariables in `type` that are not already in `init`.
 -/

tests/lean/interactive/autoBoundIssue.lean

@@ -26,3 +26,8 @@ structure Ex where
                 --^ $/lean/plainTermGoal
   boo : HasType k ctx ty → Prop := fun _ => True
                 --^ $/lean/plainTermGoal
+
+variable (x : HasType k ctx ty)
+                      --^ $/lean/plainTermGoal
+
+#check x

tests/lean/interactive/autoBoundIssue.lean.expected.out

@@ -28,3 +28,9 @@
  {"start": {"line": 26, "character": 18}, "end": {"line": 26, "character": 21}},
  "goal":
  "aux : {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty : Ty} → HasType k ctx ty\nk : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"}
+{"textDocument": {"uri": "file://autoBoundIssue.lean"},
+ "position": {"line": 29, "character": 24}}
+{"range":
+ {"start": {"line": 29, "character": 24}, "end": {"line": 29, "character": 27}},
+ "goal":
+ "k : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"}