trolled by undergrad

Stream: general

[Kevin Buzzard]

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]

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]

I don't understand what you are asking for

[Kevin Buzzard]

Cut and paste that code -- it times out

[Kevin Buzzard]

deterministic time-out

[Chris Hughes]

1 ≤ k ≤ n

[Kevin Buzzard]

:-)

[Kevin Buzzard]

I spotted it when I changed n to 1

[Kevin Buzzard]

I was quite surprised that the statement managed to parse

[Kevin Buzzard]

in retrospect

[Mario Carneiro]

because obviously k ≤ n is also a nat

[Mario Carneiro]

bigger than one no less

[Chris Hughes]

is ≤ left or right associative?

[Mario Carneiro]

left assoc, my bad

[Mario Carneiro]

infix ≤        := has_le.le

infix means infixl

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

1 ≤ k ≤ (n ≤ 1) parses just fine

[Chris Hughes]

Because Prop has an order structure for some reason.

[Mario Carneiro]

because Prop has a natural order structure...

[Mario Carneiro]

which we use funky notation for

[Mario Carneiro]

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

[Mario Carneiro]

@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]

example without trolling:

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

[Mario Carneiro]

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]

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]

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]

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]

@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]

If you like I can make a mathlib-free example

[Sebastian Ullrich]

That would be great, thanks

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

and soon Gabriel, according to Leo's talk

[Sebastian Ullrich]

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

[Mario Carneiro]

is typeclass search done in the type context?

[Patrick Massot]

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

[Sebastian Ullrich]

@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]

@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]

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]

Yes, exactly