chore: fix tests

src/Init/Syntax.lean

@@ -3,12 +3,9 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
-
 module
-
 prelude
 public import Init.Data.Array.Set
-
 public section
 
 /-!

src/Lean/Compiler/LCNF/Basic.lean

@@ -746,7 +746,7 @@ def Decl.isTemplateLike (decl : Decl pu) : CoreM Bool := do
   let env ← getEnv
   if ← hasLocalInst decl.type then
     return true -- `decl` applications will be specialized
-  else if Meta.isInstanceCore env decl.name then
+  else if (← isInstanceReducible decl.name) then
     return true -- `decl` is "fuel" for code specialization
   else if decl.inlineable || hasSpecializeAttribute env decl.name then
     return true -- `decl` is going to be inlined or specialized

src/Lean/Compiler/LCNF/LambdaLifting.lean

@@ -214,7 +214,7 @@ def eagerLambdaLifting : Pass where
   name       := `eagerLambdaLifting
   run        := fun decls => do
     decls.foldlM (init := #[]) fun decls decl => do
-      if decl.inlineable || (← Meta.isInstance decl.name) then
+      if decl.inlineable || (← isInstanceReducible decl.name) then
         return decls.push decl
       else
         return decls ++ (← decl.lambdaLifting (liftInstParamOnly := true) (allowEtaContraction := false) (suffix := `_elam))

src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean

@@ -56,7 +56,7 @@ def inlineCandidate? (e : LetValue .pure) : SimpM (Option InlineCandidateInfo) :
       We assume that at the base phase these annotations are for the instance methods that have been lambda lifted.
       -/
       if (← inBasePhase) then
-        if (← Meta.isInstance decl.name) then
+        if (← isInstanceReducible decl.name) then
           unless decl.name == ``instDecidableEqBool do
             /-
             TODO: remove this hack after we refactor `Decidable` as suggested by Gabriel.

src/Lean/Compiler/LCNF/Simp/Main.lean

@@ -76,7 +76,7 @@ def etaPolyApp? (letDecl : LetDecl .pure) : OptionT SimpM (FunDecl .pure) := do
   let .const declName us args := letDecl.value | failure
   let some info := (← getEnv).find? declName | failure
   guard <| (← hasLocalInst info.type)
-  guard <| !(← Meta.isInstance declName)
+  guard <| !(← isInstanceReducible declName)
   let some ⟨.pure, decl⟩ ← getDecl? declName | failure
   guard <| decl.getArity > args.size
   let params ← mkNewParams letDecl.type

src/Lean/Compiler/LCNF/Specialize.lean

@@ -399,7 +399,7 @@ mutual
   partial def specializeApp? (e : LetValue .pure) : SpecializeM (Option (LetValue .pure)) := do
     let .const declName us args := e | return none
     if args.isEmpty then return none
-    if (← Meta.isInstance declName) then return none
+    if (← isInstanceReducible declName) then return none
     let some specEntry ← getSpecEntry? declName | return none
     unless (← shouldSpecialize specEntry args) do return none
     let some ⟨.pure, decl⟩ ← getDecl? declName | return none

src/Lean/Elab/DeclModifiers.lean

@@ -125,6 +125,10 @@ def Modifiers.addFirstAttr (modifiers : Modifiers) (attr : Attribute) : Modifier
 def Modifiers.filterAttrs (modifiers : Modifiers) (p : Attribute → Bool) : Modifiers :=
   { modifiers with attrs := modifiers.attrs.filter p }
 
+/-- Returns `true` if `modifiers` contains an attribute satisfying `p`. -/
+def Modifiers.anyAttr (modifiers : Modifiers) (p : Attribute → Bool) : Bool :=
+  modifiers.attrs.any p
+
 instance : ToFormat Modifiers := ⟨fun m =>
   let components : List Format :=
     (match m.docString? with

src/Lean/Elab/DefView.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 module
-
 prelude
 public import Lean.Elab.DeclNameGen
 public import Lean.Elab.DeclUtil
-
 public section
-
 namespace Lean.Elab
 
 inductive DefKind where
@@ -165,11 +162,18 @@ def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView :=
 
 def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
   -- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
+  /-
+  **Note**: add `instance_reducible` attribute if declaration is not already marked with `@[reducible]`
+  -/
+  let modifiers       := if modifiers.anyAttr fun attr => attr.name == `reducible then
+    modifiers
+  else
+    modifiers.addAttr { name := `instance_reducible }
   let attrKind        ← liftMacroM <| toAttributeKind stx[0]
   let prio            ← liftMacroM <| expandOptNamedPrio stx[2]
   let attrStx         ← `(attr| instance $(quote prio):num)
-  let (binders, type) := expandDeclSig stx[4]
   let modifiers       := modifiers.addAttr { kind := attrKind, name := `instance, stx := attrStx }
