From 87db970cfa842176e9ecfea25366f1ae914f40a1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 7 Sep 2020 08:42:39 -0700
Subject: [PATCH] chore: control code size explosion

---
 src/Lean/Meta/Basic.lean | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 39d9bc670c..20fc8b2b4c 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -667,17 +667,23 @@ forallTelescopeReducingAuxAux isClassExpensive? false none k lctx #[] 0 type
 def forallTelescope {α} (type : Expr) (k : Array Expr → Expr → n α) : n α :=
 map2MetaM (fun _ k => forallTelescopeImp type k) k
 
+@[noinline] private def forallTelescopeReducingImp {α} (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α :=
+forallTelescopeReducingAux isClassExpensive? type none k
+
 /--
   Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,
   it reduces `A` and continues bulding the telescope if it is a `forall`. -/
 def forallTelescopeReducing {α} (type : Expr) (k : Array Expr → Expr → n α) : n α :=
-map2MetaM (fun _ k => forallTelescopeReducingAux isClassExpensive? type none k) k
+map2MetaM (fun _ k => forallTelescopeReducingImp type k) k
+
+@[noinline] private def forallBoundedTelescopeImp {α} (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) : MetaM α :=
+forallTelescopeReducingAux isClassExpensive? type maxFVars? k
 
 /--
   Similar to `forallTelescopeReducing`, stops constructing the telescope when
   it reaches size `maxFVars`. -/
 def forallBoundedTelescope {α} (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) : n α :=
-map2MetaM (fun _ k => forallTelescopeReducingAux isClassExpensive? type maxFVars? k) k
+map2MetaM (fun _ k => forallBoundedTelescopeImp type maxFVars? k) k
 
 /-- Similar to `forallTelescopeAuxAux` but for lambda and let expressions. -/
 private partial def lambdaTelescopeAux {α}