The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Thanks for the suggestion, that solves our problem!

On 12/13/2016 05:33 PM, Jason Gross wrote:
> 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
> <mailto: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 *)