From 9f49ea63e2f3434c7bec208dc435486df530d60f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 4 Apr 2026 11:05:33 -0700 Subject: [PATCH] feat: add `backward.isDefEq.respectTransparency.types` option (#13280) This PR adds a new option `backward.isDefEq.respectTransparency.types` that controls the transparency used when checking whether the type of a metavariable matches the type of the term being assigned to it during `checkTypesAndAssign`. Previously, this check always bumped transparency to `.default` (via `withInferTypeConfig`), which is overly permissive. The new option uses `.instances` transparency instead (via `withImplicitConfig`), matching the behavior already used for implicit arguments. The option defaults to `false` (preserving old behavior) until stage0 is updated and breakage is assessed. If `backward.isDefEq.respectTransparency` (already in v4.29) is set to `false`, then `backward.isDefEq.respectTransparency.types` is automatically treated as `false` too. When `diagnostics` is enabled, a trace message is emitted if the stricter transparency fails but `.default` would have succeeded, helping identify affected code. To investigate failures when enabling `backward.isDefEq.respectTransparency.types`, use: ``` set_option diagnostics true set_option trace.diagnostics true ``` Also renames `withInstanceConfig` to `withImplicitConfig` since it now serves implicit argument and type checking, not just instances. Registers the `diagnostics` trace class in `CoreM`. Co-authored-by: Claude Opus 4.6 --- src/Lean/CoreM.lean | 2 ++ src/Lean/Meta/ExprDefEq.lean | 61 +++++++++++++++++++++++++++--------- stage0/src/stdlib_flags.h | 1 + 3 files changed, 50 insertions(+), 14 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 1891279502..b2dee8594f 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -20,6 +20,8 @@ register_builtin_option diagnostics : Bool := { descr := "collect diagnostic information" } +builtin_initialize registerTraceClass `diagnostics + register_builtin_option diagnostics.threshold : Nat := { defValue := 20 descr := "only diagnostic counters above this threshold are reported by the definitional equality" diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 0f2e7395e8..43bf97a60c 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -48,6 +48,16 @@ register_builtin_option backward.isDefEq.respectTransparency : Bool := { when checking whether implicit arguments are definitionally equal" } +/-- +Controls the transparency used to check whether the type of metavariable matches the type of the +term being assigned to it. +-/ +register_builtin_option backward.isDefEq.respectTransparency.types : Bool := { + defValue := false -- TODO: replace with `true` after we fix stage0 + descr := "if true, do not bump transparency to `.default` \ + when checking whether the type of a metavariable matches the type of the term being assigned to it." +} + /-- Controls whether *all* implicit arguments (not just instance-implicit `[..]`) get their transparency bumped to `TransparencyMode.instances` during `isDefEq`. @@ -335,10 +345,10 @@ private def isDefEqArgsFirstPass /-- Ensure `MetaM` configuration is strong enough for checking definitional equality of -instances. For example, we must be able to unfold instances, `beta := true`, `proj := .yesWithDelta` -are essential. +implicit arguments (e.g., instances) and types. +For example, we must be able to unfold instances, `beta := true`, `proj := .yesWithDelta` are essential. -/ -@[inline] def withInstanceConfig (x : MetaM α) : MetaM α := +@[inline] def withImplicitConfig (x : MetaM α) : MetaM α := withAtLeastTransparency .instances do let cfg ← getConfig if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaHave && cfg.zetaDelta && cfg.proj == .yesWithDelta then @@ -382,7 +392,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta -- Bump to `.instances` so that `[implicit_reducible]` definitions (instances, `Nat.add`, -- `Array.size`, etc.) are unfolded. The user doesn't choose implicit arguments directly, -- so Lean should try harder than the caller's transparency to make them match. - unless (← withInstanceConfig <| Meta.isExprDefEqAux a₁ a₂) do return false + unless (← withImplicitConfig <| Meta.isExprDefEqAux a₁ a₂) do return false else if respectTransparency then unless (← Meta.isExprDefEqAux a₁ a₂) do return false else @@ -392,7 +402,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta let a₁ := args₁[i]! let a₂ := args₂[i]! if respectTransparency && (implicitBump || finfo.paramInfo[i]!.isInstance) then - unless (← withInstanceConfig <| Meta.isExprDefEqAux a₁ a₂) do return false + unless (← withImplicitConfig <| Meta.isExprDefEqAux a₁ a₂) do return false else if !respectTransparency && finfo.paramInfo[i]!.isInstance then -- Old behavior unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do return false @@ -454,6 +464,19 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr) let lctx ← getLCtx isDefEqBindingAux lctx #[] a b #[] +/-- +Returns `true` if both `backward.isDefEq.respectTransparency` and `backward.isDefEq.respectTransparency.types` is true. + +The option `backward.isDefEq.respectTransparency.types` is newer than ``backward.isDefEq.respectTransparency`, +and is used to enable the transparency bump when checking metavariable assignments. + +If `backward.isDefEq.respectTransparency` is `false`, then we automatically disable +`backward.isDefEq.respectTransparency.types` too. +-/ +abbrev respectTransparencyAtTypes : CoreM Bool := do + let opts ← getOptions + return backward.isDefEq.respectTransparency.types.get opts && backward.isDefEq.respectTransparency.get opts + private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool := withTraceNodeBefore `Meta.isDefEq.assign.checkTypes (fun _ => return m!"({mvar} : {← inferType mvar}) := ({v} : {← inferType v})") do if !mvar.isMVar then @@ -462,14 +485,24 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool := else -- must check whether types are definitionally equal or not, before assigning and returning true let mvarType ← inferType mvar - -- **TODO**: avoid transparency bump. Let's fix other issues first - withInferTypeConfig do - let vType ← inferType v - if (← Meta.isExprDefEqAux mvarType vType) then - mvar.mvarId!.assign v - pure true - else - pure false + let vType ← inferType v + if (← respectTransparencyAtTypes) then + withImplicitConfig do + if (← Meta.isExprDefEqAux mvarType vType) then + mvar.mvarId!.assign v + return true + else + if (← isDiagnosticsEnabled) then withInferTypeConfig do + if (← Meta.isExprDefEqAux mvarType vType) then + trace[diagnostics] "failure when assigning metavariable with type{indentExpr mvarType}\nwhich is not definitionally equal to{indentExpr vType}\nwhen using `.instances` transparency, but it is with `.default`.\nWorkaround: `set_option backward.isDefEq.respectTransparency.types false`" + return false + else + withInferTypeConfig do + if (← Meta.isExprDefEqAux mvarType vType) then + mvar.mvarId!.assign v + return true + else + return false /-- Auxiliary method for solving constraints of the form `?m xs := v`. @@ -2062,7 +2095,7 @@ private def isDefEqProj : Expr → Expr → MetaM Bool for instance-implicit parameters. -/ let fromClass := isClass (← getEnv) m let isDefEqStructArgs (x : MetaM Bool) : MetaM Bool := - if fromClass then withInstanceConfig x else x + if fromClass then withImplicitConfig x else x if (← read).inTypeClassResolution then -- See comment at `inTypeClassResolution` pure (i == j && m == n) <&&> isDefEqStructArgs (Meta.isExprDefEqAux t s) diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index e444447049..b50af122c4 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,3 +1,4 @@ +// update me! #include "util/options.h" namespace lean {