Can't use a local which has 'erased' as its type, since that's just been
substituted in while working out how many arguments a local function
needs to have. Also need to ensure we've searched for default hints when
encountering IBindImplicits rather than after because otherwise it might
find the wrong instance.
Both these problems result it terms which don't type check getting past
the elaborator! So, also added a --debug-elab-check flag to check the
result of elaboration. It's not on by default because there are cases
where it really hurts performance, typically when inferring implicits
with lots of sharing. So we'll keep it as a debug flag, for now at
least.
I got this wrong in the last patch - we need to go under the environment
where the guess was created. This will fix up the term so that it has
the right type after unification.
These functions use the NonEmpty predicate type in order to prove
that the operation will be valid.
Implementations copied from Idris1's Prelude.List module, except without
expanding the auto implicit argument.
Add an 'addName' function to Contex.idr interface for adding a new
name to the context.
Modify checkLock to always add the newly bound names to the context
The list of binding occurrences we iterate over must not have
duplicates, so we remove them with nub.
Instead of %allow_overloads, which I've never documented or explained,
now we have:
+ if there's more than one possible name after pruning according to
return type, and there is at least one name with a concrete return
type, rule out the names which do not have a concrete return type.
Effectively this means if there is a clash between a concrete name and a
polymorphic name, we'll always take the concrete one, which is
consistent with Idris 1.
I still don't know if this is the right choice, but all the possibile
ways of resolving ambiguity have some problems, and this is the fastest
to resolve in the common case!
If the unification problem is delayed, and there's only one constraint,
allow inserting the laziness coercion when rechecking. We need this for
the situation where it's not yet known whether a term is lazy or not
(e.g. the laziness is computed by a type level function)
See e.g. Applicative instance in Data.Vect. This allows implementations
to use implicits at run time (by default, they'd be 0 multiplicity so
erased, but it might be useful to have an index available at run time).
At the moment, the parser requires implicits to be given before
constraints. Ideally it should be possible to give them in any order.
I'll come back to this.
When writing to ttc, need to take the length in bytes rather than the
length in characters. Also need to write to scheme in the appropriate
format for each scheme system.
While we're at it, Idris 1 supports unicode identifiers (although we
don't encourage it :)) so this allows any characeter >127 in an
identifier.
Instead of returning the intermediate types as a Term, return them as a
Glued, so we don't keep converting back and forth between Terms and NF
when unelaborating applications. This appears to be really significant
for bigger applications, and is important for coverage checking where we
occasionally have to recheck a generated term.
For the types of local names, don't write out the environment - it's
going to be repeated for every name, mostly it's unhelpful, and if you
want to see the types of other names you can ask directly. This can save
a huge amount of time when environments are slightly complicated.
This includes: metadata collected when elaborating impossible cases,
which are just discarded whatever happens; and, types of names of global
definitions, which we can get from the context anyway. This has quite an
impact on performance, because their environment and types have to be
encoded and written out (which, by the way, we could probably do a lot
quicker by organising them by environment so we only have to write out
each environment once).
Turns out you can contrive to have buffer overruns if you use an unsafe
buffer library... oops! When resizing a buffer, we need to make sure
that the new size is enough for the thing we're about to add. This is
almost certainly the cause of #95.
If a default method implementation refers to another method in the
interface, it's going to be one from the interface being defined, so
push it through explicitly.
This is only going to be guaranteed to be the case for default method
implementations - we can't assume anything for other implementations.
Fixes#77
This makes it easier for more complicated packages (e.g. network, which
needs to install a C shared library) to know where to put things without
having to work out the prefix themselves.
This could allow us to actually erase (rather than compile with nil)
although experiments show that has no impact on performance. It is
useful to see, though, and other back ends may benefit.
