refactor: CasesOnApp.refineThrough can return a lambda, not an open t…

…erm (leanprover#2974)

which also removes an error condition at the use site.

While I am at it, I rename a parameter in `GuessLex` that I forgot to
rename earlier.

The effect will be user-visible (in obscure corner cases) with leanprover#2960, so
I’ll have the test there.

A few places would benefit from a `lambdaTelescopeBounded` that
garantees the result has the right length (eta-expanding when
necessary). I’ll look into that separately, and left TODOs here.

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

@@ -92,90 +92,92 @@ abbrev M (recFnName : Name) (α β : Type) : Type :=
 Traverses the given expression `e`, and invokes the continuation `k`
 at every saturated call to `recFnName`.
 
-The expression `scrut` is passed along, and refined when going under a matcher
+The expression `param` is passed along, and refined when going under a matcher
 or `casesOn` application.
 -/
-partial def withRecApps {α} (recFnName : Name) (fixedPrefixSize : Nat) (scrut : Expr) (e : Expr)
+partial def withRecApps {α} (recFnName : Name) (fixedPrefixSize : Nat) (param : Expr) (e : Expr)
     (k : Expr → Array Expr → MetaM α) : MetaM (Array α) := do
   trace[Elab.definition.wf] "withRecApps: {indentExpr e}"
-  let (_, as) ← loop scrut e |>.run #[] |>.run' {}
+  let (_, as) ← loop param e |>.run #[] |>.run' {}
   return as
 where
-  processRec (scrut : Expr) (e : Expr) : M recFnName α Unit := do
+  processRec (param : Expr) (e : Expr) : M recFnName α Unit := do
     if e.getAppNumArgs < fixedPrefixSize + 1 then
-      loop scrut (← etaExpand e)
+      loop param (← etaExpand e)
     else
-      let a ← k scrut e.getAppArgs
+      let a ← k param e.getAppArgs
       modifyThe (Array α) (·.push a)
 
-  processApp (scrut : Expr) (e : Expr) : M recFnName α Unit := do
+  processApp (param : Expr) (e : Expr) : M recFnName α Unit := do
     e.withApp fun f args => do
-      args.forM (loop scrut)
+      args.forM (loop param)
       if f.isConstOf recFnName then
-        processRec scrut e
+        processRec param e
       else
-        loop scrut f
+        loop param f
 
   containsRecFn (e : Expr) : M recFnName α Bool := do
     modifyGetThe (HasConstCache recFnName) (·.contains e)
 
-  loop (scrut : Expr) (e : Expr) : M recFnName α Unit := do
+  loop (param : Expr) (e : Expr) : M recFnName α Unit := do
     if !(← containsRecFn e) then
       return
     match e with
     | Expr.lam n d b c =>
-      loop scrut d
+      loop param d
       withLocalDecl n c d fun x => do
-        loop scrut (b.instantiate1 x)
+        loop param (b.instantiate1 x)
     | Expr.forallE n d b c =>
-      loop scrut d
+      loop param d
       withLocalDecl n c d fun x => do
-        loop scrut (b.instantiate1 x)
+        loop param (b.instantiate1 x)
     | Expr.letE n type val body _ =>
-      loop scrut type
-      loop scrut val
+      loop param type
+      loop param val
       withLetDecl n type val fun x => do
-        loop scrut (body.instantiate1 x)
+        loop param (body.instantiate1 x)
     | Expr.mdata _d b =>
       if let some stx := getRecAppSyntax? e then
-        withRef stx <| loop scrut b
+        withRef stx <| loop param b
       else
-        loop scrut b
-    | Expr.proj _n _i e => loop scrut e
-    | Expr.const .. => if e.isConstOf recFnName then processRec scrut e
+        loop param b
+    | Expr.proj _n _i e => loop param e
+    | Expr.const .. => if e.isConstOf recFnName then processRec param e
     | Expr.app .. =>
       match (← matchMatcherApp? e) with
       | some matcherApp =>
         if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
-          processApp scrut e
+          processApp param e
         else
-          if let some altScruts ← matcherApp.refineThrough? scrut then
-            (Array.zip matcherApp.alts (Array.zip matcherApp.altNumParams altScruts)).forM
-              fun (alt, altNumParam, altScrut) =>
-                lambdaTelescope alt fun xs altBody => do
-                  unless altNumParam ≤ xs.size do
-                    throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
-                  let altScrut := altScrut.instantiateRev xs[:altNumParam]
-                  loop altScrut altBody
+          if let some altParams ← matcherApp.refineThrough? param then
+            (Array.zip matcherApp.alts (Array.zip matcherApp.altNumParams altParams)).forM
+              fun (alt, altNumParam, altParam) =>
+                lambdaTelescope altParam fun xs altParam => do
+                  -- TODO: Use boundedLambdaTelescope
+                  unless altNumParam = xs.size do
+                    throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}"
+                  let altBody := alt.beta xs
+                  loop altParam altBody
           else
-            processApp scrut e
+            processApp param e
       | none =>
       match (← toCasesOnApp? e) with
       | some casesOnApp =>
         if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
