stubborn refl

Stream: general

[Eric Wieser]

On this line, I have a goal state that looks like (with pp.implicit true):

R: Type u_1
M: Type u_2
_inst_1: comm_semiring R
_inst_2: add_comm_monoid M
_inst_3: @module R M (@comm_semiring.to_semiring R _inst_1) _inst_2
rs: R
⊢ @algebra_map R M _inst_1 _inst_2 _inst_3 = @algebra_map R M _inst_1 _inst_2 _inst_3

Why can't refl close this instantly? It seems to just timeout.

[Anne Baanen]

What happens if you write sorry instead? It might be the timeout is elsewhere.

[Eric Wieser]

sorry is fine

[Eric Wieser]

(by "Seems to timeout", I mean "I don't have the patience to wait")

[Anne Baanen]

Hmm, that's very weird.

[Eric Wieser]

It does eventually give (deterministic) timeout, so at least it doesn't hang forever

[Eric Wieser]

Aha, pp.universes tells me its ⇑algebra_map.{u_1 u_2 u_4} s = ⇑algebra_map.{u_1 u_2 u_5} s

[Eric Wieser]

The culprit is docs#pi_tensor_product.pempty_equiv, which has a free universe variable for the pempty

[Eric Wieser]

Ouch, not even the docs show the universe variable

[Floris van Doorn]

Can you add a comment in the docstring of docs#pi_tensor_product.pempty_equiv warning about the extra universe variable?

[Eric Wieser]

I just replaced pempty with is_empty which eliminates the universe argument, #10274