More explicit type constraints for arguments

[SReichelt]

When type checking an argument, the checker should name the expected type more explicitly.

• The set (without any manipulation) should be displayed in error messages and in the GUI (e.g. in place of the preview, before anything is selected).
• If the argument contains a placeholder and we are checking a specific substitution for that placeholder, embeddings of the substituted argument should normally not be followed. E.g. if the substitution (more precisely, the argument containing the substituted term) is an integer, we should normally not consider this argument as a natural number, as in most cases it will not actually be a natural number.
  However, it is important to follow embeddings on the "other side", i.e. in the parameter type. This needs to work a bit differently than it currently does: The traversal of embeddings needs to stop once it reaches the construction that is determined by the substituted argument.
  Moreover, this restriction needs to be made optional, as described in Handle embeddings more restrictively in GUI #61. This also implies that the mechanism described in this issue could merely be an optimization for the more general solution in Handle embeddings more restrictively in GUI #61.