flip are defined twice in stdlib with the same definition: without universe polymorphism in
Program.Basics and with universe polymorphism in
The name clash makes some behaviors difficult to trace. Is there a strong reason to have both? If so is there a standard way to give different names in such a situation?
it's possible that program doesn't need them to be monomorphic, in which case we could just define the polymorphic version somewhere that both depend on (probably Init/Datatypes)
Beware with flip, any lemma that mentions it would turn it into a polymorphic one, causing mayhem in performance of setoid rewriting
flip is caveat emptor, then I think it should have some warning...
arrow is also used by setoid rewriting, but I don't know whether it's as critical as flip, which is used pervasively for relation normalization
(see https://github.com/coq/coq/issues/14488 for a taste of this kind of horror)
your daily type-theoretic Lovecraftian horror, as narrated by PMP (something like this but with Coq syntax?)
Our every step unsettled the ancient earth. But we were in a realm of death and madness... In the end, I alone fled laughing and wailing through those blackened arcades of antiquity.
Benchmark does not look that bad.
Some project failures should be corrected with the updated commits.
But I have no idea why coq/coq#1939 is back.
Ah, yes, actually this is probably fine. The important part for performance is that the lemmas that are part of the TC resolution are monomorphic. Just making
flip polymorphic is not enough to make them polymorphic as well, so there is no problem there. It'd be more problematic if we started sharing instances of Proper and the like, but thankfully universe polymorphism is not strong enough to allow Prop instantiations (yet) so we're safe on that side for now.
Last updated: Feb 01 2023 at 13:03 UTC