Infer implicit args; Give type to metavars

* src/lexp.ml (lexp): Add type to `Metavar`.
(lexp_unparse): (somewhat) Handle Metavar and Sort.

* src/lparse.ml (global_substitution): Move, so elab_check_sort can use it.
(mkMetavar): Add type arg.
(mkMetalevel, mkMetatype): New functions.
(elab_check_sort._lexp_p_infer): Use them.
(_lexp_p_check.unify_with_arrow): Use the explicit arg type if present.
(elab_check_sort.lexp_call.handle_fun_args): Infer missing implicit arg.

* src/opslexp.ml (lexp_whnf): Rewrite to reduce diff w.r.t `trunk`.
(check): Add case of `Metavar`.

* src/unification.ml (mkMetavar): Remove.

* tests/eval_test.ml ("Lists"): Remove explicit-implicit args.

* tests/unify_test.ml: Remove unsupported `case` on integers.

* tests/utest_lib.ml (for_all_tests): Remove try/with which hides the
better backtrace one gets with OCAMLRUNPARAM=b.