Port to Idris2

[clayrat]

I've pushed an initial attempt to the idris2 branch, the core library itself seems to compile (at least with the latest master version), but the examples still need some work.

[eayus]

Currently the idris2 branch fails to compile with many errors like:

Mismatch between:
    Box ?a ?j
and
    Box (Parser mn p a) n

Passing the a and j arguments explicitly doesn't seem to solve this, and only results a type mismatch between two identical terms:

Mismatch between:
    Box (Parser mn p a) n
and
    Box (Parser mn p a) n

Not sure whether this is related to this issue: https://github.com/edwinb/Idris2/issues/236. I've had a mess around and haven't had any luck, does anyone have any ideas on how to solve this?

[clayrat]

TBH I haven't tried recompiling this branch for a few months, as Idris2 is currently a bit of a moving target. However given that @gallais is a team member now, we should probably give it another try.

[gallais]

So I have managed to track down the last issue: https://github.com/idris-lang/Idris2/pull/269

Once this patch is installed, everything goes through and then Idris2 spends 14G of RAM on trying to typecheck STLC with only test enabled before I kill it. Ohad and Edwin are currently discussing a potential performance regression so I'll hold up reporting this problem for now. The confusing thing is if you evaluate Test at the toplevel it does not take that long.

[clayrat]

Ah, if it's down to just a performance issue, that sounds pretty good, given that Edwin lately seems to prioritize those :)

[edwinb]

I'm pretty sure this (and Ohad's performance problem) are down to things from the prelude/base libraries not being evaluated, so blocking and causing huge terms that need quoting/writing out. Idris 1 exported a lot more publicly. I wonder if we're generally doing this wrong, in that a lot of things in the Prelude - and some base libraries - are often needed at the type level and therefore should be public export as they were in Idris 1.

There's also a question of evaluation at the REPL vs evaluation in the type checker. At the REPL, it reduces everything whether public export or not.

[clayrat]

I've updated the examples but still none of them work except Ambig, somehow. I wonder what it is getting stuck at now?

[clayrat]

What's curious is that (at least for NList and Parentheses) if you comment out the test cases and run the corresponding parse commands in the REPL manually, you get the expected answer. However if you uncomment them and run the same commands in the REPL, you get a big unevaluated term instead.

[clayrat]

@gallais have you had any progress on debugging this, or should I take a look?

[gallais]

I have not had a look.

[gallais]

I cleaned up some modules today, reusing Data.List1 and the Bifunctor from base most notably.

I had a look at NList and :log eval.stuck 5 does not report anything getting stuck during evaluation. I am starting to suspect it's the normalisation strategy used during typechecking that is problematic in our case because:

• parseType "((1,2,3),(4,5,6))" (nnats 2) evaluates immediately to Singleton [[1, 2, 3], [4, 5, 6]]
• the it (MkSingleton [[1, 2, 3], [4, 5, 6]]) succeeds immediately
• but the (parseType "((1,2,3),(4,5,6))" (nnats 2)) (MkSingleton [[1, 2, 3], [4, 5, 6]]) takes seemingly forever

I'll try to see with Edwin if we could maybe have a primitive forcing eager full normalisation of its argument.

In the meantime, I have experienced something weird:

head' was (sometimes only!?) getting stuck even though it's defined as public export in Data.List. It turns out that I had not explicitly imported Data.List in the module where I was trying to get head' to reduce. Importing Data.List fixed that. Something to keep in mind for the future.