diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean
index 706908fa92a7..b543ffffa8cb 100644
--- a/src/Lean/Compiler/IR/Basic.lean
+++ b/src/Lean/Compiler/IR/Basic.lean
@@ -24,12 +24,12 @@ abbrev Index := Nat
 /-- Variable identifier -/
 structure VarId where
   idx : Index
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 /-- Join point identifier -/
 structure JoinPointId where
   idx : Index
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 abbrev Index.lt (a b : Index) : Bool := a < b
 
@@ -83,7 +83,7 @@ inductive IRType where
   | irrelevant | object | tobject
   | struct (leanTypeName : Option Name) (types : Array IRType) : IRType
   | union (leanTypeName : Name) (types : Array IRType) : IRType
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 namespace IRType
 
@@ -236,7 +236,7 @@ structure Param where
   x : VarId
   borrow : Bool
   ty : IRType
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 @[export lean_ir_mk_param]
 def mkParam (x : VarId) (borrow : Bool) (ty : IRType) : Param := ⟨x, borrow, ty⟩
diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean
index e7def8dd01cb..ff0cd416544f 100644
--- a/src/Lean/Compiler/IR/Borrow.lean
+++ b/src/Lean/Compiler/IR/Borrow.lean
@@ -258,7 +258,8 @@ def preserveTailCall (x : VarId) (v : Expr) (b : FnBody) : M Unit := do
   let ctx ← read
   match v, b with
   | (Expr.fap g ys), (FnBody.ret (Arg.var z)) =>
-    if ctx.decls.any (·.name == g) && x == z then
+    -- NOTE: we currently support TCO for self-calls only
+    if ctx.currFn == g && x == z then
       let ps ← getParamInfo (ParamMap.Key.decl g)
       ownParamsUsingArgs ys ps
   | _, _ => pure ()
diff --git a/tests/lean/4240.lean b/tests/lean/4240.lean
new file mode 100644
index 000000000000..371651dbb031
--- /dev/null
+++ b/tests/lean/4240.lean
@@ -0,0 +1,25 @@
+/-! Check for bug accidentally marking `m` as owned. -/
+
+class MyClass (α : Type u) where
+
+instance : MyClass Nat where
+
+inductive MyOption (α : Type u) where
+  | none
+  | some (key : α)
+
+namespace MyOption
+
+def isSomeWithInstance [MyClass α] : MyOption α → Bool
+  | none => false
+  | some _ => true
+
+def isSome : MyOption α → Bool
+  | none => false
+  | some _ => true
+
+end MyOption
+
+set_option trace.compiler.ir.result true in
+def isSomeWithInstanceNat (m : { m : Array (MyOption Nat) // 0 < m.size }) : Bool :=
+  (m.1.uget 0 m.2).isSomeWithInstance
diff --git a/tests/lean/4240.lean.expected.out b/tests/lean/4240.lean.expected.out
new file mode 100644
index 000000000000..174456c8f3ed
--- /dev/null
+++ b/tests/lean/4240.lean.expected.out
@@ -0,0 +1,26 @@
+
+[result]
+def MyOption.isSomeWithInstance._at.isSomeWithInstanceNat._spec_1 (x_1 : @& obj) : u8 :=
+  case x_1 : obj of
+  MyOption.none →
+    let x_2 : u8 := 0;
+    ret x_2
+  MyOption.some →
+    let x_3 : u8 := 1;
+    ret x_3
+def isSomeWithInstanceNat (x_1 : @& obj) : u8 :=
+  let x_2 : usize := 0;
+  let x_3 : obj := Array.uget ◾ x_1 x_2 ◾;
+  let x_4 : u8 := MyOption.isSomeWithInstance._at.isSomeWithInstanceNat._spec_1 x_3;
+  dec x_3;
+  ret x_4
+def MyOption.isSomeWithInstance._at.isSomeWithInstanceNat._spec_1._boxed (x_1 : obj) : obj :=
+  let x_2 : u8 := MyOption.isSomeWithInstance._at.isSomeWithInstanceNat._spec_1 x_1;
+  dec x_1;
+  let x_3 : obj := box x_2;
+  ret x_3
+def isSomeWithInstanceNat._boxed (x_1 : obj) : obj :=
+  let x_2 : u8 := isSomeWithInstanceNat x_1;
+  dec x_1;
+  let x_3 : obj := box x_2;
+  ret x_3
\ No newline at end of file
diff --git a/tests/lean/603.lean b/tests/lean/603.lean
deleted file mode 100644
index 75b1f4a75e79..000000000000
--- a/tests/lean/603.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-set_option trace.compiler.ir.result true
-
--- should be tail calls
-mutual
-
-  partial def even (a : Nat) : Nat := if a == 0 then 1 else odd (a - 1)
-
-  partial def odd (a : Nat) : Nat := if a == 0 then 0 else even (a - 1)
-
-end