Problem with type class search

Stream: general

[Johannes Hölzl]

Question: how much instances of decidable (fin n) are found by Lean? And why does it matter? Answer: https://github.com/johoelzl/tc-log-parser/blob/master/problem.md#answer

fin n is just an example, even decidable is not the problem in itself. The problem will happen with each diamond where we have two ways to construct the same instance.

[Johannes Hölzl]

It looks like this is something we cannot solve in mathlib, but requires changes in Lean. @Sebastian Ullrich: the type class search in Lean 4 will be the same as in Lean 3? So it would make sense to improve it in Lean 3 and then port it to Lean 4?

[Sebastian Ullrich]

Semantically it will probably stay the same, but Leo wants to look into possible optimizations. I will note this as one potential optimization opportunity, thanks for the write-up. No promises though.

[Johannes Hölzl]

Good to hear!

[Patrick Massot]

@Johannes Hölzl Could you tell us more about this repository?

[Patrick Massot]

@Sebastian Ullrich I think you should ask @Cyril Cohen about ideas to improve the type class search semantic. In Amsterdam he told several things that got added to Coq recently and seemed like they could be very useful for large scale type class search

[Johannes Hölzl]

The idea is to have a parser for the log produced by Lean when searching for type class instances. All it currently does is to outpute the computed instances until a mark ff instance is looked up. This was the essential information I needed.

But I'm sure it can be used to analyse other problems too

[Johannes Hölzl]

Hm, this problem seams to be even worse: is_add_monoid_hom (coe : ℤ → ℤ) does not terminate. Now is_ring_hom (coe : ℤ → ℤ) doesn't work due to some unification problems. But is_ring_hom.is_semiring_hom is_semiring_hom.is_add_monoid_hom is looking for a ring instance and then for the is_ring_hom instance. The is_ring_hom instance is not found, hence it starts to enumerate all the ways to construct ring for int.

Maybe a solution would be to annotate class constants with a attribute, saying that there should be no backtracking, i.e. there should be only one canonical instance.

[Johan Commelin]

Maybe a solution would be to annotate class constants with a attribute, saying that there should be no backtracking, i.e. there should be only one canonical instance.

Isn't this how type class search is supposed to work anyway. So we can just bake that assumption in. If you found an instance, and it didn't work, just stop. No need to look for another instance.

[Johannes Hölzl]

Right, it should be the default behaviour.

[Johannes Hölzl]

Or even not configurable

[Rob Lewis]

@Paul-Nicolas Madelaine and I came across a problem that I've seen before. Because of left-to-right elaboration, Lean won't coerce n to ℤ here:

import data.int.basic
example (n : ℕ) (z : ℤ) : n < z :=
sorry

Instead, it decides that < is over ℕ and tries to coerce z. This should fail, but in practice it times out. I've noticed this many times but never had a chance to investigate. Turns out this is is another instance of the same type class issue Johannes reports. int.cast_coe looks, in order, for has_zero ℕ, has_one ℕ, has_add ℕ, and has_neg ℕ. There are tons of paths to the first three. (Presumably. I didn't count.) The last one fails. So the search goes effectively forever.

There's an easy solution for this particular case, though: change int.cast_coe to look for has_neg first. Then it fails fast. Nothing in mathlib breaks with this change. (I didn't compare compilation times.) This points to a general design strategy, as long as type class inference has this behavior: put the hardest (rarest, least likely) classes as early as possible.

[Johan Commelin]

Good idea. I'll try to keep it in mind while writing code.

[Kevin Buzzard]

So today will be remembered as the day that the age old question of why Lean times out when failing to coerce from int to nat is solved! @Johannes Hölzl @Sebastian Ullrich this trips up beginner mathematicians and is hard for them to debug. I think Johannes has found a fundamental issue which needs some serious thought.

[Kevin Buzzard]

So what Rob is saying, I think, is that in data.int.basic in mathlib, one of the lines here

section cast
variables {α : Type*}

section
variables [has_zero α] [has_one α] [has_add α] [has_neg α]

/-- Canonical homomorphism from the integers to any ring(-like) structure `α` -/
protected def cast : ℤ → α
| (n : ℕ) := n
| -[1+ n] := -(n+1)

@[priority 0] instance cast_coe : has_coe ℤ α := ⟨int.cast⟩

should be changed: the order of the variables should be changed.

[Johannes Hölzl]

Yes

[Johan Commelin]

That seems like an easy PR :grinning:

[Johan Commelin]

