# Preventing pollution of the instance context during Import

**URL:** <https://discourse.rocq-prover.org/t/preventing-pollution-of-the-instance-context-during-import/942>\
**Category:** Using Rocq\
**Created:** [July 11, 2020, 3:54pm UTC](https://discourse.rocq-prover.org/t/preventing-pollution-of-the-instance-context-during-import/942 "2020-07-11T15:54:55Z")\
**Posts on this page:** 11\
**Page:** 1

<div class="post-metadata">

**Author:** ![Yannick](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yannick/32/321_2.png) [@Yannick](https://discourse.rocq-prover.org/u/Yannick)\
**Post date:** [July 11, 2020, 3:54pm UTC](https://discourse.rocq-prover.org/t/preventing-pollution-of-the-instance-context-during-import/942/1 "2020-07-11T15:54:55Z")

</div>

Hello everyone 🙂

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](https://github.com/coq/coq/issues/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](https://github.com/DeepSpec/InteractionTrees/blob/master/tutorial/Imp.v#L379). 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:

```auto
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?

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [July 11, 2020, 4:32pm UTC](https://discourse.rocq-prover.org/t/preventing-pollution-of-the-instance-context-during-import/942/2 "2020-07-11T16:32:25Z")

</div>

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

## Solution 1: `Loose Hint Behavior` (impractical)

> [@Yannick](#):
>
> Is there a way to import a file _without_ putting in scope the global instances that it declares?

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](https://coq.github.io/doc/v8.12/refman/proof-engine/tactics.html#hint-locality) — but I think there’s a mistake, see [tactics.rst: `Require A` is enough for `A`'s hints by Blaisorblade · Pull Request #12681 · rocq-prover/rocq · GitHub](https://github.com/coq/coq/pull/12681) 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 `Definition`s 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

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

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [July 11, 2020, 4:43pm UTC](https://discourse.rocq-prover.org/t/preventing-pollution-of-the-instance-context-during-import/942/3 "2020-07-11T16:43:11Z")

</div>

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

> **[theories/base.v · master · Iris / stdpp](https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/base.v#L274-277)**
>
> An extended "Standard Library" for Coq. \[\[coqdoc\]\](https://plv.mpi-sws.org/coqdoc/stdpp/)

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

```coq
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

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

```coq
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'.

```

---

<div class="post-metadata">

**Author:** ![Yannick](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yannick/32/321_2.png) [@Yannick](https://discourse.rocq-prover.org/u/Yannick)\
**Post date:** [July 11, 2020, 5:43pm UTC](https://discourse.rocq-prover.org/t/preventing-pollution-of-the-instance-context-during-import/942/4 "2020-07-11T17:43:03Z")

</div>

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:

```auto
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

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [July 13, 2020, 1:06pm UTC](https://discourse.rocq-prover.org/t/preventing-pollution-of-the-instance-context-during-import/942/5 "2020-07-13T13:06:17Z")

</div>

> [@Blaisorblade](#):
>
> 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.

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.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [July 13, 2020, 1:07pm UTC](https://discourse.rocq-prover.org/t/preventing-pollution-of-the-instance-context-during-import/942/6 "2020-07-13T13:07:23Z")

</div>

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](https://github.com/coq/coq/pull/12681#pullrequestreview-447225016).

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [July 13, 2020, 1:22pm UTC](https://discourse.rocq-prover.org/t/preventing-pollution-of-the-instance-context-during-import/942/8 "2020-07-13T13:22:24Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [July 13, 2020, 1:24pm UTC](https://discourse.rocq-prover.org/t/preventing-pollution-of-the-instance-context-during-import/942/9 "2020-07-13T13:24:16Z")

</div>

> [@Blaisorblade](#):
>
> @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](https://github.com/coq/coq/pull/12681#pullrequestreview-447225016).

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…

---

<div class="post-metadata">

**Author:** ![Yannick](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yannick/32/321_2.png) [@Yannick](https://discourse.rocq-prover.org/u/Yannick)\
**Post date:** [July 14, 2020, 2:38am UTC](https://discourse.rocq-prover.org/t/preventing-pollution-of-the-instance-context-during-import/942/10 "2020-07-14T02:38:00Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [September 8, 2020, 2:26pm UTC](https://discourse.rocq-prover.org/t/preventing-pollution-of-the-instance-context-during-import/942/11 "2020-09-08T14:26:42Z")

</div>

Sorry for not answering earlier.

> [@Yannick](#):
>
> 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?

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

> [@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?

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

---

<div class="post-metadata">

**Author:** ![mwuttke97](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mwuttke97/32/104_2.png) [@mwuttke97](https://discourse.rocq-prover.org/u/mwuttke97)\
**Post date:** [September 8, 2020, 3:08pm UTC](https://discourse.rocq-prover.org/t/preventing-pollution-of-the-instance-context-during-import/942/12 "2020-09-08T15:08:48Z")

</div>

> [@Zimmi48](#):
>
> 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).

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](https://github.com/coq/coq/wiki/Discourse).

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