diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 2ce3273390..1a7fabfcc0 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/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 diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 2ed1491175..9652db7729 100644 --- a/src/Lean/MetavarContext.lean +++ 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. diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index 200bc3da45..a2b4083373 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/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}} diff --git a/tests/lean/run/meta5.lean b/tests/lean/run/meta5.lean index f7418fc6ce..b2054f434a 100644 --- a/tests/lean/run/meta5.lean +++ b/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