## Stream: general

### Topic: Problem with type class search

#### Johannes Hölzl (Mar 22 2019 at 10:22):

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 (Mar 22 2019 at 10:23):

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 (Mar 22 2019 at 10:28):

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.

Good to hear!

#### Patrick Massot (Mar 22 2019 at 13:24):

@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 (Mar 23 2019 at 17:22):

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 (Mar 25 2019 at 22:05):

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 (Mar 26 2019 at 07:14):

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 (Mar 26 2019 at 08:23):

Right, it should be the default behaviour.

#### Johannes Hölzl (Mar 26 2019 at 08:23):

Or even not configurable

#### Rob Lewis (Mar 27 2019 at 11:06):

@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 (Mar 27 2019 at 11:47):

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

#### Kevin Buzzard (Mar 27 2019 at 19:56):

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 (Mar 27 2019 at 20:03):

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.

Yes

#### Johan Commelin (Mar 27 2019 at 20:05):

That seems like an easy PR :grinning:

#### Johan Commelin (Mar 27 2019 at 20:05):

Could even do that from the Github editor (-;

#### Johannes Hölzl (Mar 27 2019 at 20:06):

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 (Mar 27 2019 at 20:07):

Who is keeping track of all the benefits of forking?

#### Kevin Buzzard (Mar 27 2019 at 20:07):

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

#### Kevin Buzzard (Mar 27 2019 at 20:08):

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

#### Rob Lewis (Mar 27 2019 at 20:11):

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 (Mar 27 2019 at 20:55):

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 (Mar 27 2019 at 20:59):

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

#### Chris Hughes (Mar 27 2019 at 21:50):

We should make a Lean 4 todo list.

#### Kevin Buzzard (Mar 27 2019 at 22:23):

[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 (Mar 27 2019 at 22:24):

[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 (Mar 27 2019 at 22:25):

with_top very popular I see.

#### Kevin Buzzard (Mar 27 2019 at 22:28):

All from the output of

import data.int.basic

set_option trace.class_instances true

example : has_coe ℤ ℕ := by apply_instance


#### Johannes Hölzl (Mar 27 2019 at 22:28):

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...

Aah I see.

#### Alexander Bentkamp (Mar 28 2019 at 19:46):

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] (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] (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 (Mar 30 2019 at 05:39):

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 (Apr 03 2019 at 00:41):

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?

Last updated: May 10 2021 at 00:31 UTC