We were only doing implicits, so add auto implicits too. It's slightly
tricky, because we might also have implicits given of the form @{x}
which stands for the next auto implicit.
Fixes#50
Just like all other pi-bound things, if m is an unbound implicit and we
have m ?x = m y as a unification problem, we can conclude ?x = y because
it has to be true for all ms.
This was implemented in Blodwen but I hadn't got around to it yet for
Idris2... fortunately it's a bit easier in Idris2!
Fixes#44
This will be useful shortly, and in general because it'll give us more
flexibility in unification to be able to spot things which are
guaranteed invertible like constructors.
Add "installation problem", and while I'd rather not have larger proposals on the tracker, it would still be useful to list small requests where it's objectively clear what the resolution is.
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
