fix: prevent addPPExplicitToExposeDiff from assigning metavariables (…

…#5276)

Type mismatch errors have a nice feature where expressions are annotated
with `pp.explicit` to expose differences via `isDefEq` checking.
However, this procedure has side effects since `isDefEq` may assign
metavariables. This PR wraps the procedure with `withoutModifyingState`
to prevent assignments from escaping.

Assignments can lead to confusing behavior. For example, in the
following a higher-order unification fails, but the difference-finding
procedure unifies metavariables in a naive way, producing a baffling
error message:
```lean
theorem test {f g : Nat → Nat} (n : Nat) (hfg : ∀a, f (g a) = a) :
    f (g n) = n := hfg n

example {g2 : ℕ → ℕ} (n2 : ℕ) : (λx => x * 2) (g2 n2) = n2 := by
  with_reducible refine test n2 ?_
  /-
  type mismatch
    test n2 ?m.648
  has type
    (fun x ↦ x * 2) (g2 n2) = n2 : Prop
  but is expected to have type
    (fun x ↦ x * 2) (g2 n2) = n2 : Prop
  -/
```
With the change, it now says `has type ?m.153 (?m.154 n2) = n2`.

Note: this uses `withoutModifyingState` instead of `withNewMCtxDepth`
because we want to know something about where `isDefEq` failed — we are
trying to simulate a very basic version of `isDefEq` for function
applications, and we want the state at the point of failure to know
which argument is "at fault".

src/Lean/Meta/Check.lean

@@ -74,44 +74,69 @@ partial def addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr) := do
   if (← getOptions).getBool `pp.all false || (← getOptions).getBool `pp.explicit false then
     return (a, b)
   else
-    visit (← instantiateMVars a) (← instantiateMVars b)
+    -- We want to be able to assign metavariables to work out what why `isDefEq` failed,
+    -- but we don't want these assignments to leak out of the function.
+    -- Note: we shouldn't instantiate mvars in `visit` to prevent leakage.
+    withoutModifyingState do
+      visit (← instantiateMVars a) (← instantiateMVars b)
 where
   visit (a b : Expr) : MetaM (Expr × Expr) := do
     try
