From 10338ed1b00a9c3fb864ee80b02b311cd7c9e2c5 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 20 Apr 2026 08:41:32 +0200 Subject: [PATCH] fix: wrapInstance: do not leak via un-reducible instances (#13441) This PR ensures that if wrapInstance encounters an instance that cannot be reduced to a constructor, the wrapping definition is left at semireducible transparency to avoid leakage. --- src/Lean/Meta/WrapInstance.lean | 1 - tests/elab/inferInstanceAs.lean | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Lean/Meta/WrapInstance.lean b/src/Lean/Meta/WrapInstance.lean index 944197641a..bbbb45cdaf 100644 --- a/src/Lean/Meta/WrapInstance.lean +++ b/src/Lean/Meta/WrapInstance.lean @@ -145,7 +145,6 @@ public partial def wrapInstance (inst expectedType : Expr) (compile : Bool := tr else let name ← mkAuxDeclName let wrapped ← mkAuxDefinition name expectedType inst (compile := false) - setReducibilityStatus name .implicitReducible if isMeta then modifyEnv (markMeta · name) if compile then compileDecls (logErrors := logCompileErrors) #[name] diff --git a/tests/elab/inferInstanceAs.lean b/tests/elab/inferInstanceAs.lean index 61a0260ade..76da829dc6 100644 --- a/tests/elab/inferInstanceAs.lean +++ b/tests/elab/inferInstanceAs.lean @@ -46,7 +46,7 @@ instCD2._aux_1 #guard_msgs in #print instCD2 /-- -info: @[implicit_reducible] private def instCD2._aux_1 : C D2 := +info: private def instCD2._aux_1 : C D2 := instCI2 -/ #guard_msgs in