Stacking cmra combinators can dramatically slow down type-checking/unification
As noticed by !907 (merged), stacking too many (u)cmra combinators can dramatically slow down type-checking/unification.
A somewhat minimal example that shows the problem is the following:
From iris.algebra Require Import agree frac_auth.
From iris.base_logic Require Import own.
Time Lemma stack_frac_auths2 `{!inG Σ (frac_authUR $ frac_authUR $ agreeR $ natO)} γ1 (n : nat) :
own γ1 ((●F (●F (to_agree n)))) ⊢ own γ1 ((●F (●F (to_agree n)))).
Abort.
Time Lemma stack_frac_auths3 `{!inG Σ (frac_authUR $ frac_authUR $ frac_authUR $ agreeR $ natO)} γ1 (n : nat) :
own γ1 (●F (●F (●F (to_agree n)))) ⊢ own γ1 (●F (●F (●F (to_agree n)))).
Abort.
Time Lemma stack_frac_auths4 `{!inG Σ (frac_authUR $ frac_authUR $ frac_authUR $ frac_authUR $ agreeR $ natO)} γ1 (n : nat) :
own γ1 (●F (●F (●F (●F (to_agree n))))) ⊢ own γ1 (●F (●F (●F (●F (to_agree n))))).
Abort.
Time Lemma stack_frac_auths5 `{!inG Σ (frac_authUR $ frac_authUR $ frac_authUR $ frac_authUR $ frac_authUR $ agreeR $ natO)} γ1 (n : nat) :
own γ1 (●F (●F (●F (●F (●F (to_agree n)))))) ⊢ own γ1 (●F (●F (●F (●F (●F (to_agree n)))))).
Abort.
Note that we are not entering any proof mode yet, but type-checking lemma statement stack_frac_auths2
still takes 0.1 seconds on my machine, while I haven't waited long enough for stack_frac_auths3
to terminate.
The problem is caused by writing frac_authUR
while a frac_authR
would suffice. The former returns a ucmra
, but Coq expects a cmra
, and so it inserts the ucmra_cmraR
coercion. So now we have something of type inG Σ (ucmra_cmraR $ frac_authUR _ )
while we need something of type inG Σ (frac_authR _)
(as implicit argument to own
), and the _
may feature the same problem. Coq must check that these types coincide definitionally, and this takes a long time to check.
The band-aid fix from !907 (merged) is to add a Strategy command to speed up this type-checking. By unfolding some of the projections eagerly, the computation finishes faster: stack_frac_auths2
now type-checks nearly instantly.
However, the problem persists: stack_frac_auths3
takes 0.1 seconds, while stack_frac_auths4
takes 4 seconds, and stack_frac_auths5
takes about 140 seconds.
Paraphrasing from !907 (merged):
I suspect just (Strategy
) annotations cannot make this fast. To make this fast, I think we need to have a solution for the following question:
How do we keep type-checking/unification fast for structures (like ofe
, cmra
and ucmra
) that have combinators (like optionUR : cmra → ucmra
) and coercions (like ucmra_cmraR : cmra → ucmra
), especially when stacking alot of these combinators?