We have ambiguous coercion paths

When compiling with Coq master, we see lots of these:

[constRF; rFunctor_diag] : cmraT >-> Funclass
[ucmra_cmraR; constRF; rFunctor_diag] : ucmraT >-> Funclass

Also see e.g. this build log.

Is this a problem? Can we do anything about it?

One of the ambiguities is that we have [ucmra_cmraR; constRF; rFunctor_diag] and [constURF; urFunctor_diag] both go from ucmraT to Funclass.

@jjourdan @robbertkrebbers is there any trick to fix such ambiguities when you have diamonds in your hierarchy? Can we reasonable make one of the involved coercions not a coercion?

In principle, these ambiguities should not matter---no matter what path you take, the result should be convertible.

If we want to get rid of the error, we could either:

• Remove constRF and constURF
• Remove rFunctor_diag and urFunctor_diag

Not sure what is most natural or results in the least number of changes.

Turns out this might also be a Coq bug: https://github.com/coq/coq/issues/10247

Okay so looks like it's not a Coq bug -- we have had these ambiguous paths all along, but so far that would not show up as warnings when using coqc.

According to https://github.com/coq/coq/pull/9743, ambiguous paths warnings are not shown when things are convertible, so that might also be a way forward.

mentioned in merge request !257 (merged)

added ~196 T-algebra labels

Latest Coq tells us what the ambiguous paths are:

New coercion path [gFunctors.singleton; gFunctors_lookup] : gFunctor >-> Funclass is ambiguous with existing 
[gFunctor_F; rFunctor_diag] : gFunctor >-> Funclass.

added A-coq label

And another, probably harder-to-fix ambiguity:

New coercion path [ucmra_cmraR; constRF; rFunctor_diag] : ucmraT >-> Funclass is ambiguous with existing 
[ucmra_ofeO; constOF; oFunctor_diag] : ucmraT >-> Funclass.

mentioned in merge request !322 (merged)

With latest version of Iris, I identified these two sets of ambiguous paths:

• from ucmraT to Funclass (extends your previous message):

  [ucmra_ofeO; constOF; oFunctor_diag]  : ucmraT >-> Funclass
  [ucmra_cmraR; constRF; rFunctor_diag] : ucmraT >-> Funclass
  [constURF; urFunctor_diag]            : ucmraT >-> Funclass

• from cmraT to Funclass:

  [cmra_ofeO; constOF; oFunctor_diag]   : cmraT >-> Funclass
  [constRF; rFunctor_diag]              : cmraT >-> Funclass

mentioned in merge request !413 (merged)

closed via commit 4f6d4de7

mentioned in commit 4f6d4de7