The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

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