We were only checking parameters, meaning that there were potential
clashes leading to confusing behaviour, and meaning that it was somehow
relevant what the names were in the interface!
Now by marking a method as multiplicity 0, we can explicitly say that
it's compile time only, so we can use it to compute types based on other
erased things - see tests/idris2/interface008 for a small example.
This fixes#8 - at least in that it allows the interface to be expressed
properly now, although the multiplicity annotations mean that
unfortunately it can't be compatible with Idris 1.
A local variable can't be applied to itself when searching (otherwise,
for example, we could end up trying something like id id id id id id etc
forever). So remove it from the environment before searching for its
arguments.
This and the previous patch fix#24. (Or, at least, the minimised cases
reported as part of it!)
Don't use the interface itself when checking parent implementations
exist, otherwise we'll end up in a cycle (because the parent
implementation will sort of exist as a result!)
We can't begin a search until we know what we're searching for! For some
reason I forgot to add this case, and without it the search space can
explode, or we might find an answer too soon and commit to the wrong
thing!
Fixes#36
This means that even if the relevant parameters aren't used by a method
body, the method can still see what the implicits are (though they will
be 0 multiplicity).
This is relevant to #8, but doesn't really fix it because we still need
a way of saying that methods are 0 multiplicity.
We need to turn pairs into separate constraints, which is a bit of a
hack but the constraints need to be separate in order to build the
chasing functions which find the parent constraints correctly.
Possibly there is a neater way, which is to teach the search algorithm
to look in the hints for pairs, but that's a lot more complicated (and
probably unnecessarily so).
Fixes#25
This is a bit rough, but does yield an executable with a ~40% speedup in
startup latency on one test. The resulting executable is a .so file with a #!
invocation of the local chez scheme executable to run it, so the binary isn't
portable (even to a machine with the same architecture/OS) unless there's an
identical chez installation on both machines.
As with the .ss source, the .so is currently leaked in the temporary directory.
They're just about deciding whether it's okay to start an auto implicit
search, not whether it's okay to continue search, which is part of the
problem in #25.
This hasn't been tested much (and indeed isn't in the test suite because
I haven't found the way to load shared objects nicely portably yet!) so
I hadn't noticed, but primitive types are translated to names before
compilation to support matching on types, so we need to account for
this.
Also, CG directives need to be processed after loading from ttc
We can't nest delayed elaborators (this is an efficiency constraint, to
prevent excessive searching for ambiguous names) to run elaborator
immediately if delays aren't allowed in delayElab
This is part of what we used to have in Enum but I think it's better to
separate the two. Added implementations for Nat, and anything in
Integral/Ord/Neg, so that we get range syntax (at least when its
implemeted) for the most useful cases.
This required a small change to auto implicit search (and I'm still not
sure about this). Now search arguments right to left, because solving
later arguments may resolve earlier arguments by unification and this
can happen in particular when chasing parent interfaces (which may have
fewer parameters).
Take the earliest failure message, since they'll typically be more
precise (later search groups being for chasing parent interfaces and
defaults). This is mostly as a heuristic to help show whether one part
of a pair failed in implicit search.
At least on Linux, \r needs to be in singles quotes as an argument to tr
or it removes all the 'r' instead! Hopefully it also works this way on
Windows...
These are 'nested' namespaces which are a bit special in that even
private names are visible from the enclosing namespace. This gets the
behaviour for record visibility from Idris 1.
Need to set up nested names appropriately for the with function so that
the environment gets passed through correctly, and use abstractEnvType
to get the type of the with function rather than simply binding the
environment as is.
Now supports with applications on the RHS when auto implicits are
involved. Auto implicit bound names in patterns now become searches on
the rhs in a with-application (I should write this construct up properly
in a paper some time!)
We don't use level, so remove it. Added a field bindingVars which
records whether implicit names should be bound if unsolved. This needs
to be separate from the elaboration mode because we might encounter new
holes inside dot patterns which are matched elsewhere.
We use this to decide whether a determining argument is satisfied or not
for unbound implicits. We can tell from the name, which would be a PV,
but this way relies on fewer assumptions.
Elaborate via either === (homogeneous equality) or ~=~ (heterogeneous
equality) both of which are synonyms for Equal. This is to get the Idris
1 behaviour that equality is homogeneous by default to reduce the need
for type annotations, but heterogeneous if that doesn't work.
There's a bit of a trade off here. It would be better to report the
ambiguity but this would lead to a need for (I think) excessive
precision in types which would impact usability. It will always take the
leftmost interface.
Chapter 7 tests added.
Idris 1 will fill in the last metavariables by matching rather than
unification, as a convenience. I still think this is okay, even if it's
a bit hacky, because it's a huge convenience and doesn't affect other
unification problems.
Also abstract over lets in guesses, like in delayed elaborators, to
avoid any difficulties when linearity checking and to make sure that let
bound things don't get reevaluated.
This is enough to get the Chapter 6 TypeDD tests working
Allow matching rather than unification, as long as it doesn't solve any
metavariables on the way. I noticed a potential unification bug on the
way, forgetting to update whether holes are solved when unifying
argument lists.
This was left over from Blodwen (where it was also wrong :)) but the way
we apply metavariables now means we don't need to do anything fancy when
unelaborating them for pretty printing.
Like in delayed ambiguity resolution, we need to reevaluate the target
type because it might have changed - and that's why we delayed in the
first place!
Where "simple" means the solution is just a local variable or smaller
metavariable application. This is a big win when environments get big,
and I suspect there might be more where this came from if we always
shrink the environments of metavariable solutions as far as possible. It
really saves a lot of work in "quote" in particular.
Surprisingly == on Nat in the Idris prelude is linear! So shortcut that
by converting to an Integer first. Also a couple of small things in the
evaluator that have a small but noticeable effect when environments are
big.
This has shown up a problem with 'case' which is hard to fix - since it
works by generating a function with the appropriate type, it's hard to
ensure that let bindings computational behaviour is propagated while
maintaining appropriate dependencies between arguments and keeping the
let so that it only evaluates once. So, I've disabled the computational
behaviour of 'let' inside case blocks. I hope this isn't a big
inconvenience (there are workarounds if it's ever needed, anyway).
Need to add by full name, due to ordering of loading (the name it's
attached to may not be resolved yet!). This doesn't seem to cause any
performance problems but we can revisit if it does.
Don't use the type of a scrutinee to restrict possible patterns, because
it might have been refined by a Rig0 argument that has a missing case.
Instead, generate all the possible cases and check that the generated
ones are impossible (there's no obvious change in performance)
Small change needed to fix one - assume given implicits which are of the
form x@_ arise from types. It's a bit of a hack but I don't think
there's any need for anything more complicated.
Only valid if unifying the pattern at the end doesn't solve any
metavariables. Also when elaborating applications of fromInteger etc to
constants on the LHS we need to be in expression mode, then reduce the
result later.
This was a slight difference from Blodwen that wasn't accounted for -
there might be lets in the nested environment, so when building the
expanded application type, make sure we go under them
This wasn't necessary before, since we always inlined, but since we can
now postpone things longer and don't always inline until much later, we
need to know what names everything refers to earlier.
Since lookup up a binding can be expensive in a big environment, and we
only need to reduce it if it turns out to be a let, caching it can be a
noticeable win
We can't refine by a name in Rig0 because we can't assume it covers all
possibilities, so only refine by them at the end, at which point we
check that there's only one case left (otherwise we have to match on it,
which is not allowed for an erased thing)
