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

)

please elaborate, this works:

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

or minimize, rather :-)

My bad, sorry... I just realized that `T`

is actually an `ordType`

(from https://github.com/arthuraa/extructures/blob/master/theories/ord.v).

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.

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

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

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

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

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.

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: Jun 23 2024 at 01:02 UTC