This commit introduced a bad regression in typing/product.v. In d5ab6f51, that file took <20sec, now it is almost 180sec.

I assume this is caused by updating Iris from b0418bd57b9341dbf5e58669c689201daa561bd7 to b863cfd7640f5dccb14c17e9ffefb475f1b7d0d8. Unfortunately, that diff is very big as it contains removing the prelude...

Cc @jjourdan @robbertkrebbers

Will investigate.

Since LambdaRust commit ce54063e the time of typing/product.v is back < 20 times.

The culprit was Iris commit fd81b328 which made f_equiv more powerful (*). In combination with the equality of LambdaRust types that was not sealed off, this resulted in unification unfolding too much.

(*) It no longer requires the functions on both sides of the relation to be syntactically the same. Before that Iris commit, f_equiv would fail on something like @cons nat x1 y2 ≡ @cons (ofe_car natC) x2 y2.)

Nice :) Thanks!