From 3878432ac75628c64cad16eb33a3250542b0002b Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 20 Jun 2025 23:26:32 -0700 Subject: [PATCH] fix: make sure local instance detection sees through reductions (#8903) This PR make sure that the local instance cache calculation applies more reductions. In #2199 there was an issue where metavariables could prevent local variables from being considered as local instances. We use a slightly different approach that ensures that, for example, `let`s at the ends of telescopes do not cause similar problems. These reductions were already being calculated, so this does not require any additional work to be done. Metaprogramming interface addition: the various forall telescope functions that do reduction now have a `whnfType` flag (default false). If it's true, then the callback `k` is given the WHNF of the type. This is a free operation, since the telescope function already computes it. --- src/Lean/Meta/Basic.lean | 65 +++++++++++++++++------------ tests/lean/docStr.lean.expected.out | 2 +- tests/lean/run/2199.lean | 38 ++++++++++++++++- 3 files changed, 77 insertions(+), 28 deletions(-) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index e21ab96a5a..a1403290a3 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -1358,11 +1358,15 @@ mutual If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope. + + If `whnfIfReducing` is true, then in the `reducing == true` case, `k` is given the whnf of the type. + This does not have any performance cost. -/ private partial def forallTelescopeReducingAuxAux (reducing : Bool) (maxFVars? : Option Nat) (type : Expr) - (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) : MetaM α := do + (k : Array Expr → Expr → MetaM α) + (cleanupAnnotations : Bool) (whnfTypeIfReducing : Bool) : MetaM α := do let rec process (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (type : Expr) : MetaM α := do match type with | .forallE n d b bi => @@ -1387,43 +1391,47 @@ mutual let newType ← whnf type if newType.isForall then process lctx fvars fvars.size newType + else if whnfTypeIfReducing then + k fvars newType else k fvars type else k fvars type process (← getLCtx) #[] 0 type - private partial def forallTelescopeReducingAux (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) : MetaM α := do + private partial def forallTelescopeReducingAux (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) (whnfType : Bool) : MetaM α := do match maxFVars? with - | some 0 => k #[] type + | some 0 => + if whnfType then + k #[] (← whnf type) + else + k #[] type | _ => do let newType ← whnf type if newType.isForall then - forallTelescopeReducingAuxAux true maxFVars? newType k cleanupAnnotations + forallTelescopeReducingAuxAux true maxFVars? newType k cleanupAnnotations whnfType + else if whnfType then + k #[] newType else k #[] type - -- Helper method for isClassExpensive? - private partial def isClassApp? (type : Expr) (instantiated := false) : MetaM (Option Name) := do + /-- + Helper method for `isClassExpensive?`. The type `type` is in WHNF. + -/ + private partial def isClassApp? (type : Expr) : MetaM (Option Name) := do match type.getAppFn with | .const c _ => let env ← getEnv if isClass env c then return some c else - -- Use whnf to make sure abbreviations are unfolded - match (← whnf type).getAppFn with - | .const c _ => if isClass env c then return some c else return none - | _ => return none - | .mvar .. => - if instantiated then return none - isClassApp? (← instantiateMVars type) true + return none | _ => return none private partial def isClassExpensive? (type : Expr) : MetaM (Option Name) := withReducible do -- when testing whether a type is a type class, we only unfold reducible constants. - forallTelescopeReducingAux type none (cleanupAnnotations := false) fun _ type => isClassApp? type + forallTelescopeReducingAux type none (cleanupAnnotations := false) (whnfType := true) fun _ type => isClassApp? type private partial def isClassImp? (type : Expr) : MetaM (Option Name) := do match (← isClassQuick? type) with @@ -1452,8 +1460,8 @@ private def withNewLocalInstancesImpAux (fvars : Array Expr) (j : Nat) : n α partial def withNewLocalInstances (fvars : Array Expr) (j : Nat) : n α → n α := mapMetaM <| withNewLocalInstancesImpAux fvars j -@[inline] private def forallTelescopeImp (type : Expr) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) : MetaM α := do - forallTelescopeReducingAuxAux (reducing := false) (maxFVars? := none) type k cleanupAnnotations +@[inline] private def forallTelescopeImp (type : Expr) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) (whnfType : Bool) : MetaM α := do + forallTelescopeReducingAuxAux (reducing := false) (maxFVars? := none) type k cleanupAnnotations whnfType /-- Given `type` of the form `forall xs, A`, execute `k xs A`. @@ -1463,7 +1471,7 @@ partial def withNewLocalInstances (fvars : Array Expr) (j : Nat) : n α → n α If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope. -/ def forallTelescope (type : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α := - map2MetaM (fun k => forallTelescopeImp type k cleanupAnnotations) k + map2MetaM (fun k => forallTelescopeImp type k cleanupAnnotations (whnfType := false)) k /-- Given a monadic function `f` that takes a type and a term of that type and produces a new term, @@ -1482,29 +1490,34 @@ and then builds the lambda telescope term for the new term. def mapForallTelescope (f : Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do mapForallTelescope' (fun _ e => f e) forallTerm -private def forallTelescopeReducingImp (type : Expr) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) : MetaM α := - forallTelescopeReducingAux type (maxFVars? := none) k cleanupAnnotations +private def forallTelescopeReducingImp (type : Expr) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) (whnfType : Bool) : MetaM α := + forallTelescopeReducingAux type (maxFVars? := none) k cleanupAnnotations (whnfType := whnfType) /-- Similar to `forallTelescope`, but given `type` of the form `forall xs, A`, it reduces `A` and continues building the telescope if it is a `forall`. If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope. --/ -def forallTelescopeReducing (type : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α := - map2MetaM (fun k => forallTelescopeReducingImp type k cleanupAnnotations) k -private def forallBoundedTelescopeImp (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) : MetaM α := - forallTelescopeReducingAux type maxFVars? k cleanupAnnotations + If `whnfType` is `true`, we give `k` the `whnf` of the resulting type. This is a free operation. +-/ +def forallTelescopeReducing (type : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) (whnfType := false) : n α := + map2MetaM (fun k => forallTelescopeReducingImp type k cleanupAnnotations (whnfType := whnfType)) k + +private def forallBoundedTelescopeImp (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) (whnfType : Bool) : MetaM α := + forallTelescopeReducingAux type maxFVars? k cleanupAnnotations (whnfType := whnfType) /-- Similar to `forallTelescopeReducing`, stops constructing the telescope when it reaches size `maxFVars`. If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope. + + If `whnfType` is `true`, we give `k` the `whnf` of the resulting type. + This is a free operation unless `maxFVars? == some 0`, in which case it computes the `whnf`. -/ -def forallBoundedTelescope (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α := - map2MetaM (fun k => forallBoundedTelescopeImp type maxFVars? k cleanupAnnotations) k +def forallBoundedTelescope (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) (whnfType := false) : n α := + map2MetaM (fun k => forallBoundedTelescopeImp type maxFVars? k cleanupAnnotations (whnfType := whnfType)) k private partial def lambdaTelescopeImp (e : Expr) (consumeLet : Bool) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations := false) : MetaM α := do diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out index 6b5d000ce6..84d505e216 100644 --- a/tests/lean/docStr.lean.expected.out +++ b/tests/lean/docStr.lean.expected.out @@ -17,7 +17,7 @@ doc string for 'g' is not available "let rec documentation at g " "Gadget for optional parameter support.\n\nA binder like `(x : α := default)` in a declaration is syntax sugar for\n`x : optParam α default`, and triggers the elaborator to attempt to use\n`default` to supply the argument if it is not supplied.\n" "Auxiliary declaration used to implement named patterns like `x@h:p`. " -"Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\nit reduces `A` and continues building the telescope if it is a `forall`.\n\nIf `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.\n" +"Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\nit reduces `A` and continues building the telescope if it is a `forall`.\n\nIf `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.\n\nIf `whnfType` is `true`, we give `k` the `whnf` of the resulting type. This is a free operation.\n" Foo := { range := { pos := { line := 3, column := 0 }, charUtf16 := 0, diff --git a/tests/lean/run/2199.lean b/tests/lean/run/2199.lean index c95d133e82..925cf30666 100644 --- a/tests/lean/run/2199.lean +++ b/tests/lean/run/2199.lean @@ -1,8 +1,44 @@ +/-! +# Make sure local instance detection can handle metavariables and other reductions +-/ + +/-! +Reported in https://github.com/leanprover/lean4/issues/2199 +The `inferInstance` was failing due to metavariables introduced by `cases`. +-/ theorem exists_foo : ∃ T : Type, Nonempty T := ⟨Unit, ⟨()⟩⟩ -set_option trace.Meta.debug true example : True := by cases exists_foo rename_i T hT have : Nonempty T := inferInstance trivial + +/-! +The `let` would inhibit `inst` from being seen as a local `Decidable` instance. +Two tests: one where `let` starts a telescope, and another where it's at the end. +(Having `let`s in the middle of a forall telescope always worked.) +-/ +axiom p : Nat → Prop + +axiom inst : let n := 5; Decidable (p n) + +example : True := by + have := inst + have : Decidable (p 5) := inferInstance + trivial + +axiom inst' : ∀ k, let n := k; Decidable (p n) + +example : True := by + have := inst' + have : Decidable (p 5) := inferInstance + trivial + +/-! +This worked before, but here's an extra test that abbreviations are correctly handled. +-/ +abbrev D (p : Prop) := Decidable p + +example (p : Prop) [D p] : (if p then True else False) ↔ p := by + split <;> simp_all