Hint Mode + again about bedrock2 HOT 9 OPEN

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

from bedrock2.

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?

from bedrock2.

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).

from bedrock2.

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.

from bedrock2.

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?

from bedrock2.

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 ...

from bedrock2.

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.

from bedrock2.

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.

from bedrock2.

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 coq/coq#14707

from bedrock2.