Preventing pollution of the instance context during Import

Using Coq
1

Hello everyone :slight_smile:

In the abstract, my question(s) is the following.

  • Is there a way to require import a file without putting in scope the global instances that it declares?
  • Alternatively, what is the status of #7342, for having a command to remove an Instance from the Visible scope?
  • Even better, are there any plans to associate sets of instances to namespaces in the style of hint databases?
  • And finally, in the temporary absence of these, does any one have a good hack to achieve the initial goal?

For more of a specific, concrete context for the curious, I got bitten hard by the following issue. In the Interaction Trees library, we heavily rely on type classes to work with rewriting for non-trivial relations. Overall, it’s fairly stable, we’re quite happy with it.

However I have been working on using this library to prove a pass of compilation from a language developed independently, and things there got slow and unpredictable. I eventually fired up some debugging: turns out that while trying to justify rewrites, the inference mechanism is now exploring branches relying on checking whether my structure wouldn’t happen to be a lattice, semi-group, and so on…
And indeed, even if I don’t import it locally, the language depends on MathClasses! So that a myriads of instances sneaked in behind my back, and happily try to contribute where I don’t need them.

The smallest example for reference that I have at hand would be to consider the rewrite H happening here. If I trace it, I get a reasonable resolution in 9 steps, with the deepest branch being of depth 3.
Now if I first do Require Import MathClasses.interfaces.abstract_algebra., and perform the same rewrite, it still works, but now after more than 200 steps, exploring dead branches of roughly depth 15.

Once in my actual context where the rewrites happen in non-trivial terms, it gets unreasonable, and the import is imposed on me.

I would love to hear of any potentially hacky way to get around this problem immediately, but would also be happy to discuss long term solutions to tackle this issue in general.

Best,
Yannick

EDIT: Here is a self contained example avoiding any dependency on itrees:

From Coq Require Import
     Setoid
     Morphisms
     RelationClasses.

Section Foo.

  Variable op: nat -> nat.

  Variable rel: nat -> nat -> Prop.

  Context {rel_op_Proper: (Proper (rel ==> rel) op)}.
  Context {rel_refl: Transitive rel}.
  

  Goal forall (a b: nat) (REL: rel a b),
      rel (op a) (op b).
  Proof.
    intros.
    Typeclasses eauto := debug.
    rewrite REL.
    (* Resolution in 6 steps *)
    Undo.
    Require Import MathClasses.interfaces.abstract_algebra.
    rewrite REL.
    (* Resolution in over 100 steps *)
  Abort.

End Foo.

In my use case:

  • I cannot avoid this Require Import because I inherit it transitively from a file that I have to Require Import
  • I do not use on my side any reasoning inherited from MathClasses, I therefore do not need any Hint/Instances they export
  • I cannot afford this blowup in TC resolution.

Is there a way for the second rewrite in this example to still lead to the same resolution as the first one?

2

You’re right about the problem, but the direct solution doesn’t work so well.

Solution 1: Loose Hint Behavior (impractical)

Beware that Require is enough to get instances and hints imported, and that’s crucial to your problem — Import isn’t transitive, Require is and must be. The difference is that Import affects what names are available, while Require is about what modules are loaded at all.

Long term, what you’d want is Set Loose Hint Behavior "Warn" or Set Loose Hint Behavior "Strict" — but I’m not sure there are libraries that work with it, and you can only enable it if all libraries you use support it.

For details, see the manual — but I think there’s a mistake, see tactics.rst: `Require A` is enough for `A`'s hints by Blaisorblade · Pull Request #12681 · coq/coq · GitHub for a fix.

A possible alternative: Typeclass Opaque

Take an arbitrary instance among the problematic ones, and call it inst.

Hopefully (and I don’t know here), inst doesn’t apply to any term t but only to ones matching some pattern foo. If some of those instances doesn’t have a pattern, please post again with details.

However, after Definition bar := foo, typeclass search can still try inst — because bar is Typeclass Transparent. Often, and in your case, that’s undesirable, and you want Coq Definitions to act as (lightweight) abstraction barriers, at least for typeclass search. To that end, you can use Typeclasses Opaque bar.
If you want instances for foo to apply to bar, you can lift them explicitly before making bar TC-opaque; for instance, if you have Reflexive foo and want Reflexive bar, then you can declare

Instance: Reflexive bar := _. 
Typeclasses Opaque bar.

That can require some boilerplate, which can be annoying, but that boilerplate is easy to write and can save headaches — I’ve learned this style from Robbert Krebbers, one of the Iris authors and who IIUC also contributed to math-classes.

3

Separately, Params instances can also help speed up TC search for setoid rewriting — they help infer the correct arity to consider.

Reducing the arity can help, so in Iris you’d go as far as swapping the two arguments of interp_imp. Then, instead of

