## Stream: Coq users

### Topic: Identity Coercions

#### Pierre Roux (Feb 24 2022 at 07:59):

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.

#### Enrico Tassi (Feb 24 2022 at 10:08):

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.

#### Pierre Roux (Feb 24 2022 at 11:06):

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 ).

#### Enrico Tassi (Feb 24 2022 at 12:13):

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`)

#### Enrico Tassi (Feb 24 2022 at 12:14):

I was talking abut the other direction

#### Enrico Tassi (Feb 24 2022 at 12:15):

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

#### Paolo Giarrusso (Feb 24 2022 at 13:54):

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.`

#### Paolo Giarrusso (Feb 24 2022 at 13:56):

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.

#### Paolo Giarrusso (Feb 24 2022 at 13:57):

I think `SubClass C' := fun (x1 : nat) (x2 : unit) => C x1 x2 true` should produce the right direction (it's a definition + identity coercion)

#### Pierre Roux (Mar 11 2022 at 13:28):

@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

#### Ana de Almeida Borges (Mar 22 2022 at 14:00):

https://github.com/coq/coq/pull/15789

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).
``````

#### Pierre Roux (Mar 22 2022 at 14:04):

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.

#### Ali Caglayan (Mar 22 2022 at 14:05):

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

#### Pierre Roux (Mar 22 2022 at 14:05):

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

#### Pierre Roux (Mar 22 2022 at 14:06):

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

#### Ana de Almeida Borges (Mar 22 2022 at 14:08):

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?

#### Ali Caglayan (Mar 22 2022 at 14:08):

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

#### Pierre Roux (Mar 22 2022 at 14:27):

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

#### Pierre Roux (Mar 22 2022 at 14:30):

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".`)

#### Ana de Almeida Borges (Mar 22 2022 at 14:46):

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:

#### Cyril Cohen (Mar 23 2022 at 17:29):

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

#### Pierre Roux (Mar 24 2022 at 12:48):

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

#### Ana de Almeida Borges (Apr 02 2022 at 15:17):

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