typeclass loop in lift_lift and option

Stream: general

[Eric Wieser]

This hits a typeclass search loop:

prelude

import init.coe

set_option trace.class_instances true
set_option class.instance_max_depth 50

/- without this line, we hit a typeclass search loop for
`has_lift_t (list (with_zero (with_zero ... (with_zero ℕ)))) (cycle ℕ)` -/
-- local attribute [-instance] lift_list

example : ℕ := ↑[(1 : ℕ)]

[Eric Wieser]

It ends up looking for a stupid instance like

(list (option (option (option (option (option (option (option (option (option (option (option (option ℕ)))))))))))))
  ℕ :=

where the number of options is bounded only by the max depth

[Eric Wieser]

This only gets worse without the prelude, as widget.html and with_zero also join the game

[Reid Barton]

interestingly
https://github.com/leanprover-community/lean/blob/a0fb1e8c7ac81dfd2e80ad0de08f4e57ee853d82/library/init/coe.lean#L105

[Reid Barton]

Ah this is really about lift_list

[Eric Wieser]

Right, one of docs#lift_list and docs#coe_option is to blame here, unless the transitivity mechanism itself is flawed. I guess that's also quite possible, given Lean4 chose to design it differently.

[Kevin Buzzard]

Just to be clear -- you're not expecting such a coercion to exist right?

[Eric Wieser]

No, I'm not expecting it to exist, that would be nonsense!

[Floris van Doorn]

In docs#lift_list we should probably either

• replace the type-class assumption from [has_lift_t a b] to [has_lift a b]; or
• replace the conclusion from has_lift (list a) (list b) to has_lift_t (list a) (list b)

[Eric Wieser]

Should we have an instance for both cases?

[Floris van Doorn]

That seems unnecessary. I think the instance [has_lift a b] : has_lift (list a) (list b) is fully general, since we can do docs#lift_trans on the list level (e.g. if we have lifts a -> b and b -> c which gives lifts list a -> list b and list b -> list c so we get a has_lift_t (list a) (list c)).

[Floris van Doorn]

lean#626