type checking arrows with existentials in output

- re-used same approach for inferring instantiations in input world
- in fall-thru case of function body, if synthesized type is bot, then
  no need to check expected world. otherwise, need to infer instantiation
  and check.
- case for return must compute a substitution for expected output world.