Could even do that from the Github editor (-;

[Johannes Hölzl]

Another thing we need to change is actually Lean 3. We could fork Lean 3 and remove the ability to backtrack in Lean 3 and see what breaks in mathlib. This would make the type class search much easier.

[Johan Commelin]

Who is keeping track of all the benefits of forking?

[Johan Commelin]

There was a thread about this somewhere, right?

[Kevin Buzzard]

This is an edit to mathlib we're talking about here

[Kevin Buzzard]

Oh I see, Johannes is suggesting changing the C++ code?

[Rob Lewis]

The edit to mathlib should happen. And it seems worthwhile to experiment with a different type class search in a forked Lean. I would not want to port mathlib to this forked Lean 3, at least not without more knowledge of the Lean 4 type class mechanism.

[Kevin Buzzard]

Results of a completely unscientific test; on this desktop, it took just under 15 minutes to compile mathlib HEAD, and then with the variable line in data/int/basic.lean changed to

variables [has_neg α] [has_add α] [has_one α] [has_zero α]

(100% reversal) it took just under 14 minutes.

[Kevin Buzzard]

and example : has_coe ℤ ℕ := by apply_instance now fails instantly! I have never seen that before!

[Chris Hughes]

We should make a Lean 4 todo list.

[Kevin Buzzard]

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_one ℕ := @with_top.has_one ?x_1 ?x_2 ?x_3
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := @with_bot.has_one ?x_4 ?x_5
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := @with_zero.has_one ?x_6 ?x_7
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := @with_one.has_one ?x_8
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := @units.has_one ?x_9 ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := unsigned.has_one
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := @fin.has_one ?x_11
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := int.has_one
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := nat.has_one

Which one should Lean have tried first, to find a one for nat? with_zero.has_one or nat.has_one?

[Kevin Buzzard]

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_to_format tactic_state := int.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := @with_top.has_to_format ?x_1 ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := @with_bot.has_to_format ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := tactic.rcases_patt.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := tactic.rcases_patt_inverted.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := @array.has_to_format ?x_5 ?x_6 ?x_7
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := subsingleton_info.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := fun_info.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := param_info.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := occurrences.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := tactic_state.has_to_format

rofl

[Kevin Buzzard]

with_top very popular I see.

[Kevin Buzzard]

All from the output of

import data.int.basic

set_option trace.class_instances true

example : has_coe ℤ ℕ := by apply_instance

[Johannes Hölzl]

The instances added last get checked first. But this is usually not a problem, unification fails fast in these cases. The problem is if they match and the instance search runs in the wrong direction...

[Kevin Buzzard]

Aah I see.

[Alexander Bentkamp]

I had the same issue here:

import algebra.module analysis.normed_space.basic data.real.basic

class real_inner_product_space (V : Type*) [add_comm_group V] extends vector_space ℝ V :=
(inner : V → V → ℝ)
(inner_axioms : false /- (axioms omitted here) -/)

instance is_normed_space (V : Type*) [add_comm_group V] [real_inner_product_space V] :
  normed_space ℝ V := sorry

set_option trace.class_instances true
noncomputable example : add_comm_group ℝ := by apply_instance
/- This easy instance cannot be found any more (infinte loop):
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : add_comm_group ℝ := @normed_group.to_add_comm_group ?x_1 ?x_2
[class_instances] (1) ?x_2 : normed_group ℝ := @normed_space.to_normed_group ?x_3 ?x_4 ?x_5 ?x_6
[class_instances] (2) ?x_6 : @normed_space ?x_3 ℝ ?x_5 := @is_normed_space ?x_7 ?x_8 ?x_9
[class_instances] (3) ?x_8 : add_comm_group ℝ := @normed_group.to_add_comm_group ?x_10 ?x_11
[class_instances] (4) ?x_11 : normed_group ℝ := @normed_space.to_normed_group ?x_12 ?x_13 ?x_14 ?x_15
...
 -/

My current workaround is to put add_comm_group V after extends in real_inner_product_space, i.e.

class real_inner_product_space (V : Type*) extends add_comm_group V, vector_space ℝ V :=

But of course this could lead to a messy hierarchy if I wanted to extend real_inner_product_space further.

[Reid Barton]

Another thing we need to change is actually Lean 3. We could fork Lean 3 and remove the ability to backtrack in Lean 3 and see what breaks in mathlib. This would make the type class search much easier.

For what it's worth, GHC has no backtracking in instance search (even with GHC extensions) and it seems to work pretty well for Haskell. Hard to say if it would also work well for a project like mathlib of course.

[Johan Commelin]

Results of a completely unscientific test; on this desktop, it took just under 15 minutes to compile mathlib HEAD, and then with the variable line in data/int/basic.lean changed to

variables [has_neg α] [has_add α] [has_one α] [has_zero α]

(100% reversal) it took just under 14 minutes.

Anyone who wants to merge #877?