fix: make sure irreducible constants are not unfolded when using the default reducibility setting

src/Lean/Meta/GetConst.lean

@@ -10,7 +10,7 @@ namespace Lean.Meta
 private def canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
   match cfg.transparency with
   | TransparencyMode.all => return true
-  | TransparencyMode.default => return true
+  | TransparencyMode.default => return !(← isIrreducible info.name)
   | m =>
     if (← isReducible info.name) then
       return true

src/Lean/ReducibilityAttrs.lean

@@ -29,18 +29,23 @@ def setReducibilityStatusImp (env : Environment) (declName : Name) (s : Reducibi
   | Except.ok env => env
   | _ => env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails
 
-def getReducibilityStatus {m} [Monad m] [MonadEnv m] (declName : Name) : m ReducibilityStatus := do
+def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m ReducibilityStatus := do
   return getReducibilityStatusImp (← getEnv) declName
 
-def setReducibilityStatus {m} [Monad m] [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit := do
+def setReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit := do
   modifyEnv fun env => setReducibilityStatusImp env declName s
 
-def setReducibleAttribute {m} [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
+def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
   setReducibilityStatus declName ReducibilityStatus.reducible
 
-def isReducible {m} [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
+def isReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   match (← getReducibilityStatus declName) with
   | ReducibilityStatus.reducible => true
   | _ => false
 
+def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
+  match (← getReducibilityStatus declName) with
+  | ReducibilityStatus.irreducible => true
+  | _ => false
+
 end Lean

tests/lean/run/irreducibleIssue.lean

@@ -0,0 +1,20 @@
+class Trait (X : Type u) where
+  R : Type v
+
+attribute [reducible] Trait.R
+
+class SemiInner (X : Type u) (R : Type v) where
+  semiInner : X → X → R
+
+@[reducible] instance (X) (R : Type u) [SemiInner X R] : Trait X := ⟨R⟩
+
+def norm {X} [Trait X] [inst : SemiInner X (Trait.R X)] (x : X) : Trait.R X := SemiInner.semiInner x x
+
+section Real
+  def ℝ := Float
+  instance : SemiInner ℝ ℝ := ⟨λ x y : Float => x * y⟩
+
+  attribute [irreducible] ℝ
+
+  variable (x : ℝ)
+  #check (norm x : ℝ)