fix: type occurs check bug (#6128)

This PR does the same fix as #6104, but such that it doesn't break the
test/the file in `Plausible`. This is done by not creating unused let
binders in metavariable types that are made by `elimMVar`. (This is also
a positive thing for users looking at metavariable types, for example in
error messages)

We get rid of `skipAtMostNumBinders`. This function was originally
defined for the purpose of making this test work, but it is a hack
because it allows cycles in the metavariable context.

It would make sense to split these changes into 2 PRs, but I combined
them here to show that the combination of them closes #6013 without
breaking anything

Closes #6013

src/Lean/Meta/ExprDefEq.lean

@@ -939,29 +939,6 @@ def check (hasCtxLocals : Bool) (mctx : MetavarContext) (lctx : LocalContext) (m
 
 end CheckAssignmentQuick
 
-/--
-Auxiliary function used at `typeOccursCheckImp`.
-Given `type`, it tries to eliminate "dependencies". For example, suppose we are trying to
-perform the assignment `?m := f (?n a b)` where
-```
-?n : let k := g ?m; A -> h k ?m -> C
-```
-If we just perform occurs check `?m` at the type of `?n`, we get a failure, but
-we claim these occurrences are ok because the type `?n a b : C`.
-In the example above, `typeOccursCheckImp` invokes this function with `n := 2`.
-Note that we avoid using `whnf` and `inferType` at `typeOccursCheckImp` to minimize the
-performance impact of this extra check.
-
-See test `typeOccursCheckIssue.lean` for an example where this refinement is needed.
-The test is derived from a Mathlib file.
--/
-private partial def skipAtMostNumBinders (type : Expr) (n : Nat) : Expr :=
-  match type, n with
-  | .forallE _ _ b _, n+1 => skipAtMostNumBinders b n
-  | .mdata _ b,       n   => skipAtMostNumBinders b n
-  | .letE _ _ v b _,  n   => skipAtMostNumBinders (b.instantiate1 v) n
-  | type,             _   => type
-
 /-- `typeOccursCheck` implementation using unsafe (i.e., pointer equality) features. -/
 private unsafe def typeOccursCheckImp (mctx : MetavarContext) (mvarId : MVarId) (v : Expr) : Bool :=
   if v.hasExprMVar then
@@ -982,19 +959,11 @@ where
     -- this function assumes all assigned metavariables have already been
     -- instantiated.
     go.run' mctx
-  visitMVar (mvarId' : MVarId) (numArgs : Nat := 0) : Bool :=
+  visitMVar (mvarId' : MVarId) : Bool :=
     if let some mvarDecl := mctx.findDecl? mvarId' then
-      occursCheck (skipAtMostNumBinders mvarDecl.type numArgs)
+      occursCheck mvarDecl.type
     else
       false
-  visitApp (e : Expr) : StateM (PtrSet Expr) Bool :=
-    e.withApp fun f args => do
-      unless (← args.allM visit) do
-        return false
-      if f.isMVar then
-        return visitMVar f.mvarId! args.size
-      else
-        visit f
   visit (e : Expr) : StateM (PtrSet Expr) Bool := do
     if !e.hasExprMVar then
       return true
@@ -1003,7 +972,7 @@ where
     else match e with
       | .mdata _ b       => visit b
       | .proj _ _ s      => visit s
-      | .app ..          => visitApp e
+      | .app f a         => visit f <&&> visit a
       | .lam _ d b _     => visit d <&&> visit b
       | .forallE _ d b _ => visit d <&&> visit b
       | .letE _ t v b _  => visit t <&&> visit v <&&> visit b

src/Lean/MetavarContext.lean

@@ -1059,7 +1059,7 @@ mutual
 
     Note: It is assumed that `xs` is the result of calling `collectForwardDeps` on a subset of variables in `lctx`.
   -/
-  private partial def mkAuxMVarType (lctx : LocalContext) (xs : Array Expr) (kind : MetavarKind) (e : Expr) : M Expr := do
+  private partial def mkAuxMVarType (lctx : LocalContext) (xs : Array Expr) (kind : MetavarKind) (e : Expr) (usedLetOnly : Bool) : M Expr := do
     let e ← abstractRangeAux xs xs.size e
     xs.size.foldRevM (init := e) fun i e => do
       let x := xs[i]!
@@ -1070,16 +1070,25 @@ mutual
           let type ← abstractRangeAux xs i type
           return Lean.mkForall n bi type e
         | LocalDecl.ldecl _ _ n type value nonDep _ =>
-          let type := type.headBeta
-          let type  ← abstractRangeAux xs i type
-          let value ← abstractRangeAux xs i value
-          let e := mkLet n type value e nonDep
-          match kind with
-          | MetavarKind.syntheticOpaque =>
-            -- See "Gruesome details" section in the beginning of the file
-            let e := e.liftLooseBVars 0 1
-            return mkForall n BinderInfo.default type e
-          | _ => pure e
+          if !usedLetOnly || e.hasLooseBVar 0 then
+            let type := type.headBeta
+            let type  ← abstractRangeAux xs i type
+            let value ← abstractRangeAux xs i value
+            let e := mkLet n type value e nonDep
+            match kind with
+            | MetavarKind.syntheticOpaque =>
+              -- See "Gruesome details" section in the beginning of the file
+              let e := e.liftLooseBVars 0 1
+              return mkForall n BinderInfo.default type e
+            | _ => pure e
+          else
+            match kind with
+            | MetavarKind.syntheticOpaque =>
+              let type := type.headBeta
+              let type  ← abstractRangeAux xs i type
+              return mkForall n BinderInfo.default type e
+            | _ =>
+              return e.lowerLooseBVars 1 1
       else
         -- `xs` may contain metavariables as "may dependencies" (see `findExprDependsOn`)
         let mvarDecl := (← get).mctx.getDecl x.mvarId!
@@ -1099,7 +1108,7 @@ mutual
 
     See details in the comment at the top of the file.
   -/
-  private partial def elimMVar (xs : Array Expr) (mvarId : MVarId) (args : Array Expr) : M (Expr × Array Expr) := do
+  private partial def elimMVar (xs : Array Expr) (mvarId : MVarId) (args : Array Expr) (usedLetOnly : Bool) : M (Expr × Array Expr) := do
     let mvarDecl  := (← getMCtx).getDecl mvarId
     let mvarLCtx  := mvarDecl.lctx
     let toRevert  := getInScope mvarLCtx xs
@@ -1127,7 +1136,7 @@ mutual
       let newMVarLCtx   := reduceLocalContext mvarLCtx toRevert
       let newLocalInsts := mvarDecl.localInstances.filter fun inst => toRevert.all fun x => inst.fvar != x
       -- Remark: we must reset the cache before processing `mkAuxMVarType` because `toRevert` may not be equal to `xs`
-      let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type
+      let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type usedLetOnly
       let newMVarId    := { name := (← get).ngen.curr }
       let newMVar      := mkMVar newMVarId
       let result       := mkMVarApp mvarLCtx newMVar toRevert newMVarKind
@@ -1168,7 +1177,8 @@ mutual
         if (← read).mvarIdsToAbstract.contains mvarId then
           return mkAppN f (← args.mapM (visit xs))
         else
-          return (← elimMVar xs mvarId args).1
+          -- We set `usedLetOnly := true` to avoid unnecessary let binders in the new metavariable type.
+          return (← elimMVar xs mvarId args (usedLetOnly := true)).1
     | _ =>
       return mkAppN (← visit xs f) (← args.mapM (visit xs))
 
@@ -1190,7 +1200,9 @@ partial def elimMVarDeps (xs : Array Expr) (e : Expr) : M Expr :=
 -/
 partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr) :=
   withFreshCache do
-    elimMVar xs mvarId #[]
+    -- We set `usedLetOnly := false`, because in the `revert` tactic
+    -- we expect that reverting a let variable always results in a let binder.
+    elimMVar xs mvarId #[] (usedLetOnly := false)
 
 /--
   Similar to `Expr.abstractRange`, but handles metavariables correctly.

tests/lean/interactive/hover.lean.expected.out

@@ -573,7 +573,7 @@
  {"start": {"line": 269, "character": 2}, "end": {"line": 269, "character": 3}},
  "contents":
  {"value":
-  "```lean\nlet x :=\n  match 0 with\n  | x => 0;\nℕ\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
+  "```lean\nℕ\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 272, "character": 4}}

tests/lean/run/meta5.lean

@@ -9,7 +9,7 @@ withLetDecl `x (mkConst `Nat) (mkNatLit 0) $ fun x => do {
   let mvar ← mkFreshExprMVar (mkConst `Nat) MetavarKind.syntheticOpaque;
   trace[Meta.debug] mvar;
   let r ← mkLambdaFVars #[y, x] mvar;
-  trace[Message.debug] r;
+  trace[Meta.debug] r;
   let v := mkApp2 (mkConst `Nat.add) x y;
   mvar.mvarId!.assign v;
   trace[Meta.debug] mvar;
@@ -24,15 +24,15 @@ set_option trace.Meta.debug true
 
 /--
 info: [Meta.debug] ?_
+[Meta.debug] fun y =>
+      let x := 0;
+      ?_
 [Meta.debug] x.add y
 [Meta.debug] fun y =>
       let x := 0;
       x.add y
 [Meta.debug] ?_uniq.3037 : Nat
-[Meta.debug] ?_uniq.3038 : Nat →
-      Nat →
-        let x := 0;
-        Nat
+[Meta.debug] ?_uniq.3038 : Nat → Nat → Nat
 -/
 #guard_msgs in
 #eval tst1