Identity Coercions · Coq users · Zulip Chat Archive

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

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

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

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

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

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

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

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

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

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:

Stream: Coq users

Topic: Identity Coercions

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