diff --git a/library/init/core.lean b/library/init/core.lean
index 757c8744d7..cc4faddc7c 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -846,7 +846,7 @@ Exists.rec h₂ h₁
 
 /- Decidable -/
 
-@[macroInline] def Decidable.toBool (p : Prop) [h : Decidable p] : Bool :=
+@[inlineIfReduce, nospecialize] def Decidable.toBool (p : Prop) [h : Decidable p] : Bool :=
 Decidable.casesOn h (λ h₁, false) (λ h₂, true)
 
 instance beqOfEq {α : Type u} [DecidableEq α] : HasBeq α :=
diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp
index 93bffd5b8d..ca25137ddf 100644
--- a/src/library/compiler/erase_irrelevant.cpp
+++ b/src/library/compiler/erase_irrelevant.cpp
@@ -342,6 +342,10 @@ class erase_irrelevant_fn {
                 return visit_quot_mk(args);
             } else if (fn == get_quot_lift_name()) {
                 return visit_quot_lift(args);
+            } else if (fn == get_decidable_to_bool_name() && args.size() == 2) {
+                /* Decidable.toBool is the "identify" function since Decidable and Bool have
+                   the same runtime representation. */
+                return args[1];
             }
         }
         return visit_app_default(f, args);