Gather unsolved meta-variables, "solve" them with magic, and add their types to the list of goals.
Print the list of goals generated by elaboration.