+  let (binders, type) := expandDeclSig stx[4]
   let declId ← match stx[3].getOptional? with
     | some declId =>
       if ← isTracingEnabledFor `Elab.instance.mkInstanceName then

src/Lean/Elab/Deriving/Basic.lean

@@ -205,7 +205,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) : TermElabM Unit
   let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
   addAndCompile (logCompileErrors := !(← read).isNoncomputableSection) <| Declaration.defnDecl decl
   trace[Elab.Deriving] "Derived instance `{.ofConstName instName}`"
-  addInstance instName AttributeKind.global (eval_prio default)
+  registerInstance instName AttributeKind.global (eval_prio default)
   addDeclarationRangesFromSyntax instName (← getRef)
 
 end Term

src/Lean/Elab/MutualDef.lean

@@ -4,14 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Elab.Deriving.Basic
 public import Lean.Elab.PreDefinition.Main
 import all Lean.Elab.ErrorUtils
-
 public section
-
 namespace Lean.Elab
 open Lean.Parser.Term
 

src/Lean/Elab/Print.lean

@@ -4,14 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Eqns
 public import Lean.Elab.Command
 import Lean.PrettyPrinter.Delaborator.Builtins
-
 public section
-
 namespace Lean.Elab.Command
 
 private def throwUnknownId (id : Name) : CommandElabM Unit :=
@@ -29,9 +26,10 @@ private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
 private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) (sig : Bool := true) : CommandElabM MessageData := do
   let mut attrs := #[]
   match (← getReducibilityStatus id) with
-  | ReducibilityStatus.irreducible =>   attrs := attrs.push m!"irreducible"
-  | ReducibilityStatus.reducible =>     attrs := attrs.push m!"reducible"
-  | ReducibilityStatus.semireducible => pure ()
+  | .irreducible =>   attrs := attrs.push m!"irreducible"
+  | .reducible =>     attrs := attrs.push m!"reducible"
+  | .instanceReducible => attrs := attrs.push m!"instance_reducible"
+  | .semireducible => pure ()
 
   let env ← getEnv
   if env.header.isModule && (env.setExporting true |>.find? id |>.any (·.isDefinition)) then

src/Lean/Elab/Structure.lean

@@ -1498,7 +1498,7 @@ private def addParentInstances (parents : Array StructureParentInfo) : MetaM Uni
   let instParents := instParents.filter fun parent =>
     !resOrders.any (fun resOrder => resOrder[1...*].any (· == parent.structName))
   for instParent in instParents do
-    addInstance instParent.projFn AttributeKind.global (eval_prio default)
+    registerInstance instParent.projFn AttributeKind.global (eval_prio default)
 
 @[builtin_inductive_elab Lean.Parser.Command.«structure»]
 def elabStructureCommand : InductiveElabDescr where

src/Lean/Elab/Tactic/Grind/Main.lean

@@ -212,7 +212,7 @@ def elabGrindLocals (params : Grind.Params) : MetaM Grind.Params := do
     -- Filter similar to LibrarySuggestions.isDeniedPremise (but inlined to avoid dependency)
     -- Skip internal details, but allow private names (which are accessible from current module)
     if name.isInternalDetail && !isPrivateName name then continue
-    if (← Meta.isInstance name) then continue
+    if (← isInstanceReducible name) then continue
     match ci with
     | .defnInfo _ =>
       try

src/Lean/Elab/Tactic/Simp.lean

@@ -427,7 +427,7 @@ def elabSimpLocals (thms : SimpTheorems) (kind : SimpKind) : MetaM SimpTheorems
   for (name, ci) in env.constants.map₂.toList do
     -- Skip internal details, but allow private names (which are accessible from current module)
     if name.isInternalDetail && !isPrivateName name then continue
-    if (← Meta.isInstance name) then continue
+    if (← isInstanceReducible name) then continue
     match ci with
     | .defnInfo _ =>
       -- Definitions are added to unfold

src/Lean/Elab/Term/TermElabM.lean

@@ -1024,8 +1024,8 @@ private def applyAttributesCore
       withRef attr.stx do withLogging do
       let env ← getEnv
       match getAttributeImpl env attr.name with
-      | Except.error errMsg => throwError errMsg
-      | Except.ok attrImpl  =>
+      | .error errMsg => throwError errMsg
+      | .ok attrImpl  =>
         let runAttr := attrImpl.add declName attr.stx attr.kind
         let runAttr := do
           -- not truly an elaborator, but a sensible target for go-to-definition

src/Lean/LibrarySuggestions/Basic.lean

@@ -76,7 +76,7 @@ unsafe def fold {α : Type} (f : Name → α → MetaM α) (e : Expr) (acc : α)
         return acc
       else
         modify fun s => { s with visitedConsts := s.visitedConsts.insert c }
-        if ← isInstance c then
+        if ← isInstanceReducible c then
           return acc
         else
           f c acc
@@ -320,7 +320,7 @@ def isDeniedPremise (env : Environment) (name : Name) (allowPrivate : Bool := fa
   if name == ``sorryAx then return true
   -- Allow private names through if allowPrivate is set (e.g., for currentFile selector)
   if name.isInternalDetail && !(allowPrivate && isPrivateName name) then return true
-  if Lean.Meta.isInstanceCore env name then return true
+  if isInstanceReducibleCore env name then return true
   if Lean.Linter.isDeprecated env name then return true
   if (nameDenyListExt.getState env).any (fun p => name.anyS (· == p)) then return true
   if let some moduleIdx := env.getModuleIdxFor? name then

src/Lean/Meta/GetUnfoldableConst.lean

@@ -5,7 +5,8 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.GlobalInstances
+public import Lean.Meta.GlobalInstances -- **TODO**: Delete after update stage0
+import Lean.ReducibilityAttrs
 public section
 namespace Lean.Meta
 
@@ -15,9 +16,11 @@ private def canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool :
   | .all  => return true
   | .default => return !(← isIrreducible info.name)
   | m =>
-    if (← isReducible info.name) then
+    let status ← getReducibilityStatus info.name
+    if status == .reducible then
       return true
-    else if m == .instances && isGlobalInstance (← getEnv) info.name then
+    -- **TODO**: Delete `isGlobalInstance` after update stage0
+    else if m == .instances && (isGlobalInstance (← getEnv) info.name || status == .instanceReducible) then
       return true
     else
       return false

src/Lean/Meta/Instances.lean

@@ -8,6 +8,7 @@ prelude
 public import Init.Data.Range.Polymorphic.Stream
 public import Lean.Meta.DiscrTree.Main
 public import Lean.Meta.CollectMVars
+import Lean.ReducibilityAttrs
 import Lean.Meta.WHNF
 public section
 namespace Lean.Meta
@@ -230,11 +231,44 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
 def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
   let c ← mkConstWithLevelParams declName
   let keys ← mkInstanceKey c
+  let status ← getReducibilityStatus declName
+  unless status matches .reducible | .instanceReducible do
+    let info ← getConstInfo declName
+    if info.isDefinition then
+      -- **TODO**: uncomment after update stage0
+      -- logWarning m!"instance `{declName}` must be marked with @[reducible] or @[instance_reducible]"
+      pure ()
   addGlobalInstance declName attrKind
   let projInfo? ← getProjectionFnInfo? declName
   let synthOrder ← computeSynthOrder c projInfo?
   instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
 
+/-
+Adds instance **and** marks it with reducibility status `@[instance_reducible]`. We use this function
+to elaborate `instance` command.
+
+**Note**: We used to check whether `declName` had `instance` reducibility by using `isInstance declName`.
+However, this was not a robust solution because:
+
+- We have scoped instances, and `isInstance declName` returns true only if the scope is active.
+
+- We have auxiliary declarations used to construct instances manually, such as:
+  ```
+  def lt_wfRel : WellFoundedRelation Nat
+  ```
+  `isInstance` also returns `false` for this kind of declaration.
+
+In both cases, the declaration may be (or may have been) used to construct an instance, but `isInstance`
+returns `false`. We claim it is a mistake to check the reducibility status using `isInstance`.
+`isInstance` indicates whether a declaration is available for the type class resolution mechanism,
+not its transparency status.
+
+Thus, we added a new transparency setting and set it here.
+-/
+def registerInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
+  setReducibilityStatus declName .instanceReducible
+  addInstance declName attrKind prio
+
 /--
 Registers type class instances.
 
@@ -334,4 +368,15 @@ def getDefaultInstancesPriorities [Monad m] [MonadEnv m] : m PrioritySet :=
 def getDefaultInstances [Monad m] [MonadEnv m] (className : Name) : m (List (Name × Nat)) :=
   return defaultInstanceExtension.getState (← getEnv) |>.defaultInstances.find? className |>.getD []
 
-end Lean.Meta
+end Meta
+
+-- **TODO**: Move to `ReducibilityAttrs.lean` after update stage0
+def isInstanceReducibleCore (env : Environment) (declName : Name) : Bool :=
+  getReducibilityStatusCore env declName matches .instanceReducible
+    || Meta.isInstanceCore env declName -- **TODO**: Delete after update stage0
+
+/-- Return `true` if the given declaration has been marked as `[instance_reducible]`. -/
+def isInstanceReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
+  return isInstanceReducibleCore (← getEnv) declName
+
+end Lean

src/Lean/Meta/SizeOf.lean

@@ -519,7 +519,7 @@ def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
                         safety      := .safe
                         hints       := .abbrev
                       }
-                    addInstance instDeclName AttributeKind.global (eval_prio default)
+                    registerInstance instDeclName AttributeKind.global (eval_prio default)
                     enableRealizationsForConst instDeclName
           if genSizeOfSpec.get (← getOptions) then
             mkSizeOfSpecTheorems indInfo.all.toArray fns recMap

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -445,7 +445,7 @@ Returns `true` if we should use `funCC` for applications of the given constant s
 private def useFunCongrAtDecl (declName : Name) : GrindM Bool := do
   if (← hasFunCCModifier declName) then
     return true
-  if (← isInstance declName) then
+  if (← isInstanceReducible declName) then
     /- **Note**: Instances are support elements. No `funCC` -/
     return false
   if let some projInfo ← getProjectionFnInfo? declName then

src/Lean/Meta/Tactic/Grind/MBTC.lean

@@ -85,7 +85,7 @@ private def mkCandidate (a b : ArgInfo) (i : Nat) : GoalM SplitInfo := do
 /-- Returns `true` if `f` is a type class instance -/
 private def isFnInstance (f : Expr) : CoreM Bool := do
   let .const declName _ := f | return false
-  isInstance declName
+  isInstanceReducible declName
 
 /-- Model-based theory combination. -/
 def mbtc (ctx : MBTC.Context) : GoalM Bool := do

src/Lean/ReducibilityAttrs.lean

@@ -16,13 +16,14 @@ namespace Lean
 Reducibility status for a definition.
 -/
 inductive ReducibilityStatus where
-  | reducible | semireducible | irreducible
+  | reducible | semireducible | irreducible | instanceReducible
   deriving Inhabited, Repr, BEq
 
 def ReducibilityStatus.toAttrString : ReducibilityStatus → String
   | .reducible => "[reducible]"
   | .irreducible => "[irreducible]"
   | .semireducible => "[semireducible]"
+  | .instanceReducible => "[instance_reducible]"
 
 builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ←
   registerPersistentEnvExtension {
@@ -111,37 +112,52 @@ private def validate (declName : Name) (status : ReducibilityStatus) (attrKind :
   -- downstream non-`module`s.
   withoutExporting do
   unless allowUnsafeReducibility.get (← getOptions) do
-    match (← getConstInfo declName) with
-    | .defnInfo _ =>
-      let statusOld := getReducibilityStatusCore (← getEnv) declName
-      match attrKind with
-      | .scoped =>
-        throwError "failed to set reducibility status for `{.ofConstName declName}`, the `scoped` modifier is not recommended for this kind of attribute{suffix}"
-      | .global =>
-        if (← getEnv).getModuleIdxFor? declName matches some _ then
-          throwError "failed to set reducibility status, `{.ofConstName declName}` has not been defined in this file, consider using the `local` modifier{suffix}"
-        match status with
-        | .reducible =>
-          unless statusOld matches .semireducible do
-            throwError "failed to set `[reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
-        | .irreducible =>
-          unless statusOld matches .semireducible do
-            throwError "failed to set `[irreducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
-        | .semireducible =>
-          throwError "failed to set `[semireducible]` for `{.ofConstName declName}`, declarations are `[semireducible]` by default{suffix}"
-      | .local =>
-        match status with
-        | .reducible =>
-          throwError "failed to set `[local reducible]` for `{.ofConstName declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution{suffix}"
-        | .irreducible =>
-          unless statusOld matches .semireducible do
-            throwError "failed to set `[local irreducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}"
-        | .semireducible =>
-          unless statusOld matches .irreducible do
-            throwError "failed to set `[local semireducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected{suffix}"
-    | _ => throwError "failed to set reducibility status, `{.ofConstName declName}` is not a definition{suffix}"
+    unless (← getConstInfo declName).isDefinition do
+      throwError "failed to set reducibility status, `{.ofConstName declName}` is not a definition{suffix}"
+    let statusOld := getReducibilityStatusCore (← getEnv) declName
+    match attrKind with
+    | .scoped =>
+      throwError "failed to set reducibility status for `{.ofConstName declName}`, the `scoped` modifier is not recommended for this kind of attribute{suffix}"
+    | .global =>
+      if (← getEnv).getModuleIdxFor? declName matches some _ then
+        throwError "failed to set reducibility status, `{.ofConstName declName}` has not been defined in this file, consider using the `local` modifier{suffix}"
+      match status with
+      | .reducible =>
+        unless statusOld matches .semireducible do
+          throwError "failed to set `[reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
+      | .irreducible =>
+        unless statusOld matches .semireducible do
+          throwError "failed to set `[irreducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
+      | .instanceReducible =>
+        unless statusOld matches .semireducible do
+          throwError "failed to set `[instance_reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
+      | .semireducible =>
+        throwError "failed to set `[semireducible]` for `{.ofConstName declName}`, declarations are `[semireducible]` by default{suffix}"
+    | .local =>
+      match status with
+      | .reducible =>
+        throwError "failed to set `[local reducible]` for `{.ofConstName declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution{suffix}"
+      | .irreducible =>
+        unless statusOld matches .semireducible do
+          throwError "failed to set `[local irreducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}"
+      | .instanceReducible =>
+        unless statusOld matches .semireducible do
+          throwError "failed to set `[local instance_reducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}"
+      | .semireducible =>
+        unless statusOld matches .irreducible do
+          throwError "failed to set `[local semireducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected{suffix}"
+
+/-
+**Note**: Some instances are not definitions, but theorems. Thus, they don't need the `[instance_reducible]` attribute,
+but the current frontend adds the attribute `[instance_reducible]` when pre-processing the command `instance` before
+we know whether its type is a proposition or not. Thus, we just skip these annotations for now.
+-/
+private def ignoreAttr (status : ReducibilityStatus) (declName : Name) : CoreM Bool := do
+  let .instanceReducible := status | return false
+  return !(← getConstInfo declName).isDefinition
 
 private def addAttr (status : ReducibilityStatus) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do
+  if (← ignoreAttr status declName) then return ()
   Attribute.Builtin.ensureNoArgs stx
   validate declName status attrKind
   let ns ← getCurrNamespace
@@ -174,6 +190,15 @@ builtin_initialize
     applicationTime := .afterTypeChecking
  }
 
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `instance_reducible
+    descr           := "semireducible declaration"
+    add             := addAttr .instanceReducible
+    applicationTime := .afterTypeChecking
+ }
+
 /-- Return the reducibility attribute for the given declaration. -/
 def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m ReducibilityStatus := do
   return getReducibilityStatusCore (← getEnv) declName
@@ -188,15 +213,11 @@ def setReducibleAttribute [MonadEnv m] (declName : Name) : m Unit :=
 
 /-- Return `true` if the given declaration has been marked as `[reducible]`. -/
 def isReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
-  match (← getReducibilityStatus declName) with
-  | .reducible => return true
-  | _ => return false
+  return (← getReducibilityStatus declName) matches .reducible
 
 /-- Return `true` if the given declaration has been marked as `[irreducible]` -/
 def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
-  match (← getReducibilityStatus declName) with
-  | .irreducible => return true
-  | _ => return false
+  return (← getReducibilityStatus declName) matches .irreducible
 
 /-- Set the given declaration as `[irreducible]` -/
 def setIrreducibleAttribute [MonadEnv m] (declName : Name) : m Unit :=

stage0/src/stdlib_flags.h

@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {

tests/lean/defInst.lean.expected.out

@@ -10,5 +10,5 @@ fun x y => x == y : Foo → Foo → Bool
 false
 true
 true
-def instMonadM : Monad M :=
+@[instance_reducible] def instMonadM : Monad M :=
 ReaderT.instMonad

tests/lean/diamond4.lean.expected.out

@@ -1,4 +1,4 @@
-def D.toB : {α : Type} → [self : D α] → B α :=
+@[instance_reducible] def D.toB : {α : Type} → [self : D α] → B α :=
 fun (α : Type) [self : D α] => self.1
-def D.toC : {α : Type} → [self : D α] → C α :=
+@[instance_reducible] def D.toC : {α : Type} → [self : D α] → C α :=
 fun (α : Type) (self : D α) => @C.mk α (@B.toA α (@D.toB α self)) (@D.mul α self)

tests/lean/diamond6.lean.expected.out

@@ -16,7 +16,7 @@ FooAC.mk {α : Type} [toFooComm : FooComm α] [toMul : Mul.{0} α]
       @Eq.{1} α (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b)
         (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) :
   FooAC α
-def FooAC.toFooAssoc : {α : Type} → [self : FooAC α] → FooAssoc α :=
+@[instance_reducible] def FooAC.toFooAssoc : {α : Type} → [self : FooAC α] → FooAssoc α :=
 fun (α : Type) (self : FooAC α) =>
   @FooAssoc.mk α (@FooComm.toFoo α (@FooAC.toFooComm α self)) (@FooAC.toMul α self) (@FooAC.add_assoc α self)
     (@FooAC.mul_assoc α self)
@@ -39,7 +39,7 @@ FooAC'.mk {α : Type} [toFooComm : FooComm α] [toMul : Mul.{0} α]
       @Eq.{1} α (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b)
         (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) :
   FooAC' α
-def FooAC'.toFooAssoc' : {α : Type} → [self : FooAC' α] → FooAssoc' α :=
+@[instance_reducible] def FooAC'.toFooAssoc' : {α : Type} → [self : FooAC' α] → FooAssoc' α :=
 fun (α : Type) (self : FooAC' α) =>
   @FooAssoc'.mk α
     (@FooAssoc.mk α (@FooComm.toFoo α (@FooAC'.toFooComm α self)) (@FooAC'.toMul α self) (@FooAC'.add_assoc α self)

tests/lean/diamond7.lean.expected.out

@@ -6,7 +6,8 @@ CommMonoid.mk.{u} {α : Type u} [toMonoid : Monoid.{u} α]
         (@HMul.hMul.{u, u, u} α α α (@instHMul.{u} α (@Semigroup.toMul.{u} α (@Monoid.toSemigroup.{u} α toMonoid))) b
           a)) :
   CommMonoid.{u} α
-def CommMonoid.toCommSemigroup.{u} : {α : Type u} → [self : CommMonoid.{u} α] → CommSemigroup.{u} α :=
+@[instance_reducible] def CommMonoid.toCommSemigroup.{u} : {α : Type u} →
+  [self : CommMonoid.{u} α] → CommSemigroup.{u} α :=
 fun (α : Type u) (self : CommMonoid.{u} α) =>
   @CommSemigroup.mk.{u} α (@Monoid.toSemigroup.{u} α (@CommMonoid.toMonoid.{u} α self))
     (@CommMonoid.mul_comm.{u} α self)
@@ -19,12 +20,12 @@ CommGroup.mk.{u} {α : Type u} [toGroup : Group.{u} α]
         (@HMul.hMul.{u, u, u} α α α
           (@instHMul.{u} α (@Semigroup.toMul.{u} α (@Monoid.toSemigroup.{u} α (@Group.toMonoid.{u} α toGroup)))) b a)) :
   CommGroup.{u} α
-def CommGroup.toCommMonoid.{u} : {α : Type u} → [self : CommGroup.{u} α] → CommMonoid.{u} α :=
+@[instance_reducible] def CommGroup.toCommMonoid.{u} : {α : Type u} → [self : CommGroup.{u} α] → CommMonoid.{u} α :=
 fun (α : Type u) (self : CommGroup.{u} α) =>
   @CommMonoid.mk.{u} α (@Group.toMonoid.{u} α (@CommGroup.toGroup.{u} α self)) (@CommGroup.mul_comm.{u} α self)
 Field.mk.{u} {α : Type u} [toDivisionRing : DivisionRing α] (mul_comm : ∀ (a b : α), a * b = b * a) : Field α
-def Field.toDivisionRing.{u} : {α : Type u} → [self : Field.{u} α] → DivisionRing.{u} α :=
+@[instance_reducible] def Field.toDivisionRing.{u} : {α : Type u} → [self : Field.{u} α] → DivisionRing.{u} α :=
 fun (α : Type u) [self : Field.{u} α] => self.1
-def Field.toCommRing.{u} : {α : Type u} → [self : Field.{u} α] → CommRing.{u} α :=
+@[instance_reducible] def Field.toCommRing.{u} : {α : Type u} → [self : Field.{u} α] → CommRing.{u} α :=
 fun (α : Type u) (self : Field.{u} α) =>
   @CommRing.mk.{u} α (@DivisionRing.toRing.{u} α (@Field.toDivisionRing.{u} α self)) (@Field.mul_comm.{u} α self)

tests/lean/run/derivingBEq.lean

@@ -54,7 +54,7 @@ inductive L' (α : Type u) : Type u
 
 end InNamespace
 /--
-info: @[expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α)
+info: @[instance_reducible, expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α)
 -/
 #guard_msgs in #print sig InNamespace.instBEqL'
 /--
@@ -163,7 +163,7 @@ private structure PrivStruct where
 deriving BEq
 
 -- Instance and spec should be private
-/-- info: private def instBEqPrivStruct : BEq PrivStruct -/
+/-- info: @[instance_reducible] private def instBEqPrivStruct : BEq PrivStruct -/
 #guard_msgs in
 #print sig instBEqPrivStruct
 

tests/lean/run/derivingBEqLinear.lean

@@ -58,7 +58,7 @@ inductive L' (α : Type u) : Type u
 
 end InNamespace
 /--
-info: @[expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α)
+info: @[instance_reducible, expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α)
 -/
 #guard_msgs in #print sig InNamespace.instBEqL'
 /--
@@ -150,7 +150,7 @@ private structure PrivStruct where
 deriving BEq
 
 -- Instance and spec should be private
-/-- info: private def instBEqPrivStruct : BEq PrivStruct -/
+/-- info: @[instance_reducible] private def instBEqPrivStruct : BEq PrivStruct -/
 #guard_msgs in
 #print sig instBEqPrivStruct
 

tests/lean/run/derivingDelta.lean

@@ -62,7 +62,7 @@ def MyNat := Nat
 deriving OfNat
 
 /--
-info: def instOfNatMyNat : (_x_1 : Nat) → OfNat MyNat _x_1 :=
+info: @[instance_reducible] def instOfNatMyNat : (_x_1 : Nat) → OfNat MyNat _x_1 :=
 fun _x_1 => instOfNatNat _x_1
 -/
 #guard_msgs in #print instOfNatMyNat
@@ -72,7 +72,7 @@ Explicit parameterization
 -/
 deriving instance (n : Nat) → OfNat _ n for MyNat
 /--
-info: def instOfNatMyNat_1 : (n : Nat) → OfNat MyNat n :=
+info: @[instance_reducible] def instOfNatMyNat_1 : (n : Nat) → OfNat MyNat n :=
 fun n => instOfNatNat n
 -/
 #guard_msgs in #print instOfNatMyNat_1
@@ -85,7 +85,7 @@ variable (m : Nat)
 deriving instance OfNat _ m for MyNat
 end
 /--
-info: def instOfNatMyNat_2 : (m : Nat) → OfNat MyNat m :=
+info: @[instance_reducible] def instOfNatMyNat_2 : (m : Nat) → OfNat MyNat m :=
 fun m => instOfNatNat m
 -/
 #guard_msgs in #print instOfNatMyNat_2
@@ -132,7 +132,7 @@ def MyFin'' := Fin
 deriving C1
 
 /--
-info: def instC1NatMyFin'' : @C1 Nat instDecidableEqNat MyFin'' :=
+info: @[instance_reducible] def instC1NatMyFin'' : @C1 Nat instDecidableEqNat MyFin'' :=
 instC1NatFin
 -/
 #guard_msgs in set_option pp.explicit true in #print instC1NatMyFin''
@@ -164,12 +164,12 @@ instance (n : Nat) : OfNat' n Int := {}
 def MyInt := Int
 deriving OfNat', OfNat
 /--
-info: def instOfNat'MyInt : (_x_1 : Nat) → OfNat' _x_1 MyInt :=
+info: @[instance_reducible] def instOfNat'MyInt : (_x_1 : Nat) → OfNat' _x_1 MyInt :=
 fun _x_1 => instOfNat'Int _x_1
 -/
 #guard_msgs in #print instOfNat'MyInt
 /--
-info: def instOfNatMyInt : (_x_1 : Nat) → OfNat MyInt _x_1 :=
+info: @[instance_reducible] def instOfNatMyInt : (_x_1 : Nat) → OfNat MyInt _x_1 :=
 fun _x_1 => instOfNat
 -/
 #guard_msgs in #print instOfNatMyInt
@@ -201,7 +201,7 @@ def NewRing (R : Type _) [Semiring R] := R
 deriving Module R
 
 /--
-info: def instModuleNewRing.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing R) :=
+info: @[instance_reducible] def instModuleNewRing.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing R) :=
 fun R [Semiring R] => instModule R
 -/
 #guard_msgs in #print instModuleNewRing
@@ -221,7 +221,7 @@ def NewRing' (R : Type _) := R
 deriving instance Module R for NewRing' R
 
 /--
-info: def instModuleNewRing'.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing' R) :=
+info: @[instance_reducible] def instModuleNewRing'.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing' R) :=
 fun R [Semiring R] => instModule R
 -/
 #guard_msgs in #print instModuleNewRing'
@@ -236,7 +236,7 @@ instance : C2 Type Prop := {}
 def Prop' := Prop
 deriving C2
 /--
-info: def instC2TypeProp' : C2 Type Prop' :=
+info: @[instance_reducible] def instC2TypeProp' : C2 Type Prop' :=
 instC2TypeProp
 -/
 #guard_msgs in #print instC2TypeProp'

tests/lean/run/derivingInhabited.lean

@@ -54,7 +54,7 @@ structure A where
 deriving Inhabited
 
 /--
-info: private def instInhabitedA : Inhabited A :=
+info: @[instance_reducible] private def instInhabitedA : Inhabited A :=
 { default := instInhabitedA.default }
 -/
 #guard_msgs in

tests/lean/run/derivingRepr.lean

@@ -146,7 +146,7 @@ public structure Public where
 deriving Repr
 
 /--
-info: @[expose] def instReprPublic : Repr Public :=
+info: @[instance_reducible, expose] def instReprPublic : Repr Public :=
 { reprPrec := instReprPublic.repr }
 -/
 #guard_msgs in

tests/lean/run/diagnostics.lean

@@ -6,46 +6,36 @@ def f (x : Nat) : Nat :=
 
 theorem f_eq : f (x + 1) = q (f x) := rfl
 
-set_option trace.Meta.debug true
-
 /--
 trace: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 15, num: 6):
+  [reduction] unfolded declarations (max: 15, num: 4):
     [reduction] Nat.rec ↦ 15
     [reduction] Add.add ↦ 10
     [reduction] HAdd.hAdd ↦ 10
     [reduction] Nat.add ↦ 10
-    [reduction] f ↦ 5
-    [reduction] OfNat.ofNat ↦ 5
-  [reduction] unfolded instances (max: 5, num: 1):
-    [reduction] instOfNatNat ↦ 5
   [reduction] unfolded reducible declarations (max: 15, num: 1):
     [reduction] Nat.casesOn ↦ 15
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example : f (x + 5) = q (q (q (q (q (f x))))) :=
-  set_option diagnostics.threshold 4 in
+  set_option diagnostics.threshold 5 in
   set_option diagnostics true in
   rfl
 
 /--
 trace: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 15, num: 6):
+  [reduction] unfolded declarations (max: 15, num: 4):
     [reduction] Nat.rec ↦ 15
     [reduction] Add.add ↦ 10
     [reduction] HAdd.hAdd ↦ 10
     [reduction] Nat.add ↦ 10
-    [reduction] f ↦ 5
-    [reduction] OfNat.ofNat ↦ 5
-  [reduction] unfolded instances (max: 5, num: 1):
-    [reduction] instOfNatNat ↦ 5
   [reduction] unfolded reducible declarations (max: 15, num: 1):
     [reduction] Nat.casesOn ↦ 15
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example : f (x + 5) = q (q (q (q (q (f x))))) := by
-  set_option diagnostics.threshold 4 in
+  set_option diagnostics.threshold 5 in
   set_option diagnostics true in
   rfl

tests/lean/run/issue10678.lean

@@ -9,7 +9,7 @@ deriving Lean.ToExpr, Inhabited
 -- same namespace for instance and aux decls
 
 /--
-info: def A.instToExprA.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (A α) :=
+info: @[instance_reducible] def A.instToExprA.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (A α) :=
 fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] =>
   { toExpr := instToExprA.toExpr inst_1, toTypeExpr := (Lean.Expr.const `A.A [Lean.toLevel]).app (Lean.toTypeExpr α) }
 -/
