In theory argument elaboration order doesn't matter, but in practice we
sometimes make choices for performance reasons, like helping with
disambiguation by knowing the target type.
This was kind of messy, now we can more clearly see what's going on.
Also, more importantly, it gives us a bit more control which we
sometimes need. For example, if we go choose to go right to left for
some performance heuristic it might turn out we don't have enough
information yet, in which case we need to delay and try again later.
Fixes#1743
While the discussion about how to refactor test framework is not
finished (#1654), make this change: move `rm -rf build` in the
beginning of the test. For these reasons:
* it is useful to inspect the contents of the `build` directory
especially after the test failure
* if build crashes mid-test (e.g. process killed), next run should
not be affected by the `build` directory from the previous run
We already did this, but missed a few cases due to the way arguments are
elaborated. So now, when checking an LHS, we don't allow LHS argument
types to be inferred from the pattern, but rather they must be inferred
from elsewhere. To do this, we keep track of the constraints which would
be solved when inferring the type, and make sure they don't solve any
new metavariables. Fixes#1510, and also now gets the error location
right as a bonus!
We do this during desugaring because elaboration may insert valid
`?` values on the LHS (e.g. when elaborating things that cannot be
pattern-matched on and should be checked to be forced).
