No reset/reuse instructions for simple conversion function

[TwoFX]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

In the example

set_option trace.compiler.ir.reset_reuse true

def Sigma.toProd : (_ : α) × β → α × β
  | ⟨a, b⟩ => (a, b)

we get the IR

[reset_reuse]
def Sigma.toProd._rarg (x_1 : obj) : obj :=
  case x_1 : obj of
  Sigma.mk →
    let x_2 : obj := proj[0] x_1;
    let x_3 : obj := proj[1] x_1;
    let x_4 : obj := ctor_0[Prod.mk] x_2 x_3;
    ret x_4
def Sigma.toProd (x_1 : ◾) (x_2 : ◾) : obj :=
  let x_3 : obj := pap Sigma.toProd._rarg;
  ret x_3

As we can see, the memory cell of the input is not reused, even though the Sigma and Prod constructors are compatible. Ideally, the generated IR would be

[reset_reuse]
def Sigma.toProd._rarg (x_1 : obj) : obj :=
  case x_1 : obj of
  Sigma.mk →
    let x_2 : obj := proj[0] x_1;
    let x_3 : obj := proj[1] x_1;
    let x_5 : obj := reset[2] x_1;
    let x_4 : obj := reuse x_5 in ctor_0[Prod.mk] x_2 x_3;
    ret x_4
def Sigma.toProd (x_1 : ◾) (x_2 : ◾) : obj :=
  let x_3 : obj := pap Sigma.toProd._rarg;
  ret x_3

so that the memory cell is reused if possible.

Context

The algorithm from the Counting Immutable Beans paper would insert reset/reuse instructions in this case. However, there is an explicit check in the Lean compiler that checks that reset/reuse instructions are only inserted if the type matches up. This makes sense: in an example like

def foo : List (Nat × Nat) → List Nat
  | [] => []
  | x :: xs => match x with
      | (a, _) => a :: foo xs

without the check that the types match, the generated code would try to reuse the memory cells of the pairs instead of the list, so we wouldn't get a traditional destructive update, leading to performance degradation if the pairs in the input are all shared but the list itself is unique.

However, inserting some reset/reuse instructions should always be better than inserting none at all, so it would be nice if the heuristic could be tweaked to cover the case of conversion functions like Sigma.toProd.

Steps to Reproduce

1. Inspect the generated IR for the function Sigma.toProd above.

Expected behavior: reset and reuse instructions should be present in the IR.

Actual behavior: No reset and reuse instructions.

Versions

Lean (version 4.9.0, commit 883a3e7, Release)

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.