Zulip Chat Archive

Stream: general

Topic: typeclass inference loop for `has_scalar`

Scott Morrison (Mar 26 2019 at 05:04):

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

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

Scott Morrison (Mar 26 2019 at 05:50):

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

Scott Morrison (Mar 26 2019 at 06:02):

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 (Mar 26 2019 at 06:03):

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 (Mar 26 2019 at 06:03):

Do we have a work-around?

Scott Morrison (Mar 26 2019 at 06:03):

This seems bad. :-(

Mario Carneiro (Mar 26 2019 at 06:48):

wait, so is the search supposed to succeed?

Johannes Hölzl (Mar 26 2019 at 06:50):

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 (Mar 26 2019 at 06:51):

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

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

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

Kevin Buzzard (Mar 26 2019 at 08:33):

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


Johan Commelin (Mar 26 2019 at 08:37):

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

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

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.

Last updated: Aug 03 2023 at 10:10 UTC