# Zulip Chat Archive

## Stream: general

### Topic: trolled by undergrad

#### Kevin Buzzard (Jul 20 2018 at 18:34):

It took me 20 minutes to diagnose this deterministic time-out:

import analysis.real theorem infinite_cover {a b : ℝ} {c : set (set ℝ)} (n : ℕ) : ∃ k : ℕ, 1 ≤ k ≤ n ∧ ∀ c' ⊆ c, {r : ℝ | a+(k-1)*(a+b)/n ≤ r ∧ r ≤ a+k*(a+b)/n} ⊆ ⋃₀ c' → ¬ set.finite c' := sorry

In my defence, the code was far longer to begin with, and probably about 15 were spent reducing it to this.

#### Kevin Buzzard (Jul 20 2018 at 18:48):

I'm about to set off for home and I'll spill the beans if nobody has spotted it by the time I get in

#### Patrick Massot (Jul 20 2018 at 18:49):

I don't understand what you are asking for

#### Kevin Buzzard (Jul 20 2018 at 18:50):

Cut and paste that code -- it times out

#### Kevin Buzzard (Jul 20 2018 at 18:50):

deterministic time-out

#### Chris Hughes (Jul 20 2018 at 18:50):

`1 ≤ k ≤ n`

#### Kevin Buzzard (Jul 20 2018 at 18:50):

:-)

#### Kevin Buzzard (Jul 20 2018 at 18:50):

I spotted it when I changed `n`

to `1`

#### Kevin Buzzard (Jul 20 2018 at 18:51):

I was quite surprised that the statement managed to parse

#### Kevin Buzzard (Jul 20 2018 at 18:51):

in retrospect

#### Mario Carneiro (Jul 20 2018 at 18:52):

because obviously `k ≤ n`

is also a nat

#### Mario Carneiro (Jul 20 2018 at 18:52):

bigger than one no less

#### Chris Hughes (Jul 20 2018 at 18:52):

is `≤`

left or right associative?

#### Mario Carneiro (Jul 20 2018 at 19:01):

left assoc, my bad

#### Mario Carneiro (Jul 20 2018 at 19:02):

infix ≤ := has_le.le

`infix`

means `infixl`

#### Mario Carneiro (Jul 20 2018 at 19:02):

oh I see so it tried to find a Prop coercion for `n`

#### Mario Carneiro (Jul 20 2018 at 19:03):

and then it means "if `1 <= k`

then `n`

"

#### Mario Carneiro (Jul 20 2018 at 19:04):

`1 ≤ k ≤ (n ≤ 1)`

parses just fine

#### Chris Hughes (Jul 20 2018 at 19:04):

Because Prop has an order structure for some reason.

#### Mario Carneiro (Jul 20 2018 at 19:04):

because Prop has a natural order structure...

#### Mario Carneiro (Jul 20 2018 at 19:05):

which we use funky notation for

#### Mario Carneiro (Jul 20 2018 at 19:06):

In fact I'm pretty sure boolean algebras are basically generalized Prop

#### Mario Carneiro (Jul 21 2018 at 02:17):

@Sebastian Ullrich I just noticed that this error is a bit subtler than expected. It doesn't give a instance overflow error, it times out and produces no output in the trace. Do you know how the typeclass instance mechanism could run out of time without overflowing?

#### Mario Carneiro (Jul 21 2018 at 02:19):

example without trolling:

import analysis.real example (n : ℕ) : Prop := n

#### Mario Carneiro (Jul 21 2018 at 02:45):

Ah, I finally got an instance trace, and it does something I didn't think the typeclass inference engine does: it repeatedly does the same search, at the same depth level, which is why it timeouts from iteration rather than recursion. Here's the beginning, with the depth shown using indentation:

