diff --git a/library/init/lean/compiler/ir/basic.lean b/library/init/lean/compiler/ir/basic.lean
index 915d72ecf9..0279ddcdd6 100644
--- a/library/init/lean/compiler/ir/basic.lean
+++ b/library/init/lean/compiler/ir/basic.lean
@@ -225,6 +225,7 @@ inductive FnBody
 | inc (x : VarId) (n : Nat) (c : Bool) (b : FnBody)
 /- RC decrement for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not. -/
 | dec (x : VarId) (n : Nat) (c : Bool) (b : FnBody)
+| del (x : VarId) (b : FnBody)
 | mdata (d : MData) (b : FnBody)
 | case (tid : Name) (x : VarId) (cs : Array (AltCore FnBody))
 | ret (x : Arg)
@@ -268,6 +269,7 @@ def FnBody.body : FnBody → FnBody
 | (FnBody.release _ _ b)    := b
 | (FnBody.inc _ _ _ b)      := b
 | (FnBody.dec _ _ _ b)      := b
+| (FnBody.del _ b)          := b
 | (FnBody.mdata _ b)        := b
 | other                     := other
 
@@ -280,6 +282,7 @@ def FnBody.setBody : FnBody → FnBody → FnBody
 | (FnBody.release x i _)    b := FnBody.release x i b
 | (FnBody.inc x n c _)      b := FnBody.inc x n c b
 | (FnBody.dec x n c _)      b := FnBody.dec x n c b
+| (FnBody.del x _)          b := FnBody.del x b
 | (FnBody.mdata d _)        b := FnBody.mdata d b
 | other                     b := other
 
@@ -535,6 +538,7 @@ partial def FnBody.alphaEqv : IndexRenaming → FnBody → FnBody → Bool
 | ρ (FnBody.release x₁ i₁ b₁)       (FnBody.release x₂ i₂ b₂)         := x₁ =[ρ]= x₂ && i₁ == i₂ && FnBody.alphaEqv ρ b₁ b₂
 | ρ (FnBody.inc x₁ n₁ c₁ b₁)        (FnBody.inc x₂ n₂ c₂ b₂)          := x₁ =[ρ]= x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂
 | ρ (FnBody.dec x₁ n₁ c₁ b₁)        (FnBody.dec x₂ n₂ c₂ b₂)          := x₁ =[ρ]= x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂
