The bug occurs when floating `cases_on` application in code of the form
```
let x := C.cases_on ...
in t
```
and when the type of `t` depends on `x`.
The issue here is that the `x` declaration disappears after the float, but the resulting type still depends on it.
We fix the bug by replacing `x` with its value in the type.
cc @kha
There is only one missing transformation: insert explicit reference counting instructions.
We will implement this transformation at `llnf.cpp`. After that, we are
ready to emit C++ code.
Some of the primitives do not have optimal implementation.
@Kha Could you please check if everything we use in the parser has a
reasonable implementation?
Motivation: consider the following example
```
let m := if b then m1 else m2,
state.bind m (fun p, BIG p.1 p.2)
```
we first eta-expand the term, put in LCNF and inline state.bind
```
fun s,
let m := decidable.cases_on b (fun h, m1) (fun h, m2) in
let x_1 := m s in
prod.cases_on x_1 (fun a s', BIG a s')
```
then, we apply `*-of-cases` at `m := ...` and its continuation, but we
need a joint point since the continuation is big. Then, we get
```
fun s,
let j_1 := fun x_1,
let x_1 := m s in
prod.cases_on x_1 (fun a s', BIG a s') in
decidable.cases_on b
(fun h, let y := m1 in j_1 y)
(fun h, let y := m2 in j_1 y)
```
This code is not good if `m1` and `m2` are functions. At runtime, we
need to create a closure and pass it to the join point.
If we apply `app-of-cases` before other floating `cases` variants we
avoid this problem.
Here is the sequence of transformations if we apply `app-of-cases`
eagerly. We get
```
fun s,
let m := decidable.cases_on b (fun h, m1) (fun h, m2) in
let x_1 := m s in
prod.cases_on x_1 (fun a s', BIG a s')
```
as before. Then, we apply `app-of-cases` at `m s`, and get
```
fun s,
let x_1 := decidable.cases_on b (fun h, m1 s) (fun h, m2 s) in
prod.cases_on x_1 (fun a s', BIG a s')
```
Then, we apply `cases-of-cases`, but we again create a join point.
```
fun s,
let j_1 := fun x_1, prod.cases_on x_1 (fun a s', BIG a s') in
decidable.cases_on b
(fun h, let y := m1 s in j_1 y)
(fun h, let y := m2 s in j_1 y)
```
However, this time we are passing a value to `j_1` instead of a closure.
`app-of-cases` has two benefits:
1- It never creates new join points since applications are always small in LCNF
2- It may reduce a `cases` that returns a closure into a `cases` that
returns a value.
