coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Importing module duplicates instances

From: Li-yao Xia <lysxia AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Importing module duplicates instances
Date: Thu, 8 Feb 2018 21:06:40 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lysxia AT gmail.com; spf=Pass smtp.mailfrom=lysxia AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f47.google.com
Ironport-phdr: 9a23:d+BNkRIaMgAw72kSZtmcpTZWNBhigK39O0sv0rFitYgQI/nxwZ3uMQTl6Ol3ixeRBMOHs6sC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffxhEiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhjkHOTAk82/ZhMJ/g61HrxyuvBF/34zZbZuJOPZicK7Qf9UXTndBUMZLUCxBB5uxYY0OD+YYPedXtY79rEYPohu/HwanGeTiyjtIh3/t0qw60v4uHBrJ3AwlBd0OsXDUoM/pO6cVVOC41a/FxijAYfNOwTrx9pTEfxQ7rfyPXb98a9TdxVQhGg/fgVidq5TpMy2J2ukMqWSX8vRsWOK1h2MmtQ19uCajy8cqh4LUnIwa0ErE+j98wIstJd23Vkp7Ydm8HZtVrS6aNo92Tto8Q2FrpCo207MGtJG5cSQQx5QnwBnfa/ODc4eW+B7sSOGRITJgiHJkfrKwmQqy/FC+xuHgUsS4ylVHoypfntXSq3wA2Qbf58eFR/dl+0euwzeP1wTd6uFeJkA0kLLWK5ohw74rmZsTsF7MEzT5mEXzlqCWd0Ek9vK05OTgZ7XqvoWcOJNsigHiLqQundSyDvg/MggXRmSU5eC81KD48kDiW7VLjvg2krHDv5zAJMQboLS5Aw5P3Yo55Ra/FWTu7NNNln4eaVlBZRivjo7zOliILuqrI+24hgGIkXJ6zveODrzoSsHJP2PTkb7JcrN06koaww02m4MMr6lIA60MdaqgEnT6s8bVW0dgYl6Eht3/AdA47bswHGeGA6uXKqTX6Aba6ecmIu3Kb4gQ6m+kd6oVosX2hHp8omczOLGz1MJOOn+9F/ViZU6eZCi024pTISIxpgM7CdfSphiCXDpUPSvgWqs94nQlC9rjA9ucAI+qh7OF0WGwGZgEPm0=

Hello everyone,

I'd like to rename some module M to N. However, using "Module N := M.", instance resolution will try every typeclass instance in M a second time in N, commonly resulting in exponential-time behavior.

Below is a minimal example (tested with Coq 8.6 and 8.7). Shouldn't both "Check" commands to produce the same debug output?

Is there a better way to rename modules?

Li-yao

---

Module M.
Class C (n : nat) := {}.
Instance CS (n : nat) `{C n} : C (S n).
Definition f (n : nat) `{C n} : unit := tt.
End M.

Set Typeclasses Debug.

(* simple apply M.CS *)
Check (M.f 1).

Module N := M.

(* simple apply N.CS
simple apply M.CS *)
Check (N.f 1).

[Coq-Club] Importing module duplicates instances, Li-yao Xia, 02/09/2018