Hint Mode + again

[samuelgruetter]

While working on silveroak, I got an error where straightline_call says Error: Cannot infer this placeholder of type "spec_of put_wait_get" (no type class instance found), and Check (_ : spec_of put_wait_get) and Check (_ : spec_of "put_wait_get") both agree, they can’t find any instance either.

However, the following instance is available:

spec_of_put_wait_get : forall {word : word 32}, map.map word byte -> spec_of "put_wait_get"

and it is registered as a typeclass instance and shows up in Print HintDb typeclass_instances as

For spec_of ->   simple eapply @spec_of_put_wait_get(level 3, pattern spec_of "put_wait_get", id 0) 

and if I do

Set Printing Implicit.
Check spec_of_put_wait_get.

I get

@spec_of_put_wait_get (@MMIO.word p) (@MMIO.mem p)
     : spec_of "put_wait_get"

from which I conclude that Coq is also able to infer the missing arguments of @spec_of_put_wait_get, so overall, the typeclass search should succeed, so why does it fail??

So why can Check spec_of_put_wait_get infer the missing arguments, whereas Check (_: spec_of put_wait_get) cannot?

Using Set Typeclasses Debug Verbosity 2 and comparing the output of the two, I think I found out why: Check spec_of_put_wait_get first looks for a word 32, finds (@MMIO.word p), and then looks for a (map.map (@MMIO.word p) byte), which succeeds as well. On the other hand, Check (_: spec_of put_wait_get) starts by finding spec_of_put_wait_get, which opens two subgoals, and since the first subgoal appears as a dependency in the second subgoal, the first subgoal is shelved, and typeclass search works on the second subgoal, which appears as (map.map ?word byte). Now, since we have a Global Hint Mode map.map + + : typeclass_instances in coqutil.Map.Interface, the two arguments of map.map are treated as inputs to typeclass search, and since one of them is unknown, this subgoal is “suspended”, and resolution continues “on the remaining goals”, but there are none (because the shelved ones are not considered), so it tries one more time, and then sees that it has reached “a fixed point when the set of remaining suspended goals does not change”, so no solution is found. This explanation is derived from combining the output of Set Typeclasses Debug Verbosity 2 with the explanation in this paragraph in the the manual:

The mode hints (see Hint Mode) associated with a class are taken into account by typeclasses eauto. When a goal does not match any of the declared modes for its head (if any), instead of failing like eauto, the goal is suspended and resolution proceeds on the remaining goals. If after one run of resolution, there remains suspended goals, resolution is launched against on them, until it reaches a fixed point when the set of remaining suspended goals does not change.

A simple solution to this problem is to simply do Global Hint Mode map.map - - : typeclass_instances, because then typeclass search succeeds on the (map.map ?word byte) subgoal.

I also tried Set Typeclasses Dependency Order, but that didn’t help.

Another solution might be to redeclare each instance like Instance spec_of_put_wait_get': spec_of "put_wait_get" := spec_of_put_wait_get., and to adapt the program logic Ltac to unfold all spec_of instances until they look like a spec rather than a redeclared instance, but that sounds cumbersome.

The reason why this hasn’t shown up earlier is that all previous code either had all declarations and usages of spec_of instances in the same Section, so that the instances were not parameterized over map instances, or the map instances were inside a parameter record that got inferred as a whole, but as soon as a spec_of instance declared in one Section depends on a map instance and is needed in a different file or Section, typeclass search will fail as described above.

This is quite a bad usability issue, and I expect it to appear more often the more bedrock2 is used, especially when library functions are reused by different client functions.

Currently my only solution is Global Hint Mode map.map - - : typeclass_instances, but I’d be curious if you find another solution @andres-erbsen?

[JasonGross]

I don't suppose setting a mode of - for word changes anything? I think this might also be worth a bug report on Coq?

[andres-erbsen]

since the first subgoal appears as a dependency in the second subgoal, the first subgoal is shelved, and typeclass search works on the second subgoal

This is the part that seems wrong/surprising to me. It'd be great if we got coqdev advice on whether this is intended and/or how to avoid it.

Would "just use parameter records instead of word and map parameters" be an acceptable workaround in your use case?

[samuelgruetter]

I don't suppose setting a mode of - for word changes anything?

It does change something: It sends typeclass search into an infinite loop! I minimized the infinite loop to the following:

Class word := { }.

