Deadly Diamond of Death in Coq

Question

I'm trying to create a rather straight-forward type hierarchy. Here's a minimal working example:

Record R0 : Type := {
  R0_S :> Type
}.

Record R1 : Type := {
  R1_S   : Type;
  op1    : R1_S -> R1_S
}.

Record R2 : Type := {
  R2_S   : Type;
  op2    : R2_S -> R2_S
}.

Record R12: Type := {
  R12_S   : Type;
  R12_op1 : R12_S -> R12_S;
  R12_op2 : R12_S -> R12_S
}.

Definition R1_0 (r1: R1) := (Build_R0 (R1_S r1)).
Coercion   R1_0 : R1 >-> R0.

Definition R2_0 (r2: R2) := (Build_R0 (R2_S r2)).
Coercion   R2_0 : R2 >-> R0.

Definition R12_1 (r12: R12) := (Build_R1 (R12_S r12) (R12_op1 r12)).
Coercion   R12_1 : R12 >-> R1.

Definition R12_2 (r12: R12) := (Build_R2 (R12_S r12) (R12_op2 r12)).
Coercion   R12_2 : R12 >-> R2.  (* Warning *)

That last coercion generates the following warning:

Ambiguous paths:
[R12_2; R2_0] : R12 >-> R0
[R12_2; R2_0; R0_S] : R12 >-> Sortclass
R12_2 is now a coercion

Indeed, the coercion from R12 to R0 (or Sortclass) can take two different paths. And I understand why Coq would disallow this in the general case. Because... which of them would be used?

However, in this case it can be shown that the coercion by both paths R1_0 (R12_1 r12) and R2_0 (R12_2 r12) is exactly the same. But still I'm not able to add the following seemingly valid axioms:

Parameter r12 : R12.
Parameter x : r12.
Axiom id1 : (op1 _ x) = x.  (* OK    *)
Axiom id2 : (op2 _ x) = x.  (* Error *)

Question: So is there a way to convince Coq that this is OK?

Answer 1

I believe there is no way of convincing Coq that this is OK. However, you achieve a similar effect by using other features, such as canonical structures or type classes. This is how one could translate your example with type classes, for instance:

Class R1 T :=
{
  op1 : T -> T
}.

Class R2 T :=
{
  op2 : T -> T
}.

Class R12 T `{R1 T} `{R2 T} :=
{}.

Section S.

Context T `{R12 T}.
Variable x : T.

Hypothesis id1 : op1 x = x.
Hypothesis id2 : op2 x = x.

End S.

Notice that class R12 doesn't have any methods of its own, but requires type T to be an instance both of R1 and R2, which results morally in the same thing. The Context declaration forces Coq to assume instances for R1 and R2 automatically, in virtue of those requirements.

Edit:

If you try to add an R0 class to complete the diagram, you may get a weird error resulting from a failing type-class inference. One solution is to turn off the automatic generalization in R12 (i.e., remove the back quotes), and force R1 and R2 to be based on the same R0 instance:

Class R0 (T : Type) := {}.

Class R1 T `{R0 T} :=
{
  op1 : T -> T
}.

Class R2 T `{R0 T} :=
{
  op2 : T -> T
}.

Class R12 T `{R0 T} {r1:R1 T} {r2:R2 T} :=
{}.

Section S.

Context T `{R12 T}.
Variable x : T.

Hypothesis id1 : op1 x = x.
Hypothesis id2 : op2 x = x.

End S.

Unfortunately, I don't really have a good explanation to why an error could occur there, as type class inference is somewhat complex. However, I think it is not related to the problem you had had first, because there aren't actually ambiguous paths like before.