typing: precise diagnostics for failed operator applications

[strub]

Operator selection unified arguments and result type in one shot and
dropped every rejected candidate, so a failure was always reported as
"no matching operator for the parameters' type" — even when the
parameters matched and only the result type (or a single argument, or
the arity) was wrong.

Rework selection to classify failures:

• EcUnify.classify_application unifies a candidate against the expected
  arguments one at a time (head-normalising to see through type
  abbreviations), pinpointing the first argument / result / arity
  failure. select_op now returns OK / KO outcomes carrying the reason,
  the declared type and the inferred partial instantiation.

• The same classification is applied to program variables (select_pv)
  and to local variables (in form_of_opselect, where a local that
  shadows an operator fails to apply). The new UnappliedOp error and its
  printer describe each failing candidate (operator, program variable or
  local), the argument types, and for operators the declared polymorphic
  type with the inferred type-parameter instantiation. Genuinely unknown
  names keep the previous UnknownVarOrOp message.

Also add an "expect fail "..."" command that asserts a command fails
with a given error message, and use it in a new regression test covering
result/argument/arity mismatches, partial instantiation, multiple and
mixed-kind candidates, formula context and unknown names.

Closes #1048, #825.

[oskgo]

Would it be feasible to deduplicate the "but a value of type T was expected" when multiple candidates fail? Is there a case I'm missing where T could be different in the different failures?

[oskgo]

Indeed I was missing such a case. One example is the following:

theory T1.
op x: int -> 'a.
end T1.

theory T2.
op x: 'a -> int.
end T2.
import T1 T2.

op y: unit = x true.

Here one candidate fails because true has the wrong type, while the other fails because of the expected return type. It's not obvious to me how one should consolidate information about what was expected while handling cases such as these.

LGTM.

[strub]

You have been faster than me to answer your own question :)