@@ -17,7 +17,7 @@ fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] =>
 
 
 /--
-info: def A.instInhabitedA.{u_1} : {a : Type u_1} → [Inhabited a] → Inhabited (A a) :=
+info: @[instance_reducible] def A.instInhabitedA.{u_1} : {a : Type u_1} → [Inhabited a] → Inhabited (A a) :=
 fun {a} [Inhabited a] => { default := instInhabitedA.default }
 -/
 #guard_msgs in #print A.instInhabitedA
@@ -35,14 +35,14 @@ deriving Lean.ToExpr, Inhabited
 end
 
 /--
-info: def instToExprB.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (B α) :=
+info: @[instance_reducible] def instToExprB.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (B α) :=
 fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] =>
   { toExpr := instToExprB.toExpr_1 inst_1, toTypeExpr := (Lean.Expr.const `B [Lean.toLevel]).app (Lean.toTypeExpr α) }
 -/
 #guard_msgs in
 #print instToExprB
 /--
-info: def instToExprC.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (C α) :=
+info: @[instance_reducible] def instToExprC.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (C α) :=
 fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] =>
   { toExpr := instToExprB.toExpr_2 inst_1, toTypeExpr := (Lean.Expr.const `C [Lean.toLevel]).app (Lean.toTypeExpr α) }
 -/