Module MMIO.
  Class parameters := {
    word :> word;
  }.
End MMIO.

Instance MMIO_compiler_params{word: word}: MMIO.parameters := {
  MMIO.word := word;
}.

Check MMIO.word. (* loops for a few seconds, then stack overflow *)

I'm surprised that Coq doesn't have any mechanism to avoid such loops. Is it my responsibility to set Hint Mode or other flags appropriately in the code base to make sure no loops happen? If so, do you have a systematic approach to convince yourself that a codebase is typeclass-search-loop free? Or is this a Coq bug?

I think this might also be worth a bug report on Coq?

I'll try to also isolate the original bug above.

This is the part that seems wrong/surprising to me. It'd be great if we got coqdev advice on whether this is intended and/or how to avoid it.

I'll ask once I have isolated it.

Would "just use parameter records instead of word and map parameters" be an acceptable workaround in your use case?

No, because I'm still trying to get rid of parameter records, which are one of the biggest sources of user-unfriendliness (syntactically different implicit arguments cause rewrite, lia, ecancel_assumption and many other tactics to stop working).

[JasonGross]

I'm surprised that Coq doesn't have any mechanism to avoid such loops.

It has a manual mechanism called Hint Cut

Is it my responsibility to set [...] flags appropriately in the code base to make sure no loops happen?

Generally, yes

If so, do you have a systematic approach to convince yourself that a codebase is typeclass-search-loop free?

Write out the typeclass hint graph and make sure it's a dag?

Or is this a Coq bug?

What's the typeclass debug log? It's probably not a bug, but we need to see the log to be sure.

[samuelgruetter]

It has a manual mechanism called Hint Cut

That only allows regular expressions to match branches to cut, but I'd like to cut all branches with a duplicate hint, but I guess that's not expressible as a regex.

Write out the typeclass hint graph and make sure it's a dag?

The way we were intending to use parameter records keeps creating situations where it's not a DAG. Here's an example:

Module Semantics.
  Class parameters := {}.
End Semantics.

Module Lib1.
  Class parameters := {
    foo: nat;
    semantics_params :> Semantics.parameters;
  }.
End Lib1.

Module SubprojectWithFooEqual42.
  Module CommonDefinitions.
    Instance make_Lib1_params{p: Semantics.parameters}: Lib1.parameters := {
      foo := 42;
      semantics_params := p;
    }.
  End CommonDefinitions.

  Module File1.
    Section WithParams.
      Context {p: Semantics.parameters}.
      (* use definitions of Lib1... *)
    End WithParams.
  End File1.

  Module File2.
    Section WithParams.
      Context {p: Semantics.parameters}.
      (* use definitions of Lib1... *)
    End WithParams.
  End File2.

  Module File3.
    Section OoopsForgotToRequireParameters.
      Fail Timeout 1 Check (_ : Semantics.parameters).
    End OoopsForgotToRequireParameters.
  End File3.
End SubprojectWithFooEqual42.

To break the loop, we'd have to stop sharing parameter record transformer instances like make_Lib1_params, and each file would have to redeclare all of them. This would lead to boilerplate explosion and even more syntactically mismatching implicit arguments. Or is there a better way to do parameter records in this example?

[samuelgruetter]

I guess make_Lib1_params could be a Definition, and then I'd do Existing Instance make_Lib1_params in each section, but still not so thrilled by it ...

[samuelgruetter]

Or maybe we should just ban :> inside typeclass definitions, and instead of doing tc_field :> T, do Existing Instance tc_field but only inside sections. This would require a series of Existing Instance lines at the beginning of each section, but would maintain the invariant that Requireing a file never adds parameter record projections as typeclass hints, so in order to know all parameter record projections in the typeclass hints, it suffices to look at all Existing Instance commands of the current section. And since in this setting, a loop always contains at least one projection, the local list of Existing Instance could serve as a starting point for checking for loops.

[samuelgruetter]

On the other hand, one benefit of parameter records is that if several files take the same n arguments, we only need to spell them out once in the definition of a parameter record, instead of spelling them out at the beginning of each file, but if we require an Existing Instance command for each field which itself is a typeclass, that benefit is gone.

[samuelgruetter]

This is the part that seems wrong/surprising to me. It'd be great if we got coqdev advice on whether this is intended and/or how to avoid it.

See https://github.com/coq/coq/issues/14707