chore: remove [irreducible] from letFun

src/Init/Prelude.lean

@@ -72,12 +72,11 @@ This is equal to `(fun x => b) v`, so the value of `x` is not accessible to `b`.
 This is in contrast to `let x := v; b`, where the value of `x` is accessible to `b`.
 
 There is special support for `letFun`.
-Both WHNF and `simp` are aware of `letFun` and can reduce it when zeta reduction is enabled,
-despite the fact it is marked `irreducible`.
+Both WHNF and `simp` are aware of `letFun` and can reduce it when zeta reduction is enabled.
 For metaprogramming, the function `Lean.Expr.letFun?` can be used to recognize a `let_fun` expression
 to extract its parts as if it were a `let` expression.
 -/
-@[irreducible] def letFun {α : Sort u} {β : α → Sort v} (v : α) (f : (x : α) → β x) : β v := f v
+def letFun {α : Sort u} {β : α → Sort v} (v : α) (f : (x : α) → β x) : β v := f v
 
 set_option checkBinderAnnotations false in
 /--

src/Lean.lean

@@ -37,3 +37,4 @@ import Lean.Log
 import Lean.Linter
 import Lean.SubExpr
 import Lean.LabelAttribute
+import Lean.AddDecl

src/Lean/AddDecl.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.ReducibilityAttrs
+
+namespace Lean
+
+def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment :=
+  let decl := setReducibilityHintsOverride env opts decl
+  addDeclCore env decl
+
+def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment := do
+  let env ← addDecl env opts decl
+  compileDecl env opts decl
+
+def addDecl (decl : Declaration) : CoreM Unit := do
+  profileitM Exception "type checking" (← getOptions) do
+    withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
+      if !(← MonadLog.hasErrors) && decl.hasSorry then
+        logWarning "declaration uses 'sorry'"
+      match (← getEnv).addDecl (← getOptions) decl with
+      | .ok    env => setEnv env
+      | .error ex  => throwKernelException ex
+
+def addAndCompile (decl : Declaration) : CoreM Unit := do
+  addDecl decl
+  compileDecl decl
+
+end Lean

src/Lean/Compiler/InitAttr.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.AddDecl
 import Lean.Elab.InfoTree.Main
 
 namespace Lean

src/Lean/Compiler/Old.lean