@@ -51,14 +51,14 @@ fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] =>
 
 
 /--
-info: def instInhabitedB.{u_1} : {a : Type u_1} → Inhabited (B a) :=
+info: @[instance_reducible] def instInhabitedB.{u_1} : {a : Type u_1} → Inhabited (B a) :=
 fun {a} => { default := instInhabitedB.default_1 }
 -/
 #guard_msgs in
 #print instInhabitedB
 
 /--
-info: def instInhabitedC.{u_1} : {a : Type u_1} → Inhabited (C a) :=
+info: @[instance_reducible] def instInhabitedC.{u_1} : {a : Type u_1} → Inhabited (C a) :=
 fun {a} => { default := instInhabitedC.default_1 }
 -/
 #guard_msgs in

tests/lean/run/reduceBEqSimproc.lean

@@ -54,7 +54,7 @@ end Linear
 namespace A
 inductive L where | nil  : L | cons : Nat → L → L deriving BEq
 -- NB: Instance, op and theorem are private
-/-- info: private def A.instBEqL : BEq L -/
+/-- info: @[instance_reducible] private def A.instBEqL : BEq L -/
 #guard_msgs in #print sig instBEqL
 /-- info: private def A.instBEqL.beq : L → L → Bool -/
 #guard_msgs in #print sig instBEqL.beq
