Goal Type -> Type.
set (T := Type).
clearbody T.
refine (@id _).
Qed.