fix: add new addAutoBoundImplicits that avoids the hack at addAutoBoundImplicitsOld

src/Lean/Elab/Inductive.lean

@@ -76,7 +76,7 @@ private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc :
         let u ← mkFreshLevelMVar
         let type := mkSort u
         Term.synthesizeSyntheticMVarsNoPostponing
-        Term.addAutoBoundImplicitsOld params fun params => do
+        Term.addAutoBoundImplicits' params type fun params type => do
           pure <| acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
       | some typeStx =>
         let (type, numImplicitIndices) ← Term.withAutoBoundImplicit do
@@ -84,9 +84,9 @@ private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc :
           unless (← isTypeFormerType type) do
             throwErrorAt typeStx "invalid inductive type, resultant type is not a sort"
           Term.synthesizeSyntheticMVarsNoPostponing
-          Term.addAutoBoundImplicitsOld #[] fun indices =>
-            return (← mkForallFVars indices type, indices.size)
-        Term.addAutoBoundImplicitsOld params fun params => do
+          let indices ← Term.addAutoBoundImplicits #[]
+          return (← mkForallFVars indices type, indices.size)
+        Term.addAutoBoundImplicits' params type fun params type => do
           pure <| acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
     elabHeaderAux views (i+1) acc
   else
@@ -219,12 +219,12 @@ private def elabCtors (indFVars : Array Expr) (indFVar : Expr) (params : Array E
             k type
         elabCtorType fun type => do
           Term.synthesizeSyntheticMVarsNoPostponing
-          Term.addAutoBoundImplicitsOld ctorParams fun ctorParams => do
-            let type ← mkForallFVars ctorParams type
-            Term.mvarsToParams type fun extraCtorParams type => do
-              let type ← mkForallFVars extraCtorParams type
-              let type ← mkForallFVars params type
-              return { name := ctorView.declName, type }
+          let ctorParams ← Term.addAutoBoundImplicits ctorParams
+          let type  ← mkForallFVars ctorParams type
+          let extraCtorParams ← Term.collectUnassignedMVars type
+          let type ← mkForallFVars extraCtorParams type
+          let type ← mkForallFVars params type
+          return { name := ctorView.declName, type }
 where
   checkParamOccs (ctorType : Expr) : MetaM Expr :=
     let visit (e : Expr) : MetaM TransformStep := do

src/Lean/Elab/Term.lean

@@ -1391,6 +1391,74 @@ where
     | 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`.
+-/
+partial def collectUnassignedMVars (type : Expr) (init : Array Expr := #[]) : TermElabM (Array Expr) := do
+  let mvarIds ← getMVars type
+  if mvarIds.isEmpty then
+    return init
+  else
+    go mvarIds.toList init
+where
+  go (mvarIds : List MVarId) (result : Array Expr) : TermElabM (Array Expr) := do
+    match mvarIds with
+    | [] => return result
+    | mvarId :: mvarIds => do
+      if (← isExprMVarAssigned mvarId) then
+        go mvarIds result
+      else
+        let mvarType := (← getMVarDecl mvarId).type
+        let mvarIdsNew ← getMVars mvarType
+        if mvarIdsNew.isEmpty then
+          let mvar := mkMVar mvarId
+          if result.contains mvar then
+            go mvarIds result
+          else
+            go  mvarIds (result.push (mkMVar mvarId))
+        else
+          go (mvarIdsNew.toList ++ mvarId :: mvarIds) result
+
+/--
+  Return `autoBoundImplicits ++ xs`
+  This methoid throws an error if a variable in `autoBoundImplicits` depends on some `x` in `xs`.
+  The `autoBoundImplicits` may contain free variables created by the auto-implicit feature, and unassigned free variables.
+  It avoids the hack used at `autoBoundImplicitsOld`.
+
+  Remark: we cannot simply replace every occurrence of `addAutoBoundImplicitsOld` with this one because a particular
+  use-case may not be able to handle the metavariables in the array being given to `k`.
+-/
+def addAutoBoundImplicits (xs : Array Expr) : TermElabM (Array Expr) := do
+  let autos := (← read).autoBoundImplicits
+  go autos.toList #[]
+where
+  go (todo : List Expr) (autos : Array Expr) : TermElabM (Array Expr) := do
+    match todo with
+    | [] =>
+      for auto in autos do
+        if auto.isFVar then
+          let localDecl ← getLocalDecl auto.fvarId!
+          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}'"
+      return autos ++ xs
+    | auto :: todo =>
+      let autos ← collectUnassignedMVars (← inferType auto) autos
+      go todo (autos.push auto)
+
+/--
+  Similar to `autoBoundImplicits`, but immediately if the resulting array of expressions contains metavariables,
+  it immediately use `mkForallFVars` + `forallBoundedTelescope` to convert them into free variables.
+  The type `type` is modified during the process if type depends on `xs`.
+  We use this method to simplify the conversion of code using `autoBoundImplicitsOld` to `autoBoundImplicits`
+-/
+def addAutoBoundImplicits' (xs : Array Expr) (type : Expr) (k : Array Expr → Expr → TermElabM α) : TermElabM α := do
+  let xs ← addAutoBoundImplicits xs
+  if xs.all (·.isFVar) then
+    k xs type
+  else
+    forallBoundedTelescope (← mkForallFVars xs type) xs.size fun xs type => k xs type
+
 def mkAuxName (suffix : Name) : TermElabM Name := do
   match (← read).declName? with
   | none          => throwError "auxiliary declaration cannot be created when declaration name is not available"

tests/lean/fixedIndicesToParams.lean.expected.out

@@ -1,15 +1,15 @@
 inductive sublist.{u_1} : {α : Type u_1} → List α → List α → Prop
 number of parameters: 1
 constructors:
-sublist.slnil : ∀ {a : Type u_1}, sublist [] []
-sublist.cons : ∀ {a : Type u_1} (l₁ l₂ : List a) (a_1 : a), sublist l₁ l₂ → sublist l₁ (a_1 :: l₂)
-sublist.cons2 : ∀ {a : Type u_1} (l₁ l₂ : List a) (a_1 : a), sublist l₁ l₂ → sublist (a_1 :: l₁) (a_1 :: l₂)
+sublist.slnil : ∀ {x : Type u_1}, sublist [] []
+sublist.cons : ∀ {x : Type u_1} (l₁ l₂ : List x) (a : x), sublist l₁ l₂ → sublist l₁ (a :: l₂)
+sublist.cons2 : ∀ {x : Type u_1} (l₁ l₂ : List x) (a : x), sublist l₁ l₂ → sublist (a :: l₁) (a :: l₂)
 inductive Foo.{u_1} : {α : Type u_1} → List α → Type u_1
 number of parameters: 1
 constructors:
-Foo.mk₁ : {a : Type u_1} → Foo []
+Foo.mk₁ : {x : Type u_1} → Foo []
 Foo.mk₂ : {α : Type u_1} → {as : List α} → (a : α) → Foo as → Foo (a :: as)
-inductive Bla.{u_1} : {a : Type u_1} → {as : List a} → Foo as → Type
+inductive Bla.{u_1} : {x : Type u_1} → {as : List x} → Foo as → Type
 number of parameters: 1
 constructors:
-Bla.mk₁ : {a : Type u_1} → Bla Foo.mk₁
+Bla.mk₁ : {x : Type u_1} → Bla Foo.mk₁

tests/lean/interactive/autoBoundIssue.lean

@@ -0,0 +1,18 @@
+inductive Vector (α : Type u) : Nat → Type u
+  | nil : Vector α 0
+  | cons : α → Vector α n → Vector α (n+1)
+
+infix:67 " :: " => Vector.cons
+
+inductive Ty where
+  | int
+  | bool
+  | fn (a r : Ty)
+
+inductive HasType : Fin n → Vector Ty n → Ty → Type where
+  | stop : HasType 0 (ty :: ctx) ty
+  | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty
+                   --^ $/lean/plainTermGoal
+
+inductive Foo : HasType k ctx ty → Prop
+                        --^ $/lean/plainTermGoal

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

@@ -0,0 +1,12 @@
+{"textDocument": {"uri": "file://autoBoundIssue.lean"},
+ "position": {"line": 13, "character": 21}}
+{"range":
+ {"start": {"line": 13, "character": 21}, "end": {"line": 13, "character": 24}},
+ "goal":
+ "HasType : {n : Nat} → Fin n → Vector Ty n → Ty → Type\nk : Fin ?m\nctx : Vector Ty ?m\nty u : Ty\n⊢ Vector Ty ?m"}
+{"textDocument": {"uri": "file://autoBoundIssue.lean"},
+ "position": {"line": 16, "character": 26}}
+{"range":
+ {"start": {"line": 16, "character": 26}, "end": {"line": 16, "character": 29}},
+ "goal":
+ "k : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"}