Fixes#92, because it wasn't re-evaluating the type and establishing
that the thing it was looking for must be a Fin for fromInteger so
resorting to the default integer literal instead.
Sometimes we swap the arguments, to reduce code duplication, but we need
to remember we've done that since (1 x : a) -> b is valid for an
argument of type (x : a) -> b, but not vice versa (that is, we have a
teensy bit of subtying to deal with, for convenience...).
This fix seems a bit ugly, but we do at least now propagate the
information. Fixes#82.
I don't know why I originally made it 'Inf' only in the evaluator... but
we certainly want 'Lazy' delays to block too, especially if they're
guarding non-terminating computations.
This is supported by Idris 1 and is handy for breaking cycles in
modules. To achieve this, we just need to make sure that complete
definitions aren't overwritten with empty definitions on loading.
Checking the let expression in full can break sharing when unifying the
types, and it's unnecessary because we've already checked the type of
the scope unifies with the expected type.
Fixes#63
Elaborate the scope of a let without the computational behaviour,
meaning that `let x = v in e` is equivalent to `(\x => e) v`. This makes
things more consistent (in that let bindings already don't propagate
inside case or with blocks) at the cost of not being able to rely on the
computational behaviour in types. More importantly, it removes a
significant potential source of slowness.
Fixes#58
If you need the computational behaviour, you can use a local function
definition instead.
This is for finding support libraries for code generators, e.g. the
shared objects that chez will load for glue code for foreign libraries.
It'll be used more shortly...
Fixes#42. If we don't do this, the name is treated in the saem way as
an unbound implicit, which is not what we want, so update with the
method applied to the parameters.
