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