doc: remove transparency.md (design still in flux)

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Init/MetaTypes.lean

@@ -25,18 +25,70 @@ structure Module where
 namespace Meta
 
 /--
-Which constants should be unfolded?
+Controls which constants `isDefEq` (definitional equality) and `whnf` (weak head normal form)
+are allowed to unfold.
+
+## Background: "try-hard" vs "speculative" modes
+
+During **type checking of user input**, we assume the input is most likely correct, and we want
+Lean to try hard before reporting a failure. Here, it is fine to unfold `[semireducible]` definitions
+(the `.default` setting).
+
+During **proof automation** (`simp`, `rw`, type class resolution), we perform many speculative
+`isDefEq` calls — most of which *fail*. In this setting, we do *not* want to try hard: unfolding
+too many definitions is a performance footgun. This is why `.reducible` exists.
+
+## The transparency hierarchy
+
+The levels form a linear order: `none < reducible < instances < default < all`.
+Each level unfolds everything the previous level does, plus more:
+
+- **`reducible`**: Only unfolds `[reducible]` definitions. Used for speculative `isDefEq` checks
+  (e.g., discrimination tree lookups in `simp`, type class resolution). Think of `[reducible]` as
+  `[inline]` for type checking and indexing.
+
+- **`instances`**: Also unfolds `[instance_reducible]` definitions. Instance diamonds are common:
+  for example, `Add Nat` can come from a direct instance or via `Semiring`. These instances are all
+  definitionally equal but structurally different, so `isDefEq` must unfold them to confirm equality.
+  However, instances must not be *eagerly* reduced (they become huge terms), and discrimination trees
+  do not index instances. This makes `.instances` safe for speculative checks involving instance
+  arguments without the performance cost of `.default`.
+
+- **`default`**: Also unfolds `[semireducible]` definitions (anything not `[irreducible]`).
+  Used for type checking user input where we want to try hard.
+
+- **`all`**: Also unfolds `[irreducible]` definitions. Rarely used.
+
+## Implicit arguments and transparency
+
+When proof automation (e.g., `simp`, `rw`) applies a lemma, explicit arguments are checked at the
+caller's transparency (typically `.reducible`). But implicit arguments are often "invisible" to the
+user — if a lemma fails to apply because of an implicit argument mismatch, the user is confused.
+Historically, Lean bumped transparency to `.default` for implicit arguments, but this eventually
+became a performance bottleneck in Mathlib. The option `backward.isDefEq.respectTransparency`
+(default: `true`) disables this bump. Instead, instance-implicit arguments (`[..]`) are checked at
+`.instances`, and other implicit arguments are checked at the caller's transparency.
+
+See also: `ReducibilityStatus`, `backward.isDefEq.respectTransparency`,
+`backward.whnf.reducibleClassField`.
 -/
 inductive TransparencyMode where
   /-- Unfolds all constants, even those tagged as `@[irreducible]`. -/
   | all
-  /-- Unfolds all constants except those tagged as `@[irreducible]`. -/
+  /-- Unfolds all constants except those tagged as `@[irreducible]`. Used for type checking
+  user-written terms where we expect the input to be correct and want to try hard. -/
   | default
-  /-- Unfolds only constants tagged with the `@[reducible]` attribute. -/
+  /-- Unfolds only constants tagged with the `@[reducible]` attribute. Used for speculative
+  `isDefEq` in proof automation (`simp`, `rw`, type class resolution) where most checks fail
+  and we must not try too hard. -/
   | reducible
-  /-- Unfolds reducible constants and constants tagged with the `@[instance]` attribute. -/
+  /-- Unfolds reducible constants and constants tagged with `@[instance_reducible]`.
+  Used for checking instance-implicit arguments during proof automation, and for unfolding
+  class projections applied to instances. Instance diamonds (e.g., `Add Nat` from a direct instance
+  vs from `Semiring`) are definitionally equal but structurally different, so `isDefEq` must unfold
+  them. -/
   | instances
-  /-- Do not unfold anything -/
+  /-- Do not unfold anything. -/
   | none
   deriving Inhabited, BEq
 

src/Lean/Meta/ExprDefEq.lean

@@ -21,6 +21,25 @@ register_builtin_option backward.isDefEq.lazyWhnfCore : Bool := {
   descr    := "specifies transparency mode when normalizing constraints of the form `(f a).i =?= s`, if `true` only reducible definitions and instances are unfolded when reducing `f a`. Otherwise, the default setting is used"
 }
 
