Fix bug when pretty printing function applications where the head is a meta-variable.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Use expected type of a definition in the elaborator. Improve elaborator solver. Add new example

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>