I'm trying to understand that paragraph of the refman: https://coq.inria.fr/refman/addendum/implicit-coercions.html#identity-coercions

I think the following setting fits in the use case in the text (with k = 2, n = 3 and m = 2):

```
Parameters (C : nat -> unit -> bool -> Set) (D : nat -> unit -> Set).
Parameter f : forall (x1 : nat) (x2 : unit) (y : C x1 x2 true), D x1 x2.
```

indeed, `f`

doesn't satisfy the uniform inheritance condition, which Coq appropriately warns about

```
Parameter c : C 0 tt true. (* a C, for testing purpose *)
Parameter T : D 0 tt -> nat. (* something expecting a D *)
(* Coercion f : C >-> D. *)
(* as expected *)
(* Warning: f does not respect the uniform inheritance condition *)
```

and the coercion doesn't work (as expected)

```
(* Fail Check T c. (* and coercion doesn't apply *) *)
```

So following the documentation, we declare an identity coercion

```
Definition C' := fun (x1 : nat) (x2 : unit) => C x1 x2 true. (* as in the doc *)
Identity Coercion Id_C'_C : C' >-> C.
Print Id_C'_C. (* as in the doc *)
```

I would then expect the following to work

```
Coercion f : C' >-> D. (* Cannot recognize C' as a source class of f. *)
```

according to the following sentence in the doc "We can now declare f as coercion from C' to D"

There is an example below in the doc, but it seems reverse to me: it first declares a coercion then an identity coercion. The identity coercion seems useless (commenting it, the example still works the same).

I'm willing to submit a PR to either improve the refman (or the code), but I first need to understand what is the expected behavior.

I would expect it to work, so maybe its a bug. But I'm not a big fan about identity coercions and the non uniform inheritance condition, so if you have energy to work on that code I'd not stop at the bugfix ;-)

The condition has some sense if the coercions describe a hierarchy, @Kazuhiko Sakaguchi can confirm this.

But I bet that the condition was originally put so that the application of coercions does not require type inference.

In particular from an expected type `C1 x1 .. xn`

it lets you fill the `_i`

in the casted term `f _1 .. _n t`

with `x1 .. xn`

. If you don't have the condition, then you could still typecheck the term and infer the missing pieces.

This code is somehow already there since `Program`

uses `existsT`

as a coercion, (you want to map, say, a `n:nat`

to a `{n:nat & n > 0}`

. You can't possibly infer the `_`

there (the proof of positivity) from the "arguments of the type", but you can elaborate the `_`

to a new subgoal.

If you use that code I really don't see why one would need identity coercions, which are a poor may way of describing how to synthesize `_1 .. _m`

out of `x1 .. xn`

. The system is already able to figure out silly cases (in your case the `true`

is in the type of `c`

, the casted term) and even let you do interactive (or via TC search) the non trivial ones.

Thanks for your opinion. I fully agree and I'll try to prepare a PR along those lines (there may be some work, the fact that `existsT`

seems to be handled in a quite ad-hoc way is a bit frightening: https://github.com/coq/coq/blob/master/pretyping/coercion.mli#L39 ).

I was thinking about the other way around. The one you point to is also ad-hoc because it cannot just be expressed with coercions since the target would be a parameter, not a constant (from `sigT A P >-> A`

)

I was talking abut the other direction

Anyway, I was just writing here what I would do if I had the time ;-)

according to the following sentence in the doc "We can now declare f as coercion from C' to D"

IME, as a rule of thumb, coercions ignore definitional equality entirely, so instead of

`Parameter f : forall (x1 : nat) (x2 : unit) (y : C x1 x2 true), D x1 x2.`

you'll probably need

`Parameter f : forall (x1 : nat) (x2 : unit) (y : C' x1 x2), D x1 x2.`

but (while Enrico knows more than me) I don't get how this should work as-is: to coerce from `C`

to `D`

you'll need a coercion from `C`

to `C'`

and one from `C'`

to `D`

— so `Id_C'_C`

is backwards.

I think `SubClass C' := fun (x1 : nat) (x2 : unit) => C x1 x2 true`

should produce the right direction (it's a definition + identity coercion)

@Enrico Tassi here is the PR: https://github.com/coq/coq/pull/15789 . CI seem impressively happy (appart from one stupid conflict made apparent in math-comp and another simple fix in Unimath)

@Kazuhiko Sakaguchi you may also be interested

This is pretty cool! Does it mean the uniform inheritance condition is now irrelevant in all contexts? I still get warned about it (in the definition of `onat_of_obool`

below), even though the following works on master and the last line fails on 8.15:

```
Coercion nat_of_bool (b : bool) := if b then 1 else 0.
Check (true : nat).
Coercion onat_of_obool (x : option bool) :=
match x with
| Some b => Some (nat_of_bool b)
| None => None
end.
Check (Some true : option nat).
```

We kept the warning because, as indicated in the doc, uniform inheritance condition still guarantees completeness of the non-ambiguous-coercion-paths check. So it is still advisable to satisfy the condition if possible, in order to avoid spurious warnings about ambiguous paths.

The difference now being the coercion is actually still added rather than silently dropped?

Exactly (I still think what is now a warning should have been an error previously).

(well, the coercions were still behaving as such for printing, but even that was broken)

So if it is not possible to satisfy the uniform inheritance condition, the idea is to turn off both uniform inheritance and ambiguous paths warnings?

I am confused about one thing from that PR however. The UIC is sufficient for non-ambiguous-coercion-paths but is it necessary?

The UIC is sufficient for the check to be *complete* but not necessary (as far as I understand).

Ana de Almeida Borges said:

So if it is not possible to satisfy the uniform inheritance condition, the idea is to turn off both uniform inheritance and ambiguous paths warnings?

If it were me, I would turn off the warnings locally when I know they are spurious (with `Set Warnings "-uniform-inheritance". Coercion [...]. Set Warnings "uniform-inheritance".`

)

Yeah, I usually do that, but I'm usually not that confident that they are not spurious, so I always second guess myself :sweat_smile:

Could you add an attribute e.g. `#[nonuniform] Coercion [...]`

?

Here it is: https://github.com/coq/coq/pull/15853

That was a great idea and I think it could be extended to other warnings as well: https://github.com/coq/coq/issues/15893

Last updated: Jul 13 2024 at 04:02 UTC