@@ -67,9 +67,4 @@ opaque compileDecls (env : Environment) (opt : @& Options) (decls : @& List Name
 def compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment :=
   compileDecls env opt (Compiler.getDeclNamesForCodeGen decl)
 
-
-def addAndCompile (env : Environment) (opt : Options) (decl : Declaration) : Except KernelException Environment := do
-  let env ← addDecl env decl
-  compileDecl env opt decl
-
 end Environment

src/Lean/CoreM.lean

@@ -338,15 +338,6 @@ def mkArrow (d b : Expr) : CoreM Expr :=
 /-- Iterated `mkArrow`, creates the expression `a₁ → a₂ → … → aₙ → b`. Also see `arrowDomainsN`. -/
 def mkArrowN (ds : Array Expr) (e : Expr) : CoreM Expr := ds.foldrM mkArrow e
 
-def addDecl (decl : Declaration) : CoreM Unit := do
-  profileitM Exception "type checking" (← getOptions) do
-    withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
-      if !(← MonadLog.hasErrors) && decl.hasSorry then
-        logWarning "declaration uses 'sorry'"
-      match (← getEnv).addDecl decl with
-      | Except.ok    env => setEnv env
-      | Except.error ex  => throwKernelException ex
-
 private def supportedRecursors :=
   #[``Empty.rec, ``False.rec, ``Eq.ndrec, ``Eq.rec, ``Eq.recOn, ``Eq.casesOn, ``False.casesOn, ``Empty.casesOn, ``And.rec, ``And.casesOn]
 
@@ -400,10 +391,6 @@ def compileDecls (decls : List Name) : CoreM Unit := do
   | Except.error ex =>
     throwKernelException ex
 
-def addAndCompile (decl : Declaration) : CoreM Unit := do
-  addDecl decl;
-  compileDecl decl
-
 def getDiag (opts : Options) : Bool :=
   diagnostics.get opts
 

src/Lean/Declaration.lean

@@ -79,11 +79,34 @@ def isRegular : ReducibilityHints → Bool
 
 end ReducibilityHints
 
+/--
+When type checking definitions and theorems, we allow users
+to provide reducibility overrides.
+The overrides come from two different sources:
+- Attribute `[irreducible]` attached to imported declarations.
+- Locally sealed/unsealed declarations.
+-/
+inductive ReducibilityHintsOverride where
+  /--
+  Instruct the kernel to use only `ReducibilityHints` in the
+  convertibility checker.
+  -/
+  | ignore
+  /--
+  Instruct the kernel to treat a constant `c` as irreducible/opaque IF
+  1- It comes from an imported file, has the attribute `[irreducible]`
+     and is **not** in `unsealed`.
+  2- It is in `sealed`.
+  -/
+  | override (sealed : List Name) (unsealed : List Name)
+  deriving Repr, Inhabited, BEq
+
 /-- Base structure for `AxiomVal`, `DefinitionVal`, `TheoremVal`, `InductiveVal`, `ConstructorVal`, `RecursorVal` and `QuotVal`. -/
 structure ConstantVal where
   name : Name
   levelParams : List Name
   type : Expr
+  override : ReducibilityHintsOverride := .ignore
   deriving Inhabited, BEq
 
 structure AxiomVal extends ConstantVal where

src/Lean/Elab/BuiltinCommand.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.AddDecl
 import Lean.Util.CollectLevelParams
 import Lean.Meta.Reduce
 import Lean.Elab.DeclarationRange
@@ -123,7 +124,7 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   n[1].forArgsM addUnivLevel
 
 @[builtin_command_elab «init_quot»] def elabInitQuot : CommandElab := fun _ => do
-  match (← getEnv).addDecl Declaration.quotDecl with
+  match (← getEnv).addDecl (← getOptions) Declaration.quotDecl with
   | Except.ok env   => setEnv env
   | Except.error ex => throwError (ex.toMessageData (← getOptions))
 

src/Lean/Environment.lean

@@ -246,7 +246,7 @@ namespace Environment
 
 /-- Type check given declaration and add it to the environment -/
 @[extern "lean_add_decl"]
-opaque addDecl (env : Environment) (decl : @& Declaration) : Except KernelException Environment
+opaque addDeclCore (env : Environment) (decl : @& Declaration) : Except KernelException Environment
 
 end Environment
 

src/Lean/Meta/Closure.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.MetavarContext
 import Lean.Environment
+import Lean.AddDecl
 import Lean.Util.FoldConsts
 import Lean.Meta.Basic
 import Lean.Meta.Check

src/Lean/Meta/Constructions.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.AuxRecursor
+import Lean.AddDecl
 import Lean.Meta.AppBuilder
 
 namespace Lean

src/Lean/Meta/Eqns.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ReservedNameAction
+import Lean.AddDecl
 import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
 import Lean.Meta.Match.MatcherInfo

src/Lean/Meta/Eval.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura
 -/
 prelude
+import Lean.AddDecl
 import Lean.Meta.Check
 
 namespace Lean.Meta

src/Lean/Meta/SizeOf.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.List.BasicAux
+import Lean.AddDecl
 import Lean.Meta.AppBuilder
 import Lean.Meta.Instances
 

src/Lean/Meta/Tactic/AuxLemma.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.AddDecl
 import Lean.Meta.Basic
 
 namespace Lean.Meta

src/Lean/ReducibilityAttrs.lean

@@ -6,9 +6,9 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Attributes
 import Lean.ScopedEnvExtension
+import Lean.Util.CollectConsts
 
 namespace Lean
-
 /--
 Reducibility status for a definition.
 -/
@@ -184,4 +184,64 @@ def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   | .irreducible => return true
   | _ => return false
 
+register_builtin_option kernel.irreducibleHints : Bool := {
+  defValue := true
+  descr    := "use `[irreducible]` annotations as hints when type-checking in the kernel"
+}
+
+/--
+Set reducibility hints override fields at the given declaration using the
+current status of `reducibilityCoreExt` and `reducibilityExtraExt`.
+-/
+def setReducibilityHintsOverride (env : Environment) (opts : Options) (d : Declaration) : Declaration :=
+  let override := go d.collectConsts
+  match d with
+  | .defnDecl val => .defnDecl { val with override }
+  | .thmDecl val => .thmDecl { val with override }
+  | .opaqueDecl val => .opaqueDecl { val with override }
+  | .mutualDefnDecl vals => .mutualDefnDecl <| vals.map fun val => { val with override }
+  | _ => d
+where
+  go (declNames : Array Name) : ReducibilityHintsOverride := Id.run do
+    if kernel.irreducibleHints.get opts then
+      let mut sealed := #[]
+      let mut unsealed := #[]
+      for declName in declNames do
+        let currentStatus := getReducibilityStatusCore env declName
+        match env.getModuleIdxFor? declName with
+        | some modIdx =>
+          let importedStatus :=
+            match (reducibilityCoreExt.getModuleEntries env modIdx).binSearch (declName, .semireducible) (fun a b => Name.quickLt a.1 b.1) with
+            | some (_, status) => status
+            | none => .semireducible
+          if currentStatus != importedStatus then
+            if currentStatus matches .irreducible then
+              sealed := sealed.push declName
+            else
+              unsealed := unsealed.push declName
+        | none =>
+          -- `declName` was declared in the current module
+          if currentStatus matches .irreducible then
+            sealed := sealed.push declName
+      return .override sealed.toList unsealed.toList
+    else
+      return .ignore
+
+/--
+Auxiliary function used by the kernel to decide whether `declName` should be
+treated as irreducible or not.
+-/
+@[export lean_kernel_is_irreducible_override]
+def isIrreducibleOverride (env : Environment) (override : ReducibilityHintsOverride) (declName : Name) : Bool :=
+  match override with
+  | .ignore => false
+  | .override sealed unsealed =>
+    sealed.contains declName ||
+    match env.getModuleIdxFor? declName with
+    | none => false
+    | some modIdx =>
+      match (reducibilityCoreExt.getModuleEntries env modIdx).binSearch (declName, .semireducible) (fun a b => Name.quickLt a.1 b.1) with
+      | some (_, status) => status == .irreducible && !unsealed.contains declName
+      | none => false
+
 end Lean

src/Lean/Replay.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 prelude
 import Lean.CoreM
+import Lean.AddDecl
 import Lean.Util.FoldConsts
 
 /-!
@@ -56,7 +57,7 @@ def throwKernelException (ex : KernelException) : M Unit := do
 
 /-- Add a declaration, possibly throwing a `KernelException`. -/
 def addDecl (d : Declaration) : M Unit := do
-  match (← get).env.addDecl d with
+  match (← get).env.addDecl {} d with
   | .ok env => modify fun s => { s with env := env }
   | .error ex => throwKernelException ex
 

src/Lean/Util.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.Util.CollectFVars
 import Lean.Util.CollectLevelParams
 import Lean.Util.CollectMVars
+import Lean.Util.CollectConsts
 import Lean.Util.FindMVar
 import Lean.Util.FindLevelMVar
 import Lean.Util.MonadCache

src/Lean/Util/CollectConsts.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Expr
+import Lean.Declaration
+
+namespace Lean.CollectConsts
+
+structure State where
+  visitedExprPtr  : HashSet USize := {}
+  constSet        : HashSet Name := {}
+  consts          : Array Name := #[]
+  deriving Inhabited
+
+def State.add (s : State) (declName : Name) : State :=
+  if s.constSet.contains declName then
+    s
+  else
+    { s with constSet := s.constSet.insert declName, consts := s.consts.push declName }
+
+abbrev Visitor := State → State
+
+mutual
+  unsafe def visit (e : Expr) : Visitor := fun s =>
+    let addr := ptrAddrUnsafe e
+    if s.visitedExprPtr.contains addr then s
+    else main e { s with visitedExprPtr := s.visitedExprPtr.insert addr }
+
+  unsafe def main : Expr → Visitor
+    | .proj _ _ e      => visit e
+    | .forallE _ d b _ => visit b ∘ visit d
+    | .lam _ d b _     => visit b ∘ visit d
+    | .letE _ t v b _  => visit b ∘ visit v ∘ visit t
+    | .app f a         => visit a ∘ visit f
+    | .mdata _ b       => visit b
+    | .const n _       => fun s => s.add n
+    | _                => id
+end
+
+end CollectConsts
+
+def collectConsts (s : CollectConsts.State) (e : Expr) : CollectConsts.State :=
+  unsafe CollectConsts.main e s
+
+def Declaration.collectConsts (d : Declaration) : Array Name :=
+  let s := Id.run <| d.foldExprM Lean.collectConsts {}
+  s.consts
+
+end Lean

tests/lean/partialIssue.lean

@@ -1,4 +1,4 @@
-import Lean.CoreM
+import Lean.AddDecl
 
 #eval Lean.addDecl <| .mutualDefnDecl [{
   name := `False_intro