Stream: Coq users

Topic: `Typeclasses Dependency Order`


view this post on Zulip Jason Gross (Oct 31 2022 at 20:51):

Does Typeclasses Dependency Order actually do anything?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...)

view this post on Zulip 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: Jan 29 2023 at 05:03 UTC