refactor: termination arguments as Expr, not Syntax (#3658)

Before, the termination argument as inferred by `GuessLex` was passed
further
on as `Syntax`, to be elaborated later in `WF.Rel`.

This didn’t feel quite right anymore. In particular if we want to teach
`GuessLex` about guessing more complex termination arguments like
`xs.size -
i`, using `Expr` here is more natural.

So this introduces `TerminationArgument` based on an `Expr` to be used
here.

A side-effect of how the termination arguments are elaborated is that
the unused
variables linter will now look at `termination_by` variables, and that
parameters
past the colon are not even invisibly in scope, so `‹_›` will not find
them
See https://github.com/leanprover-community/mathlib4/pull/11370/files
for examples
of fixing these changes.

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -175,8 +175,9 @@ but it works for now.
 def groupGoalsByFunction (argsPacker : ArgsPacker) (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId)) := do
   let mut r := mkArray numFuncs #[]
   for goal in goals do
-    let (.mdata _ (.app _ param)) ← goal.getType
-        | throwError "MVar does not look like like a recursive call"
+    let type ← goal.getType
+    let (.mdata _ (.app _ param)) := type
+        | throwError "MVar does not look like a recursive call:{indentExpr type}"
     let (funidx, _) ← argsPacker.unpack param
     r := r.modify funidx (·.push goal)
   return r
