typeclass inference loop for `has_scalar`

Stream: general

[Scott Morrison]

I think this MWE exhibits a problem in the design of algebra/module.lean, but I'm not quite sure what's going on yet:

import algebra.module
import data.real.basic

def X : Type := sorry
instance ring_X : ring X := sorry

set_option trace.class_instances true
example : has_scalar ℝ X := infer_instance -- times out

[Scott Morrison]

(oops, initial example over-minimised... fixed now)

[Scott Morrison]

I've been staring at the trace output, but having trouble identifying where the problem could be.

[Scott Morrison]

Oh "dear". This is the same problem @Johannes Hölzl identified at https://github.com/johoelzl/tc-log-parser/blob/master/problem.md

[Scott Morrison]

semimodule.to_has_scalar : Π (α : Type u) (β : Type v) [_inst_1 : semiring α] [_inst_2 : add_comm_monoid β] [c : semimodule α β],
  has_scalar α β

is maybe the problem. semimodule ℝ X is going to fail, but it's going to try solving for it over and over again with different values of _inst_1 and _inst_2?

[Scott Morrison]

Do we have a work-around?

[Scott Morrison]

This seems bad. :-(

[Mario Carneiro]

wait, so is the search supposed to succeed?

[Johannes Hölzl]

Not this specific setting. But it may happen that in a similar instance search such a problem occurs. Then it doesn't terminate, or takes a long time.

[Johannes Hölzl]

Let's say we want to prove C t s, and one of the instances is I : semiring R x -> ... -> C x y and another one is J : C t x. If the semiring instance is looked up first we fail. If we are lucky then J is tried first.

[Johan Commelin]

I agree that this seems very bad. I think we need a smarter type class search. I agree that it should be deterministic. But it should be possible to still have something "smart" and also faster.

[Johan Commelin]

We will only become more dependent on type class search the deeper down we get in higher maths

[Kevin Buzzard]

Is this a current workaround: in complicated situations, the user can just supply the instances they want lean to find in some cases? This is what I have been doing to avoid having to change the default instance depth search. I know that the Lean 3 instance search needs some guidance sometimes, but because in practice I know what the answer is, it's not hard to guide Lean the right direction.

Or is there a fundamental problem which this approach will not deal with?

In my experience, timeouts are almost always because of "user error" in the sense that I ask Lean to fill in an instance which it cannot be reasonably expected to do (eg because it's not there)

[Johan Commelin]

https://github.com/leanprover-community/lean-perfectoid-spaces/blob/71b680fec8dfd4a47e06b7b686e9c3839b4937f9/src/Huber_ring/localization.lean#L328

[Johan Commelin]

That bound isn't tight, but I think 120 is an under bound.

[Johannes Hölzl]

the search depth is a very limited parameter. If you have something like module A i1 i2 _, now the instance search already found i1 and i2, and is now looking at the _. Let's assume the i1 and i2 are already large terms. Now we have a lot of choice points in i1 and i2. Remember that choice points are possible further choice, even if there is no further successful choice. With this the "instance depth search" (which is not about term depth, but backtracking depth) needs to be already quiet high, even if we didn't start the search for _ yet.