Yao Li (Jun 17 2020 at 02:11): Yao Li (Jun 17 2020 at 02:11):Hi, I wonder if there's a way to make implicit coercions work with type class constraints? For example:
Class Cl (a : Type).
Parameter A : Type.
Instance cl_a : Cl A.
Parameter Foo Bar : Type -> Type.
Parameter conv : forall {k} `{Cl k}, Foo k -> Bar k.
Parameter func : Bar A -> bool.
Coercion conv : Foo >-> Bar.
Fail Definition test (b : Foo A) : bool := func b.
Coq cannot insert conv to test even though it's OK to do that---A is an instance of Cl type class.
Gaëtan Gilbert (Jun 17 2020 at 08:44):kinda reminds me of https://github.com/coq/coq/pull/11327 but not quite the same
Yao Li (Jun 17 2020 at 15:55):Since I only need a specialized Foo in my use case so I tried this, but it still does not work:
Class Cl (a : Type).
Parameter A : Type.
Declare Instance cl_a : Cl A.
Parameter Foo Bar : Type -> Type.
Parameter conv : forall {k} `{Cl k}, Foo k -> Bar k.
Parameter func : forall {a}, Bar a -> bool.
Definition conv_A : Foo A -> Bar A := conv.
Coercion conv_A : Foo >-> Bar.
Fail Definition test (b : Foo A) : bool := func b.
Any thoughts how to make it work? Is there something I have missed in Coq's implicit coercion features?
Paolo Giarrusso (Jun 17 2020 at 16:34):I was surprised Coq accepted that code — but both coercions warn about "the uniform inheritance condition", which IME means the coercion will never be used. I've been able to work around this in the past by extra definitions FooA := Foo A and BarA := Bar A (with coercions to the new aliases), but then you must often use FooA and BarA explicitly — see experiments below.
In general, coercions distinguish between types that are definitionally equal but syntactically different, and so they're really strict about what code they allow.
Class Cl (a : Type).
Parameter A : Type.
Declare Instance cl_a : Cl A.
Parameter Foo Bar : Type -> Type.
Parameter conv : forall {k} `{Cl k}, Foo k -> Bar k.
Parameter func : forall {a}, Bar a -> bool.
SubClass FooA := Foo A.
SubClass BarA := Bar A.
Coercion conv_A := conv : FooA -> BarA.
(* Not used, doesn't help *)
(* Coercion bar_a_back := @id _ : BarA -> Bar A.
Coercion foo_a_back := @id _ : FooA -> Foo A. *)
(* Not usable, it violates uniform inheritance *)
(* Coercion conv_A' := conv : Foo A -> Bar A. *)
Definition test1 (b : FooA) : bool := func b.
Fail Definition test2 (b : Foo A) : bool := func b.
(* Print Coercion Paths Foo BarA. *)
Definition func_A : Bar A -> bool := func.
Definition test_3 (b : FooA) : bool := func_A b.
Fail Definition test_4 (b : Foo A) : bool := func_A b.
Definition func_A_1 : BarA -> bool := func.
Definition test_5 (b : FooA) : bool := func_A_1 b.
Fail Definition test_6 (b : Foo A) : bool := func_A_1 b.
Thank you @Paolo G. Giarrusso for the detailed explanation! That makes sense, though in my actual use case there are already a lot of functions using Foo and I suppose it would probably just be easier to write down the explicit coercions rather than wrapping those functions with ones that use FooA. Anyway, thanks for the very helpful information that helps me understand better how implicit coercions work!
Last updated: Oct 08 2024 at 14:01 UTC