Leonardo de Moura

@dselsam I believe the problem is the `sizeof` instances of nested inductive datatypes. They use the internal recursors generated by the inductive compiler. Example: ```lean @[irreducible] protected def _nest_2_2.toml.value._mut_.sizeof :...

> [Wearing my (on-and-off) developer hat] I like this fix. With well-founded recursion, it will be easy enough for a user to define their own size function. Ok, I will...

I tried to fix this issue yesterday. The commit above prevents the VM failure from happening. We get the following error message instead: ``` 1518.lean:28:17: error: equation compiler failed to...

> Do you refer to the recursors for the internal unrolled inductive type (i.e., _nest_1_1.toml.value.rec)? Then the problem with the equations compiler should be solved as soon as we use...

> Yes, but we can use the user-facing cases_on recursor (which is compiled correctly) instead of the internal one. As far as I can tell, we only need to use...

@kha I agree with you. I also didn't see a pure-Lean solution. I like the `solve1_itactic`. I think it is worth to add it since `case` is super useful.

The commit above fixes the segfault. Now, we get the following error: ``` let.lean:87:0: error: deep recursion was detected at 'replace' (potential solution: increase stack space in your system) ```...

> Heuristic: Do not extend import statement to unindented lines. Works "out of the box", but we aren't usually whitespace sensitive. This heuristic would solve other issues we have. By...

@kha I'm happy to hear more whitespace sensitive hacks that would make Lean nicer to use. Do you have more suggestions? :)

> So the heuristic may need to be a bit cleverer, e.g. only forbid blank lines inside top-level applications (which should be a very safe assumption). I think if we...