-      if !a.isApp || !b.isApp then
-        return (a, b)
-      else if a.getAppNumArgs != b.getAppNumArgs then
-        return (a, b)
-      else if !(← isDefEq a.getAppFn b.getAppFn) then
-        return (a, b)
-      else
-        let fType ← inferType a.getAppFn
-        forallBoundedTelescope fType a.getAppNumArgs fun xs _ => do
+      match a, b with
+      | .mdata _ a', _ =>
+        let (a', b) ← visit a' b
+        return (a.updateMData! a', b)
+      | _, .mdata _ b' =>
+        let (a, b') ← visit a b'
+        return (a, b.updateMData! b')
+      | .app .., .app .. =>
+        if a.getAppNumArgs != b.getAppNumArgs then
+          return (a, b)
+        else if a.getAppFn'.isMVar || b.getAppFn'.isMVar then
+          -- This is a failed higher-order unification. Do not proceed to `isDefEq`.
+          return (a, b)
+        else if !(← isDefEq a.getAppFn b.getAppFn) then
+          let (fa, fb) ← visit a.getAppFn b.getAppFn
+          return (mkAppN fa a.getAppArgs, mkAppN fb b.getAppArgs)
+        else
+          -- The function might be "overapplied", so we can't use `forallBoundedTelescope`.
+          -- That is to say, the arity might depend on the values of the arguments.
+          -- We look for the first explicit argument that is different.
+          -- Otherwise we look for the first implicit argument.
+          -- We try `isDefEq` on all arguments to get discretionary mvar assigments.
           let mut as := a.getAppArgs
           let mut bs := b.getAppArgs
-          if let some (as', bs') ← hasExplicitDiff? xs as bs then
-            return (mkAppN a.getAppFn as', mkAppN b.getAppFn bs')
+          let mut aFnType ← inferType a.getAppFn
+          let mut bFnType ← inferType b.getAppFn
+          let mut firstExplicitDiff? := none
+          let mut firstImplicitDiff? := none
+          for i in [0:as.size] do
+            unless aFnType.isForall do aFnType ← withTransparency .all <| whnf aFnType
+            unless bFnType.isForall do bFnType ← withTransparency .all <| whnf bFnType
+            -- These pattern matches are expected to succeed:
+            let .forallE _ _ abody abi := aFnType | return (a, b)
+            let .forallE _ _ bbody bbi := bFnType | return (a, b)
+            aFnType := abody.instantiate1 as[i]!
+            bFnType := bbody.instantiate1 bs[i]!
+            unless (← isDefEq as[i]! bs[i]!) do
+              if abi.isExplicit && bbi.isExplicit then
+                firstExplicitDiff? := firstExplicitDiff? <|> some i
+              else
+                firstImplicitDiff? := firstImplicitDiff? <|> some i
+          if let some i := firstExplicitDiff? <|> firstImplicitDiff? then
+            let (ai, bi) ← visit as[i]! bs[i]!
+            as := as.set! i ai
+            bs := bs.set! i bi
+          let a := mkAppN a.getAppFn as
+          let b := mkAppN b.getAppFn bs
+          if firstExplicitDiff?.isSome then
+            return (a, b)
           else
-            for i in [:as.size] do
-              unless (← isDefEq as[i]! bs[i]!) do
-                let (ai, bi) ← visit as[i]! bs[i]!
-                as := as.set! i ai
-                bs := bs.set! i bi
-            let a := mkAppN a.getAppFn as
-            let b := mkAppN b.getAppFn bs
-            return (a.setAppPPExplicit, b.setAppPPExplicit)
+            return (a.setPPExplicit true, b.setPPExplicit true)
+      | _, _ => return (a, b)
     catch _ =>
       return (a, b)
 
-  hasExplicitDiff? (xs as bs : Array Expr) : MetaM (Option (Array Expr × Array Expr)) := do
-    for i in [:xs.size] do
-      let localDecl ← xs[i]!.fvarId!.getDecl
-      if localDecl.binderInfo.isExplicit then
-         unless (← isDefEq as[i]! bs[i]!) do
-           let (ai, bi) ← visit as[i]! bs[i]!
-           return some (as.set! i ai, bs.set! i bi)
-    return none
-
 /--
   Return error message "has type{givenType}\nbut is expected to have type{expectedType}"
 -/

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -58,8 +58,8 @@ a : α
           • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
             • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
           • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.636 -> _uniq.312
-          • FVarAlias α: _uniq.635 -> _uniq.310
+          • FVarAlias a: _uniq.632 -> _uniq.312
+          • FVarAlias α: _uniq.631 -> _uniq.310
           • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
           • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
           • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -73,8 +73,8 @@ a : α
           • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
             • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
           • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.667 -> _uniq.312
-          • FVarAlias n: _uniq.666 -> _uniq.310
+          • FVarAlias a: _uniq.663 -> _uniq.312
+          • FVarAlias n: _uniq.662 -> _uniq.310
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
             • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
             • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩

tests/lean/1870.lean.expected.out

@@ -1,7 +1,7 @@
 1870.lean:12:2-12:35: error: type mismatch
-  congrArg (@OfNat.ofNat Nat 0) (congrArg (@Zero.toOfNat0 Nat) ?_)
+  congrArg ?_ (congrArg ?_ ?_)
 has type
-  OfNat.ofNat 0 = OfNat.ofNat 0 : Prop
+  ?_ (?_ ?_) = ?_ (?_ ?_) : Prop
 but is expected to have type
   OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
 1870.lean:16:2-16:16: error: tactic 'apply' failed, failed to unify

tests/lean/run/4405.lean

@@ -1,31 +1,33 @@
 import Lean.Elab.Command
 
+set_option pp.mvars false
+
 /--
 error: application type mismatch
-  ⟨Nat.lt_irrefl ↑(?m.58 n), Fin.is_lt (?m.58 n)⟩
+  ⟨Nat.lt_irrefl ↑(?_ n), Fin.is_lt (?_ n)⟩
 argument
-  Fin.is_lt (?m.58 n)
+  Fin.is_lt (?_ n)
 has type
-  ↑(?m.58 n) < ?m.57 n : Prop
+  ↑(?_ n) < ?_ n : Prop
 but is expected to have type
-  ↑(?m.58 n) < ↑(?m.58 n) : Prop
+  ↑(?_ n) < ↑(?_ n) : Prop
 -/
 #guard_msgs in
 def foo := fun n => (not_and_self_iff _).mp ⟨Nat.lt_irrefl _, Fin.is_lt _⟩
 
 /--
 error: type mismatch
-  Fin.is_lt ?m.185
+  Fin.is_lt ?_
 has type
-  ↑?m.185 < ?m.184 : Prop
+  ↑?_ < ?_ : Prop
 but is expected to have type
-  ?a < ?a : Prop
+  ?_ < ?_ : Prop
 ---
 error: unsolved goals
 case a
 ⊢ Nat
 
-this : ?a < ?a
+this : ?_ < ?_
 ⊢ True
 -/
 #guard_msgs in

tests/lean/run/addPPExplicitToExposeDiff.lean

@@ -0,0 +1,65 @@
+/-!
+# Tests of `addPPExplicitToExposeDiff`
+-/
+set_option pp.mvars false
+
+/-!
+Basic example.
+-/
+/--
+error: type mismatch
+  rfl
+has type
+  ?_ = ?_ : Prop
+but is expected to have type
+  1 = 2 : Prop
+-/
+#guard_msgs in example : 1 = 2 := by
+  exact rfl
+
+
+/-!
+Error message shouldn't fake a higher-order unification. This next one used to give
+```
+  type mismatch
+    test n2 ?_
+  has type
+    (fun x ↦ x * 2) (g2 n2) = n2 : Prop
+  but is expected to have type
+    (fun x ↦ x * 2) (g2 n2) = n2 : Prop
+```
+It now doesn't for the stronger reason that we don't let `addPPExplicitToExposeDiff` have side effects,
+but still it avoids doing incorrect higher-order unifications in its reasoning.
+-/
+
+theorem test {f g : Nat → Nat} (n : Nat) (hfg : ∀ a, f (g a) = a) :
+    f (g n) = n := hfg n
+
+/--
+error: type mismatch
+  test n2 ?_
+has type
+  ?_ (?_ n2) = n2 : Prop
+but is expected to have type
+  (fun x => x * 2) (g2 n2) = n2 : Prop
+-/
+#guard_msgs in
+example {g2 : Nat → Nat} (n2 : Nat) : (fun x => x * 2) (g2 n2) = n2 := by
+  with_reducible refine test n2 ?_
+
+
+/-!
+Exposes an implicit argument because the explicit arguments can be unified.
+-/
+def f {a : Nat} (b : Nat) : Prop := a + b = 0
+/--
+error: type mismatch
+  sorry
+has type
+  @f 0 ?_ : Prop
+but is expected to have type
+  @f 1 2 : Prop
+-/
+#guard_msgs in
+example : @f 1 2 := by
+  exact (sorry : @f 0 _)