I would like to implement what I discussed here: https://coq.discourse.group/t/generalizing-coercions-to-infer-typeclass-arguments/1241/4?u=cohencyril and tried to impulse one day here: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Reverse.20coercions

@Enrico Tassi

Hello, is this the same thing as https://arxiv.org/abs/1103.3320

Can we meet in breakout room 2 and talk about it?

Did you implement it in Matita ?

ok for room two

Hacking session on this topic tomorrow at 10:20 AM

Great @Enrico Tassi , you mind updating the schedule in the wiki too?

FYI We are starting hacking coercions in room 1

https://github.com/coq/coq/pull/15693

We resumed working with @Enrico Tassi. We noticed a failure in mathcomp when trying out the PR when replacing the old def of `{poly R}`

by a simpler one.

We are in Room 1

The problem was that we immediately encounter an occurrence of `predArgType >-> Type <-< ringType`

The solution for now is to deal only with types which have coercions either to `Sortclass`

or `Funclass`

What are reverse coercions? / what's the idea?

@Jason Gross Here is the original discussion

The paper I wrote a long ago is in topic. We did open a draft pr with a few examples.

Thanks! And sorry, I missed the earlier messages. I guess I should narrow streams more to see the context.

We did push a bunch of commits cleaning up a lot and kind of implementing the search for a common point to which the inferred and expected type can be coerced, on coercion path must be reversible (although the check for reversibility is still dummy).

Last updated: Jan 29 2023 at 14:02 UTC