Fix lamToLet in Erasure.hs

[ziman]

There were two bugs:

• The original code did not address overapplied lambdas but there should be no problem with these -- just reapply the extra arguments under the let bindings.
• The original code did not weaken terms when moving them under let binders.

This caused problems in https://github.com/edwinb/Idris2/pull/333 and is (hopefully) fixed in this patch.

[gallais]

This makes sense to me. Nice to have someone who knows the feature well jump in!

The CI failure seems like a fluke. https://travis-ci.org/github/idris-lang/Idris-dev/jobs/680313824 seems to need restarting

[gallais]

I have tried to pull this branch, install it (using make install) and rebuild
my PR however I am getting inexplicable out of scope errors for throw & catch
in idris2's Idris/ModTree now.

I'll try to revert back to an hackage-sourced idris1 and see whether that solves
my new & unrelated problem. :/

[ziman]

On Tue, Apr 28, 2020 at 03:00:06AM -0700, G. Allais wrote: I have tried to pull this branch, install it (using `make install`) and rebuild my PR however I am getting inexplicable out of scope errors for `throw` & `catch` in idris2's `Idris/ModTree` now.

Oh. I haven't tried to rebuild Idris2 using this branch. I'll try after work.

[gallais]

It seems unrelated: I am getting the same error with an hackage-installed idris1.
It is very strange because Control.Catchable is publically exported by Core.Core
so these methods should be in scope!

Edit: now I'm getting an out of scope error for List. This seems very dodgy...

[andrevidela]

I get the same No such variable List and No such variable Maybe when compiling TParsec with this branch. I'm having the same idris: Erasure.hs:lamToLet': unexpected input: in another project (https://github.com/statebox/fsm-oracle)

edit: actually the list problem might be unrelated

[ziman]

Erasure does not affect any terms before the IR/LTerm stage so those "No such variable" errors will be something else.

"Unexpected input" in lamToLet is exactly what this patch eliminates. Even if it did not work right, this error message is no longer present in the source.

[ziman]

BTW @gallais could your scope errors be caused by outdated IBC files? I can imagine that tweaking erasure analysis makes cached runtime code in IBC files no longer make sense, and then fail in mysterious ways.

Should I bump the IBC version?

[gallais]

Should I bump the IBC version?

Sounds like a good idea. I'll have another crack at this once the version is
changed to see whether I end up in the same dead end.

[melted]

Is this ready to merge?

[ziman]

It should be. Let's see what Travis says.

[gallais]

The travis failures are extremely strange.

[ziman]

The AppVeyor failure is even stranger.

[melted]

I have dropped GHC 8.2 in Travis on master, no need to support it anymore, and the Idris 2 job wasn't working. So it looks fine. Appveyor must have dumped core or something on one of the tests, but only two failed. So good enough, I guess.

[melted]

Missed the 1.3.3 release I did last night though.