From 770649ce1d3ba48b226e81240be7eeb6b2c037eb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Dec 2019 10:57:19 -0800
Subject: [PATCH] refactor: do not save/restore cache at "telescope" methods

@kha @dselsam FYI

The original motivation for saving/restoring the cache was not
correctness, but cache size management. When we go inside a binder
using the telescope methods, we extend the local context with new fresh
free variables, execute the action `k` using the new extended local
context, and then restore it. Any cached result containing these
fresh variables is dead after executing `k`. So, `savingCache` here
could be viewed as a "checkpoint". However, it also removes any
cached entry that does not contain the new fresh variables.
I found this inconvenient in practice, and it is the wrong choice
in a few cases. Example: we have a `forall` expr (aka arrow), and use a
telescope to go inside, and then invoke TC. If the telescope uses
`savingCache`, we lose the cached TC instance witness. This is
wasteful since the witness often doesn't even depend on the new fresh
free variables created by the telescope.
Thus, this commit removes the `savingCache` occurrences from
the "telescope" methods. Users may still manually use it if
they think it is appropriate. That is, they can write
```lean
savingCache $ forallTelescope e $ fun xs body => <code>
```
if they really want to discard any new cache entry created while
executing `<code>`.
---
 src/Init/Lean/Meta/Basic.lean | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index 26c60d931d..c786a6d54c 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -527,10 +527,9 @@ resettingSynthInstanceCache $
     (isClassExpensive : Expr → MetaM (Option Name))
     (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) : MetaM α :=
 do newType ← whnf type;
-   if newType.isForall then
-     savingCache $ do
-       lctx ← getLCtx;
-       forallTelescopeReducingAuxAux isClassExpensive true maxFVars? k lctx #[] 0 newType
+   if newType.isForall then do
+     lctx ← getLCtx;
+     forallTelescopeReducingAuxAux isClassExpensive true maxFVars? k lctx #[] 0 newType
    else
      k #[] type
 
@@ -548,9 +547,8 @@ partial def isClassExpensive : Expr → MetaM (Option Name)
   This combinator will declare local declarations, create free variables for them,
   execute `k` with updated local context, and make sure the cache is restored after executing `k`. -/
 @[inline] def forallTelescope {α} (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α :=
-savingCache $ do
-  lctx ← getLCtx;
-  forallTelescopeReducingAuxAux isClassExpensive false none k lctx #[] 0 type
+do lctx ← getLCtx;
+   forallTelescopeReducingAuxAux isClassExpensive false none k lctx #[] 0 type
 
 /--
   Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,
@@ -597,9 +595,8 @@ do c? ← isClassQuick type;
 /-- Similar to `forallTelescope` but for lambda and let expressions. -/
 @[specialize] def lambdaTelescope {α}
     (e : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α :=
-savingCache $ do
-  lctx ← getLCtx;
-  lambdaTelescopeAux k lctx #[] 0 e
+do lctx ← getLCtx;
+   lambdaTelescopeAux k lctx #[] 0 e
 
 private partial def forallMetaTelescopeReducingAux
     (reducing? : Bool) (maxMVars? : Option Nat)