Stream: Coq users

Topic: Hint Mode on type classes, best practice?


view this post on Zulip Li-yao (Jan 09 2024 at 15:40):

Some time ago, I discovered Hint Mode on type classes, and got the idea that ! is the best mode by default, but I kinda forgot the details why since then. Would any typeclass experts like to weigh in about such a practice? For concreteness, I am experimenting with such a change in coq-ext-lib https://github.com/coq-community/coq-ext-lib/pull/126 and found exactly one (fixable) breakage caused by it on opam, but perhaps there are other uses of the current behavior elsewhere?

view this post on Zulip Paolo Giarrusso (Jan 09 2024 at 19:41):

Coq's default mode is appropriate for _output_ variables, while mode ! is better for inputs... but if you have Class Foo (X : Type) := ..., X should typically _not_ be an output.
Examples:

view this post on Zulip Paolo Giarrusso (Jan 09 2024 at 19:44):

Let's assume we declare Class Foo (X : Type) := foo : X. Then

Instance fooPair {A B} `{Foo A, Foo B} : Foo (A, B). Definition baz := foo.

Here, typechecking baz will diverge!

view this post on Zulip Paolo Giarrusso (Jan 09 2024 at 19:46):

Here, TC search for @foo ?X ?FooX can apply @fooPair ?A ?B ?FooA ?FooB, and search for ?FooA : Foo ?A and ?FooB : Foo ?B — and fooPair applies to both, leading to a loop!

view this post on Zulip Paolo Giarrusso (Jan 09 2024 at 19:47):

Using mode !, instead, searches for Foo ?X will be stuck, because there is no info to drive the search.

view this post on Zulip Paolo Giarrusso (Jan 09 2024 at 19:48):

This shows why Lean defaults to !, and TC-heavy libraries like stdpp and Iris strive to use it too.

view this post on Zulip Paolo Giarrusso (Jan 09 2024 at 19:50):

Sometimes, switching to ! will require extra annotations where inference picked the correct solution. This is a bit unfortunate, but usually it is hard to avoid. _Some_ cases are due to bugs, but stdpp/Iris for instance have moved to ! regardless if the impact of bugs isn't excessive.

view this post on Zulip Paolo Giarrusso (Jan 09 2024 at 19:53):

Forgot: with Instance fooNat : Foo nat. Definition bar1 := foo. Instance fooN : Foo N. Definition bar2 := foo. will give foo1 : nat and foo2 : N. Among all instances that have the highest priority (here, all instances), the instance that is declared or loaded latest has the higher priority.

view this post on Zulip Paolo Giarrusso (Jan 09 2024 at 19:54):

Sorry the snippets are untested, this is all from memory.

view this post on Zulip Karl Palmskog (Jan 09 2024 at 20:00):

in my experience, adding hint modes mostly means adding a bunch of ! with an occasional -

view this post on Zulip Karl Palmskog (Jan 09 2024 at 20:02):

the problem is that adding modes will generally lead to complex breakages in projects that depend on the classes, so it's not easy to do in isolation. Probably the best place to try to enforce hint mode best practices is the Coq Platform

view this post on Zulip Li-yao (Jan 10 2024 at 14:51):

Thanks a lot @Paolo Giarrusso and @Karl Palmskog That is comforting to know :)


Last updated: Jun 23 2024 at 05:02 UTC