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!
