Revert "Playing around with cases not failing with index mismatch"

This reverts commit 9fb68c1.

Author: nomeata

src/Lean/Meta/Match/Match.lean

@@ -513,7 +513,7 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
   let subgoals? ← commitWhenSome? do
      let subgoals ←
        try
-         p.mvarId.cases x.fvarId! (mayLeaveEquations := true)
+         p.mvarId.cases x.fvarId!
        catch ex =>
          if p.alts.isEmpty then
            /- If we have no alternatives and dependent pattern matching fails, then a "missing cases" error is better than a "stuck" error message. -/

src/Lean/Meta/Tactic/Cases.lean

@@ -226,20 +226,19 @@ private def toCasesSubgoals (s : Array InductionSubgoal) (ctorNames : Array Name
     { ctorName           := ctorName,
       toInductionSubgoal := s }
 
-partial def unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst)
-    (caseName? : Option Name := none) (mayFail : Bool := false) : MetaM (Option (MVarId × FVarSubst)) := withIncRecDepth do
+partial def unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (caseName? : Option Name := none): MetaM (Option (MVarId × FVarSubst)) := withIncRecDepth do
   if numEqs == 0 then
     return some (mvarId, subst)
   else
     let (eqFVarId, mvarId) ← mvarId.intro1
-    if let some { mvarId, subst, numNewEqs } ← unifyEq? mvarId eqFVarId subst MVarId.acyclic caseName? (mayFail := mayFail) then
-      unifyEqs? (numEqs - 1 + numNewEqs) mvarId subst caseName? (mayFail := mayFail)
+    if let some { mvarId, subst, numNewEqs } ← unifyEq? mvarId eqFVarId subst MVarId.acyclic caseName? then
+      unifyEqs? (numEqs - 1 + numNewEqs) mvarId subst caseName?
     else
       return none
 
-private def unifyCasesEqs (numEqs : Nat) (subgoals : Array CasesSubgoal) (mayFail := false) : MetaM (Array CasesSubgoal) :=
+private def unifyCasesEqs (numEqs : Nat) (subgoals : Array CasesSubgoal) : MetaM (Array CasesSubgoal) :=
   subgoals.filterMapM fun s => do
-    match (← unifyEqs? numEqs s.mvarId s.subst s.ctorName (mayFail := mayFail)) with
+    match (← unifyEqs? numEqs s.mvarId s.subst s.ctorName) with
     | none                 => pure none
     | some (mvarId, subst) =>
       return some { s with
@@ -259,7 +258,7 @@ private def inductionCasesOn (mvarId : MVarId) (majorFVarId : FVarId) (givenName
   let s ← mvarId.induction majorFVarId casesOn givenNames
   return toCasesSubgoals s ctors majorFVarId us params
 
-def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) (mayLeaveEquations := false) : MetaM (Array CasesSubgoal) := do
+def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) : MetaM (Array CasesSubgoal) := do
   try
     mvarId.withContext do
       mvarId.checkNotAssigned `cases
@@ -278,7 +277,7 @@ def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNam
           trace[Meta.Tactic.cases] "after generalizeIndices\n{MessageData.ofGoal s₁.mvarId}"
           let s₂ ← inductionCasesOn s₁.mvarId s₁.fvarId givenNames ctx
           let s₂ ← elimAuxIndices s₁ s₂
-          unifyCasesEqs s₁.numEqs s₂ (mayFail := mayLeaveEquations)
+          unifyCasesEqs s₁.numEqs s₂
   catch ex =>
     throwNestedTacticEx `cases ex
 
@@ -293,9 +292,8 @@ Apply `casesOn` using the free variable `majorFVarId` as the major premise (aka
   It enables using `Nat.casesAuxOn` instead of `Nat.casesOn`,
   which causes case splits on `n : Nat` to be represented as `0` and `n' + 1` rather than as `Nat.zero` and `Nat.succ n'`.
 -/
-def _root_.Lean.MVarId.cases (mvarId : MVarId) (majorFVarId : FVarId)
-    (givenNames : Array AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) (mayLeaveEquations := false) : MetaM (Array CasesSubgoal) :=
-  Cases.cases mvarId majorFVarId givenNames (useNatCasesAuxOn := useNatCasesAuxOn) (mayLeaveEquations := mayLeaveEquations)
+def _root_.Lean.MVarId.cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) : MetaM (Array CasesSubgoal) :=
+  Cases.cases mvarId majorFVarId givenNames (useNatCasesAuxOn := useNatCasesAuxOn)
 
 /--
 Keep applying `cases` on any hypothesis that satisfies `p`.

