Typecore.type_application: handle empty argument list

List of argument can be empty if all arguments were explicitly selected
implicit instance. Drop the apply node in this case.
Typeimplicit: fix generation of fresh identifiers for implicit arguments

This is completely handled during Subst
Typeimplicit: also unlink with constraints
Typecore: check presence of implicit when typing top-level identifier
Ctype: fix equation generation when computing type equality

Matching wasn't commutative
Typeimplicit: refactor & unify free variables after successful search.

When entering search, free variables in the module are converted to
newtypes.
After search, free variables are restored and unified with generated
equations.