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!)
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.
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).
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...
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!)
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.
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.
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)
With the --yaffle flag, you get the old behaviour which is to invoke the
checker for the core theory (and all the tests are updated appropriately
for this).
This gives useful information for expression search, because we can add
lambdas while we're still building the environment, and start looking at
locals after that.
Mostly direct from Blodwen (some minor modifications to deal with new
way of going into a new scope in the elaborator as well as the usual
bits dealing with name lookup and Glued terms)
And process them on loading. We record that hints need saving out when
adding them, and clear that list unless we happen to be reexporting the
thing we've just read (import public).