+| ρ (FnBody.del x₁ b₁)              (FnBody.del x₂ b₂)                := x₁ =[ρ]= x₂ && FnBody.alphaEqv ρ b₁ b₂
 | ρ (FnBody.mdata m₁ b₁)            (FnBody.mdata m₂ b₂)              := m₁ == m₂ && FnBody.alphaEqv ρ b₁ b₂
 | ρ (FnBody.case n₁ x₁ alts₁)       (FnBody.case n₂ x₂ alts₂)         := n₁ == n₂ && x₁ =[ρ]= x₂ && Array.isEqv alts₁ alts₂ (λ alt₁ alt₂,
    match alt₁, alt₂ with
diff --git a/library/init/lean/compiler/ir/checker.lean b/library/init/lean/compiler/ir/checker.lean
index 4af64cd935..385d854394 100644
--- a/library/init/lean/compiler/ir/checker.lean
+++ b/library/init/lean/compiler/ir/checker.lean
@@ -110,6 +110,7 @@ partial def checkFnBody : FnBody → M Unit
 | (FnBody.release x _ b)    := checkVar x *> checkFnBody b
 | (FnBody.inc x _ _ b)      := checkVar x *> checkFnBody b
 | (FnBody.dec x _ _ b)      := checkVar x *> checkFnBody b
+| (FnBody.del x b)          := checkVar x *> checkFnBody b
 | (FnBody.mdata _ b)        := checkFnBody b
 | (FnBody.jmp j ys)         := checkJP j *> checkArgs ys
 | (FnBody.ret x)            := checkArg x
diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean
index 7635c5b29d..53ed7de581 100644
--- a/library/init/lean/compiler/ir/emitcpp.lean
+++ b/library/init/lean/compiler/ir/emitcpp.lean
@@ -322,6 +322,9 @@ emit "(" *> emit x,
 when (n != 1) (emit ", " *> emit n),
 emitLn ");"
 
+def emitDel (x : VarId) : M Unit :=
+do emit "lean::free_heap_obj(", emit x, emitLn ");"
+
 def emitRelease (x : VarId) (i : Nat) : M Unit :=
 do emit "lean::cnstr_release(", emit x, emit ", ", emit i, emitLn ");"
 
@@ -587,6 +590,7 @@ partial def emitBlock (emitBody : FnBody → M Unit) : FnBody → M Unit
 | (FnBody.vdecl x t v b)    := do isTail ← isTailCall x v b, if isTail then emitTailCall v else emitVDecl x t v *> emitBlock b
 | (FnBody.inc x n c b)      := emitInc x n c *> emitBlock b
 | (FnBody.dec x n c b)      := emitDec x n c *> emitBlock b
+| (FnBody.del x b)          := emitDel x *> emitBlock b
 | (FnBody.release x i b)    := emitRelease x i *> emitBlock b
 | (FnBody.set x i y b)      := emitSet x i y *> emitBlock b
 | (FnBody.uset x i y b)     := emitUSet x i y *> emitBlock b
diff --git a/library/init/lean/compiler/ir/format.lean b/library/init/lean/compiler/ir/format.lean
index fad407abfe..5ce356241a 100644
--- a/library/init/lean/compiler/ir/format.lean
+++ b/library/init/lean/compiler/ir/format.lean
@@ -86,6 +86,7 @@ partial def formatFnBody (indent : Nat := 2) : FnBody → Format
 | (FnBody.release x i b)     := "release " ++ format x ++ "[" ++ format i ++ "];" ++ Format.line ++ formatFnBody b
 | (FnBody.inc x n c b)       := "inc" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ formatFnBody b
 | (FnBody.dec x n c b)       := "dec" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ formatFnBody b
+| (FnBody.del x b)           := "del " ++ format x ++ ";" ++ Format.line ++ formatFnBody b
 | (FnBody.mdata d b)         := "mdata " ++ format d ++ ";" ++ Format.line ++ formatFnBody b
 | (FnBody.case tid x cs)     := "case " ++ format x ++ " of" ++ cs.foldl (λ r c, r ++ Format.line ++ formatAlt formatFnBody indent c) Format.nil
 | (FnBody.jmp j ys)          := "jmp " ++ format j ++ formatArray ys
diff --git a/library/init/lean/compiler/ir/freevars.lean b/library/init/lean/compiler/ir/freevars.lean
index 1a76c39baf..4a85dbec74 100644
--- a/library/init/lean/compiler/ir/freevars.lean
+++ b/library/init/lean/compiler/ir/freevars.lean
@@ -66,6 +66,7 @@ partial def collectFnBody : FnBody → Collector
 | (FnBody.release x _ b)    := collectVar x; collectFnBody b
 | (FnBody.inc x _ _ b)      := collectVar x; collectFnBody b
 | (FnBody.dec x _ _ b)      := collectVar x; collectFnBody b
+| (FnBody.del x b)          := collectVar x; collectFnBody b
 | (FnBody.mdata _ b)        := collectFnBody b
 | (FnBody.case _ x alts)    := collectVar x; collectAlts collectFnBody alts
 | (FnBody.jmp j ys)         := collectJP j; collectArgs ys
@@ -160,6 +161,7 @@ partial def collectFnBody : FnBody → Collector
 | (FnBody.release x _ b)    := collectVar x; collectFnBody b
 | (FnBody.inc x _ _ b)      := collectVar x; collectFnBody b
 | (FnBody.dec x _ _ b)      := collectVar x; collectFnBody b
+| (FnBody.del x b)          := collectVar x; collectFnBody b
 | (FnBody.mdata _ b)        := collectFnBody b
 | (FnBody.case _ x alts)    := collectVar x; collectAlts collectFnBody alts
 | (FnBody.jmp j ys)         := collectJP j; collectArgs ys
@@ -217,6 +219,7 @@ partial def visitFnBody (w : Index) : FnBody → Bool
 | (FnBody.release x _ b)    := visitVar w x || visitFnBody b
 | (FnBody.inc x _ _ b)      := visitVar w x || visitFnBody b
 | (FnBody.dec x _ _ b)      := visitVar w x || visitFnBody b
+| (FnBody.del x b)          := visitVar w x || visitFnBody b
 | (FnBody.mdata _ b)        := visitFnBody b
 | (FnBody.jmp j ys)         := visitJP w j || visitArgs w ys
 | (FnBody.ret x)            := visitArg w x
diff --git a/library/init/lean/compiler/ir/livevars.lean b/library/init/lean/compiler/ir/livevars.lean
index ce9ea28acb..e4ca0ad2a1 100644
--- a/library/init/lean/compiler/ir/livevars.lean
+++ b/library/init/lean/compiler/ir/livevars.lean
@@ -55,6 +55,7 @@ partial def visitFnBody (w : Index) : FnBody → M Bool
 | (FnBody.release x _ b)    := visitVar w x <||> visitFnBody b
 | (FnBody.inc x _ _ b)      := visitVar w x <||> visitFnBody b
 | (FnBody.dec x _ _ b)      := visitVar w x <||> visitFnBody b
+| (FnBody.del x b)          := visitVar w x <||> visitFnBody b
 | (FnBody.mdata _ b)        := visitFnBody b
 | (FnBody.jmp j ys)         := visitArgs w ys <||> do {
     ctx ← get,
@@ -141,6 +142,7 @@ partial def collectFnBody : FnBody → JPLiveVarMap → Collector
 | (FnBody.release x _ b)    m := collectVar x >> collectFnBody b m
 | (FnBody.inc x _ _ b)      m := collectVar x >> collectFnBody b m
 | (FnBody.dec x _ _ b)      m := collectVar x >> collectFnBody b m
+| (FnBody.del x b)          m := collectVar x >> collectFnBody b m
 | (FnBody.mdata _ b)        m := collectFnBody b m
 | (FnBody.ret x)            m := collectArg x
 | (FnBody.case _ x alts)    m := collectVar x >> collectArray alts (λ alt, collectFnBody alt.body m)
diff --git a/library/init/lean/compiler/ir/normids.lean b/library/init/lean/compiler/ir/normids.lean
index c415ab107d..52de9a603b 100644
--- a/library/init/lean/compiler/ir/normids.lean
+++ b/library/init/lean/compiler/ir/normids.lean
@@ -108,6 +108,7 @@ partial def normFnBody : FnBody → N FnBody
 | (FnBody.release x i b)     := do x ← normVar x, FnBody.release x i <$> normFnBody b
 | (FnBody.inc x n c b)       := do x ← normVar x, FnBody.inc x n c <$> normFnBody b
 | (FnBody.dec x n c b)       := do x ← normVar x, FnBody.dec x n c <$> normFnBody b
+| (FnBody.del x b)           := do x ← normVar x, FnBody.del x <$> normFnBody b
 | (FnBody.mdata d b)         := FnBody.mdata d <$> normFnBody b
 | (FnBody.case tid x alts)   := do
   x ← normVar x,