feat: @[instance_reducible] (#12247)

This PR adds the new transparency setting `@[instance_reducible]`. We
used to check whether a declaration had `instance` reducibility by using
the `isInstance` predicate. However, this was not a robust solution
because:

- We have scoped instances, and `isInstance` returns `true` only if the
scope is active.

- We have auxiliary declarations used to construct instances manually,
such as:

```lean
    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`. Thus, 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.

**We are decoupling whether a declaration is available for type class
resolution from its transparency status.**

**Remak**: We need a update stage0 to complete this feature.

---------

Co-authored-by: Sebastian Ullrich <[email protected]>

Author: leodemoura

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