feat: validate reducibility attribute setting (#4052)

and new option `set_option allowUnsafeReductibility true` to override
validation.

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>

src/Lean/Meta/LazyDiscrTree.lean

@@ -745,7 +745,6 @@ instance : Append (PreDiscrTree α) where
 end PreDiscrTree
 
 /-- Initial entry in lazy discrimination tree -/
-@[reducible]
 structure InitEntry (α : Type) where
   /-- Return root key for an entry. -/
   key : Key

src/Lean/ReducibilityAttrs.lean

@@ -16,6 +16,11 @@ inductive ReducibilityStatus where
   | reducible | semireducible | irreducible
   deriving Inhabited, Repr, BEq
 
+def ReducibilityStatus.toAttrString : ReducibilityStatus → String
+  | .reducible => "[reducible]"
+  | .irreducible => "[irreducible]"
+  | .semireducible => "[semireducible]"
+
 builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ←
   registerPersistentEnvExtension {
     name            := `reducibilityCore
@@ -48,7 +53,7 @@ def getReducibilityStatusCore (env : Environment) (declName : Name) : Reducibili
     | none => .semireducible
   | none => (reducibilityCoreExt.getState env).find? declName |>.getD .semireducible
 
-def setReducibilityStatusCore (env : Environment) (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) (currNamespace : Name) : Environment :=
+private def setReducibilityStatusCore (env : Environment) (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) (currNamespace : Name) : Environment :=
   if attrKind matches .global then
     match env.getModuleIdxFor? declName with
     | some _ =>
@@ -65,15 +70,75 @@ def setReducibilityStatusCore (env : Environment) (declName : Name) (status : Re
 private def setReducibilityStatusImp (env : Environment) (declName : Name) (status : ReducibilityStatus) : Environment :=
   setReducibilityStatusCore env declName status .global .anonymous
 
+/-
+TODO: it would be great if we could distinguish between the following two situations
+
+1-
+```
+@[reducible] def foo := ...
+```
+
+2-
+```
+def foo := ...
+...
+attribute [reducible] foo
+```
+
+Reason: the second one is problematic if user has add simp theorems or TC instances that include `foo`.
+Recall that the discrimination trees unfold `[reducible]` declarations while indexing new entries.
+-/
+
+register_builtin_option allowUnsafeReducibility : Bool := {
+  defValue := false
+  descr    := "enables users to modify the reducibility settings for declarations even when such changes are deemed potentially hazardous. For example, `simp` and type class resolution maintain term indices where reducible declarations are expanded."
+}
+
+private def validate (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) : CoreM Unit := do
+  let suffix := "use `set_option allowUnsafeReducibility true` to override reducibility status validation"
+  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 `{declName}`, the `scoped` modifier is not recommended for this kind of attribute\n{suffix}"
+      | .global =>
+        if (← getEnv).getModuleIdxFor? declName matches some _ then
+          throwError "failed to set reducibility status, `{declName}` has not been defined in this file, consider using the `local` modifier\n{suffix}"
+        match status with
+        | .reducible =>
+          unless statusOld matches .semireducible do
+            throwError "failed to set `[reducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`\n{suffix}"
+        | .irreducible =>
+          unless statusOld matches .semireducible do
+            throwError "failed to set `[irreducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`\n{suffix}"
+        | .semireducible =>
+          throwError "failed to set `[semireducible]` for `{declName}`, declarations are `[semireducible]` by default\n{suffix}"
+      | .local =>
+        match status with
+        | .reducible =>
+          throwError "failed to set `[local reducible]` for `{declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution\n{suffix}"
+        | .irreducible =>
+          unless statusOld matches .semireducible do
+            throwError "failed to set `[local irreducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected\n{suffix}"
+        | .semireducible =>
+          unless statusOld matches .irreducible do
+            throwError "failed to set `[local semireducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected\n{suffix}"
+    | _ => throwError "failed to set reducibility status, `{declName}` is not a definition\n{suffix}"
+
+private def addAttr (status : ReducibilityStatus) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do
+  Attribute.Builtin.ensureNoArgs stx
+  validate declName status attrKind
+  let ns ← getCurrNamespace
+  modifyEnv fun env => setReducibilityStatusCore env declName status attrKind ns
+
 builtin_initialize
   registerBuiltinAttribute {
     ref             := by exact decl_name%
     name            := `irreducible
     descr           := "irreducible declaration"
-    add             := fun declName stx attrKind => do
-      Attribute.Builtin.ensureNoArgs stx
-      let ns ← getCurrNamespace
-      modifyEnv fun env => setReducibilityStatusCore env declName .irreducible attrKind ns
+    add             := addAttr .irreducible
     applicationTime := .afterTypeChecking
  }
 
@@ -82,10 +147,7 @@ builtin_initialize
     ref             := by exact decl_name%
     name            := `reducible
     descr           := "reducible declaration"
-    add             := fun declName stx attrKind => do
-      Attribute.Builtin.ensureNoArgs stx
-      let ns ← getCurrNamespace
-      modifyEnv fun env => setReducibilityStatusCore env declName .reducible attrKind ns
+    add             := addAttr .reducible
     applicationTime := .afterTypeChecking
  }
 
@@ -94,10 +156,7 @@ builtin_initialize
     ref             := by exact decl_name%
     name            := `semireducible
     descr           := "semireducible declaration"
-    add             := fun declName stx attrKind => do
-      Attribute.Builtin.ensureNoArgs stx
-      let ns ← getCurrNamespace
-      modifyEnv fun env => setReducibilityStatusCore env declName .reducible attrKind ns
+    add             := addAttr .semireducible
     applicationTime := .afterTypeChecking
  }
 

tests/lean/run/1123.lean

@@ -3,11 +3,9 @@ class OpAssoc (op : α → α → α) : Prop where
 
 abbrev op_assoc (op : α → α → α) [self : OpAssoc op] := self.op_assoc
 
-@[reducible]
 structure SemigroupSig (α) where
   op : α → α → α
 
-@[reducible]
 structure SemiringSig (α) where
   add : α → α → α
   mul : α → α → α

tests/lean/run/reducibilityAttrValidation.lean

@@ -0,0 +1,93 @@
+def f (x : Nat) := x + 1
+
+/--
+error: failed to set `[semireducible]` for `f`, declarations are `[semireducible]` by default
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [semireducible] f
+
+attribute [reducible] f
+
+/--
+error: failed to set `[reducible]`, `f` is not currently `[semireducible]`, but `[reducible]`
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [reducible] f -- should fail because of double reducible setting
+
+-- "Reset" `f`
+set_option allowUnsafeReducibility true in
+attribute [semireducible] f
+
+attribute [irreducible] f
+
+/--
+error: failed to set `[irreducible]`, `f` is not currently `[semireducible]`, but `[irreducible]`
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [irreducible] f
+
+attribute [local semireducible] f
+
+/--
+error: failed to set `[local semireducible]`, `f` is currently `[semireducible]`, `[irreducible]` expected
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [local semireducible] f
+
+attribute [local irreducible] f
+
+/--
+error: failed to set `[local irreducible]`, `f` is currently `[irreducible]`, `[semireducible]` expected
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [local irreducible] f
+
+/--
+error: failed to set `[local reducible]` for `f`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [local reducible] f
+
+/--
+error: failed to set reducibility status, `Nat.add` has not been defined in this file, consider using the `local` modifier
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [semireducible] Nat.add
+
+/--
+error: failed to set reducibility status, `Nat.add` has not been defined in this file, consider using the `local` modifier
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [reducible] Nat.add
+
+/--
+error: failed to set reducibility status, `Nat.add` has not been defined in this file, consider using the `local` modifier
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [irreducible] Nat.add
+
+/-- error: scoped attributes must be used inside namespaces -/
+#guard_msgs in
+attribute [scoped reducible] Nat.add
+
+namespace Foo
+/--
+error: failed to set reducibility status for `Nat.add`, the `scoped` modifier is not recommended for this kind of attribute
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [scoped reducible] Nat.add
+
+set_option allowUnsafeReducibility true in
+attribute [scoped reducible] Nat.add
+
+end Foo

tests/lean/run/rewrite.lean

@@ -40,6 +40,7 @@ example : f 1 = f 2 := by
 example : f 1 = f 2 := by
   rw [s 1 3, s 3 4] -- Closes the goal via `rfl`
 
+set_option allowUnsafeReducibility true
 -- For the remaining tests we prevent `rfl` from closing the goal.
 attribute [irreducible] f
 
@@ -109,5 +110,3 @@ example : f 2 = f 0 := by
   -- we can return the problem to the user.
   rw [@t' 2 ?_]
   constructor
-
-

tests/lean/run/scopedLocalReducibility.lean

@@ -1,5 +1,5 @@
 @[irreducible] def f (x : Nat) := x + 1
-
+set_option allowUnsafeReducibility true
 /--
 error: type mismatch
   rfl

tests/pkg/builtin_attr/UserAttr/Tst.lean

@@ -3,7 +3,7 @@ import UserAttr.BlaAttr
 @[bar] def f (x : Nat) := x + 2
 @[bar] def g (x : Nat) := x + 1
 
-attribute [irreducible] myFun
+attribute [local irreducible] myFun
 
 /--
 error: type mismatch