Relax the ambiguous path condition of coercion

The `Coercion` command did report many ambiguous paths when one declared
multiple inheritances.  This change makes the `Coercion` command to do not
report them when
1. all the coercion in the potentially ambiguous paths respect the uniform
   inheritance condition and
2. functional compositions of the potentially ambiguous paths are convertible to
   each other.
The first condition is not explicitly checked but is used to make the checking
process of the second condition easy.

The key idea of this change:
Let us consider a sequence of coercion
f_1 : C_1 >-> C_2, f_2 : C_2 >-> C_3, ..., f_n : C_n >-> C_(n+1)
which respect the uniform inheritance condition and where the user-defined
classes C_i have m_i parameters respectively (i <= n).
The functional composition f_1 . ... . f_n can be expressed as follows:
(fun x_1 ... x_(m_1) y =>
  f_n _ ... _ (* m_n times repetition of holes *)
      (...
           (f_2 _ ... _ (* m_2 times repetition of holes *)
                (f_1 x_1 ... x_(m_1) y))...)),
and the contents of all the holes can be determined (inferred) without leaving
any existential variables in them thanks to the uniform inheritance condition.

Misc:
- A test case for this change: test-suite/output/relaxed_ambiguous_paths.v
- Turn the ambiguous paths messages into warnings to do output test.

0 files changed, 0 insertions, 0 deletions