The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

On Thu, Feb 13, 2014 at 5:03 PM, Kirill Taran <kirill.t256 AT gmail.com> wrote:

I can't reproduce it on small example and my real code is too complex to paste it here.

I have some scripts at https://github.com/JasonGross/coq-bug-finder that will minimize erroring Coq code (by removing unused definitions, admitting lemmas, etc), which might help you reduce it, at least if the complexity is spread across definitions and lemmas.  I'd be glad to provide help with running it, if you're interested.

I'd suggest turning on [Set Printing All] and maybe [Set Printing Universes] and ensuring that implicits aren't hiding things.  Also make sure that you're not shadowing the relevant names with local variables.  Barring that, try replacing [y] with [y : Container (Tag2Type TagA)] and see where it gives the error message.  Then try [(y : Container TypeA) : Container (Tag2Type TagA)] and [((fun x => x) : Container TypeA -> Container (Tag2Type TagA)) y].

-Jason