Zulip Chat Archive

Stream: mathlib4

Topic: CoeFun instance not found?

Eric Rodriguez (Mar 24 2023 at 12:13):

Consider this mwe:

import Mathlib

set_option synthInstance.etaExperiment true --neither setting works
set_option autoImplicit false

example {K} [Field K] (f : Unit → K) (p : MvPolynomial Unit K) : MvPolynomial.eval f p = 0 :=
by induction n

This fails with "failed to synthesize CoeFun (MvPolynomial Unit K →+* K) ?m.178, maximum number of heartbeats (20000) has been reached".

Eric Rodriguez (Mar 24 2023 at 12:13):

How can this be? I'm super confused

Adam Topaz (Mar 24 2023 at 12:16):

this also fails

import Mathlib

set_option synthInstance.etaExperiment true --neither setting works
set_option autoImplicit false


example (A B) [Field A] [Field B] (f : A →+* B) (a : A) : B := f a

Adam Topaz (Mar 24 2023 at 12:18):

yeah I think there might be an issue with the path RingHom -> RingHomClass -> CoeFun

Adam Topaz (Mar 24 2023 at 12:19):

IIRC the solution from the linear algebra library where a similar thing came up was to add a CoeFunFunLike instance manually.

Adam Topaz (Mar 24 2023 at 12:19):

Let me try to dig up that old thread.

Eric Rodriguez (Mar 24 2023 at 12:21):

image.png it seems that even if you say exactly what FunLike instance you want, it still searches for some generic weird one

Matthew Ballard (Mar 24 2023 at 12:21):

How high do you have to bump the heart beats for it to succeed?

Eric Rodriguez (Mar 24 2023 at 12:25):

2000000000 doesn't seem to be enough

Matthew Ballard (Mar 24 2023 at 12:25):

How about 0?

Eric Rodriguez (Mar 24 2023 at 12:27):

the error switches to timeouts at whnf and isDefEq

Matthew Ballard (Mar 24 2023 at 12:28):

Similar but not as egregious behavior in !4#2364.

Eric Rodriguez (Mar 24 2023 at 12:28):

and those seem to be looping as it doesn't resolve after ~1m, with etaExperiment on or off.

Matthew Ballard (Mar 24 2023 at 12:29):

Does the synth trace show where it gets stuck?

Adam Topaz (Mar 24 2023 at 12:29):

well, here's a bit more info:

instance (A B α) [Semiring A] [Semiring B] [RingHomClass α A B] :
  FunLike α A (fun _ => B) := sorry -- inferInsance fails

example (A B) [Semiring A] [Semiring B] (f : A →+* B) (a : A) : B := f a -- works

Matthew Ballard (Mar 24 2023 at 12:31):

The first one succeeds as an example right?

Adam Topaz (Mar 24 2023 at 12:31):

Is it trying to dig through something like RingHomClass -> MulHomClass -> ... -> FunLike?

Adam Topaz (Mar 24 2023 at 12:31):

well yes, but not without the sorry

Adam Topaz (Mar 24 2023 at 12:31):

i.e. tc search doesn't find the instance

Matthew Ballard (Mar 24 2023 at 12:32):

Right. Just wondering if the supplied instance confused it

Adam Topaz (Mar 24 2023 at 12:32):

what path is is supposed to find for the first instance? I

Eric Rodriguez (Mar 24 2023 at 12:33):

image.png there seems to be some weird loop in some of the trace

Matthew Ballard (Mar 24 2023 at 12:33):

Oh right. Misreading

Matthew Ballard (Mar 24 2023 at 12:33):

It’s really trying hard

Eric Rodriguez (Mar 24 2023 at 12:36):

image.png Yeah there's some weird looping going on

Eric Rodriguez (Mar 24 2023 at 12:36):

I tried removing Ordinal files to see what happens and it starts going on some other horrific loop

Adam Topaz (Mar 24 2023 at 12:37):

StoneCech!?

Eric Rodriguez (Mar 24 2023 at 12:37):

I have a feeling that maybe what's going on in that linear algebra file is similar, there's finally enough imports for issues like this to show up

Matthew Ballard (Mar 24 2023 at 12:37):

As I said it is trying hard

Adam Topaz (Mar 24 2023 at 12:37):

Does anyone actually understand FunLike instances in lean4?

Reid Barton (Mar 24 2023 at 12:40):

Lean is just trying to compute a projective resolution of your space

Matthew Ballard (Mar 24 2023 at 12:42):

In !4#2364, it started by complaining about FunLike or CoeFun but behind that was a long attempt to chain together CoeT, CoeOTC, CoeHCTC, and friends

Matthew Ballard (Mar 24 2023 at 12:44):

So this might be different. Sounds closer to lean4#2055 in success mode Wrong!

Matthew Ballard (Mar 24 2023 at 12:46):

But there must be loop in TC graph right?

Anne Baanen (Mar 24 2023 at 12:58):

Looks like the issue is more of an instance search starting on some type with metavariables: this ?m.1426 should not appear when searching for TopologicalSpace.

Anne Baanen (Mar 24 2023 at 13:08):

Specifically, what's going on is when searching for FunLike α A B in the example above, A and B are outParam so they are replaced with new metavariables _tc.0 and _tc.1, then Lean tries a few classes before hitting ContinuousMapClass. Then it decides α might be a HomotopyLike so it needs to unify _tc.0 with unitInterval x ?m.484 and this ?m.484 is what needs the TopologicalSpace instance that sends Lean into a loop.

Adam Topaz (Mar 24 2023 at 13:11):

Isn't this always going to be an issue with the FooLike classes?

Anne Baanen (Mar 24 2023 at 13:12):

Yes, as long as Lean 4 is happy to try and solve TopologicalSpace ?m.484 instances, the whole FunLike design will easily lead to loops.

Anne Baanen (Mar 24 2023 at 13:13):

In general I've had quite a few issues in Lean 4 with instance parameters depending on out parameters (such as TopologicalSpace in this case). The solution is either to improve the synthesis algorithm, or to unbundle RingHomClass from FunLike: class RingHomClass [FunLike F A B] := ... instead of class RingHomClass extends FunLike F A B.

Anne Baanen (Mar 24 2023 at 13:13):

In the unbundled case, the FunLike parameter will supply values to the outParam before searching for the dependent instances.

Eric Rodriguez (Mar 24 2023 at 13:15):

Anne Baanen said:

Specifically, what's going on is when searching for FunLike α A B in the example above, A and B are outParam so they are replaced with new metavariables _tc.0 and _tc.1, then Lean tries a few classes before hitting ContinuousMapClass. Then it decides α might be a HomotopyLike so it needs to unify _tc.0 with unitInterval x ?m.484 and this ?m.484 is what needs the TopologicalSpace instance that sends Lean into a loop.

why does it metavar them? if A/B are already there from unification, I really don't see why it then decides that it has to forget them

Matthew Ballard (Mar 24 2023 at 13:17):

I think this is by design in TC synthesis. This was discussed somewhere unless I am confused.
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/What.20is.20an.20outParam.3F/near/323532517

Adam Topaz (Mar 24 2023 at 13:18):

Yeah a priori there could be some way to via the unit interval as the type of ring Homs between some rings?

Eric Rodriguez (Mar 24 2023 at 13:27):

make elaboration less dependent on the exact elaboration ordering

what does this mean?

Anne Baanen (Mar 24 2023 at 13:30):

I think the following reply explains the philosophy best:
Sebastian Ullrich said:

The most important property for elaboration robustness is what I and maybe no-one else is calling monotonicity: assigning a metavariable should not change the output of a subsequent elaboration step other than to change it from failure to success. But if we allowed mixed in/out TC parameters, [OrderHomClass F ?α ?β] and OrderHomClass F α ?β] could certainly both succeed with different answers.

Eric Rodriguez (Mar 24 2023 at 13:36):

but that's only if you break the OutParam philosophy, right?

Eric Rodriguez (Mar 24 2023 at 13:36):

like that should _only_ break if you break the promise you made when you set a, b to be outparams

Anne Baanen (Mar 24 2023 at 13:38):

I totally agree with you, overlapping instances should be a (linting?) error, not a feature of the inference algorithm.

Matthew Ballard (Mar 24 2023 at 15:37):

What fraction of whnf and elaboratortimeouts we are seeing in algebra are from this issue?

Matthew Ballard (Mar 24 2023 at 15:41):

I've seen similar very wide-ranging searches there. Bumping the heartbeat limit gets you through. Importing the world there would probably bust that though.

Gabriel Ebner (Mar 24 2023 at 17:31):

Anne Baanen said:

Looks like the issue is more of an instance search starting on some type with metavariables: this ?m.1426 should not appear when searching for TopologicalSpace.

Anne is completely correct here. Usually the dangerousInstances linter should prevent this. Does the file pass linting?

Eric Rodriguez (Mar 24 2023 at 23:36):

What's the solution then, Gabriel?

Gabriel Ebner (Mar 24 2023 at 23:53):

The plot thickens:

-- `f₀` and `f₁` are `outParam` so this is not dangerous
attribute [nolint dangerousInstance] HomotopyLike.toContinuousMapClass

Adam Topaz (Mar 25 2023 at 00:02):

Why do we need all these FooBarLike classes in the first place!?!? I know they’re useful for the algebra hierarchy, but is this homotopy thing really useful?

Gabriel Ebner (Mar 25 2023 at 00:08):

!4#3089

Matthew Ballard (Mar 25 2023 at 00:12):

There appeared to be something in OrderedRing also right?

Gabriel Ebner (Mar 25 2023 at 00:17):

I'm waiting until CI has built the caches before debugging again.

Adam Topaz (Mar 25 2023 at 00:20):

Are there any other nolint dangerousInstances in mathlib4?

Adam Topaz (Mar 25 2023 at 00:20):

This thread is makes me think that we shouldn’t even be able to turn off this linter

Matthew Ballard (Mar 25 2023 at 00:23):

So far in ML4

Adam Topaz (Mar 25 2023 at 00:28):

Ok so presumably the same trick should work for all those. E.g. for algebra Homs the base ring’s type should be an outparam etc

Adam Topaz (Mar 25 2023 at 00:29):

At least I think that’s the right thing to do. @Gabriel Ebner can you verify?

Gabriel Ebner (Mar 25 2023 at 00:31):

No some of these are unfortunately unavoidable atm (because we currently always infer the subgoals strictly left-to-right). I'm cleaning up lean4#2117 now which should make all of these {_ : TopologicalSpace X} workarounds unnecessary.

Gabriel Ebner (Mar 25 2023 at 01:08):

Both of the coercions at the beginning of the thread work now. Please ping me if you run into any other issues.

Kevin Buzzard (Mar 25 2023 at 07:42):

Thanks so so much Gabriel!

Filippo A. E. Nuccio (Apr 06 2023 at 16:30):

I wonder if I am running into the same sort of troubles. I am trying to port analysis\normed_space\linear_isometry and I have

protected theorem congr_arg [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] {f : 𝓕} :
  ∀ {x x' : E}, x = x' → f x = f x' -- Lean complains

I get the error failed to synthesize (deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached. I would imagine that it is uncapable of coercing f from the semi_linear_isometry_class to a function. Is that possible?

Matthew Ballard (Apr 06 2023 at 16:38):

If you set_option maxHeartbeats 0 in and set_option synthInstance.maxHeartbeats 0 in it still might succeed. What if you just do

example [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] {f : 𝓕}  : E →  E₂ := f

Failures occur with SemilinearMapClass getting coerced to a function. That is “fixed” with etaExperiment but usually does not present as a timeout

Filippo A. E. Nuccio (Apr 06 2023 at 16:41):

Matthew Ballard said:

If you set_option maxHeartbeats 0 in and set_option synthInstance.maxHeartbeats 0 in it still might succeed. What if you just do

example [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] {f : 𝓕}  : E →  E₂ := f

Failures occur with SemilinearMapClass getting coerced to a function. That is “fixed” with etaExperiment but usually does not present as a timeout

Unfortunately

example [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] {f : 𝓕}  : E →  E₂ := f

still fails with error type mismatch f has type 𝓕 : Type ?u.433175 but is expected to have type E → E₂ : Type (max ?u.433160 ?u.433163). On the other hand,

example (h : SemilinearIsometryClass 𝓕 σ₁₂ E E₂) {f : 𝓕}  : E →  E₂ := h.coe f

succeeds, as if the problem were finding the right instance.

Matthew Ballard (Apr 06 2023 at 16:44):

Then set_option synthInstance.etaExperiment true in might fix it

Filippo A. E. Nuccio (Apr 06 2023 at 16:45):

Unfortunately no, but should I combine it with the other two set_options?

Matthew Ballard (Apr 06 2023 at 16:45):

It can be tried but I don’t remember that combination ever being helpful to me.

Filippo A. E. Nuccio (Apr 06 2023 at 16:46):

yes, indeed it is not...

Matthew Ballard (Apr 06 2023 at 16:46):

What does turning off the limits on heartbeats do if anything?

Filippo A. E. Nuccio (Apr 06 2023 at 16:47):

Let me try

Filippo A. E. Nuccio (Apr 06 2023 at 16:47):

Is it a Lean4 setting? Or rather something

set_option maxHeartbeats 10000000 in

Matthew Ballard (Apr 06 2023 at 16:50):

0 = ∞\infty

Adam Topaz (Apr 06 2023 at 16:50):

What does the TC trace show here? Do we need some other fix similar to what Gabriel did above?

Matthew Ballard (Apr 06 2023 at 16:50):

And the one for synthInstance.maxHeartbeats

Matthew Ballard (Apr 06 2023 at 16:51):

Adam Topaz said:

What does the TC trace show here? Do we need some other fix similar to what Gabriel did above?

set_option trace.Meta.synthInstance

Matthew Ballard (Apr 06 2023 at 16:51):

Also set_option profiler helps with searching through the output

Filippo A. E. Nuccio (Apr 06 2023 at 16:53):

So, with set_option maxHeartbeats 10000000 in nothing changes. Then I got lost in what you are suggesting/asking... :sweat_smile:

Adam Topaz (Apr 06 2023 at 16:54):

Using set_option trace.Meta.synthInstance true in ... will show you a trace of the typeclass search. There may be some loop in there or some other issue.

Matthew Ballard (Apr 06 2023 at 16:55):

Sorry, 

set_option profiler true in
set_option trace.Meta.synthInstance true in
set_option trace.Meta.isDefEq true in
set_option maxHeartbeats 0 in
set_option synthInstance.maxHeartbeats 0 in

Matthew Ballard (Apr 06 2023 at 16:55):

Is my go-to first combo

Adam Topaz (Apr 06 2023 at 16:55):

if there's a loop, that 0 would make it take a little while ;)

Filippo A. E. Nuccio (Apr 06 2023 at 16:55):

...and the answer is... :clock:

Matthew Ballard (Apr 06 2023 at 16:56):

Yes, go make some tea and if it is still going restart Lean and give it large but finite numbers for the heartbeats

Filippo A. E. Nuccio (Apr 06 2023 at 16:56):

OK, I will report after my tea :teapot: (indeed, the laptop is getting hot, might use if for the water...)

Matthew Ballard (Apr 06 2023 at 16:57):

Lean is only program I have had to worry about my lap with

Filippo A. E. Nuccio (Apr 06 2023 at 17:23):

No, nothing. After a long time I restarted it and changed 0 to 10000000. But it got stuck, telling me

(deterministic) timeout at 'whnf', maximum number of heartbeats (10000000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

Matthew Ballard (Apr 06 2023 at 17:24):

Did you
Matthew Ballard said:

Sorry, 

set_option profiler true in
set_option trace.Meta.synthInstance true in
set_option trace.Meta.isDefEq true in
set_option maxHeartbeats 0 in
set_option synthInstance.maxHeartbeats 0 in

Try this with 0 -> 10000000 for both heartbeat limits

Filippo A. E. Nuccio (Apr 06 2023 at 17:28):

Yes, both hearbeat with 0 first (was getting nowhere after 20 minutes); then I changed both to 10000000 , restarted the server, and got the above error.

Matthew Ballard (Apr 06 2023 at 17:28):

You should have a lot more output

Matthew Ballard (Apr 06 2023 at 17:29):

I don’t use VS Code much but I think they are blue squiggles

Filippo A. E. Nuccio (Apr 06 2023 at 17:29):

Oh, indeed I have it. I did not think it was relevant, I am going to paste it here.

Filippo A. E. Nuccio (Apr 06 2023 at 17:29):

(need to restart...)

Filippo A. E. Nuccio (Apr 06 2023 at 17:35):

(deterministic) timeout at 'whnf', maximum number of heartbeats (10000000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
LinearIsometry.lean:219:33
[Meta.isDefEq] [0.000003s] :check: Type ?u.437939 =?= Type ?u.433175

[Meta.isDefEq] [0.000002s] :check: Type ?u.433175 =?= Type ?u.433175
LinearIsometry.lean:219:36
[Meta.isDefEq] [0.000299s] :check: ?m.437940 →+* ?m.437941 =?= R →+* R₂ :play:

[Meta.isDefEq] [0.000044s] :check: R →+* R₂ =?= R →+* R₂ :play:
LinearIsometry.lean:219:40
[Meta.isDefEq] [0.000003s] :check: Type ?u.437936 =?= Type ?u.433160

[Meta.isDefEq] [0.000002s] :check: Type ?u.433160 =?= Type ?u.433160
LinearIsometry.lean:219:9
[Meta.isDefEq] [0.000011s] :check: Sort ?u.437934 =?= Type (max (max ?u.437939 ?u.437936) ?u.437935)

[Meta.synthInstance] [0.000037s] :check: Semiring R :play:

[Meta.isDefEq] [0.000000s] :check: inst:cross:³³ =?= inst:cross:³³

[Meta.synthInstance] [0.000026s] :check: Semiring R₂ :play:

[Meta.isDefEq] [0.000000s] :check: inst:cross:³² =?= inst:cross:³²

[Meta.synthInstance] [0.000029s] :check: SeminormedAddCommGroup E :play:

[Meta.isDefEq] [0.000025s] :check: ?m.437948 =?= inst:cross:⁹ :play:

[Meta.synthInstance] [0.000028s] :check: SeminormedAddCommGroup E₂ :play:

[Meta.isDefEq] [0.000023s] :check: ?m.437949 =?= inst:cross:⁸ :play:

[Meta.synthInstance] [0.000052s] :check: Module R E :play:

[Meta.isDefEq] [0.000050s] :check: ?m.437950 =?= inst:cross:⁵ :play:

[Meta.synthInstance] [0.000049s] :check: Module R₂ E₂ :play:

[Meta.isDefEq] [0.000042s] :check: ?m.437951 =?= inst:cross:⁴ :play:

[Meta.isDefEq] [0.000009s] :check: Type (max (max ?u.433163 ?u.433160) ?u.433175) =?= Type (max (max ?u.433175 ?u.433160) ?u.433163)
LinearIsometry.lean:219:42
[Meta.isDefEq] [0.000003s] :check: Type ?u.437935 =?= Type ?u.433163

[Meta.isDefEq] [0.000002s] :check: Type ?u.433163 =?= Type ?u.433163
LinearIsometry.lean:219:51
[Meta.isDefEq] [0.000006s] :check: Sort ?u.437953 =?= Type ?u.433175
LinearIsometry.lean:219:58
[Meta.isDefEq] [0.000002s] :check: Sort ?u.437956 =?= Type ?u.433160
LinearIsometry.lean:219:63
[Meta.isDefEq] [0.000003s] :check: Sort ?u.437957 =?= Type ?u.433163
LinearIsometry.lean:219:69
type mismatch
f
has type
𝓕 : Type ?u.433175
but is expected to have type
E → E₂ : Type (max ?u.433160 ?u.433163)
LinearIsometry.lean:219:69
[Meta.isDefEq] [0.000026s] :cross_mark: E → E₂ =?= 𝓕 :play:

[Meta.isDefEq] [0.000007s] :cross_mark: 𝓕 =?= E → E₂ :play:

[Meta.synthInstance] [293.306474s] :boom: CoeFun 𝓕 ?m.437963

Matthew Ballard (Apr 06 2023 at 17:45):

(Sorry got distracted asking GPT-4 which journal to submit to)

Matthew Ballard (Apr 06 2023 at 17:45):

Does the last expand at all?

Filippo A. E. Nuccio (Apr 06 2023 at 18:03):

The last line, you mean?

Matthew Ballard (Apr 06 2023 at 18:04):

Yeah, does it have a little triangle?

Filippo A. E. Nuccio (Apr 06 2023 at 18:04):

Yes, but VSCode tells me it still has 549 messages for me, and it seems to be stuck on showing them after I clicked on the triangle...

Matthew Ballard (Apr 06 2023 at 18:05):

If you run lean on the command line on the file and pipe the output to a file, it might be easier to search the output

Filippo A. E. Nuccio (Apr 06 2023 at 18:08):

Ah, good idea. I need to go now (evening in Europe) but I will try again tomorrow.

Filippo A. E. Nuccio (Apr 06 2023 at 18:08):

Thanks!

Matthew Ballard (Apr 06 2023 at 18:11):

It will be large :)

Matthew Ballard (Apr 06 2023 at 18:11):

(For a text file)

Adam Topaz (Apr 06 2023 at 19:10):

Matthew Ballard said:

(Sorry got distracted asking GPT-4 which journal to submit to)

What did it say?

Matthew Ballard (Apr 07 2023 at 00:29):

  1. JAG
  2. Duke
  3. Transactions
  4. Annals
  5. JAMS

Matthew Ballard (Apr 07 2023 at 00:33):

You can also ask it which journal is more prestigious. Fun stuff

Adam Topaz (Apr 07 2023 at 00:57):

Is this ordered by chance of acceptance?

Matthew Ballard (Apr 07 2023 at 01:05):

I don't think so

Filippo A. E. Nuccio (Apr 07 2023 at 14:04):

I have the text file, I am uploading it here in case someone (@Matthew Ballard ?) is willing to give it a look. It is indeed not bad, 8MB for a text file just full of errors :sweat_smile:
error.txt

Last updated: Dec 20 2023 at 11:08 UTC