-          processApp scrut e
+          processApp param e
         else
-          if let some altScruts ← casesOnApp.refineThrough? scrut then
-          (Array.zip casesOnApp.alts (Array.zip casesOnApp.altNumParams altScruts)).forM
-            fun (alt, altNumParam, altScrut) =>
-              lambdaTelescope alt fun xs altBody => do
-                unless altNumParam ≤ xs.size do
+          if let some altParams ← casesOnApp.refineThrough? param then
+          (Array.zip casesOnApp.alts (Array.zip casesOnApp.altNumParams altParams)).forM
+            fun (alt, altNumParam, altParam) =>
+              lambdaTelescope altParam fun xs altParam => do
+                -- TODO: Use boundedLambdaTelescope
+                unless altNumParam = xs.size do
                   throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}"
-                let altScrut := altScrut.instantiateRev xs[:altNumParam]
-                loop altScrut altBody
+                let altBody := alt.beta xs
+                loop altParam altBody
           else
-            processApp scrut e
-      | none => processApp scrut e
+            processApp param e
+      | none => processApp param e
     | e => do
       let _ ← ensureNoRecFn recFnName e
 

src/Lean/Meta/CasesOn.lean

@@ -124,18 +124,14 @@ def CasesOnApp.addArg? (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := f
   casesOn As (fun is x => motive[is, xs]) is major  (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining
   ```
   and an expression `B[is, major]` (which may not be a type, e.g. `n : Nat`)
-  for every alternative `i`, construct the type `B[_, C_i[ys_i]]`
-  with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `CasesOnApp.altNumParams`.
+  for every alternative `i`, construct the expression `fun ys_i => B[_, C_i[ys_i]]`
 
   This is similar to `CasesOnApp.addArg` when you only have an expression to
   refined, and not a type with a value.
 
   This is used in in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive
   calls to refine the functions' paramter, which may mention `major`.
   See there for how to use this function.
-
-  It returns an open term, rather than following the idiom of applying a continuation,
-  so that `CasesOn.refineThrough?` can reliably recognize failure from within this function.
 -/
 def CasesOnApp.refineThrough (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) :=
   lambdaTelescope c.motive fun motiveArgs _motiveBody => do
@@ -163,13 +159,13 @@ def CasesOnApp.refineThrough (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) :=
     forallTelescope auxType fun altAuxs _ => do
       let altAuxTys ← altAuxs.mapM (inferType ·)
       (Array.zip c.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do
-        forallTelescope altAuxTy fun fvs body => do
+        forallBoundedTelescope altAuxTy altNumParams fun fvs body => do
           unless fvs.size = altNumParams do
-            throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments"
+            throwError "failed to transfer argument through `casesOn` application, alt type must be telescope with #{altNumParams} arguments"
           -- extract type from our synthetic equality
           let body := body.getArg! 2
           -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out
-          Expr.abstractM body fvs
+          mkLambdaFVars fvs body
 
 /-- A non-failing version of `CasesOnApp.refineThrough` -/
 def CasesOnApp.refineThrough? (c : CasesOnApp) (e : Expr) :

src/Lean/Meta/Match/Match.lean

@@ -967,9 +967,8 @@ def MatcherApp.addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option Matc
 
 /-- Given
   - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and
-  - a type `B[discrs]` (which may not be a type, e.g. `n : Nat`),
-  returns the types `B[C_1[ys_1]] ... B[C_n[ys_n]]`,
-  with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `matcherApp.altNumParams`.
+  - a expression `B[discrs]` (which may not be a type, e.g. `n : Nat`),
+  returns the expressions `fun ys_1 ... ys_i => B[C_1[ys_1]] ... B[C_n[ys_n]]`,
 
   This method assumes
   - the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size`
@@ -981,9 +980,6 @@ def MatcherApp.addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option Matc
   This is used in in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive
   calls to refine the functions' paramter, which may mention `major`.
   See there for how to use this function.
-
-  It returns an open term, rather than following the idiom of applying a continuation,
-  so that `MatcherApp.refineThrough?` can reliably recognize failure from within this function
 -/
 def MatcherApp.refineThrough (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr) :=
   lambdaTelescope matcherApp.motive fun motiveArgs _motiveBody => do
@@ -1015,13 +1011,13 @@ def MatcherApp.refineThrough (matcherApp : MatcherApp) (e : Expr) : MetaM (Array
     forallTelescope auxType fun altAuxs _ => do
       let altAuxTys ← altAuxs.mapM (inferType ·)
       (Array.zip matcherApp.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do
-        forallTelescope altAuxTy fun fvs body => do
+        forallBoundedTelescope altAuxTy altNumParams fun fvs body => do
           unless fvs.size = altNumParams do
             throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments"
           -- extract type from our synthetic equality
           let body := body.getArg! 2
           -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out
-          Expr.abstractM body fvs
+          mkLambdaFVars fvs body
 
 /-- A non-failing version of `MatcherApp.refineThrough` -/
 def MatcherApp.refineThrough? (matcherApp : MatcherApp) (e : Expr) :