Stream: Coq users

Topic: Coercion source class error

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

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.

Paolo Giarrusso (Dec 22 2021 at 15:39):

or minimize, rather :-)

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

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.

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

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

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.

Paolo Giarrusso (Dec 22 2021 at 17:09):

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

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.

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: Sep 26 2023 at 12:02 UTC