This commit fixes some bugs for coercions.
1. Applying coercion should work correctly w.r.t. unification
(see  modules TrickyPolymorphic(Alpha|Beta) in bench/typing/good/coercions.mlw).
2. Union of two coercion maps now works correctly w.r.t. adding the same coercion twice
even if it is transitive closure
(see module SameTransitivityCheck in bench/typing/good/coercions.mlw).
3. Coercion error printing is now listing all components of conflicting coercion
(see bench/typing/bad/coercion_cycle3.mlw for example).

In this version, we still just lookup at head tysymbols to decide whether a coercion
can be applied. This can be improved by taking into account also the types of arguments
to decide earlier that a coercion cannot be applied.
For instance, given

type t 'a
function f (t int) : int
meta coercion function f
goal G: forall x: t bool. x = 42

results now in an error message
This term has type t bool, but is expected to have type t int

We can do better, detecting that a coercion f cannot be applied to [x] at all.
To be done.