* src/opslexp.ml (check'): Check Metavar's type annotation.

* src/opslexp.ml (conv_p'): Add partial support for SortLevel's SLlub.

* src/lparse.ml (newMetalevel, newMetatype): Fix thinko's.
(lexp_decls_macro): Use pexp_p_decls.

* src/unification.ml (_unify_metavar): Also unify the var's type.
Furthermore, when unifying two metavars, try it both ways.