From 7db4f60e505dd866d258adaa32fe394261d14bc3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Mar 2019 15:24:51 -0700
Subject: [PATCH] feat(library/init/core): eagerly expanding `Decidable.toBool`
 seems to be a bad idea

After we erase types and proofs, `Decidable.toBool` can be replaced with
the identity function since `Decidable A` and `Bool` have the same
runtime representation. By eagerly expanding `toBool`, we introduce
unnecessary `cases` expressions.
---
 library/init/core.lean                    | 2 +-
 src/library/compiler/erase_irrelevant.cpp | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)

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);