Cyril Cohen (Feb 15 2022 at 09:41): Cyril Cohen (Feb 15 2022 at 09:41):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
Cyril Cohen (Feb 15 2022 at 09:52):@Enrico Tassi
Enrico Tassi (Feb 15 2022 at 09:53):Hello, is this the same thing as https://arxiv.org/abs/1103.3320
Cyril Cohen (Feb 15 2022 at 09:54):Can we meet in breakout room 2 and talk about it?
Cyril Cohen (Feb 15 2022 at 09:54):Did you implement it in Matita ?
Enrico Tassi (Feb 15 2022 at 09:54):ok for room two
Enrico Tassi (Feb 15 2022 at 10:17):Hacking session on this topic tomorrow at 10:20 AM
Emilio Jesús Gallego Arias (Feb 15 2022 at 10:52):Great @Enrico Tassi , you mind updating the schedule in the wiki too?
Cyril Cohen (Feb 16 2022 at 09:26):FYI We are starting hacking coercions in room 1
Enrico Tassi (Feb 16 2022 at 10:50):https://github.com/coq/coq/pull/15693
Cyril Cohen (Feb 16 2022 at 13:24):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.
Cyril Cohen (Feb 16 2022 at 13:24):We are in Room 1
Cyril Cohen (Feb 16 2022 at 13:26):The problem was that we immediately encounter an occurrence of predArgType >-> Type <-< ringType
Cyril Cohen (Feb 16 2022 at 13:29):The solution for now is to deal only with types which have coercions either to Sortclass or Funclass
Jason Gross (Feb 16 2022 at 20:42):What are reverse coercions? / what's the idea?
Ali Caglayan (Feb 16 2022 at 20:57):@Jason Gross Here is the original discussion
Ali Caglayan (Feb 16 2022 at 20:57): Enrico Tassi (Feb 16 2022 at 21:13):The paper I wrote a long ago is in topic. We did open a draft pr with a few examples.
Jason Gross (Feb 16 2022 at 21:45):Thanks! And sorry, I missed the earlier messages. I guess I should narrow streams more to see the context.
Enrico Tassi (Feb 17 2022 at 13:56):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: Jun 10 2023 at 23:01 UTC