(0) ?x_3 : has_coe_to_sort ℕ := @coe_sort_trans ?x_5 ?x_6 ?x_7 ?x_8 (1) ?x_7 : has_coe_t_aux ℕ ?x_6 := @coe_base_aux ?x_9 ?x_10 ?x_11 (2) ?x_11 : has_coe ℕ ?x_10 := int.has_coe (1) ?x_8 : has_coe_to_sort ℤ := @coe_sort_trans ?x_22 ?x_23 ?x_24 ?x_25 (2) ?x_24 : has_coe_t_aux ℤ ?x_23 := @coe_base_aux ?x_26 ?x_27 ?x_28 (3) ?x_28 : has_coe ℤ ?x_27 := @int.cast_coe ?x_49 ?x_50 ?x_51 ?x_52 ?x_53 (4) ?x_50 : has_zero ?x_49 := real.has_zero (4) ?x_51 : has_one ℝ := real.has_one (4) ?x_52 : has_add ℝ := real.has_add (4) ?x_53 : has_neg ℝ := real.has_neg (2) ?x_25 : has_coe_to_sort ℝ := @coe_sort_trans ?x_55 ?x_56 ?x_57 ?x_58 (3) ?x_57 : has_coe_t_aux ℝ ?x_56 := @coe_base_aux ?x_59 ?x_60 ?x_61 (3) ?x_57 : has_coe_t_aux ℝ ?x_56 := @coe_trans_aux ?x_59 ?x_60 ?x_61 ?x_62 ?x_63 (4) ?x_53 : has_neg ℝ := @lattice.boolean_algebra.to_has_neg ?x_60 ?x_61 (5) ?x_61 : lattice.boolean_algebra ℝ := @lattice.complete_boolean_algebra.to_boolean_algebra ?x_62 ?x_63 (4) ?x_53 : has_neg ℝ := @add_group.to_has_neg ?x_55 ?x_56 (5) ?x_56 : add_group ℝ := real.add_group (2) ?x_25 : has_coe_to_sort ℝ := @coe_sort_trans ?x_58 ?x_59 ?x_60 ?x_61 (3) ?x_60 : has_coe_t_aux ℝ ?x_59 := @coe_base_aux ?x_62 ?x_63 ?x_64 (3) ?x_60 : has_coe_t_aux ℝ ?x_59 := @coe_trans_aux ?x_62 ?x_63 ?x_64 ?x_65 ?x_66 (5) ?x_56 : add_group ℝ := @add_comm_group.to_add_group ?x_59 ?x_60 (6) ?x_60 : add_comm_group ℝ := real.add_comm_group (2) ?x_25 : has_coe_to_sort ℝ := @coe_sort_trans ?x_62 ?x_63 ?x_64 ?x_65 (3) ?x_64 : has_coe_t_aux ℝ ?x_63 := @coe_base_aux ?x_66 ?x_67 ?x_68 (3) ?x_64 : has_coe_t_aux ℝ ?x_63 := @coe_trans_aux ?x_66 ?x_67 ?x_68 ?x_69 ?x_70 (6) ?x_60 : add_comm_group ℝ := @nonneg_comm_group.to_add_comm_group ?x_61 ?x_62 (7) ?x_62 : nonneg_comm_group ℝ := @linear_nonneg_ring.to_nonneg_comm_group ?x_63 ?x_64 (7) ?x_62 : nonneg_comm_group ℝ := @nonneg_ring.to_nonneg_comm_group ?x_63 ?x_64 (8) ?x_64 : nonneg_ring ℝ := @linear_nonneg_ring.to_nonneg_ring ?x_65 ?x_66 (6) ?x_60 : add_comm_group ℝ := @ring.to_add_comm_group ?x_63 ?x_64 (7) ?x_64 : ring ℝ := real.ring (2) ?x_25 : has_coe_to_sort ℝ := @coe_sort_trans ?x_66 ?x_67 ?x_68 ?x_69 (3) ?x_68 : has_coe_t_aux ℝ ?x_67 := @coe_base_aux ?x_70 ?x_71 ?x_72 (3) ?x_68 : has_coe_t_aux ℝ ?x_67 := @coe_trans_aux ?x_70 ?x_71 ?x_72 ?x_73 ?x_74 (7) ?x_64 : ring ℝ := @nonneg_ring.to_ring ?x_71 ?x_72 (8) ?x_72 : nonneg_ring ℝ := @linear_nonneg_ring.to_nonneg_ring ?x_73 ?x_74 (7) ?x_64 : ring ℝ := @domain.to_ring ?x_65 ?x_66 (8) ?x_66 : domain ℝ := real.domain