+/--
+Controls how implicit arguments are handled in `isDefEq` during proof automation.
+
+**Original behavior (`false`):** When `simp`, `rw`, or similar tactics apply a lemma, explicit
+arguments are matched at the caller's transparency (typically `.reducible`). But implicit arguments
+are "invisible" to the user — they don't choose them directly. If a lemma fails to apply because
+an implicit argument doesn't match at `.reducible`, the user sees a confusing failure with no
+obvious cause. To avoid this, we originally bumped transparency to `.default` for implicit arguments,
+so that `isDefEq` would try harder and unfold semireducible definitions to make them match.
+
+**Why `true` is now the default:** The transparency bump meant that every speculative `isDefEq` call
+in proof automation could trigger expensive unfolding of semireducible definitions on implicit
+arguments — and most of these calls *fail*. This eventually became a performance bottleneck in
+Mathlib. With `true`, implicit arguments are checked at the caller's transparency, except
+instance-implicit arguments (`[..]`) which are checked at `TransparencyMode.instances` (to resolve
+instance diamonds).
+
+See `isDefEqArgs` for the implementation and `TransparencyMode` for the overall design.
+-/
 register_builtin_option backward.isDefEq.respectTransparency : Bool := {
   defValue := true
   descr    := "if true (the default), do not bump transparency to `.default` \
@@ -315,8 +334,12 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
   let respectTransparency := backward.isDefEq.respectTransparency.get (← getOptions)
   for i in postponedImplicit do
     /- Second pass: unify implicit arguments.
-       In the second pass, we make sure we are unfolding at
-       least non reducible definitions (default setting). -/
+       When `respectTransparency` is `false` (old behavior), we bump to `.default` so that
+       semireducible definitions are unfolded — the rationale being that users don't think about
+       implicit arguments and expect them to "just work."
+       When `respectTransparency` is `true` (new behavior), we respect the caller's transparency
+       for non-instance implicits, and use `.instances` for instance-implicit arguments to resolve
+       instance diamonds. See `backward.isDefEq.respectTransparency` for the motivation. -/
     let a₁   := args₁[i]!
     let a₂   := args₂[i]!
     let info := finfo.paramInfo[i]!

src/Lean/Meta/GetUnfoldableConst.lean

@@ -9,6 +9,10 @@ public import Lean.Meta.Basic
 public section
 namespace Lean.Meta
 
+/--
+Implements the `TransparencyMode` hierarchy for unfolding decisions.
+See `TransparencyMode` and `ReducibilityStatus` for the design rationale.
+-/
 private def canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
   match cfg.transparency with
   | .none => return false

src/Lean/Meta/WHNF.lean

@@ -809,6 +809,19 @@ partial def unfoldProjInstWhenInstances? (e : Expr) : MetaM (Option Expr) := do
   else
     return none
 
+/--
+When `true`, unfolding a `[reducible]` class field at `TransparencyMode.reducible` also unfolds
+the associated instance projection at `TransparencyMode.instances`.
+
+**Motivation:** Consider `a ≤ b` where `a b : Nat` and `LE.le` is `[reducible]`. Unfolding `LE.le`
+gives `instLENat.1 a b`, which is stuck because `instLENat` is `[instance_reducible]` (not
+`[reducible]`). Similarly, `stM m (ExceptT ε m) α` unfolds to an instance projection that is stuck
+at `.reducible`. Without this option, marking a class field as `[reducible]` is pointless when the
+instance providing it is only `[instance_reducible]`. This option makes the `[reducible]` annotation
+on class fields work as the user expects by temporarily bumping to `.instances` for the projection.
+
+See `unfoldDefault` for the implementation.
+-/
 register_builtin_option backward.whnf.reducibleClassField : Bool := {
   defValue := false
   descr    := "enables better support for unfolding type class fields marked as `[reducible]`"

src/Lean/ReducibilityAttrs.lean

@@ -10,7 +10,21 @@ public section
 namespace Lean
 
 /--
-Reducibility status for a definition.
+Reducibility status for a definition. Controls when `isDefEq` and `whnf` are allowed to unfold it.
+See `TransparencyMode` for the full design rationale.
+
+- **`reducible`**: Unfolded at `TransparencyMode.reducible` or above. Reducible definitions still
+  appear in user-facing terms, but are eagerly unfolded when indexing terms into discrimination
+  trees (`simp`, type class resolution) and in `grind`. Think of it as `[inline]` for indexing.
+  Suitable for abbreviations and definitions that should be transparent to proof automation.
+- **`instanceReducible`**: Unfolded at `TransparencyMode.instances` or above. Used for type class
+  instances. Instances cannot be eagerly reduced (they expand into large terms), but must be
+  unfoldable to resolve instance diamonds (e.g., `Add Nat` via direct instance vs via `Semiring`).
+- **`semireducible`**: The default. Unfolded at `TransparencyMode.default` or above. Used for
+  ordinary definitions. Suitable for user-written code where `isDefEq` should try hard during
+  type checking, but not during speculative proof automation.
+- **`irreducible`**: Only unfolded at `TransparencyMode.all`. The definition body is effectively
+  hidden from `isDefEq` in normal usage.
 -/
 inductive ReducibilityStatus where
   | reducible | semireducible | irreducible | instanceReducible
@@ -177,6 +191,18 @@ builtin_initialize
     applicationTime := .afterTypeChecking
  }
 
+/--
+Marks a definition as `[instance_reducible]`, meaning it is unfolded at
+`TransparencyMode.instances` or above but *not* at `TransparencyMode.reducible`.
+
+This attribute decouples whether a definition participates in type class resolution
+(the `[instance]` attribute) from its transparency. The `instance` command automatically
+adds both `[instance]` and `[instance_reducible]`.
+
+When using `attribute [instance]` on an existing definition, you typically also need
+`attribute [instance_reducible]` so that `isDefEq` can unfold the definition when resolving
+instance diamonds.
+-/
 builtin_initialize
   registerBuiltinAttribute {
     ref             := by exact decl_name%