@@ -66,7 +66,7 @@ end A
 namespace B
 public inductive L where | nil  : L | cons : Nat → L → L deriving BEq
 -- NB: Instance is public and exposed, op and theorem are private
-/-- info: @[expose] def B.instBEqL : BEq L -/
+/-- info: @[instance_reducible, expose] def B.instBEqL : BEq L -/
 #guard_msgs in #print sig instBEqL
 /-- info: def B.instBEqL.beq : L → L → Bool -/
 #guard_msgs in #print sig instBEqL.beq
@@ -79,7 +79,7 @@ end B
 namespace C
 public inductive L where | nil  : L | cons : Nat → L → L deriving @[expose] BEq
 -- NB: Public exposed instances, implementation and public theorem
-/-- info: @[expose] def C.instBEqL : BEq L -/
+/-- info: @[instance_reducible, expose] def C.instBEqL : BEq L -/
 #guard_msgs in #print sig instBEqL
 /-- info: @[expose] def C.instBEqL.beq : L → L → Bool -/
 #guard_msgs in #print sig instBEqL.beq

tests/lean/run/structInst.lean

@@ -274,7 +274,7 @@ instance : B where
 instance : C where
 
 /--
-info: def Issue6046.instC : C :=
+info: @[instance_reducible] def Issue6046.instC : C :=
 { b := B.b }
 -/
 #guard_msgs in #print Issue6046.instC
