Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Module Include leads to duplicate type class instances

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Module Include leads to duplicate type class instances


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Module Include leads to duplicate type class instances
  • Date: Tue, 13 Dec 2016 16:33:24 +0000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f172.google.com
  • Ironport-phdr: 9a23:zwu4+xXWie8JQXAyFJU9UcBQ/izV8LGtZVwlr6E/grcLSJyIuqrYZRyFt8tkgFKBZ4jH8fUM07OQ6PG7HzJcqs3e+DBaKdoXCE9D0Z1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/hKiO/MjYZBwNjz6ga/smJxKv6A7Vq8M+gI14K693xAGf8VVSfOED52pzIlTbsAz7/dz4qJxq6CNWtOgm7NURear/dqU8C7dfCWJ1YCgO+MT3uEybHkO07XwGXzBOnw==

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



Archive powered by MHonArc 2.6.18.

Top of Page