#### Mario Carneiro (Jul 21 2018 at 02:45):

notice that `(2) ?x_25 : has_coe_to_sort ℝ`

keeps coming up; this continues for all 38000 lines of output before it times out

#### Mario Carneiro (Jul 21 2018 at 03:24):

Oh whoa I just figured out why this is happening, and why it's called a "prolog-like search" - nota bene @Kevin Buzzard :)

Whenever it tries something which doesn't work, it reverts all the metavariable assignments up to that point and then tries again. Like here around the newline:

(2) ?x_25 : has_coe_to_sort ℝ := @coe_sort_trans ?x_55 ?x_56 ?x_57 ?x_58 (3) ?x_57 : has_coe_t_aux ℝ ?x_56 := @coe_base_aux ?x_59 ?x_60 ?x_61 (3) ?x_57 : has_coe_t_aux ℝ ?x_56 := @coe_trans_aux ?x_59 ?x_60 ?x_61 ?x_62 ?x_63 (4) ?x_53 : has_neg ℝ := @lattice.boolean_algebra.to_has_neg ?x_60 ?x_61 (5) ?x_61 : lattice.boolean_algebra ℝ := @lattice.complete_boolean_algebra.to_boolean_algebra ?x_62 ?x_63 (4) ?x_53 : has_neg ℝ := @add_group.to_has_neg ?x_55 ?x_56 (5) ?x_56 : add_group ℝ := real.add_group (2) ?x_25 : has_coe_to_sort ℝ := @coe_sort_trans ?x_58 ?x_59 ?x_60 ?x_61 (3) ?x_60 : has_coe_t_aux ℝ ?x_59 := @coe_base_aux ?x_62 ?x_63 ?x_64 (3) ?x_60 : has_coe_t_aux ℝ ?x_59 := @coe_trans_aux ?x_62 ?x_63 ?x_64 ?x_65 ?x_66 (5) ?x_56 : add_group ℝ := @add_comm_group.to_add_group ?x_59 ?x_60 (6) ?x_60 : add_comm_group ℝ := real.add_comm_group

The line `(5) ?x_56 : add_group ℝ := real.add_group`

is a failure, but it assigns a value to `?x_56`

from the (2) line. So it rolls all the way back to the (2) line and replays the same assignments until it gets to the bad choice `real.add_group`

, and tries something different, in this case `@add_comm_group.to_add_group ?x_59 ?x_60`

.

#### Mario Carneiro (Jul 21 2018 at 03:28):

I wonder if typeclass search will change in lean 4. This seems like such a poor strategy I'm surprised it works as well as it does in mathlib. I know Leo thinks many things about lean 3 are fundamentally broken, and I wouldn't be surprised if this was on the list

#### Sebastian Ullrich (Jul 21 2018 at 08:21):

@Mario Carneiro This is not how class inference should work, nor have I seen such a trace before. Class inference uses temporary mvars that can be unassigned individually. https://github.com/leanprover/lean/blob/ceacfa7445953cbc8860ddabc55407430a9ca5c3/src/library/type_context.cpp#L1405

#### Mario Carneiro (Jul 21 2018 at 08:23):

If you like I can make a mathlib-free example

#### Sebastian Ullrich (Jul 21 2018 at 08:26):

That would be great, thanks

#### Mario Carneiro (Jul 21 2018 at 08:39):

