Jason Gross (Oct 31 2022 at 20:51): Jason Gross (Oct 31 2022 at 20:51):Does Typeclasses Dependency Order actually do anything?
Jason Gross (Oct 31 2022 at 20:54):Typeclass resolution seems to always try to solve the nondependent typeclass goal first, regardless of how I set this
Gaëtan Gilbert (Oct 31 2022 at 21:24):I think you would need to find a caller that uses split:false, ie unification.ml or rewrite.ml, to see a difference
Jason Gross (Oct 31 2022 at 22:51):Why is it set up like that? (And what does split do?)
(It's documented at https://coq.inria.fr/refman/addendum/type-classes.html#coq:flag.Typeclasses-Dependency-Order as a general setting for typeclass resolution...)
Jason Gross (Oct 31 2022 at 23:02):@Gaëtan Gilbert Do you know how to make https://github.com/coq/coq/issues/16760 work?
Last updated: Oct 13 2024 at 01:02 UTC