@@ -342,7 +342,7 @@ class Bar extends Foo where
 instance instBar : Bar where
 
 /--
-info: def Ex6769_1.instBar : Bar :=
+info: @[instance_reducible] def Ex6769_1.instBar : Bar :=
 { x := 0 }
 -/
 #guard_msgs in #print instBar
@@ -361,7 +361,7 @@ instance instBar : Bar where
   x := 0
 
 /--
-info: def Ex6769_2.instBar : Bar :=
+info: @[instance_reducible] def Ex6769_2.instBar : Bar :=
 { x := 0, hx := Mathlib12129.bar._proof_1, hx' := Mathlib12129.bar._proof_1 }
 -/
 #guard_msgs in #print instBar
@@ -380,7 +380,7 @@ instance instBar : Bar where
   x := 0
 
 /--
-info: def Ex6769_3.instBar : Bar :=
+info: @[instance_reducible] def Ex6769_3.instBar : Bar :=
 { x := 0, hx := Mathlib12129.bar._proof_1, hx' := Mathlib12129.bar._proof_1 }
 -/
 #guard_msgs in #print instBar

tests/pkg/module/Module/Basic.lean

@@ -423,7 +423,7 @@ meta structure Foo where
 deriving TypeName
 
 /--
-info: private meta def instTypeNameFoo : TypeName Foo :=
+info: @[instance_reducible] private meta def instTypeNameFoo : TypeName Foo :=
 inst✝
 -/
 #guard_msgs in