(atj-type-annotate-args args var-types mv-typess guards$ wrld) → (mv annotated-args resulting-types new-mv-typess)