@@ -190,8 +191,9 @@ def solveDecreasingGoals (argsPacker : ArgsPacker) (decrTactics : Array (Option
     match decrTactic? with
     | none => do
       for goal in goals do
+        let type ← goal.getType
         let some ref := getRecAppSyntax? (← goal.getType)
-          | throwError "MVar does not look like like a recursive call"
+          | throwError "MVar not annotated as a recursive call:{indentExpr type}"
         withRef ref <| applyDefaultDecrTactic goal
     | some decrTactic => withRef decrTactic.ref do
       unless goals.isEmpty do -- unlikely to be empty

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -14,7 +14,7 @@ import Lean.Elab.Quotation
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
-import Lean.Elab.PreDefinition.WF.TerminationHint
+import Lean.Elab.PreDefinition.WF.TerminationArgument
 import Lean.Data.Array
 
 
@@ -564,61 +564,6 @@ partial def solve {m} {α} [Monad m] (measures : Array α)
     -- None found, we have to give up
     return .none
 
-/--
-Create Tuple syntax (`()` if the array is empty, and just the value if its a singleton)
--/
-def mkTupleSyntax : Array Term → MetaM Term
-  | #[]  => `(())
-  | #[e] => return e
-  | es   => `(($(es[0]!), $(es[1:]),*))
-
-/--
-Given an array of `MutualMeasures`, creates a `TerminationWF` that specifies the lexicographic
-combination of these measures. The parameters are
-
-* `originalVarNamess`: For each function in the clique, the original parameter names, _including_
-  the fixed prefix.  Used to determine if we need to fully qualify `sizeOf`.
-* `varNamess`: For each function in the clique, the parameter names to be used in the
-  termination relation. Excludes the fixed prefix. Includes names like `x1` for unnamed parameters.
-* `measures`: The measures to be used.
--/
-def buildTermWF (originalVarNamess : Array (Array Name)) (varNamess : Array (Array Name))
-  (needsNoSizeOf : Array (Array Nat)) (measures : Array MutualMeasure) : MetaM TerminationWF := do
-  varNamess.mapIdxM fun funIdx varNames => do
-    let idents := varNames.map mkIdent
-    let measureStxs ← measures.mapM fun
-      | .args varIdxs => do
-          let varIdx := varIdxs[funIdx]!
-          let v := idents[varIdx]!
-          if needsNoSizeOf[funIdx]!.contains varIdx then
-            `($v)
-          else
-            -- Print `sizeOf` as such, unless it is shadowed.
-            -- Shadowing by a `def` in the current namespace is handled by `unresolveNameGlobal`.
-            -- But it could also be shadowed by an earlier parameter (including the fixed prefix),
-            -- so look for unqualified (single tick) occurrences in `originalVarNames`
-            let sizeOfIdent :=
-              if originalVarNamess[funIdx]!.any (· = `sizeOf) then
-                mkIdent ``sizeOf -- fully qualified
-              else
-                mkIdent (← unresolveNameGlobal ``sizeOf)
-            `($sizeOfIdent $v)
-      | .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
-    let body ← mkTupleSyntax measureStxs
-    return { ref := .missing, vars := idents, body, synthetic := true }
-
-/--
-The TerminationWF produced by GuessLex may mention more variables than allowed in the surface
-syntax (in case of unnamed or shadowed parameters). So how to print this to the user? Invalid
-syntax with more information, or valid syntax with (possibly) unresolved variable names?
-The latter works fine in many cases, and is still useful to the user in the tricky corner cases, so
-we do that.
--/
-def trimTermWF (extraParams : Array Nat) (elems : TerminationWF) : TerminationWF :=
-  elems.mapIdx fun funIdx elem => { elem with
-    vars := elem.vars[elem.vars.size - extraParams[funIdx]! : elem.vars.size]
-    synthetic := false }
-
 /--
 Given a matrix (row-major) of strings, arranges them in tabular form.
 First column is left-aligned, others right-aligned.
@@ -716,16 +661,48 @@ def explainFailure (declNames : Array Name) (varNamess : Array (Array Name))
   return r
 
 /--
-Shows the termination measure used to the user, and implements `termination_by?`
+For `#[x₁, .., xₙ]` create `(x₁, .., xₙ)`.
 -/
-def reportWF (preDefs : Array PreDefinition) (wf : TerminationWF) : MetaM Unit := do
-  let extraParamss := preDefs.map (·.termination.extraParams)
-  let wf' := trimTermWF extraParamss wf
-  for preDef in preDefs, term in wf' do
+def mkProdElem (xs : Array Expr) : MetaM Expr := do
+  match xs.size with
+  | 0 => return default
+  | 1 => return xs[0]!
+  | _ =>
+    let n := xs.size
+    xs[0:n-1].foldrM (init:=xs[n-1]!) fun x p => mkAppM ``Prod.mk #[x,p]
+
+def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : MetaM α := do
+  let mut lctx ←  getLCtx
+  for x in xs, n in ns do lctx := lctx.setUserName x.fvarId! n
+  withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
+
+def toTerminationArguments (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
+    (userVarNamess : Array (Array Name)) (needsNoSizeOf : Array (Array Nat))
+    (solution : Array MutualMeasure) : MetaM TerminationArguments := do
+  preDefs.mapIdxM fun funIdx preDef => do
+    lambdaTelescope preDef.value fun xs _ => do
+      withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do
+        let args ← solution.mapM fun
+          | .args varIdxs =>
+            let arg := varIdxs[funIdx]!
+            if needsNoSizeOf[funIdx]!.contains arg then
+              pure xs[fixedPrefixSize + arg]!
+            else
+              mkAppM ``sizeOf #[xs[fixedPrefixSize + arg]!]
+          | .func funIdx' => pure <| mkNatLit <| if funIdx' == funIdx then 1 else 0
+        let fn ← mkLambdaFVars xs (← mkProdElem args)
+        let extraParams := preDef.termination.extraParams
+        return { ref := .missing, arity := xs.size, extraParams, fn}
+
+/--
+Shows the inferred termination argument to the user, and implements `termination_by?`
+-/
+def reportTermArgs (preDefs : Array PreDefinition) (termArgs : TerminationArguments) : MetaM Unit := do
+  for preDef in preDefs, termArg in termArgs do
     if showInferredTerminationBy.get (← getOptions) then
-      logInfoAt preDef.ref m!"Inferred termination argument:\n{← term.unexpand}"
+      logInfoAt preDef.ref m!"Inferred termination argument:\n{← termArg.delab}"
     if let some ref := preDef.termination.terminationBy?? then
-      Tactic.TryThis.addSuggestion ref (← term.unexpand)
+      Tactic.TryThis.addSuggestion ref (← termArg.delab)
 
 end GuessLex
 open GuessLex
@@ -738,20 +715,17 @@ terminates. See the module doc string for a high-level overview.
 -/
 def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
     (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) :
-    MetaM TerminationWF := do
-  let extraParamss := preDefs.map (·.termination.extraParams)
+    MetaM TerminationArguments := do
   let arities := argsPacker.varNamess.map (·.size)
   let userVarNamess ← argsPacker.varNamess.mapM (naryVarNames ·)
-  -- with fixed prefix, used to qualify the  measure in buildTermWf.
-  let originalVarNamess ← preDefs.mapM originalVarNames
   trace[Elab.definition.wf] "varNames is: {userVarNamess}"
 
-  let forbiddenArgs ← preDefs.mapM (getForbiddenByTrivialSizeOf fixedPrefixSize)
+  let forbiddenArgs ← preDefs.mapM (getForbiddenByTrivialSizeOf fixedPrefixSize ·)
   let needsNoSizeOf ←
     if preDefs.size = 1 then
-      preDefs.mapM (getSizeOfParams fixedPrefixSize)
+      preDefs.mapM (getSizeOfParams fixedPrefixSize ·)
     else
-      preDefs.mapM (getNatParams fixedPrefixSize)
+      preDefs.mapM (getNatParams fixedPrefixSize ·)
 
   -- The list of measures, including the measures that order functions.
   -- The function ordering measures come last
@@ -759,9 +733,9 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
 
   -- If there is only one plausible measure, use that
   if let #[solution] := measures then
-    let wf ← buildTermWF originalVarNamess userVarNamess needsNoSizeOf #[solution]
-    reportWF preDefs wf
-    return wf
+    let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess  needsNoSizeOf #[solution]
+    reportTermArgs preDefs termArgs
+    return termArgs
 
   -- Collect all recursive calls and extract their context
   let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize argsPacker
@@ -771,16 +745,9 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
 
   match ← liftMetaM <| solve measures callMatrix with
   | .some solution => do
-    let wf ← buildTermWF originalVarNamess userVarNamess needsNoSizeOf solution
-
-    let wf' := trimTermWF extraParamss wf
-    for preDef in preDefs, term in wf' do
-      if showInferredTerminationBy.get (← getOptions) then
-        logInfoAt preDef.ref m!"Inferred termination argument:\n{← term.unexpand}"
-      if let some ref := preDef.termination.terminationBy?? then
-        Tactic.TryThis.addSuggestion ref (← term.unexpand)
-
-    return wf
+    let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess needsNoSizeOf solution
+    reportTermArgs preDefs termArgs
+    return termArgs
   | .none =>
     let explanation ← explainFailure (preDefs.map (·.declName)) userVarNamess rcs
     Lean.throwError <| "Could not find a decreasing measure.\n" ++

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Elab.PreDefinition.Basic
-import Lean.Elab.PreDefinition.WF.TerminationHint
+import Lean.Elab.PreDefinition.WF.TerminationArgument
 import Lean.Elab.PreDefinition.WF.PackMutual
 import Lean.Elab.PreDefinition.WF.Preprocess
 import Lean.Elab.PreDefinition.WF.Rel
@@ -99,13 +99,16 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
     let preDefsDIte ← preDefs.mapM fun preDef => return { preDef with value := (← iteToDIte preDef.value) }
     return (fixedPrefixSize, argsPacker, ← packMutual fixedPrefixSize argsPacker preDefsDIte)
 
-  let wf ← do
+  let wf : TerminationArguments ← do
     let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.terminationBy?.isSome)
     if preDefsWith.isEmpty then
       -- No termination_by anywhere, so guess one
       guessLex preDefs unaryPreDef fixedPrefixSize argsPacker
     else if preDefsWithout.isEmpty then
-      pure <| preDefsWith.map (·.termination.terminationBy?.get!)
+      preDefsWith.mapIdxM fun funIdx predef => do
+        let arity := fixedPrefixSize + argsPacker.varNamess[funIdx]!.size
+        let hints := predef.termination
+        TerminationArgument.elab predef.declName predef.type arity hints.extraParams hints.terminationBy?.get!
     else
       -- Some have, some do not, so report errors
       preDefsWithout.forM fun preDef => do
@@ -118,7 +121,7 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
     unless type.isForall do
       throwError "wfRecursion: expected unary function type: {type}"
     let packedArgType := type.bindingDomain!
-    elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf fun wfRel => do
+    elabWFRel preDefs unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef

src/Lean/Elab/PreDefinition/WF/Rel.lean

@@ -9,76 +9,58 @@ import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Rename
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.PreDefinition.Basic
-import Lean.Elab.PreDefinition.WF.TerminationHint
+import Lean.Elab.PreDefinition.WF.TerminationArgument
+import Lean.Meta.ArgsPacker
 
 namespace Lean.Elab.WF
 open Meta
 open Term
 
-private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarId) (fvarId : FVarId) : TermElabM (Array (FVarId × MVarId)) := do
-  let rec go (i : Nat) (mvarId : MVarId) (fvarId : FVarId) (result : Array (FVarId × MVarId)) : TermElabM (Array (FVarId × MVarId)) := do
-    if i < preDefs.size - 1 then
-      let #[s₁, s₂] ←  mvarId.cases fvarId | unreachable!
-      go (i + 1) s₂.mvarId s₂.fields[0]!.fvarId! (result.push (s₁.fields[0]!.fvarId!, s₁.mvarId))
-    else
-      return result.push (fvarId, mvarId)
-  go 0 mvarId fvarId #[]
+/--
+The termination arguments must not depend on the varying parameters of the function, and in
+a mutual clique, they must be the same for all functions.
 
-private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mvarId : MVarId)
-    (fvarId : FVarId) (element : TerminationBy) : TermElabM MVarId := do
-  element.checkVars preDef.declName preDef.termination.extraParams
-  -- If `synthetic := false`, then this is user-provided, and should be interpreted
-  -- as left to right. Else it is provided by GuessLex, and may rename non-extra paramters as well.
-  -- (Not pretty, but it works for now)
-  let implicit_underscores :=
-    if element.synthetic then 0 else preDef.termination.extraParams - element.vars.size
-  let varNames ← lambdaTelescope preDef.value fun xs _ => do
-    let mut varNames ← xs.mapM fun x => x.fvarId!.getUserName
-    for h : i in [:element.vars.size] do
-      let varStx := element.vars[i]
-      if let `($ident:ident) := varStx then
-        let j := varNames.size - implicit_underscores - element.vars.size + i
-        varNames := varNames.set! j ident.getId
-    return varNames
-  let mut mvarId := mvarId
-  for localDecl in (← Term.getMVarDecl mvarId).lctx, varName in varNames[:prefixSize] do
-    unless localDecl.userName == varName do
-      mvarId ← mvarId.rename localDecl.fvarId varName
-  let numPackedArgs := varNames.size - prefixSize
-  let rec go (i : Nat) (mvarId : MVarId) (fvarId : FVarId) : TermElabM MVarId := do
-    trace[Elab.definition.wf] "i: {i}, varNames: {varNames}, goal: {mvarId}"
-    if i < numPackedArgs - 1 then
-      let #[s] ← mvarId.cases fvarId #[{ varNames := [varNames[prefixSize + i]!] }] | unreachable!
-      go (i+1) s.mvarId s.fields[1]!.fvarId!
-    else
-      mvarId.rename fvarId varNames.back
-  go 0 mvarId fvarId
+This ensures the preconditions for `ArgsPacker.uncurryND`.
+-/
+def checkCodomains (names : Array Name) (prefixArgs : Array Expr) (arities : Array Nat)
+    (termArgs : TerminationArguments) : TermElabM Expr := do
+  let mut codomains := #[]
+  for name in names, arity in arities, termArg in termArgs do
+    let type ← inferType (termArg.fn.beta prefixArgs)
+    let codomain ← forallBoundedTelescope type arity fun xs codomain => do
+      let fvars := xs.map (·.fvarId!)
+      if codomain.hasAnyFVar (fvars.contains ·) then
+        throwErrorAt termArg.ref  m!"The termination argument's type must not depend on the " ++
+          m!"function's varying parameters, but {name}'s termination argument does:{indentExpr type}\n" ++
+          "Try using `sizeOf` explicitly"
+      pure codomain
+    codomains := codomains.push codomain
 
-def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat)
-    (argType : Expr) (wf : TerminationWF) (k : Expr → TermElabM α) : TermElabM α := do
+  let codomain0 := codomains[0]!
+  for h : i in [1 : codomains.size] do
+    unless ← isDefEqGuarded codomain0 codomains[i] do
+      throwErrorAt termArgs[i]!.ref m!"The termination arguments of mutually recursive functions " ++
+        m!"must have the same return type, but the termination argument of {names[0]!} has type" ++
+        m!"{indentExpr codomain0}\n" ++
+        m!"while the termination argument of {names[i]!} has type{indentExpr codomains[i]}\n" ++
+        "Try using `sizeOf` explicitly"
+  return codomain0
+
+/--
+If the `termArgs` map the packed argument `argType` to `β`, then this function passes to the
+continuation a value of type `WellFoundedRelation argType` that is derived from the instance
+for `WellFoundedRelation β` using `invImage`.
+-/
+def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (prefixArgs : Array Expr)
+    (argsPacker : ArgsPacker) (argType : Expr) (termArgs : TerminationArguments)
+    (k : Expr → TermElabM α) : TermElabM α := withDeclName unaryPreDefName do
   let α := argType
   let u ← getLevel α
-  let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α
-  trace[Elab.definition.wf] "elabWFRel start: {(← mkFreshTypeMVar).mvarId!}"
-  withDeclName unaryPreDefName do
-    let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
-    let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
-    let (d, fMVarId) ← fMVarId.intro1
-    let subgoals ← unpackMutual preDefs fMVarId d
-    for (d, mvarId) in subgoals, element in wf, preDef in preDefs do
-      let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
-      mvarId.withContext do
-        let errorMsgHeader? := if preDefs.size > 1 then
-          "The termination argument types differ for the different functions, or depend on the " ++
-          "function's varying parameters. Try using `sizeOf` explicitly:\nThe termination argument"
-        else
-          "The termination argument depends on the function's varying parameters. Try using " ++
-          "`sizeOf` explicitly:\nThe termination argument"
-        let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
-            (errorMsgHeader? := errorMsgHeader?)
-        mvarId.assign value
-    let wfRelVal ← synthInstance (← inferType (mkMVar wfRelMVarId))
-    wfRelMVarId.assign wfRelVal
-    k (← instantiateMVars (mkMVar mainMVarId))
+  let β ← checkCodomains (preDefs.map (·.declName)) prefixArgs argsPacker.arities termArgs
+  let v ← getLevel β
+  let packedF ← argsPacker.uncurryND (termArgs.map (·.fn.beta prefixArgs))
+  let inst ← synthInstance (.app (.const ``WellFoundedRelation [v]) β)
+  let rel ← instantiateMVars (mkApp4 (.const ``invImage [u,v]) α β packedF inst)
+  k rel
 
 end Lean.Elab.WF

src/Lean/Elab/PreDefinition/WF/TerminationArgument.lean

@@ -0,0 +1,106 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Joachim Breitner
+-/
+prelude
+
+import Lean.Parser.Term
+import Lean.Elab.Term
+import Lean.Elab.Binders
+import Lean.Elab.SyntheticMVars
+import Lean.Elab.PreDefinition.WF.TerminationHint
+import Lean.PrettyPrinter.Delaborator
+
+/-!
+This module contains the data type `TerminationArgument`, the elaborated form of a `TerminationBy`
+clause, the `TerminationArguments` type for a clique and the elaboration functions.
+-/
+
+set_option autoImplicit false
+
+namespace Lean.Elab.WF
+
+open Lean Meta Elab Term
+
+/--
+Elaborated form for a `termination_by` clause.
+
+The `fn` has the same (value) arity as the recursive functions (stored in
+`arity`), and maps its arguments (including fixed prefix, in unpacked form) to
+the termination argument.
+-/
+structure TerminationArgument where
+  ref : Syntax
+  arity : Nat
+  extraParams : Nat
+  fn : Expr
+deriving Inhabited
+
+/-- A complete set of `TerminationArgument`s, as applicable to a single clique.  -/
+abbrev TerminationArguments := Array TerminationArgument
+
+/--
+Elaborates a `TerminationBy` to an `TerminationArgument`.
+
+* `type` is the full type of the original recursive function, including fixed prefix.
+* `arity` is the value arity of the recursive function; the termination argument cannot take more.
+* `extraParams` is the the number of parameters the function has after the colon; together with
+  `arity` indicates how many parameters of the function are before the colon and thus in scope.
+* `hint : TerminationBy` is the syntactic `TerminationBy`.
+-/
+def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams : Nat)
+    (hint : TerminationBy) : TermElabM TerminationArgument := withDeclName funName do
+  assert! extraParams ≤ arity
+
+  if hint.vars.size > extraParams then
+    let mut msg := m!"{parameters hint.vars.size} bound in `termination_by`, but the body of " ++
+      m!"{funName} only binds {parameters extraParams}."
+    if let `($ident:ident) := hint.vars[0]! then
+      if ident.getId.isSuffixOf funName then
+          msg := msg ++ m!" (Since Lean v4.6.0, the `termination_by` clause no longer " ++
+            "expects the function name here.)"
+    throwErrorAt hint.ref msg
+
+  -- Bring parameters before the colon into scope
+  let r ← withoutErrToSorry <|
+    forallBoundedTelescope type (arity - extraParams) fun ys type' => do
+      -- Bring the variables bound by `termination_by` into scope.
+      elabFunBinders hint.vars (some type') fun xs type' => do
+        -- Elaborate the body in this local environment
+        let body ← Lean.Elab.Term.withSynthesize <| elabTermEnsuringType hint.body none
+        -- Now abstract also over the remaining extra parameters
+        forallBoundedTelescope type'.get! (extraParams - hint.vars.size) fun zs _ => do
+          mkLambdaFVars (ys ++ xs ++ zs) body
+  -- logInfo m!"elabTermValue: {r}"
+  check r
+  pure { ref := hint.ref, arity, extraParams, fn := r}
+  where
+    parameters : Nat → MessageData
+    | 1 => "one parameter"
+    | n => m!"{n} parameters"
+
+open PrettyPrinter Delaborator SubExpr Parser.Termination Parser.Term in
+def TerminationArgument.delab (termArg : TerminationArgument) : MetaM (TSyntax ``terminationBy) := do
+  lambdaTelescope termArg.fn fun ys e => do
+    let e ← mkLambdaFVars ys[termArg.arity - termArg.extraParams:] e -- undo overshooting by lambdaTelescope
+    pure (← delabCore e (delab := go termArg.extraParams #[])).1
+  where
+    go : Nat → TSyntaxArray [`ident, `Lean.Parser.Term.hole] → DelabM (TSyntax ``terminationBy)
+    | 0, vars => do
+      -- drop trailing underscores
+      let mut vars := vars
+      while ! vars.isEmpty && vars.back.raw.isOfKind ``hole do vars := vars.pop
+      if vars.isEmpty then
+        `(terminationBy|termination_by $(← Delaborator.delab))
+      else
+        `(terminationBy|termination_by $vars* => $(← Delaborator.delab))
+    | i+1, vars => do
+      let e ← getExpr
+      unless e.isLambda do return ← go 0 vars -- should not happen
+
+      -- Delaborate unused parameters with `_`
+      if e.bindingBody!.hasLooseBVar 0 then
+        withBindingBodyUnusedName fun n => go i (vars.push ⟨n⟩)
+      else
+        descend e.bindingBody! 1 (go i (vars.push (← `(hole|_))))

src/Lean/Elab/PreDefinition/WF/TerminationHint.lean

@@ -26,18 +26,6 @@ structure TerminationBy where
   synthetic : Bool := false
   deriving Inhabited
 
-open Parser.Termination in
-def TerminationBy.unexpand (wf : TerminationBy) : MetaM (TSyntax ``terminationBy) := do
-  -- TODO: Why can I not just use $wf.vars in the quotation below?
-  let vars : TSyntaxArray `ident := wf.vars.map (⟨·.raw⟩)
-  if vars.isEmpty then
-    `(terminationBy|termination_by $wf.body)
-  else
-    `(terminationBy|termination_by $vars* => $wf.body)
-
-/-- A complete set of `termination_by` hints, as applicable to a single clique.  -/
-abbrev TerminationWF := Array TerminationBy
-
 /-- A single `decreasing_by` clause -/
 structure DecreasingBy where
   ref       : Syntax

src/Lean/Meta/Tactic/Repeat.lean

@@ -39,7 +39,7 @@ where
         match ← observing? (f g) with
         | some goals' => go n true goals' (goals::stk) acc
         | none => go n p goals stk (acc.push g)
-termination_by n p goals stk _ => (n, stk, goals)
+termination_by n _ goals stk => (n, stk, goals)
 
 /--
 `repeat' f` runs `f` on all of the goals to produce a new list of goals,

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -380,9 +380,10 @@ to true or `pp.notation` is set to false, it will not be called at all.",
 end Delaborator
 
 open SubExpr (Pos PosMap)
-open Delaborator (OptionsPerPos topDownAnalyze)
+open Delaborator (OptionsPerPos topDownAnalyze DelabM)
 
-def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (Term × PosMap Elab.Info) := do
+def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab : DelabM α) :
+  MetaM (α × PosMap Elab.Info) := do
   /- Using `erasePatternAnnotations` here is a bit hackish, but we do it
      `Expr.mdata` affects the delaborator. TODO: should we fix that? -/
   let e ← Meta.erasePatternRefAnnotations e
@@ -414,7 +415,7 @@ def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delabor
 
 /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
 def delab (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Term := do
-  let (stx, _) ← delabCore e optionsPerPos
+  let (stx, _) ← delabCore e optionsPerPos Delaborator.delab
   return stx
 
 builtin_initialize registerTraceClass `PrettyPrinter.delab

tests/lean/decreasing_by.lean.expected.out

@@ -15,20 +15,20 @@ Please use `termination_by` to specify a decreasing measure.
 decreasing_by.lean:81:13-83:3: error: unexpected token 'end'; expected '{' or tactic
 decreasing_by.lean:81:0-81:13: error: unsolved goals
 n m : Nat
-⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1
     { fst := n, snd := dec2 m } { fst := n, snd := m }
 
 n m : Nat
-⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1
     { fst := dec1 n, snd := 100 } { fst := n, snd := m }
 decreasing_by.lean:91:0-91:22: error: unsolved goals
 case a
 n m : Nat
-⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1
     { fst := n, snd := dec2 m } { fst := n, snd := m }
 
 n m : Nat
-⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1
     { fst := dec1 n, snd := 100 } { fst := n, snd := m }
 decreasing_by.lean:99:0-100:22: error: Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
@@ -39,7 +39,7 @@ The arguments relate at each recursive call as follows:
 Please use `termination_by` to specify a decreasing measure.
 decreasing_by.lean:110:0-113:17: error: unsolved goals
 n m : Nat
-⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1
     { fst := dec1 n, snd := 100 } { fst := n, snd := m }
 decreasing_by.lean:121:0-125:17: error: Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:

tests/lean/guessLex.lean.expected.out

@@ -27,7 +27,7 @@ termination_by x1 => sizeOf x1
 Inferred termination argument:
 termination_by n m => (n, sizeOf m)
 Inferred termination argument:
-termination_by m acc => m
+termination_by m => m
 Inferred termination argument:
 termination_by (sizeOf a, 1)
 Inferred termination argument:
@@ -37,13 +37,13 @@ termination_by x2' => x2'
 Inferred termination argument:
 termination_by x2 => x2
 Inferred termination argument:
-termination_by x1 x2 x3 => x2
+termination_by _ x2 => x2
 Inferred termination argument:
 termination_by x1 => sizeOf x1
 Inferred termination argument:
 termination_by x2 => SizeOf.sizeOf x2
 Inferred termination argument:
-termination_by x1 x2 => SizeOf.sizeOf x1
+termination_by x1 => SizeOf.sizeOf x1
 Inferred termination argument:
 termination_by x2 => SizeOf.sizeOf x2
 Inferred termination argument:

tests/lean/guessLexTricky2.lean.expected.out

@@ -1,4 +1,4 @@
 Inferred termination argument:
-termination_by x1 x2 x3 => (x1, x2, 0)
+termination_by x1 x2 => (x1, x2, 0)
 Inferred termination argument:
-termination_by x1 x2 x3 => (x1, x2, 1)
+termination_by x1 x2 => (x1, x2, 1)

tests/lean/issue2260.lean.expected.out

@@ -1,22 +1,9 @@
-issue2260.lean:8:20-8:21: error: The termination argument depends on the function's varying parameters. Try using `sizeOf` explicitly:
-The termination argument has type
-  DNat i : Type
-but is expected to have type
-  ?β : Sort ?u
-issue2260.lean:15:20-15:21: error: The termination argument types differ for the different functions, or depend on the function's varying parameters. Try using `sizeOf` explicitly:
-The termination argument has type
-  DNat i : Type
-but is expected to have type
-  ?β : Sort ?u
-issue2260.lean:31:20-31:21: error: The termination argument types differ for the different functions, or depend on the function's varying parameters. Try using `sizeOf` explicitly:
-The termination argument has type
-  DNat i : Type
-but is expected to have type
-  Nat : Type
-issue2260.lean:26:15-26:21: error: failed to prove termination, possible solutions:
-  - Use `have`-expressions to prove the remaining goals
-  - Use `termination_by` to specify a different well-founded relation
-  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
-n✝ : Nat
-n : DNat n✝
-⊢ sorryAx Nat true < 1 + n✝ + sizeOf n
+issue2260.lean:8:0-8:21: error: The termination argument's type must not depend on the function's varying parameters, but foo's termination argument does:
+  {i : Nat} → DNat i → DNat i
+Try using `sizeOf` explicitly
+issue2260.lean:15:0-15:21: error: The termination argument's type must not depend on the function's varying parameters, but bar1's termination argument does:
+  {i : Nat} → DNat i → DNat i
+Try using `sizeOf` explicitly
+issue2260.lean:31:0-31:21: error: The termination argument's type must not depend on the function's varying parameters, but baz2's termination argument does:
+  {i : Nat} → DNat i → DNat i
+Try using `sizeOf` explicitly

tests/lean/issue2981.lean.expected.out

@@ -3,11 +3,11 @@ Tactic is run (ideally only twice)
 Tactic is run (ideally only twice)
 Tactic is run (ideally only once, in most general context)
 n : Nat
-⊢ (invImage (fun a => a) instWellFoundedRelation).1 n (Nat.succ n)
+⊢ (invImage (fun x => x) instWellFoundedRelation).1 n (Nat.succ n)
 Tactic is run (ideally only twice, in most general context)
 Tactic is run (ideally only twice, in most general context)
 n : Nat
 ⊢ sizeOf n < sizeOf (Nat.succ n)
 n m : Nat
-⊢ (invImage (fun a => PSigma.casesOn a fun x1 snd => x1) instWellFoundedRelation).1 { fst := n, snd := m + 1 }
+⊢ (invImage (fun x => PSigma.casesOn x fun a a_1 => a) instWellFoundedRelation).1 { fst := n, snd := m + 1 }
     { fst := Nat.succ n, snd := m }

tests/lean/mutwftypemismatch.lean.expected.out

@@ -1,14 +1,10 @@
-mutwftypemismatch.lean:11:20-11:25: error: The termination argument types differ for the different functions, or depend on the function's varying parameters. Try using `sizeOf` explicitly:
-The termination argument has type
-  Prop : Type
-but is expected to have type
-  Nat : Type
-mutwftypemismatch.lean:5:10-5:15: error: failed to prove termination, possible solutions:
-  - Use `have`-expressions to prove the remaining goals
-  - Use `termination_by` to specify a different well-founded relation
-  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
-n : Nat
-⊢ sorryAx Nat true < n + 1
-mutwftypemismatch.lean:18:4-18:7: warning: declaration uses 'sorry'
-mutwftypemismatch.lean:18:4-18:7: warning: declaration uses 'sorry'
-mutwftypemismatch.lean:18:4-18:7: warning: declaration uses 'sorry'
+mutwftypemismatch.lean:11:0-11:25: error: The termination arguments of mutually recursive functions must have the same return type, but the termination argument of Ex1.foo has type
+  Nat
+while the termination argument of Ex1.bar has type
+  Prop
+Try using `sizeOf` explicitly
+mutwftypemismatch.lean:26:0-26:44: error: The termination arguments of mutually recursive functions must have the same return type, but the termination argument of Ex2.foo has type
+  Nat
+while the termination argument of Ex2.bar has type
+  Fin fixed
+Try using `sizeOf` explicitly