From 0f8c6ca797c486a4efca1daf8bf5989c815ce71c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 2 May 2021 16:58:56 -0700
Subject: [PATCH] fix: cache issue at `instantiateBetaRevRange`

---
 src/Lean/Meta/InferType.lean            | 4 ++--
 tests/lean/cacheIssue.lean              | 7 +++++++
 tests/lean/cacheIssue.lean.expected.out | 3 +++
 3 files changed, 12 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/cacheIssue.lean
 create mode 100644 tests/lean/cacheIssue.lean.expected.out

diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index 6f8235b51f..8377d68d74 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -29,11 +29,11 @@ partial def Expr.instantiateBetaRevRange (e : Expr) (start : Nat) (stop : Nat) (
   else
     e
 where
-  visit (e : Expr) (offset : Nat) : MonadStateCacheT (Expr × Nat) Expr Id Expr :=
+  visit (e : Expr) (offset : Nat) : MonadStateCacheT (ExprStructEq × Nat) Expr Id Expr :=
     if offset >= e.looseBVarRange then
       -- `e` doesn't have free variables
       return e
-    else checkCache (e, offset) fun _ => do
+    else checkCache ({ val := e : ExprStructEq }, offset) fun _ => do
       match e with
       | Expr.forallE _ d b _   => return e.updateForallE! (← visit d offset) (← visit b (offset+1))
       | Expr.lam _ d b _       => return e.updateLambdaE! (← visit d offset) (← visit b (offset+1))
diff --git a/tests/lean/cacheIssue.lean b/tests/lean/cacheIssue.lean
new file mode 100644
index 0000000000..21c9ec92d5
--- /dev/null
+++ b/tests/lean/cacheIssue.lean
@@ -0,0 +1,7 @@
+structure Foo (A B : Type) := f : Unit -> A
+def foo (P) : Foo ((p : P) -> Nat) ({p : P} -> Nat) := ⟨λ _ _ => 0⟩
+def bar (P) : Foo ((p : P) -> Nat) ({p : P} -> Int) := ⟨λ _ _ => 0⟩
+
+#check foo Bool
+#check (foo Bool).f -- (foo Bool).f : Unit → Bool → Nat
+#check (bar Bool).f -- (bar Bool).f : Unit → Bool → Nat
diff --git a/tests/lean/cacheIssue.lean.expected.out b/tests/lean/cacheIssue.lean.expected.out
new file mode 100644
index 0000000000..9ac1aecd82
--- /dev/null
+++ b/tests/lean/cacheIssue.lean.expected.out
@@ -0,0 +1,3 @@
+foo Bool : Foo (Bool → Nat) ({p : Bool} → Nat)
+(foo Bool).f : Unit → Bool → Nat
+(bar Bool).f : Unit → Bool → Nat