Lots of time is taken in finding the definitions to compile, mostly
because the definition itself needs to be decoded from the binary format
in the ttc, but we can at least make the rest of the process fast.
Inlining takes a while - we could improve this later by inlining as we
go, per file, rather than doing it just before compilation.
When we're checking if a definition is a hole and needs updating, when
loading ttc, the names might not fully resolved yet, so don't decode the
definition.
This is done during elaboration, but not for things which are solved by
unification or search, and they might be 0 if, say, they're a record
projection or other type level function.
Mostly if they arise from search, where the target of the search has a
let in the type. So, we need to consider this when checking
metavariables in the linearity check.
The old way did a lot of needless traversal, though you wouldn't
typically notice until you start having 40+ modules to build. Now make a
note of what we've looked at already.
Record name and constructor are in the outer namespace, fields in the
nested namepsace. Private names in the nested namespace is visible from
the outer namespace. Fixes#183
Also remove the 'nested' flag on INamespace, since it was only there for
records, and not really the right way to do things. The nested namespace
name is now given in the IRecord constructor (a front end might not want
to use a new namespace after all).
They might match on runtime-erased things (which is okay, since they're
erased too!) and if we try building the tree, it'll report an error
incorrectly. Fixes#229
Check that none of the generated missing cases match explicitly given
clauses, which might happen if there's some overlaps in the clauses or
if there's some matching on implicits. Ignore erased argument positions
when checking the match.
If we postpone unification problems, it's not necessarily at the top
level of a term, but then if we retry and find we need to insert a
'Delay' or 'Force' then it had better be at the top level or we'll get
an incorrect term. So, keep track of this in postponed constraints.
I dont know how I thought that was supposed to work, but it needs to get
the S and Z cases separately then build the 'if' expression, with the
default case if either are missing.
I had thought this was unnecessary, because it treats erased patterns as
variables, but it turns out we do need to erase variables where they're
sometimes used in erased positions, and sometimes not, to ensure we use
the right one.
It's a bit more expensive than just using a lambda, because they cache
the result in a thread safe way, and the Idris Force/Delay doesn't
promise to cache the result anywya.
Need to make sure we've got the right real name for the function - this
had previously only been tested in parameters blocks where the name
doesn't change.
