Type class inference loop

Stream: new members

[Nicolò Cavalleri]

What is going wrong in this simple #mwe?

import topology.constructions

variables {B : Type*} (E : B → Type*) {B' : Type*} [topological_space B']

/-- -/
def total_space := Σ x, E x

@[priority 90, nolint unused_arguments]
instance pullback.total_space.topological_space [topological_space (total_space E)] {f : B' → B} :
  topological_space (total_space (E ∘ f)) := sorry

#lint --TYPE CLASS SEARCHES TIMED OUT

[Nicolò Cavalleri]

Cross posted from https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238545

[Eric Wieser]

Is that the entire lint message?

[Nicolò Cavalleri]

No the entire message is very long:

/- The `fails_quickly` linter reports: -/
/- TYPE CLASS SEARCHES TIMED OUT.
The following instances are part of a loop, or an excessively long search.
It is common that the loop occurs in a different class than the one flagged below,
but usually an instance that is part of the loop is also flagged.
To debug:
(1) run `scripts/mk_all.sh` and create a file with `import all` and
`set_option trace.class_instances true`
(2) Recreate the state shown in the error message. You can do this easily by copying the type of
the instance (the output of `#check @my_instance`), turning this into an example and removing the
last argument in square brackets. Prove the example using `by apply_instance`.
For example, if `additive.topological_add_group` raises an error, run
``
example {G : Type*} [topological_space G] [group G] : topological_add_group (additive G) :=
by apply_instance
``
(3) What error do you get?
(3a) If the error is "tactic.mk_instance failed to generate instance",
there might be nothing wrong. But it might take unreasonably long for the type-class inference to
fail. Check the trace to see if type-class inference takes any unnecessary long unexpected turns.
If not, feel free to increase the value in the definition of the linter `fails_quickly`.
(3b) If the error is "maximum class-instance resolution depth has been reached" there is almost
certainly a loop in the type-class inference. Find which instance causes the type-class inference to
go astray, and fix that instance. -/
#check @pullback.total_space.topological_space /- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
State:
B : Type u_1,
E : B → Type u_2,
B' : Type u_3,
_inst_1 : topological_space B',
f : B' → B
⊢ topological_space (total_space (E ∘ f)) -/

/- The `has_inhabited_instance` linter reports: -/
/- TYPES ARE MISSING INHABITED INSTANCES: -/
#check @total_space /- inhabited instance missing -/

[Nicolò Cavalleri]

I was hoping someone could tell me the reason without me having to follow these long instructions

[Eric Wieser]

You can skip the mk_all step since you got this error from #lint and not CI

[Eric Rodriguez]

I guess it's trying to find everything using id

[Eric Wieser]

Yes, that is indeed the problem - ∘ is very transparent to lean, so whenever you ask for topological_space (total_space E) lean will try your instance with f = id and look for topological_space (total_space (E ∘ id))

[Nicolò Cavalleri]

Then what is going wrong here?

import topology.constructions

open topological_space

variables {B : Type*} (E : B → Type*) (F : B → Type*) {B' : Type*} [topological_space B']

/-- -/
def total_space := Σ x, E x

@[priority 90, nolint unused_arguments]
instance test [topological_space (total_space E)]{f : B' → B} :
  topological_space (total_space (λ x, E x × F x)) := sorry

#lint

[Eric Wieser]

Have you tried following the instructions to find out?

[Eric Wieser]

You only need to add a few lines to your mwe

[Nicolò Cavalleri]

Eric Wieser said:

You only need to add a few lines to your mwe

Yes in both cases it leads me to option 3a which apparently means that there's nothing wrong

[Eric Wieser]

(Also f is unused there)

[Nicolò Cavalleri]

Eric Wieser said:

(Also f is unused there)

Oh I see this was the problem, ops!

[Eric Wieser]

You turned off the linter that would have warned you of that!

[Nicolò Cavalleri]

Eric Wieser said:

Yes, that is indeed the problem - ∘ is very transparent to lean, so whenever you ask for topological_space (total_space E) lean will try your instance with f = id and look for topological_space (total_space (E ∘ id))

What is the best solution to this? Having a type synonym for the composition? Plus why is this triggered now but it was not triggered last fall? (The proof that is was not triggered is in the linked PR)

[Eric Wieser]

I'm not certain the linter existed then

[Eric Wieser]

WRT avoiding this issue; can you un- #xy the problem a little? For what E do you expect lean to find a topological_space (total_space E) instance?

[Nicolò Cavalleri]

For the composition
Eric Wieser said:

WRT avoiding this issue; can you un- #xy the problem a little? For what E do you expect lean to find a topological_space (total_space E) instance?

For any E which is the composition of a another E' with that instance and a function

[Eric Wieser]

Ok, but if that's the only instance then no instances exist

[Eric Wieser]

What other instances do you intend to have?

[Eric Wieser]

(context: what you're trying to do sounds a bit like trying to teach lean [algebra R S] [algebra S A] : algebra R Awhich while mathematically obvious isn't appropriate for Lean's typeclasses)

[Nicolò Cavalleri]

Eric Wieser said:

(context: what you're trying to do sounds a bit like trying to teach lean [algebra R S] [algebra S A] : algebra R Awhich while mathematically obvious isn't appropriate for Lean's typeclasses)

I agree: what puzzles me here is that if I use a type synonym for composition of if I silentiate the linter everything works smoothly

[Nicolò Cavalleri]

Eric Wieser said:

What other instances do you intend to have?

Any standard vector bundle, for example the product topological space on constant sigma types

[Eric Wieser]

If you follow the instruction in the linter message, you'll find the example that does not work smoothly

[Eric Wieser]

The instance on constant sigma types you're talking about is the one on total_space (λ i, E'), right?

[Eric Wieser]

If so, that instance will already match total_space ((λ i, E') ∘ f)

[Sebastien Gouezel]

My guess : if you have a typeclass foo (f ∘ g) depending on foo f, like in your examples, then this can lead to an infinite recursion as follows. When looking for foo f then Lean will try to write f as f ∘ id, then apply the above instance and try to find a foo f for this, and loop. So you should use some kind of type synonym to hide the composition from typeclass inference. (This is one of the reasons we switched from unbundled morphisms, as typeclass inference was not working properly on compositions).

[Nicolò Cavalleri]

Ok sure let's introduce a type synonym: it is very natural anyways

[Eric Wieser]

Nicolò Cavalleri said:

Any standard vector bundle, for example the product topological space on constant sigma types

Can you give another example, since as I remark above you don't need a compositional instance for this

[Nicolò Cavalleri]

Eric Wieser said:

Nicolò Cavalleri said:

Any standard vector bundle, for example the product topological space on constant sigma types

Can you give another example, since as I remark above you don't need a compositional instance for this

I am not sure if you are asking me for examples of bundles defined through composition or not since from your question above I thought you wanted examples other than the composition!

[Eric Wieser]

I want an example of a bundle not defined through composition X, such that there is also a bundled defined through composition with X, Y, that is not the same form as X

[Eric Wieser]

The constant bundle is not such an example, because the compositions with a constant sigma type remains a constant sigma type

[Nicolò Cavalleri]

Eric Wieser said:

I want an example of a bundle not defined through composition X, such that there is also a bundled defined through composition with X, Y, that is not the same form as X

Like the pullback of a Mobius bundle on a segment of $S^1$?

[Eric Wieser]

Can you write the statement of that in lean, or do we not have the pieces yet to do so?

[Nicolò Cavalleri]

Sebastien Gouezel said:

My guess : if you have a typeclass foo (f ∘ g) depending on foo f, like in your examples, then this can lead to an infinite recursion as follows. When looking for foo f then Lean will try to write f as f ∘ id, then apply the above instance and try to find a foo f for this, and loop. So you should use some kind of type synonym to hide the composition from typeclass inference. (This is one of the reasons we switched from unbundled morphisms, as typeclass inference was not working properly on compositions).

Type synonym has the disadvantage that if E (f x) is a topological space then (pullback f E) x will not be recognized anymore as a topological space, but one has to use the local attribut trick and redeclare instances... a bit annoying but ok. Other suggestions are welcome though

[Nicolò Cavalleri]

Eric Wieser said:

Can you write the statement of that in lean, or do we not have the pieces yet to do so?

We do not have the Mobius bundle yet, by now we only have the trivial one :(

[Nicolò Cavalleri]

And tangent bundles of course which is the source of our nontrivial examples