src/Lean/Meta/Tactic/UnifyEq.lean

@@ -46,22 +46,13 @@ private def toOffset? (e : Expr) : MetaM (Option (Expr × Nat)) := do
 -/
 def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {})
              (acyclic : MVarId → Expr → MetaM Bool := fun _ _ => return false)
-             (caseName? : Option Name := none) (mayFail : Bool := false)
+             (caseName? : Option Name := none)
              : MetaM (Option UnifyEqResult) := do
    mvarId.withContext do
     let eqDecl ← eqFVarId.getDecl
-    trace[Meta.Tactic.cases] "unifyEq? {mkFVar eqDecl.fvarId} : {eqDecl.type}"
     if eqDecl.type.isHEq then
-      let (varId, mvarId) ← heqToEq mvarId eqDecl.fvarId
-      if varId == eqDecl.fvarId then
-        -- heqToEq failed
-        if mayFail then
-          return some { mvarId, subst }
-        else
-          throwError "Dependent elimination failed: Failed to convert heterogeneous equality{indentExpr eqDecl.type} to homogeneous equality"
-      else
-        let (_, mvarId) ← mvarId.revert #[varId]
-        return some { mvarId, subst, numNewEqs := 1 }
+      let mvarId ← heqToEq' mvarId eqDecl
+      return some { mvarId, subst, numNewEqs := 1 }
     else match eqDecl.type.eq? with
       | none => throwError "Expected an equality, but found{indentExpr eqDecl.type}"
       | some (_, a, b) =>
@@ -86,10 +77,7 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {})
           else if (← acyclic mvarId (mkFVar eqFVarId)) then
             return none -- this alternative has been solved
           else
-            if mayFail then
-              return some { mvarId, subst }
-            else
-              throwError "Dependent elimination failed: Failed to solve equation{indentExpr eqDecl.type}"
+            throwError "Dependent elimination failed: Failed to solve equation{indentExpr eqDecl.type}"
         /- Special support for offset equalities -/
         let injectionOffset? (a b : Expr) := do
           unless (← getEnv).contains ``Nat.elimOffset do return none
@@ -130,12 +118,9 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {})
               let mvarId ←  mvarId.clear eqFVarId
               return some { mvarId, subst, numNewEqs := 1 }
             else
-              if mayFail then
-                return some { mvarId, subst }
-              else
-                match caseName? with
-                | none => throwError "Dependent elimination failed: Failed to solve equation{indentExpr eqDecl.type}"
-                | some caseName => throwError "Dependent elimination failed: Failed to solve equation{indentExpr eqDecl.type}\nat case `{.ofConstName caseName}`"
+              match caseName? with
+              | none => throwError "Dependent elimination failed: Failed to solve equation{indentExpr eqDecl.type}"
+              | some caseName => throwError "Dependent elimination failed: Failed to solve equation{indentExpr eqDecl.type}\nat case `{.ofConstName caseName}`"
         let a ← instantiateMVars a
         let b ← instantiateMVars b
         match a, b with

tests/lean/run/matchOverlapInaccesible.lean

@@ -54,23 +54,19 @@ def parity (n : MyNat) : Parity n := sorry
 -- set_option trace.Meta.Match.match true
 
 /--
-error: Dependent match elimination failed: Could not solve constraints
-  a✝.succ ≋ n✝ + n✝
+error: Tactic `cases` failed with a nested error:
+Dependent elimination failed: Failed to solve equation
+  a✝.succ = n✝.add n✝
+at case `Parity.even` after processing
+  (succ _), _
+the dependent pattern matcher can solve the following kinds of equations
+- <var> = <term> and <term> = <var>
+- <term> = <term> where the terms are definitionally equal
+- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
 -/
 #guard_msgs(pass trace, all) in
 partial def myNatToBinBad (n : MyNat) : List Bool :=
 match n, parity n with
 | zero, _             => []
 | _, Parity.even j => false :: myNatToBinBad j
 | _, Parity.odd  j => true  :: myNatToBinBad j
-
-set_option trace.Meta.Tactic.cases true
-/--
-error: Tactic `cases` failed with a nested error:
-Dependent elimination failed: Failed to solve equation
-  n.succ = n✝.add n✝
-at case `Parity.even`
--/
-#guard_msgs(pass trace, all) in
-example (h : Parity (MyNat.succ n)) : false := by
-  rcases h