Deal with unification variables after type-checking (mantis #44)

[craff]

Unification variable that remains after type-checking should get a default instanciation.

Remark: if later we keep unification constraints, this would become very important as there could be unsolvable contraints, or preferably, we should ensure all constraints have a default instanciation that we could use.