ANF, in which everything is applied to variables only, and VMCode, in
which everything is reduced to a list of assignments.
I don't plan to add a defunctionalisation step. I've tested with with a
quick hack C backend, though I don't intend to commit that (not here at
least) because even though it basically works, it's Very Slow.
Solving later arguments first means that they can refer to solutions of
earlier arguments. This isn't really the best solution for ensuring that
metavariables refer to things defined earlier, but it helps, and it does
fix#304.
Instead of the previous unreliable hack, actually look for occurrences
of the solved metavariable. Block if there are any, and fail if there
are any under a constructor. I had expected this to hurt performance
quite a bit, but it seems it doesn't.
This was prompted by #304, which is now partly fixed, but there's still
a refinement to unification needed to fix it fully (and at least it
doesn't segfault due to the cycle now!)
If it's a newtype with an erased WorldVal, turn any case blocks into
non-inlinable let bindings, which is more accurate than the fiddly thing
it was doing.
Also better usage calculation in the inliner (but we still can't inline
lets because we don't know yet which 'case' functions are guaranteed
safe to inline because they don't duplicate variables anywhere. That's
coming!)
A bug found via the very handy, but occasionally bad for performance so
off by default, --debug-elab-check. The multiplicity of a lambda type
needs to be checked against the expected multiplicity, not the given
multiplicity. Oops!
If you have any (\0 x => e) or similar, you may find you need to fix a
type error after this update...
We no longer need to do this since we now expand fromInteger. And, we
didn't even need to do it fully, because we never needed to normalise
the pattern variable types. This is a big win on code which has a lot of
type level computation.
Now only retry the constraint if at least one of the blocking holes has
some new information (either that it has been flagged invertible, or
that it is now defined). This can lead to big performance gains on
programs which use dependent types heavily.
At least as long as the number is small enough (currently set to < 100).
This is because it can open up further evaluation opportunities when
typechecking, and can make the term we're working with smaller - it also
makes display a bit neater.
Overall this makes some pathological cases of terrible performance much
better, without hurting anything else.
Flags can now be set on implementations too, where the flags get passed
to each of the methods in the implementation. We might want something a
bit more fine grained than this later. Also some small changes to the
way inlining lets is done in the compiler.
