The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Some possibilities:
- foo sets some options that change the meaning of the constants in bar when inlined (e.g., primitive projections, implicit arguments, instances), or overrides constants from the standard library.  Question: do you still have this issue if you wrap the code from foo in [Module foo. ... End foo.]?  What if you inline all of bar first, and then inline foo?  What of you inline bar without inlining foo?  What if you [Require foo.  Require bar.]?
- The code happens to trigger the fact that the universe minimization algorithm, and thus the number of universe variables and the constraints generated, is sensitive to the name of the file the constants are declared in.  What if you name your new, blank file "foo.v" (or pass -top foo, or something)?
- You used -quick, and are depending on universes of Qed'ed lemmas
- The universes assigned to things in [far] are somehow sensitive to the order of the [Require]s at the beginning of Bar.v, and importing [foo] changes this order.
- You compiled [bar] with different options (--type-in-type, --indices-matter, etc.) than you're comiling the current file.
- The universe minimization algorithm equates universes that it should not equate in bar, which would not be equated if you imported foo first.
- You do a tactic invocation or typeclass instance resolution whose success path is sensitive to existing universe constraints.

Do any of these seem plausible?

-Jason

On Sep 3, 2015 10:24 PM, "Gregory Malecha" <gmalecha AT gmail.com> wrote:

Hello --

I'm working on a development trying to track down a universe inconsistency and I've run into difficulties tracking it down. I have a blank file and do:

Require Import foo.

Require Import bar.

Here I get a universe inconsistency when including bar.

So I include the text of foo verbatim and run it, I get a universe inconsistency. I included contents of foo to find the minimal amount that is necessary to retain the universe inconsistency. So now I have,

(* a bunch of stuff included from foo *)

Require Import bar. (* <<--- universe inconsistency here *)

Now I repeat the process on bar. But when I inline the contents of bar and evaluate it, Coq accepts all of the definitions without a universe inconsistency.

Is this expected behavior? Are there extra checks that are occuring when importing a file that are not processed when the definitions are done inline? Is there some reason why inlining should make universes consistent?

Thank you.

--

gregory malecha