Global Instance eutt_interp_imp {R}:
    Proper (@eutt E R R eq ==> eq ==> @eutt E' (prod (env) R) (prod _ R) eq)
           interp_imp.

you’d have

Global Instance eutt_interp_imp {R} x:
    Proper (@eutt E R R eq ==> @eutt E' (prod (env) R) (prod _ R) eq)
           (interp_imp x).

I see that making this swap would hinder fiting your APIs in this case; maybe it helps elsewhere, or maybe you swap them but write a wrapper with the right signature.

Definition interp_imp' ... // flipped version of interp_imp.
Definition interp_imp {E A} (t : itree (ImpState +' E) A) : stateT env (itree E) A := flip interp_imp'.
4

Hi @Blaisorblade,

Thanks for your answer! I agree that the Loose Hint Behavior seems to be a significant step in what we need on the long run. However MathClass do not use it so I’m afraid in my case that’s for now inapplicable.

I’m a bit rushed by time Today so I apology to not address your suggestions fully, I will have to get back to it later. However at a first read I don’t think I quite understand your technique with Typeclass Opaque. Do you have maybe a pointer in Iris where it’s used that I could look at?

I will also look at your third suggestion to speed up things a bit later, it looks like an excellent insight that I should dig into!

That being said, speeding up things slightly on our side won’t be sufficient in this case I’m afraid.

Let me already rephrase my question as a self contained example of my issue so that it does not depend on ITrees:

From Coq Require Import
     Setoid
     Morphisms
     RelationClasses.

Section Foo.

  Variable op: nat -> nat.

  Variable rel: nat -> nat -> Prop.

  Context {rel_op_Proper: (Proper (rel ==> rel) op)}.
  Context {rel_trans: Transitive rel}.
  

  Goal forall (a b: nat) (REL: rel a b),
      rel (op a) (op b).
  Proof.
    intros.
    Typeclasses eauto := debug.
    rewrite REL.
    (* Resolution in 6 steps *)
    Undo.
    Require Import MathClasses.interfaces.abstract_algebra.
    rewrite REL.
    (* Resolution in over 100 steps *)
  Abort.

End Foo.

In my use case:

  • I cannot avoid this Require Import because I inherit it transitively from a file that I have to Require Import
  • I do not use on my side any reasoning inherited from MathClasses, I therefore do not need any Hint/Instances they export
  • I cannot afford this blowup in TC resolution.

Is there a way for the second rewrite in this example to still lead to the same resolution as the first one?

Best,
Yannick

5

I think there is a confusion here. This option changes the behavior for the user, but doesn’t help the library author to provide less invasive global instances / hints.

Since 8.12, there is finally a solution for library authors: the export attribute (to use instead of global / Global), although for now I believe it is only supported on Hint commands and not on Instance.

But for your use case, you might still have a try at using Set Loose Hint Behavior "Strict" as it might turn out to do what you need.

1 Like
6

Uh, thanks for the example. No idea what instances are triggering. Analysis would need the debug trace, at least the one from Set Typeclasses Debug; no time to install math-classes myself today.
But for now, I doubt Typeclasses Opaque would help here.

@Zimmi48 Ah, guess export gives the right behavior but must be enabled per-hint? Makes sense to me. Now I get a bit more what you meant on GitHub.

8

BTW, regarding the use of multiple instance databases, here is a trick that you could use (disclaimer: I’ve never really tried it in practice):

  1. Define your instances in a separate hint database. To do this, you need to use the Definition + Hint Resolve commands instead of the Instance command.

  2. Redirect typeclass search to your custom hint database by adding a hint like Hint Extern 0 => typeclasses eauto with my_instance_db : typeclass_instances.

The main catch (that is likely to make this not work in practice) is that typeclasses eauto and typeclasses eauto with... have a slightly different behavior that can be related to how well typeclass search is performed. But it might still be worth a shot.

9

Yes. At some point, there will probably be an option to make this the default locality, and at an even further point we can expect this export locality to become the default…

10

There is kind of two discussions overlapping here: how to design a library to restrict how invasive its Hints and Instances are, and how as a user of libraries to mitigate this invasion. I am trying to understand what have been suggested so far.

My practical situation calls for a pragmatic user-side solution if possible: to make progress, I need to be able to (transitively inherit) Require Import MathClasses.interfaces.abstract_algebra. without having it hijacking my TC resolution, as described in the minimal example above.

Having looked a bit closer into it, in my use case, I believe that the main culprit is the following External Hint:
Hint Extern 4 (?f _ = ?f _) => unshelve eapply (sm_proper (f:=f)).
It fires up early, and from there all hell is loose.

The Set Loose Hint Behavior "Strict" option appears to be close to what I need. However having given it a shot, it does not change anything in the minimal example above. I am unsure why.
On a related note, I am unsure: is the use of instances by the TC inference mechanism Hints as well, and hence affected by this mechanism, or is considered a separate mechanism?

The Remove Hints command falls short as well, since it cannot apply to External Hints.

I’ve @Zimmi48 suggestion to redirect typeclass search makes sense and would be worth trying if I’m really cornered, but I would like not to have to go to such an invasive change in the itree library if I can help it.

Unless I miss something, other propositions are propositions to limit this problem when designing libraries. Which is certainly how we should move forward, but for pragmatic reasons I need to work my way around this issue on the user side at the moment.

Thanks,
Yannick

P.S. : @Zimmi48, I was considering cross-posting to the coq-list to expand my reach. Is there any etiquette against such cross post with all the discussions plateforme we currently have?

11

Sorry for not answering earlier.

Yes, TC instances are hints (in the special typeclass_instances database).

At some point, I hope to set up something to get all posts to Discourse relayed to Coq-Club so that old schoolers are not completely left out, but in the meantime, I guess we cannot prohibit people from reaching as large an audience as possible by cross-posting (although linking back to the Discourse topic might be a strategy to avoid the spread of answers on multiple platforms).

12

To this I can add that the mailing-list support of Discourse already
works quite nice. It is possible to read posts in the comfort of your
mail client. Answering also works (as demonstrated by this post).
Starting a new topic is also possible: 1.

One big advantage of Discourse is that it is much more accessible to
users that are not familiar with mailing lists. Also, searching is much
easier (if you don’t have a large amount of mails stored on your
computer), and amending posts is possible. (But edits are not relayed to
the mailing list mode. Because of this, the posts are delayed a few
minutes before being sent to the mailing list.)

EDIT: It turned out that Discourse removed the quotation at the beginning of the post. I’ve added it again (in Discourse).

1 Like