From 2fff4c42b71fc1d451bf968a7f1a07d10993f2eb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 26 Jan 2022 11:54:21 -0800
Subject: [PATCH] fix: make sure irreducible constants are not unfolded when
 using the default reducibility setting

---
 src/Lean/Meta/GetConst.lean          |  2 +-
 src/Lean/ReducibilityAttrs.lean      | 13 +++++++++----
 tests/lean/run/irreducibleIssue.lean | 20 ++++++++++++++++++++
 3 files changed, 30 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/irreducibleIssue.lean

diff --git a/src/Lean/Meta/GetConst.lean b/src/Lean/Meta/GetConst.lean
index 7dc792ff2d..bf82908330 100644
--- a/src/Lean/Meta/GetConst.lean
+++ b/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
diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean
index 84a05d74a9..d834dd8136 100644
--- a/src/Lean/ReducibilityAttrs.lean
+++ b/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
diff --git a/tests/lean/run/irreducibleIssue.lean b/tests/lean/run/irreducibleIssue.lean
new file mode 100644
index 0000000000..42cd5d7899
--- /dev/null
+++ b/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 : ℝ)