feat: improve termination_by error messages (#3255)

as suggested in

<https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/termination_by.20regression/near/419786430>

Also refactored the code a bit and removed the code smell around
`GuessLex`-produced termination arguments (which may not be
surface-syntactically expressible) a bit by introducing an explicit flag
for those.

(cherry picked from commit f40c999)

src/Lean/Elab/LetRec.lean

@@ -97,7 +97,7 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array
 
   let toLift ← views.mapIdxM fun i view => do
     let value := values[i]!
-    let termination ← view.termination.checkVars view.binderIds.size value
+    let termination := view.termination.rememberExtraParams view.binderIds.size value
     pure {
       ref            := view.ref
       fvarId         := fvars[i]!.fvarId!

src/Lean/Elab/MutualDef.lean

@@ -642,7 +642,7 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea
   mainHeaders.size.foldM (init := preDefs) fun i preDefs => do
     let header := mainHeaders[i]!
     let termination ← declValToTerminationHint header.valueStx
-    let termination ← termination.checkVars header.numParams mainVals[i]!
+    let termination := termination.rememberExtraParams header.numParams mainVals[i]!
     let value ← mkLambdaFVars sectionVars mainVals[i]!
     let type ← mkForallFVars sectionVars header.type
     return preDefs.push {

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

@@ -575,7 +575,7 @@ def buildTermWF (originalVarNamess : Array (Array Name)) (varNamess : Array (Arr
           `($sizeOfIdent $v)
       | .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
     let body ← mkTupleSyntax measureStxs
-    return { ref := .missing, vars := idents, body }
+    return { ref := .missing, vars := idents, body, synthetic := true }
 
 /--
 The TerminationWF produced by GuessLex may mention more variables than allowed in the surface
@@ -585,8 +585,9 @@ The latter works fine in many cases, and is still useful to the user in the tric
 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] }
+  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.

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

@@ -92,7 +92,6 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
     let unaryPreDefs ← packDomain fixedPrefixSize preDefsDIte
     return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize)
 
-  let extraParamss := preDefs.map (·.termination.extraParams)
   let wf ← do
     let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.termination_by?.isSome)
     if preDefsWith.isEmpty then
@@ -110,7 +109,7 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do
     let type ← whnfForall type
     let packedArgType := type.bindingDomain!
-    elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType extraParamss wf fun wfRel => do
+    elabWFRel preDefs unaryPreDef.declName fixedPrefixSize 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

@@ -24,16 +24,15 @@ private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarI
   go 0 mvarId fvarId #[]
 
 private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mvarId : MVarId)
-    (fvarId : FVarId) (extraParams : Nat) (element : TerminationBy) : TermElabM MVarId := do
-  -- If elements.vars is ≤ extraParams, this is user-provided, and should be interpreted
+    (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.vars.size < extraParams then extraParams - element.vars.size else 0
+    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
-    if element.vars.size > varNames.size then
-      throwErrorAt element.vars[varNames.size]! "too many variable names"
     for h : i in [:element.vars.size] do
       let varStx := element.vars[i]
       if let `($ident:ident) := varStx then
@@ -55,8 +54,7 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
   go 0 mvarId fvarId
 
 def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat)
-    (argType : Expr) (extraParamss : Array Nat) (wf : TerminationWF) (k : Expr → TermElabM α) :
-    TermElabM α := do
+    (argType : Expr) (wf : TerminationWF) (k : Expr → TermElabM α) : TermElabM α := do
   let α := argType
   let u ← getLevel α
   let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α
@@ -66,8 +64,8 @@ def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPre
     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, extraParams in extraParamss, element in wf, preDef in preDefs do
-      let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d extraParams element
+    for (d, mvarId) in subgoals, element in wf, preDef in preDefs do
+      let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
       mvarId.withContext do
         let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
         mvarId.assign value

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

@@ -16,6 +16,13 @@ structure TerminationBy where
   ref       : Syntax
   vars      : TSyntaxArray [`ident, ``Lean.Parser.Term.hole]
   body      : Term
+  /--
+  If `synthetic := true`, then this `termination_by` clause was
+  generated by `GuessLex`, and `vars` refers to *all* parameters
+  of the function, not just the “extra parameters”.
+  Cf. Lean.Elab.WF.unpackUnary
+  -/
+  synthetic : Bool := false
   deriving Inhabited
 
 open Parser.Termination in
@@ -44,14 +51,13 @@ structure TerminationHints where
   ref : Syntax
   termination_by? : Option TerminationBy
   decreasing_by?  : Option DecreasingBy
-  /-- Here we record the number of parameters past the `:`. This is
-  * `GuessLex` when there is no `termination_by` annotation, so that
-     we can print the guessed order in the right form.
-  * If there are fewer variables in the `termination_by` annotation than there are extra
-    parameters, we know which parameters they should apply to.
+  /-- Here we record the number of parameters past the `:`. It is set by
+  `TerminationHints.rememberExtraParams` and used as folows:
 
-  It it set in `TerminationHints.checkVars`, which is the place where we also check that the user
-  does not bind more extra parameters than present in the predefinition.
+  * When we guess the termination argument in `GuessLex` and want to print it in surface-syntax
+    compatible form.
+  * If there are fewer variables in the `termination_by` annotation than there are extra
+    parameters, we know which parameters they should apply to (`TerminationBy.checkVars`).
   -/
   extraParams : Nat
   deriving Inhabited
@@ -70,19 +76,31 @@ def TerminationHints.ensureNone (hints : TerminationHints) (reason : String): Co
     logErrorAt hints.ref m!"unused termination hints, function is {reason}"
 
 /--
-Checks that `termination_by` binds at most as many variables are present in the outermost
-lambda of `value`, and logs (without failing) appropriate errors.
+Remembers `extraParams` for later use. Needs to happen early enough where we still know
+how many parameters came from the function header (`headerParams`).
+-/
+def TerminationHints.rememberExtraParams (headerParams : Nat) (hints : TerminationHints)
+    (value : Expr) : TerminationHints :=
+  { hints with extraParams := value.getNumHeadLambdas - headerParams }
 
-Also remembers `extraParams` for later use.
+/--
+Checks that `termination_by` binds at most as many variables are present in the outermost
+lambda of `value`, and throws appropriate errors.
 -/
-def TerminationHints.checkVars (headerParams : Nat) (hints : TerminationHints) (value : Expr) :
-    MetaM TerminationHints := do
-  let extraParams := value.getNumHeadLambdas - headerParams
-  if let .some tb := hints.termination_by? then
+def TerminationBy.checkVars (funName : Name) (extraParams : Nat) (tb : TerminationBy) : MetaM Unit := do
+  unless tb.synthetic do
     if tb.vars.size > extraParams then
-      logErrorAt tb.ref <| m!"Too many extra parameters bound; the function definition only " ++
-        m!"has {extraParams} extra parameters."
-  return { hints with extraParams := extraParams }
+      let mut msg := m!"{parameters tb.vars.size} bound in `termination_by`, but the body of " ++
+        m!"{funName} only binds {parameters extraParams}."
+      if let `($ident:ident) := tb.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 tb.ref msg
+  where
+    parameters : Nat → MessageData
+    | 1 => "one parameter"
+    | n => m!"{n} parameters"
 
 open Parser.Termination
 

tests/lean/decreasing_by.lean

@@ -77,7 +77,7 @@ end Ex4
 namespace Ex5
 -- Empty proof. Produces parse error and unsolved goals.
 def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
-termination_by n m => (n, m)
+termination_by (n, m)
 decreasing_by -- Error
 
 end Ex5

tests/lean/interactive/hover.lean

@@ -188,7 +188,7 @@ example : Nat → Nat → Nat := by
       --^ textDocument/hover
 
 def g (n : Nat) : Nat := g 0
-termination_by n => n
+termination_by n
 decreasing_by have n' := n; admit
                        --^ textDocument/hover
 

tests/lean/termination_by_vars.lean

@@ -117,3 +117,19 @@ def foo6 (v : Nat) := 5
     decreasing_by apply dec1_lt
 
 end InLetRec
+
+namespace ManyTooMany
+
+def tooManyVars (n : Nat) : Nat := tooManyVars (dec1 n)
+  termination_by x y z => x -- Error
+  decreasing_by apply dec1_lt
+
+end ManyTooMany
+
+namespace WithHelpfulComment
+
+def foo (n : Nat) : Nat := foo (dec1 n)
+  termination_by foo n => n -- Error
+  decreasing_by apply dec1_lt
+
+end WithHelpfulComment

tests/lean/termination_by_vars.lean.expected.out

@@ -1,7 +1,9 @@
-termination_by_vars.lean:14:2-14:23: error: Too many extra parameters bound; the function definition only has 0 extra parameters.
+termination_by_vars.lean:14:2-14:23: error: one parameter bound in `termination_by`, but the body of Basic.tooManyVars only binds 0 parameters.
 termination_by_vars.lean:23:2-23:21: error: no extra parameters bounds, please omit the `=>`
-termination_by_vars.lean:39:2-39:27: error: Too many extra parameters bound; the function definition only has 2 extra parameters.
-termination_by_vars.lean:49:2-49:23: error: Too many extra parameters bound; the function definition only has 0 extra parameters.
+termination_by_vars.lean:39:2-39:27: error: 3 parameters bound in `termination_by`, but the body of Basic.tooManyVariables2 only binds 2 parameters.
+termination_by_vars.lean:49:2-49:23: error: one parameter bound in `termination_by`, but the body of WithVariable.tooManyVars only binds 0 parameters.
 termination_by_vars.lean:58:2-58:21: error: no extra parameters bounds, please omit the `=>`
-termination_by_vars.lean:83:4-83:25: error: Too many extra parameters bound; the function definition only has 0 extra parameters.
+termination_by_vars.lean:83:4-83:25: error: one parameter bound in `termination_by`, but the body of InLetRec.foo1.tooManyVars only binds 0 parameters.
 termination_by_vars.lean:95:4-95:23: error: no extra parameters bounds, please omit the `=>`
+termination_by_vars.lean:124:2-124:27: error: 3 parameters bound in `termination_by`, but the body of ManyTooMany.tooManyVars only binds 0 parameters.
+termination_by_vars.lean:132:2-132:27: error: 2 parameters bound in `termination_by`, but the body of WithHelpfulComment.foo only binds 0 parameters. (Since Lean v4.6.0, the `termination_by` clause no longer expects the function name here.)