The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I would call this a misfeature or a known design issue.  There is a similar issue with module functor application.

If you just want namespacing, try this module structure instead:

Module Export foo1.
  Module bar. ... End bar.
End foo1.

Module Export foo2.
  Module bar. ... End bar.
End foo2.

...

If you also want [Import bar] to do the right thing, you can create another module [bar] which [Export]s all of the inner modules [bar].

On Tue, Dec 13, 2016, 3:22 AM Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

Hi Coq-club,

We noticed that Including a module leads to all type class instances
being redeclared. In the example below this will make type class search
backtrack on foo.c_and and bar.c_and for each subterm, and thereby
turning a search that takes linear time into a search that takes
exponential time.

Is it a feature or a bug that type class instances are being redeclared
when a module is included?

Does someone know a workaround for the problem? Some solutions that we
came up with:

- We could just not declare instances in the module `foo`, but
instead use `Existing Instances` in `bar`. [In our actual code we have
about 100 such instances in `foo`, so this does not really scale.]

- We could `Export` foo in bar instead of including it, but that makes
it impossible to refer to lemmas lem in foo as bar.lem. [In our actual
code, we are using modules this way to include several modules `foo1`,
`foo2` and `foo3` into one module `bar` so as to be able to refer to
lemmas in `foo1`, `foo2` and `foo3` through one common namespace `bar`).

Best,

Robbert

* Thanks to JH Jourdan for finding this problem in our actual code:
https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/base_logic/base_logic.v

---------------

Class C (P : Prop) := { }.

Module foo.
   Instance c_true : C True.
   Instance c_and P Q : C P -> C Q -> C (P /\ Q).
End foo.

Module bar.
   Include foo.
End bar.

Goal C (True /\ True /\ True /\ True /\ True /\ True /\ True /\ True /\
True /\ True /\ True /\ True /\ True /\ False).
Typeclasses eauto := debug.
Time try apply _. (* 2.148s *)