coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 *)
- [Coq-Club] Module Include leads to duplicate type class instances, Robbert Krebbers, 12/13/2016
- Re: [Coq-Club] Module Include leads to duplicate type class instances, Jason Gross, 12/13/2016
- Re: [Coq-Club] Module Include leads to duplicate type class instances, Robbert Krebbers, 12/13/2016
- Re: [Coq-Club] Module Include leads to duplicate type class instances, Ralf Jung, 12/15/2016
- Re: [Coq-Club] Module Include leads to duplicate type class instances, Guillaume Melquiond, 12/16/2016
- Re: [Coq-Club] Module Include leads to duplicate type class instances, Jason Gross, 12/16/2016
- Re: [Coq-Club] Module Include leads to duplicate type class instances, Ralf Jung, 12/16/2016
- Re: [Coq-Club] Module Include leads to duplicate type class instances, Jason Gross, 12/16/2016
- Re: [Coq-Club] Module Include leads to duplicate type class instances, Guillaume Melquiond, 12/17/2016
- Re: [Coq-Club] Module Include leads to duplicate type class instances, Ralf Jung, 12/16/2016
- Re: [Coq-Club] Module Include leads to duplicate type class instances, Jason Gross, 12/16/2016
- Re: [Coq-Club] Module Include leads to duplicate type class instances, Guillaume Melquiond, 12/16/2016
- Re: [Coq-Club] Module Include leads to duplicate type class instances, Jason Gross, 12/13/2016
Archive powered by MHonArc 2.6.18.