Reference counting instructions for cases

Stream: lean4

[Mario Carneiro]

I don't have a very good understanding of the reference counting instructions so this may be a misunderstanding on my part, but I think this might be a bug:

set_option trace.compiler.ir.result true in
def foo (x : Option Unit × Unit) : Unit × Unit :=
  match x.1 with
  | none => ((), ())
  | some _ => ((), x.2)

def foo (x_1 : obj) : obj :=
  let x_2 : obj := proj[0] x_1;
  inc x_2;
  case x_2 : obj of
  Option.none →
    dec x_1;
    let x_3 : obj := foo._closed_1;
    ret x_3
  Option.some →
    dec x_2;
    let x_4 : u8 := isShared x_1;
    case x_4 : u8 of
    Bool.false →
      let x_5 : obj := proj[0] x_1;
      dec x_5;
      let x_6 : obj := ctor_0[PUnit.unit];
      set x_1[0] := x_6;
      ret x_1
    Bool.true →
      let x_7 : obj := proj[1] x_1;
      inc x_7;
      dec x_1;
      let x_8 : obj := ctor_0[PUnit.unit];
      let x_9 : obj := ctor_0[Prod.mk] x_8 x_7;
      ret x_9

This has been minimized, but the part I want to point out is that in the none case, inc x_2 is called but there is no corresponding dec x_2 later. This only seems to happen for nullary variants of a data-carrying inductive, like none in this case.

[Sebastian Ullrich]

Option.none is unboxed, so there is nothing to free

[Sebastian Ullrich]

If there was such a fundamental memory leak, I do hope the leak sanitizer would have found it :)

[Sebastian Ullrich]

The inc/dec x_2 could theoretically be elided, but that would need some borrow checker-like analysis of x_2's lifetime being dominated by x_1's.