Stream: Coq users

Topic: Coercion source class error


view this post on Zulip Joshua Grosso (Dec 22 2021 at 15:08):

If I have a module with a Parameter T : Type and function f : T -> string, is there a way to define something like Coercion f : T >-> string?
(If I try that as-is, I get Error: Cannot recognize T as a source class of f.)

view this post on Zulip Paolo Giarrusso (Dec 22 2021 at 15:38):

please elaborate, this works:

Require Import Strings.String.
Parameter T : Type.
Parameter f : T -> string.
Coercion f : T >-> string.

view this post on Zulip Paolo Giarrusso (Dec 22 2021 at 15:39):

or minimize, rather :-)

view this post on Zulip Joshua Grosso (Dec 22 2021 at 16:46):

My bad, sorry... I just realized that T is actually an ordType (from https://github.com/arthuraa/extructures/blob/master/theories/ord.v).

view this post on Zulip Joshua Grosso (Dec 22 2021 at 16:49):

Unsurprisingly, Coercion won't let (Ord.sort T) be a source class... maybe I should manually Let T' : Type := Ord.sort T. and instead define f : T' -> string and Coercion f : T' >-> string, or something like that.

view this post on Zulip Paolo Giarrusso (Dec 22 2021 at 17:04):

you can, but probably not Let; also coercion matching is syntactic, so you need an identity coercion if you want to also handle Ord.sort T...

view this post on Zulip Paolo Giarrusso (Dec 22 2021 at 17:06):

Subclass lets you add a definition and coercion (https://github.com/Blaisorblade/dot-iris/blob/master/theories/Dot/examples/hoas.v#L43 has an example and the manual describes it); I'm not sure in which direction the generated coercion is...

view this post on Zulip Paolo Giarrusso (Dec 22 2021 at 17:07):

I suspect with SubClass T' := Ord.sort T. you'd get a coercion to T', which would chain with your f.

view this post on Zulip Paolo Giarrusso (Dec 22 2021 at 17:09):

Indeed, https://coq.inria.fr/refman/addendum/implicit-coercions.html#coq:cmd.SubClass agrees.

view this post on Zulip Paolo Giarrusso (Dec 22 2021 at 17:11):

Beware that coercions can be polymorphic, but only of type forall args..., class1 args... -> class2 args..., with both classes having the same arguments (this is the uniform inheritance condition); identity coercions are an exception.

view this post on Zulip Joshua Grosso (Dec 22 2021 at 20:23):

Thanks for all the details. It seems like dealing with the occasional explicit f is the path of least resistance (especially because I'm not sure if changing the type of f is worth the overhead) :-P


Last updated: Jan 27 2023 at 01:03 UTC