diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 9864e4dc4e..ce1df40067 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -122,7 +122,7 @@ private def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHe Term.synthesizeSyntheticMVarsNoPostponing let (binderIds, xs) := xs.unzip let xs ← addAutoBoundImplicits xs - let type ← mkForallFVars xs type + let type ← mkForallFVars' xs type let type ← instantiateMVars type let levelNames ← getLevelNames if view.type?.isSome then diff --git a/src/Lean/Meta/ForEachExpr.lean b/src/Lean/Meta/ForEachExpr.lean index 08f41d776e..77af54be1f 100644 --- a/src/Lean/Meta/ForEachExpr.lean +++ b/src/Lean/Meta/ForEachExpr.lean @@ -60,4 +60,46 @@ def forEachExpr (e : Expr) (f : Expr → MetaM Unit) : MetaM Unit := f e pure true +/-- + Similar to `mkForallFVars`, but tries to infer better binder names when `xs` contains metavariables. + Let `?m` be a metavariable in `xs` s.t. `?m` does not have a user facing name. + Then, we try to find an application `f ... ?m` in the other binder typer and `type`, and + (temporarily) use the corresponding parameter name (with a fresh macro scope) as the user facing name for `?m`. + The "renaming" is temporary. +-/ +def mkForallFVars' (xs : Array Expr) (type : Expr) : MetaM Expr := do + if (← xs.anyM shouldInferBinderName) then + let toReset ← IO.mkRef #[] + try + for x in xs do + visit (← inferType x) toReset + visit type toReset + mkForallFVars xs type + finally + for mvarId in (← toReset.get) do + modifyMCtx fun mctx => mctx.setMVarUserNameTemporarily mvarId Name.anonymous + else + mkForallFVars xs type +where + shouldInferBinderName (x : Expr) : MetaM Bool := do + match x with + | .mvar mvarId _ => return (← Meta.getMVarDecl mvarId).userName.isAnonymous + | _ => return false + + visit (e : Expr) (toReset : IO.Ref (Array MVarId)) : MetaM Unit := do + forEachExpr (← instantiateMVars e) fun e => do + if e.isApp then + let args := e.getAppArgs + for i in [:args.size] do + let arg := args[i] + if arg.isMVar && xs.contains arg then + let mvarId := arg.mvarId! + if (← Meta.getMVarDecl mvarId).userName.isAnonymous then + forallBoundedTelescope (← inferType e.getAppFn) (some (i+1)) fun xs _ => do + if i < xs.size then + let mvarId := arg.mvarId! + let userName ← mkFreshUserName (← getFVarLocalDecl xs[i]).userName + toReset.modify (·.push mvarId) + modifyMCtx fun mctx => mctx.setMVarUserNameTemporarily mvarId userName + end Lean.Meta diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 0318ab1c35..accef1deac 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -349,6 +349,9 @@ def setMVarKind (mctx : MetavarContext) (mvarId : MVarId) (kind : MetavarKind) : let decl := mctx.getDecl mvarId { mctx with decls := mctx.decls.insert mvarId { decl with kind := kind } } +/-- + Set the metavariable user facing name. +-/ def setMVarUserName (mctx : MetavarContext) (mvarId : MVarId) (userName : Name) : MetavarContext := let decl := mctx.getDecl mvarId { mctx with @@ -357,6 +360,16 @@ def setMVarUserName (mctx : MetavarContext) (mvarId : MVarId) (userName : Name) let userNames := mctx.userNames.erase decl.userName if userName.isAnonymous then userNames else userNames.insert userName mvarId } +/-- + Low-level version of `setMVarUserName`. + It does not update the table `userNames`. Thus, `findUserName?` cannot see the modification. + It is meant for `mkForallFVars'` where we temporarily set the user facing name of metavariables to get more + meaningful binder names. +-/ +def setMVarUserNameTemporarily (mctx : MetavarContext) (mvarId : MVarId) (userName : Name) : MetavarContext := + let decl := mctx.getDecl mvarId + { mctx with decls := mctx.decls.insert mvarId { decl with userName := userName } } + /- Update the type of the given metavariable. This function assumes the new type is definitionally equal to the current one -/ def setMVarType (mctx : MetavarContext) (mvarId : MVarId) (type : Expr) : MetavarContext := diff --git a/tests/lean/autoBoundErrorMsg.lean.expected.out b/tests/lean/autoBoundErrorMsg.lean.expected.out index 3706bde77c..c775b766dd 100644 --- a/tests/lean/autoBoundErrorMsg.lean.expected.out +++ b/tests/lean/autoBoundErrorMsg.lean.expected.out @@ -1,7 +1,7 @@ autoBoundErrorMsg.lean:1:43-1:44: error: don't know how to synthesize placeholder context: α : Sort u_1 -x✝ : Sort u_2 -a b : x✝ +α✝ : Sort u_2 +a b : α✝ h : ∀ {a b : α}, a = b ⊢ a = b diff --git a/tests/lean/autoImplicitChain.lean.expected.out b/tests/lean/autoImplicitChain.lean.expected.out index 0a53477121..b4d2707172 100644 --- a/tests/lean/autoImplicitChain.lean.expected.out +++ b/tests/lean/autoImplicitChain.lean.expected.out @@ -1,2 +1,2 @@ -def f : {x : A} → {x_1 : B x} → {c : @C x x_1} → @D x x_1 c → Bool := -fun {x} {x_1} {c} d => true +def f : {a : A} → {a_1 : B a} → {c : @C a a_1} → @D a a_1 c → Bool := +fun {a} {a_1} {c} d => true diff --git a/tests/lean/autoImplicitChainNameIssue.lean b/tests/lean/autoImplicitChainNameIssue.lean new file mode 100644 index 0000000000..b5b40e6575 --- /dev/null +++ b/tests/lean/autoImplicitChainNameIssue.lean @@ -0,0 +1,12 @@ +inductive Palindrome : List α → Prop where + | nil : Palindrome [] + | single : (a : α) → Palindrome [a] + | sandwish : (a : α) → Palindrome as → Palindrome ([a] ++ as ++ [a]) + +theorem palindrome_reverse (h : Palindrome as) : Palindrome as.reverse := by + induction h with + | nil => done + | single a => exact Palindrome.single a + | sandwish a h ih => simp; exact Palindrome.sandwish _ ih + +#check @palindrome_reverse diff --git a/tests/lean/autoImplicitChainNameIssue.lean.expected.out b/tests/lean/autoImplicitChainNameIssue.lean.expected.out new file mode 100644 index 0000000000..cd3a94fcd5 --- /dev/null +++ b/tests/lean/autoImplicitChainNameIssue.lean.expected.out @@ -0,0 +1,6 @@ +autoImplicitChainNameIssue.lean:8:11-8:15: error: unsolved goals +case nil +α✝ : Type u_1 +as : List α✝ +⊢ Palindrome (List.reverse []) +@palindrome_reverse : ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)