I think this should do the trick (WARNING: this brings VSCode to its knees due to quantity of output)

@[priority 0] instance cast_coe {α} [has_zero α] [has_one α] [has_add α] : has_coe ℕ α := ⟨λ _, 0⟩ constant R : Type instance : has_zero R := sorry set_option trace.class_instances true example (n : ℕ) : Prop := n

The `constant R`

is optional but gives the typeclass system something to fixate on rather than whatever random thing it finds first (usually `unsigned`

for me on the init library and `real`

when it is imported)

#### Sebastian Ullrich (Jul 21 2018 at 08:42):

hmm

$ lean +3.4.1 scratch.lean |& wc -l 381659 $ lean +master scratch.lean |& wc -l 3342

I guess Leo fixed it already :D

#### Mario Carneiro (Jul 21 2018 at 08:45):

well... I'm glad it was fixed, although I'm still puzzled over the cause...

#### Mario Carneiro (Jul 21 2018 at 08:59):

Oh, looking at the trace from that version, I noticed that it searches for `(1) ?x_7 : has_coe_to_sort ℤ`

2826 times (with 26000 lines in between, not counting failures) before finally getting to `(1) ?x_7 : has_coe_to_sort ℕ`

, which is the same typeclass search it started with. So I think if I let it run long enough it *would* hit the recursion limit, it would just take an extremely long time to do so.

#### Patrick Massot (Jul 21 2018 at 09:00):

Maybe it would be worth checking that it was not fixed by accident (since another modification could reinstate the bug), or at least add it to the test suite?

#### Patrick Massot (Jul 21 2018 at 09:02):

Do you think the type class search could become more programmable for users? For instance we already saw that it would be nice to be able to tell it: whenever you're looking for `ring ?x_i`

then you should give up on that branch.

#### Mario Carneiro (Jul 21 2018 at 09:02):

I'm not sure how much I should care about this bug, since it has to do with lean performance on an unsuccessful typeclass search anyway

#### Mario Carneiro (Jul 21 2018 at 09:03):

I think "negative instances" would be great, they could probably speed up the search a lot. I.e. `unsigned`

is not a field, stop looking there

#### Patrick Massot (Jul 21 2018 at 09:03):

Obviously I don't know either, this is far above my competences. My reaction is only triggered by Sebastian not knowing something has been fixed

#### Mario Carneiro (Jul 21 2018 at 09:04):

but there is a lot of planning necessary to get a feature like that right

#### Mario Carneiro (Jul 21 2018 at 09:04):

and obviously it's up to Sebastian and Leo to make that happen

#### Mario Carneiro (Jul 21 2018 at 09:05):

so I will just let them ponder and figure out whatever works

#### Patrick Massot (Jul 21 2018 at 09:05):

and soon Gabriel, according to Leo's talk

#### Sebastian Ullrich (Jul 21 2018 at 09:05):

The type context will remain in C++, so it will not be arbitrarily configurable like other parts (hopefully will)

#### Mario Carneiro (Jul 21 2018 at 09:06):

is typeclass search done in the type context?

#### Patrick Massot (Jul 21 2018 at 09:06):

You could still let users pass options to the C++ code, couldn't you?

#### Sebastian Ullrich (Jul 22 2018 at 15:30):

@Mario Carneiro Yes, it uses many type context internals. Still, reimplementing it on top of the new type context monad may be an interesting idea, now that I think about it.

#### Sebastian Ullrich (Jul 22 2018 at 15:31):

@Patrick Massot Sure, that's what I meant by "not arbitrarily". For the parts reimplemented in Lean, I'd like users to be able to completely replace the default implementations if they want to.

#### Mario Carneiro (Jul 22 2018 at 15:32):

it would certainly be good if at least potential writing of the typeclass search could guide what of the type context gets exposed to lean

#### Sebastian Ullrich (Jul 22 2018 at 15:32):

Yes, exactly

Last updated: May 18 2021 at 17:44 UTC