The result type of a join point is always equal to the function return
type. Moreover, the extra bookkeeping introduces extra work, and doesn't
really help.
@kha I keep finding problems with the float `let` inwards
transformation. It is always a nasty interaction between this
transformation and the `reset/reuse` insertion procedure.
The example I used in the new comment can be modified to a
`casesOn` with more than one branch (e.g., `Option.casesOn`).
Suppose we wrote
```
let o : Option Nat := Array.index a i in
let a := Array.update a i none in
Option.casesOn o
none
(fun n, some (Array.update a i (some (n + 1))))
```
In the example above, the compiler will float
`a := Array.update a i none` inwards.
```
let o : Option Nat := Array.index a i in
Option.casesOn o
none
(fun n,
let a := Array.update a i none in
some (Array.update a i (some (n + 1))))
```
Then, adding reset/reuse:
```
let o : Option Nat := Array.index a i in
Option.casesOn o
none
(fun n,
let o := reset o in
let a := Array.update a i none in
let n := n + 1 in
let o := reuse o (some n)
some (Array.update a i o))
```
Similarly to the example in the new comment, the `reset o` will fail since
the array `a` would still have a reference to `o`.
Remarks:
- Haskell also implements float `let` inwards.
- I am not sure how important the float `let` inward transformation is.
- I can see other nasty interactions after we implement user-defined
simplification rules. For example, I guess many users would find the
following lemma to be a good rewriting rule:
```
(Array.update (Array.update a i v) i w) = (Array.update a i w)
```
However, if we use this lemma in the example above, then `Array.update a i none` will be eliminated,
and `reset o` will fail.
@kha The move `x := val` to `casesOn` branch was producing nasty
problems. I documented the issue, and implemented a simple
and sufficient condition for preventing the problem. The approach is very
similar to the one used at `push_proj_fn` at `llnf.cpp`.
I hope this change will not impact existing benchmarks :)
