fix: IndPredBelow should not add auxiliary declarations containing …

…`sorry` (#4563)

Issue #4535 is being affected by a bug in the structural inductive
predicate termination checker (`IndPred.lean`). This module did not
exist in Lean 3, and it is buggy in Lean 4. In the given example, it
introduces an auxiliary declaration containing a `sorry`, and the fails.
This PR ensures this kind of declaration is not added to the
environment.

Closes #4535

TODO: we need a new maintainer for the `IndPred.lean`.

src/Lean/Meta/IndPredBelow.lean

@@ -434,7 +434,7 @@ partial def mkBelowMatcher
   withExistingLocalDecls (lhss.foldl (init := []) fun s v => s ++ v.fvarDecls) do
     for lhs in lhss do
       trace[Meta.IndPredBelow.match] "{lhs.patterns.map (·.toMessageData)}"
-  let res ← Match.mkMatcher { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
+  let res ← Match.mkMatcher (exceptionIfContainsSorry := true) { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
   res.addMatcher
   -- if a wrong index is picked, the resulting matcher can be type-incorrect.
   -- we check here, so that errors can propagate higher up the call stack.

src/Lean/Meta/Match/Match.lean

@@ -830,8 +830,12 @@ Each `AltLHS` has a list of local declarations and a list of patterns.
 The number of patterns must be the same in each `AltLHS`.
 The generated matcher has the structure described at `MatcherInfo`. The motive argument is of the form
 `(motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v)`
-where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition. -/
-def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor input do
+where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition.
+
+If `exceptionIfContainsSorry := true`, then `mkMatcher` throws an exception if the auxiliary
+declarations contains a `sorry`. We use this argument to workaround a bug at `IndPredBelow.mkBelowMatcher`.
+-/
+def mkMatcher (input : MkMatcherInput) (exceptionIfContainsSorry := false) : MetaM MatcherResult := withCleanLCtxFor input do
   let ⟨matcherName, matchType, discrInfos, lhss⟩ := input
   let numDiscrs := discrInfos.size
   let numEqs := getNumEqsFromDiscrInfos discrInfos
@@ -844,6 +848,11 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
   let uElim ← getLevel matchTypeBody
   let uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar
   let mkMatcher (type val : Expr) (minors : Array (Expr × Nat)) (s : State) : MetaM MatcherResult := do
+    let val ← instantiateMVars val
+    let type ← instantiateMVars type
+    if exceptionIfContainsSorry then
+      if type.hasSorry || val.hasSorry then
+        throwError "failed to create auxiliary match declaration `{matcherName}`, it contains `sorry`"
     trace[Meta.Match.debug] "matcher value: {val}\ntype: {type}"
     trace[Meta.Match.debug] "minors num params: {minors.map (·.2)}"
     /- The option `bootstrap.gen_matcher_code` is a helper hack. It is useful, for example,
@@ -857,7 +866,6 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
        | negSucc n => succ n
        ```
        which is defined **before** `Int.decLt` -/
-
     let (matcher, addMatcher) ← mkMatcherAuxDefinition matcherName type val
     trace[Meta.Match.debug] "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
     let uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen