Problem with the instance checker

Stream: lean4

[Tage Johansson]

I have a growing project with a few files that defines a few classes and instances. Now I'm starting to get "failed to synthesize" errors for obvious instances. For example:

failed to synthesize
Pure (EStateM IO.Error IO.RealWorld)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

That is, Lean cannot find an instance of Pure for IO which obviously does exist.

Do you have any advise of how to solve this, apart from increasing the number of heartbeats. Are there any kind of instances that slows down the instance checker alot? Should I try to make as few instances as possible to not overload the instance checker? Or is there anything else I can do?

Thanks,
Tage

[Alex J. Best]

What is the output with set_option trace.Meta.synthInstance true set? Or a MWE?

[Tage Johansson]

For the code:

set_option trace.Meta.synthInstance true
example : Pure IO := inferInstance

I get the output:

:play: 5:22-5:35: error:
failed to synthesize
Pure IO
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

:play: 5:22-5:35: information:
[Meta.synthInstance] :boom: Pure IO :play:

[Alex J. Best]

It works fine in the web editor:
https://lean.math.hhu.de/#code=set_option%20trace.Meta.synthInstance%20true%0Aexample%20%3A%20Pure%20IO%20%3A%3D%20inferInstance%0A
Do you have some things imported?

[Alex J. Best]

And which nightly are you using?

[Tage Johansson]

Yes, I have things imported. And it works in a plain file for me as well. The problem (I think) is that I am working in a larger project and that other instances are considered first so the instance zynthesizer doesn't find the right instance in time. I will try to make a MWE (strip as many files as possible for the error to still exist and then make a link to the repo).

[Alex J. Best]

You can expand the traces a bit too to drill down into what the synthesiser is doing

[Tage Johansson]

Thanks, that was helpful! I think I see now what instance is causing the problem. Seems as the instance checker is trying to apply the same instance over and over again:

:play: 4:22-4:35: information:
[Meta.synthInstance] :boom: Pure IO ▼
[] new goal Pure IO ▶
[] ✅ apply @Applicative.toPure to Pure IO ▶
[] ✅ apply @Alternative.toApplicative to Applicative IO ▶
[] ✅ apply @RunnerExt.instMClass to Alternative IO ▶
[] ✅ apply @RunnerExt.lift to RunnerExt Alternative IO ?m.63 ▶
[] ✅ apply @RunnerExt.instMClass to RunnerExt Alternative IO ?m.44 ▶
[] ✅ apply @RunnerExt.lift to RunnerExt (RunnerExt Alternative IO) ?m.108 ?m.110 ▶
[] ✅ apply @RunnerExt.instMClass to RunnerExt (RunnerExt Alternative IO) ?m.44 ?m.86 ▶
[] ✅ apply @RunnerExt.lift to RunnerExt (RunnerExt (RunnerExt Alternative IO) ?m.44) ?m.155 ?m.157 ▶
[] ✅ apply @RunnerExt.instMClass to RunnerExt (RunnerExt (RunnerExt Alternative IO) ?m.44) ?m.86 ?m.133 ▶
[] ✅ apply @RunnerExt.lift to RunnerExt (RunnerExt (RunnerExt (RunnerExt Alternative IO) ?m.44) ?m.86) ?m.202 ?m.204 ▶
[] ✅ apply @RunnerExt.instMClass to RunnerExt (RunnerExt (RunnerExt (RunnerExt Alternative IO) ?m.44) ?m.86) ?m.133 ?m.180 ▶
[] ✅ apply @RunnerExt.lift to RunnerExt (RunnerExt (RunnerExt (RunnerExt (RunnerExt Alternative IO) ?m.44) ?m.86) ?m.133)
?m.249 ?m.251 ▶

And it continues like that in around 14k lines.

[Tomas Skrivan]

There is an art to writing type class instances and you learn it by writing bad instances :)

You can see that the TC synthesis gets stuck in a loop of applying RunnerExt.instMClass and RunnerExt lift. Can you show us those instances?

Also do you have relatively new version of lean? There has been a recent change that fixed a common problem that had similar behaviour.

[Tage Johansson]

Here's my MWE:

class RunnerExt (mClass : (Type → Type) → Type 1)
                (m : Type → Type)
                where
  instMClass : mClass m

attribute [instance] RunnerExt.instMClass

example : Pure IO := inferInstance

Without the attribute [instance] line, it works, so I guess I will need to remove that.

[Tomas Skrivan]

I'm surprised that it allows you to even mark it as an instance as mClass is not guaranteed to be a class

[Tage Johansson]

I had nightly 2023-04-07. After updating to 2023-04-20 I am not allowed to mark it as an instance as you said.

[Tage Johansson]

I am not really sure I need it, but is there any way to mark mClass to be a class? That is, I want mClass to be a class of monads.
What is special about classes as aposed to normal structures?

[Tomas Skrivan]

It is not about class vs structure. You can't even mark a function argument to be a structure. I can pass arbitrary lambda function as mClass

[Tomas Skrivan]

Couple of time I wanted to write a similar code, I always ended up redesigning it. Maybe class RunnerExt (m : Type -> Type) [mClass m] where ... ? But yeah this is not polymorphic over mClass but mClass has to be a concrete class.

[Tage Johansson]

Thanks!
An interesting thing when upgrading Lean was that some other instances I've made doesn't work anymore. This is not the first time I have such instance problems, and perhaps those problems will go away when I've fixed these eronious instances!

[Kevin Buzzard]

Try linting your code -- we have linters which try and prevent the user from creating "bad" instances. If you do something like import Mathlib.Tactic then #lint at the end of a file will work (maybe the linters are in Std, I don't know exactly where they are)

[Tage Johansson]

This code works though, but it seems to me that mClass doesn't have to be a class/structure in this case either:

class RunnerExt (m : Type → Type) where
  mClass : (Type → Type) → Type 1
  instMClass : mClass m

attribute [instance] RunnerExt.instMClass

Is this a bug?

[Eric Wieser]

This all looks like an #xy problem to me, likely related to a previous thread of yours

[Kyle Miller]

Tage Johansson said:

What is special about classes as aposed to normal structures?

One place classes are special is that every argument whose type is a class gets added to the local instance cache. Otherwise such arguments won't be picked up when doing typeclass inference. (The algorithm is basically: look at the argument's type, if it's a pi type peel off all arguments, then see if it's of the form C x y z ..., and then look up to see if the constant C is marked as being a class.)