fix: cache issue at instantiateBetaRevRange

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

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

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