This is further progress towards a metaprogramming system in a form
similar to Elaborator Reflection or Template Haskell, but trying to
avoid leaking too many implementation details of the elaborator itself.
This is the result of running the command:
$ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} +
I confirmed before running it that this would not affect any markdown
formatting in documentation comments.
Fixes#132. When getting the names in the block, we need to return the
fully explicit name, because we can't assume they'll all be in the same
namespace as we can have namespaces inside parameters blocks.
This allows recording cumulative time for specific operations, e.g. to
check how much time unification has taken overall. Not used in the
code as things stand, but useful enough as a debugging/profiling gadget
that I think it's worth committing.
Just a small effect, but noticeable, from avoiding branching the context
where it's not needed (in Ambiguity) and hand-inlining the Functor
instance for Binder in thin.
If we're unifying applications, checking for conversion first is not a
shortcut because if it fails, we just have to redo the work, and if it
succeeds, that's more or less what we'd have done anyway! This is mostly
an issue when unifying really big expressions, which still take a long
time, but at least it's not as long.
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)
