Primitives for unifying universes? (polyproj)

[JasonGross]

I would like tactics which unify universes. I can do it now with the following notations:

Polymorphic Definition type_of {A} (_ : A) := A.
Notation unify_universes t1 t2 := (forall (x : t1) (y : t2), (x : t2) -> (y : t1)).
Notation unify_type_universes t1 t2 := (unify_universes (type_of t1) (type_of t2)).

But it would be nice to have primitive unify_unverses_of which takes in two terms A : Type and B : Type and forces their types to be the same. (I can do unify Type1 Type2 to unify universes, and I can use type of in Ltac to get the type of a term, but if I use it to get the type of a type, I just get a fresh type.)