From d4fdb5d7c061a6938c60ec445e9c4dd6fbc2a05b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 4 Oct 2024 15:04:35 +0200 Subject: [PATCH] fix: getFunInfo, inferType to use withAtLeastTransparency, not withTransparency (#5563) when the transparency mode is `.all`, then one expects `getFunInfo` and `inferType` to also work with that transparency mode. Fixes #5562 Fixes #2975 Fixes #2194 --- src/Lean/Meta/Basic.lean | 19 ++++++++--- src/Lean/Meta/FunInfo.lean | 2 +- src/Lean/Meta/InferType.lean | 27 ++++++++++----- stage0/src/stdlib_flags.h | 2 +- tests/lean/run/issue2975.lean | 19 +++++++++++ tests/lean/run/issue5562.lean | 63 +++++++++++++++++++++++++++++++++++ 6 files changed, 118 insertions(+), 14 deletions(-) create mode 100644 tests/lean/run/issue2975.lean create mode 100644 tests/lean/run/issue5562.lean diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index cf7abcf1fd..0cefdfd8c8 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -246,12 +246,20 @@ structure DefEqCache where all : PersistentHashMap (Expr × Expr) Bool := {} deriving Inhabited +/-- + A cache for `inferType` at transparency levels `.default` an `.all`. +-/ +structure InferTypeCaches where + default : InferTypeCache + all : InferTypeCache + deriving Inhabited + /-- Cache datastructures for type inference, type class resolution, whnf, and definitional equality. -/ structure Cache where - inferType : InferTypeCache := {} - funInfo : FunInfoCache := {} + inferType : InferTypeCaches := ⟨{}, {}⟩ + funInfo : FunInfoCache := {} synthInstance : SynthInstanceCache := {} whnfDefault : WhnfCache := {} -- cache for closed terms and `TransparencyMode.default` whnfAll : WhnfCache := {} -- cache for closed terms and `TransparencyMode.all` @@ -478,8 +486,11 @@ variable [MonadControlT MetaM n] [Monad n] @[inline] def modifyCache (f : Cache → Cache) : MetaM Unit := modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed, diag } -@[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit := - modifyCache fun ⟨ic, c1, c2, c3, c4, c5, c6⟩ => ⟨f ic, c1, c2, c3, c4, c5, c6⟩ +@[inline] def modifyInferTypeCacheDefault (f : InferTypeCache → InferTypeCache) : MetaM Unit := + modifyCache fun ⟨⟨icd, ica⟩, c1, c2, c3, c4, c5, c6⟩ => ⟨⟨f icd, ica⟩, c1, c2, c3, c4, c5, c6⟩ + +@[inline] def modifyInferTypeCacheAll (f : InferTypeCache → InferTypeCache) : MetaM Unit := + modifyCache fun ⟨⟨icd, ica⟩, c1, c2, c3, c4, c5, c6⟩ => ⟨⟨icd, f ica⟩, c1, c2, c3, c4, c5, c6⟩ @[inline] def modifyDefEqTransientCache (f : DefEqCache → DefEqCache) : MetaM Unit := modifyCache fun ⟨c1, c2, c3, c4, c5, defeqTrans, c6⟩ => ⟨c1, c2, c3, c4, c5, f defeqTrans, c6⟩ diff --git a/src/Lean/Meta/FunInfo.lean b/src/Lean/Meta/FunInfo.lean index d2883a4353..7b8939b5a7 100644 --- a/src/Lean/Meta/FunInfo.lean +++ b/src/Lean/Meta/FunInfo.lean @@ -55,7 +55,7 @@ private def updateHasFwdDeps (pinfo : Array ParamInfo) (backDeps : Array Nat) : private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo := checkFunInfoCache fn maxArgs? do let fnType ← inferType fn - withTransparency TransparencyMode.default do + withAtLeastTransparency TransparencyMode.default do forallBoundedTelescope fnType maxArgs? fun fvars type => do let mut paramInfo := #[] let mut higherOrderOutParams : FVarIdSet := {} diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index c574220d39..501faa10e7 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -166,13 +166,24 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do | none => fvarId.throwUnknown @[inline] private def checkInferTypeCache (e : Expr) (inferType : MetaM Expr) : MetaM Expr := do - match (← get).cache.inferType.find? e with - | some type => return type - | none => - let type ← inferType - unless e.hasMVar || type.hasMVar do - modifyInferTypeCache fun c => c.insert e type - return type + match (← getTransparency) with + | .default => + match (← get).cache.inferType.default.find? e with + | some type => return type + | none => + let type ← inferType + unless e.hasMVar || type.hasMVar do + modifyInferTypeCacheDefault fun c => c.insert e type + return type + | .all => + match (← get).cache.inferType.all.find? e with + | some type => return type + | none => + let type ← inferType + unless e.hasMVar || type.hasMVar do + modifyInferTypeCacheAll fun c => c.insert e type + return type + | _ => panic! "checkInferTypeCache: transparency mode not default or all" @[export lean_infer_type] def inferTypeImp (e : Expr) : MetaM Expr := @@ -191,7 +202,7 @@ def inferTypeImp (e : Expr) : MetaM Expr := | .forallE .. => checkInferTypeCache e (inferForallType e) | .lam .. => checkInferTypeCache e (inferLambdaType e) | .letE .. => checkInferTypeCache e (inferLambdaType e) - withIncRecDepth <| withTransparency TransparencyMode.default (infer e) + withIncRecDepth <| withAtLeastTransparency TransparencyMode.default (infer e) /-- Return `LBool.true` if given level is always equivalent to universe level zero. diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 0699845ba4..cb8a954a4d 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -6,7 +6,7 @@ options get_default_options() { // see https://lean-lang.org/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications #if LEAN_IS_STAGE0 == 1 // switch to `true` for ABI-breaking changes affecting meta code - opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `true` for changing built-in parsers used in quotations opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax diff --git a/tests/lean/run/issue2975.lean b/tests/lean/run/issue2975.lean new file mode 100644 index 0000000000..d016edd7fd --- /dev/null +++ b/tests/lean/run/issue2975.lean @@ -0,0 +1,19 @@ +import Lean +open Lean Meta Elab Term + +elab "#reduce'" t:term : command => Elab.Command.runTermElabM fun _ => do + let e ← withSynthesize <| elabTerm t none + let e ← Meta.reduce e + withTransparency TransparencyMode.all do + logInfo m!"{← inferType e}" + +structure S where + x : Nat + +def S' := S +def S'.x (s : S') : Nat := S.x s + +attribute [irreducible] S' + +variable (s : S') +#reduce' s.x diff --git a/tests/lean/run/issue5562.lean b/tests/lean/run/issue5562.lean new file mode 100644 index 0000000000..c75a7f6fff --- /dev/null +++ b/tests/lean/run/issue5562.lean @@ -0,0 +1,63 @@ +import Lean + +/-! +This test checks that we can enter, typecheck etc. terms that are only type-correct at +transparency `all`. +-/ + +open Lean Meta + + +def T := Nat → Nat +def x : T := fun n => n + 1 + +-- All well: +def n1 : Nat := x 1 + + +-- Now we make `T` irreducible. A bunch of things should break: + +attribute [irreducible] T + +/-- +error: function expected at + x +term has type + T +-/ +#guard_msgs in +def n2 : Nat := x 1 + + +-- NB: Checking does not break! Always done at transparency `all`. +run_meta do + Meta.check (.app (mkConst ``x) (mkNatLit 1)) + +-- Type inference fails: + +/-- +error: function expected + x 1 +-/ +#guard_msgs in +run_meta do + let _ ← Meta.inferType (.app (mkConst ``x) (mkNatLit 1)) + +-- But succeeds at transparency .all + +run_meta do + withTransparency .all do + let _ ← Meta.inferType (.app (mkConst ``x) (mkNatLit 1)) + +-- An elaborator that sets transparency to .all: + +elab "with_unfolding_all" t:term : term <= expectedType? => + withTransparency .all <| + Elab.Term.elabTerm t expectedType? + +/-- +error: function expected + x 1 +-/ +#guard_msgs in +def n3 : Nat := with_unfolding_all x 1