feat: WF/Fix.lean: only refine fix’s ih for atomic discriminant onlys (#7324)

This PR changes the internal construction of well-founded recursion, to
not change the type of `fix`’s induction hypothesis in non-defeq ways.

Fixes #7322 and hopefully unblocks #7166.

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

@@ -17,6 +17,11 @@ import Lean.Util.HasConstCache
 namespace Lean.Elab.WF
 open Meta
 
+register_builtin_option debug.definition.wf.replaceRecApps : Bool := {
+    defValue := false
+    descr    := "Type check every step of the well-founded definition translation"
+  }
+
 /-
 Creates a subgoal for a recursive call, as an unsolved `MVar`. The goal is cleaned up, and
 the current syntax reference is stored in the `MVar`’s type as a `RecApp` marker, for
@@ -32,11 +37,13 @@ private def mkDecreasingProof (decreasingProp : Expr) : TermElabM Expr := do
 
 private partial def replaceRecApps (recFnName : Name) (fixedPrefixSize : Nat) (F : Expr) (e : Expr) : TermElabM Expr := do
   trace[Elab.definition.wf] "replaceRecApps:{indentExpr e}"
-  trace[Elab.definition.wf] "{F} : {← inferType F}"
-  loop F e |>.run' {}
+  trace[Elab.definition.wf] "type of functorial {F} is{indentExpr (← inferType F)}"
+  let e ← loop F e |>.run' {}
+  return e
 where
   processRec (F : Expr) (e : Expr) : StateRefT (HasConstCache #[recFnName]) TermElabM Expr := do
     if e.getAppNumArgs < fixedPrefixSize + 1 then
+      trace[Elab.definition.wf] "replaceRecApp: eta-expanding{indentExpr e}"
       loop F (← etaExpand e)
     else
       let args := e.getAppArgs
@@ -55,6 +62,19 @@ where
     modifyGet (·.contains e)
 
   loop (F : Expr) (e : Expr) : StateRefT (HasConstCache #[recFnName]) TermElabM Expr := do
+    let e' ← loopGo F e
+    if (debug.definition.wf.replaceRecApps.get (← getOptions)) then
+      withTransparency .all do withNewMCtxDepth do
+        unless (← isTypeCorrect e') do
+          throwError "Type error introduced when transforming{indentExpr e}\nto{indentExpr e'}"
+        let t1 ← inferType e
+        let t2 ← inferType e'
+        unless (← isDefEq t1 t2) do
+          let (t1, t2) ← addPPExplicitToExposeDiff t1 t2
+          throwError "Type not preserved transforming{indentExpr e}\nto{indentExpr e'}\nType was{indentExpr t1}\nand now is{indentExpr t2}"
+    return e'
+
+  loopGo (F : Expr) (e : Expr) : StateRefT (HasConstCache #[recFnName]) TermElabM Expr := do
     if !(← containsRecFn e) then
       return e
     match e with
@@ -83,7 +103,8 @@ where
               unless xs.size = numParams do
                 throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
               let FAlt := xs[numParams - 1]!
-              mkLambdaFVars xs (← loop FAlt altBody)
+              let altBody' ← loop FAlt altBody
+              mkLambdaFVars xs altBody'
           return { matcherApp with alts := altsNew, discrs := (← matcherApp.discrs.mapM (loop F)) }.toExpr
         else
           processApp F e

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -37,21 +37,27 @@ private partial def updateAlts (unrefinedArgType : Expr) (typeNew : Expr) (altNu
     else
       throwError "failed to add argument to matcher application, argument type was not refined by `casesOn`"
 
-/-- 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
-  - expression `e : B[discrs]`,
-  Construct the term
-  `match_i As (fun xs => B[xs] -> motive[xs]) discrs (fun ys_1 (y : B[C_1[ys_1]]) => alt_1) ... (fun ys_n (y : B[C_n[ys_n]]) => alt_n) e remaining`.
+/--
+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
+- expression `e : B[discrs]`,
+Construct the term
+`match_i As (fun xs => B[xs] -> motive[xs]) discrs (fun ys_1 (y : B[C_1[ys_1]]) => alt_1) ... (fun ys_n (y : B[C_n[ys_n]]) => alt_n) e remaining`.
 
-  We use `kabstract` to abstract the discriminants from `B[discrs]`.
+We only abstract discriminants that are fvars.  We used to use `kabstract` to abstract all
+discriminants from `B[discrs]`, but that changes the type of the arg in ways that make it no
+longer compatible with the original recursive function (issue #7322).
 
-  This method assumes
-  - the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size`
-  - each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]`
+If this is still not great, then we could try to use `kabstract`, but only on the last paramter
+of the `arg` (the termination proof obligation).
 
-  This is used in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to
-  the argument provided by `fix` to refine type of the local variable used for recursive calls,
-  which may mention `major`. See there for how to use this function.
+This method assumes
+- the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size`
+- each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]`
+
+This is used in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to
+the argument provided by `fix` to refine type of the local variable used for recursive calls,
+which may mention `major`. See there for how to use this function.
 -/
 def addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp :=
   lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do
@@ -59,11 +65,13 @@ def addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp :=
       -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`.
       throwError "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments"
     let eType ← inferType e
-    let eTypeAbst ← matcherApp.discrs.size.foldRevM (init := eType) fun i _ eTypeAbst => do
-      let motiveArg := motiveArgs[i]!
+    let eTypeAbst := matcherApp.discrs.size.foldRev (init := eType) fun i _ eTypeAbst =>
       let discr     := matcherApp.discrs[i]
-      let eTypeAbst ← kabstract eTypeAbst discr
-      return eTypeAbst.instantiate1 motiveArg
+      if discr.isFVar then
+        let motiveArg := motiveArgs[i]!
+        eTypeAbst.replaceFVar discr motiveArg
+      else
+        eTypeAbst
     let motiveBody ← mkArrow eTypeAbst motiveBody
     let matcherLevels ← match matcherApp.uElimPos? with
       | none     => pure matcherApp.matcherLevels

tests/lean/run/issue7322.lean

@@ -0,0 +1,62 @@
+-- set_option trace.Elab.definition.fixedParams true in
+-- set_option debug.skipKernelTC true
+-- set_option debug.definition.wf.replaceRecApps true
+-- set_option trace.Elab.definition.wf true
+set_option pp.proofs true
+
+/-!
+This test case show a tricky issue, originally shown in
+`Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go_denote_eq`
+where type of `fix`’s induction hypothese change when being refined
+in a way that makes the resulting proof term type incorrect.
+-/
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+theorem demo (distance : Nat) (idx : Nat) (a : Fin distance) (fuel : Nat) :
+    a = if hidx : idx < distance then Fin.mk idx hidx else a := by
+  cases fuel
+  · sorry
+  next fuel =>
+    split
+    · rw [demo distance idx a fuel]
+      sorry
+    · rfl
+termination_by fuel
+decreasing_by sorry
+
+structure Ev (p : Prop) : Type where
+  isTrue : p
+
+/--
+warning: declaration uses 'sorry'
+---
+warning: declaration uses 'sorry'
+---
+warning: declaration uses 'sorry'
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+def bar (distance : Nat) (idx : Nat) (a : Fin distance) (fuel : Nat) :
+    Ev (a = if hidx : idx < distance then Fin.mk idx hidx else a) := by
+  cases fuel
+  · sorry
+  next fuel =>
+    split
+    · rw [(bar distance idx a fuel).isTrue]
+      sorry
+    · apply Ev.mk
+      rfl
+termination_by fuel
+decreasing_by sorry
+
+set_option Elab.async false -- for stable message ordering in guard_msgs
+
+/--
+warning: declaration uses 'sorry'
+---
+info: bar.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), (∀ (n : Nat), motive n) → motive x) (fuel : Nat) : motive fuel
+-/
+#guard_msgs in
+#check bar.induct