Typeclass search is affected by other subexpressions

Stream: general

[Eric Wieser]

Two very confusing typeclass failures:

import Mathlib.Analysis.NormedSpace.OperatorNorm

variable (𝕜 : Type*) [NontriviallyNormedField 𝕜]
variable (E : Type*) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]

abbrev Dual : Type _ := E →L[𝕜] 𝕜

def inclusionInDoubleDual : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := sorry

#check _ = ‖ContinuousLinearMap.id 𝕜 (Dual 𝕜 E)‖

-- ok
example : (by exact ‖inclusionInDoubleDual 𝕜 E‖) = ‖ContinuousLinearMap.id 𝕜 (Dual 𝕜 E)‖ := sorry

-- fail
example : ‖inclusionInDoubleDual 𝕜 E‖ = ‖ContinuousLinearMap.id 𝕜 (Dual 𝕜 E)‖ := sorry

--ok
example := @ContinuousLinearMap.norm_id_le 𝕜 (Dual 𝕜 E) _ _ _

-- fail
example : ‖inclusionInDoubleDual 𝕜 E‖ ≤ 1 := by
  have := @ContinuousLinearMap.norm_id_le 𝕜 (Dual 𝕜 E) _ _ _
  · sorry
  · sorry -- where did these goals come from?
  · sorry

[Eric Wieser]

In the first example, the ‖inclusionInDoubleDual 𝕜 E‖ on the LHS is breaking typeclass search on the RHS (unless we use by exact to isolate it)

[Eric Wieser]

In the second example, the type of the goal is somehow changing the elaboration of a have statement

[Eric Wieser]

(cc @Sebastian Ullrich, whom I discussed this with this morning)

[Eric Wieser]

Replacing Dual 𝕜 E with E →L[𝕜] 𝕜 in any of the broken examples seems to fix the issue, suggesting this is a bug in abbrev + TC search.

[Eric Wieser]

The problem seems to be a bad search cache: on the first example, I get

[Meta.synthInstance] ❌ Norm (Dual 𝕜 E →L[𝕜] Dual 𝕜 E) ▼
  [] new goal Norm (Dual 𝕜 E →L[𝕜] Dual 𝕜 E) ▼
    [instances] #[@SeminormedAddGroup.toNorm, @SeminormedGroup.toNorm, @NormedAddGroup.toNorm, @NormedGroup.toNorm, @SeminormedAddCommGroup.toNorm, @SeminormedCommGroup.toNorm, @NormedAddCommGroup.toNorm, @NormedCommGroup.toNorm, @NonUnitalSeminormedRing.toNorm, @SeminormedRing.toNorm, @NonUnitalNormedRing.toNorm, @NormedRing.toNorm, @NormedDivisionRing.toNorm, @NormedField.toNorm, @ContinuousLinearMap.hasOpNorm]
  [] ❌ apply @ContinuousLinearMap.hasOpNorm to Norm (Dual 𝕜 E →L[𝕜] Dual 𝕜 E) ▼
    [tryResolve] ❌ Norm (Dual 𝕜 E →L[𝕜] Dual 𝕜 E) ≟ Norm (?m.16472 →SL[?m.16480] ?m.16473) ▼
      [] ✅ NontriviallyNormedField 𝕜 ▼
        [] result inst✝² (cached)
      [] ✅ NontriviallyNormedField 𝕜 ▶
      [] ❌ SeminormedAddCommGroup (Dual 𝕜 E) ▼
        [] result <not-available> (cached)
<snip>

where on the last line, lean didn't even bother to look for the instance that it couldn't find and just falsely claimed it already knew it was missing

[Eric Wieser]

Another MWE, where a rw affects TC search withina have that follows it; even though the have does not ever see the main goal!

import Mathlib.Analysis.NormedSpace.OperatorNorm

variable (𝕜 : Type) [NontriviallyNormedField 𝕜]
variable (E : Type) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]

abbrev Dual : Type _ := E →L[𝕜] 𝕜

def inclusionInDoubleDual : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := sorry

example : ‖inclusionInDoubleDual 𝕜 E‖ = 0 := by
  -- this `rw` is needed to make the `have` below work
  -- rw [inclusionInDoubleDual]
  haveI : Norm (Dual 𝕜 E →L[𝕜] Dual 𝕜 E) := inferInstance
  sorry

[Sebastian Ullrich]

Underlying bug is lean4#2522. More data on impact and a non-Mathlib MWE would be greatly appreciated!

[Eric Wieser]

Thanks, your explanation is already helpful!

[Kevin Buzzard]

Making a non-Mathlib MWE will be hours of work, however it would not surprise me if someone could be persuaded to do that work if someone explained to them more details about why non-Mathlib MWEs are so important. All I know from experience is that they are very much appreciated by the lean dev community, but I don't really understand why. Is it because you don't know about lake exe cache get and think that you have to spend hours compiling mathlib? ;-) If the answer is "mathlib just makes traces much more cluttered in general" then my first reaction to this is "are you absolutely sure that mathlib is making traces much more cluttered in this particular case?". But maybe the answer is something else which I haven't internalised yet.

[Eric Wieser]

Is it because you don't know about lake exe cache get and think that you have to spend hours compiling mathlib?

If you make a fix to Lean, the cache is (probably?) invalidated and you have to rebuild it all again

[Sebastian Ullrich]

@Kevin Buzzard Also, we can't add code with dependencies to the Lean 4 test suite (whose tests' runtimes should be measured in seconds, not hours)

[Sebastian Ullrich]

But note that doing minimization the usual way starting from the full code really isn't the optimal way here I believe. Instead one should start at the traces I posted and recreate only the components mentioned there, which hopefully should be much faster.

[Kevin Buzzard]

I think that it's not unreasonable to suggest that a general tool which produces mathlib-free MWEs would be very useful for this sort of thing; of course I don't have the ability to make it. I've heard that there is one in Coq but I don't know how well it works in practice. Thanks for the responses Sebastian and Eric.

[Kevin Buzzard]

@Eric Wieser and @Patrick Massot I might well take on mathlib-free minimisation of an example this evening; just to let you know in case you've started on one as well. What is the best target? Is it this post?

[Kevin Buzzard]

Sebastian -- do you have a preference?

[Eric Wieser]

I was not planning to take this on in the immediate future, so please do so!

[Eric Wieser]

I would guess all three examples will reproduce the same way

[Kevin Buzzard]

Here is a preliminary reduction, although there is still a long way to go:

import Mathlib.Analysis.Normed.Field.Basic

variable (𝕜 : Type) [NonUnitalSeminormedRing 𝕜]
variable (E : Type) [SeminormedAddCommGroup E]

structure ContinuousLinearMap' (M : Type) [TopologicalSpace M] (M₂ : Type) [TopologicalSpace M₂] where

notation:25 M " →z " M₂ => ContinuousLinearMap' M M₂

abbrev Dual : Type := E →z 𝕜

instance ContinuousLinearMap'.toSeminormedAddCommGroup {E : Type} {F : Type}
    [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] :
  SeminormedAddCommGroup (E →z F) := sorry

def foo : E →z Dual 𝕜 (Dual 𝕜 E) := 0

example : ‖foo 𝕜 E‖ = 0 := by
  -- this `rw` is needed to make the `have` below work
  --rw [foo]
  have : SeminormedAddCommGroup (Dual 𝕜 E) := inferInstance
  sorry

But now I need to properly understand what is going on, because further attempts by me to minimise just result in the problem going away. I have two questions about the summary at lean4#2522 :

1) what is a nested TC problem?

2) If I add set_option trace.Meta.synthInstance true then I can see the failure

[Meta.synthInstance] ❌ SeminormedAddCommGroup (Dual 𝕜 E) ▼
  [] result <not-available> (cached)

at the end of the example above. My understanding is that the current belief is that the cache has been tricked to return this because of some earlier failure (when things were "nested"). But I can't find that earlier failure in the trace and am not entirely sure where I should be looking.

[Kevin Buzzard]

Aah, I've solved (2), it's deep within [Meta.synthInstance] ✅ Norm (E →z Dual 𝕜 (Dual 𝕜 E))

[Kevin Buzzard]

Aah and in my search I suspect I've also figured out what a nested typeclass search is; indeed the reason it was hard to find was because it was...erm...a typeclass search within a typeclass search.

[Kevin Buzzard]

class Norm' (E : Type) where
  norm : E → Nat

export Norm' (norm)

class TopologicalSpace' (α : Type) where
  random : α -- need something here for some reason

class SeminormedAddCommGroup' (α : Type) extends Norm' α, TopologicalSpace' α where

-- need to extend Norm' again for some reason; note that this doesn't seem to cause a diamond
class NonUnitalSeminormedRing' (α : Type) extends Norm' α, SeminormedAddCommGroup' α where

variable (𝕜 : Type) [NonUnitalSeminormedRing' 𝕜]
variable (E : Type) [SeminormedAddCommGroup' E]

structure ContinuousLinearMap' (M : Type) [TopologicalSpace' M] (M₂ : Type) [TopologicalSpace' M₂] where

notation:25 M " →z " M₂ => ContinuousLinearMap' M M₂

abbrev Dual : Type := E →z 𝕜

instance ContinuousLinearMap'.toSeminormedAddCommGroup' {E : Type} {F : Type}
    [SeminormedAddCommGroup' E] [SeminormedAddCommGroup' F] :
  SeminormedAddCommGroup' (E →z F) := sorry

def foo : E →z Dual 𝕜 (Dual 𝕜 E) := sorry

#synth SeminormedAddCommGroup' (Dual 𝕜 E) -- works fine

-- set_option trace.Meta.synthInstance true
example : norm (foo 𝕜 E) = 0 := by
  -- this `rw` is needed to make the `have` below work
  --rw [foo]
  have : SeminormedAddCommGroup' (Dual 𝕜 E) := inferInstance -- now fails!
  sorry

/-

Relevant traces in the example:

1) On `norm (foo 𝕜 E)`:

[Meta.synthInstance] ✅ Norm' (E →z Dual 𝕜 (Dual 𝕜 E)) ▼
  [] new goal Norm' (E →z Dual 𝕜 (Dual 𝕜 E)) ▶
  [] ✅ apply @NonUnitalSeminormedRing'.toNorm' to Norm' (E →z Dual 𝕜 (Dual 𝕜 E)) ▶
  [] ❌ apply inst✝¹ to NonUnitalSeminormedRing' (E →z Dual 𝕜 (Dual 𝕜 E)) ▶
  [] ✅ apply @SeminormedAddCommGroup'.toNorm' to Norm' (E →z Dual 𝕜 (Dual 𝕜 E)) ▶
  [] ❌ apply inst✝ to SeminormedAddCommGroup' (E →z Dual 𝕜 (Dual 𝕜 E)) ▶
  [] ✅ apply @ContinuousLinearMap'.toSeminormedAddCommGroup' to SeminormedAddCommGroup' (E →z Dual 𝕜 (Dual 𝕜 E)) ▼
    [tryResolve] ✅ SeminormedAddCommGroup' (E →z Dual 𝕜 (Dual 𝕜 E)) ≟ SeminormedAddCommGroup' (E →z Dual 𝕜 (Dual 𝕜 E)) ▼
      [] ✅ SeminormedAddCommGroup' E ▶
      [] ✅ SeminormedAddCommGroup' (Dual 𝕜 (Dual 𝕜 E)) ▼
        [] new goal SeminormedAddCommGroup' (Dual 𝕜 (Dual 𝕜 E)) ▶
        [] ❌ apply inst✝ to SeminormedAddCommGroup' (Dual 𝕜 (Dual 𝕜 E)) ▶
        [] ✅ apply @ContinuousLinearMap'.toSeminormedAddCommGroup' to SeminormedAddCommGroup' (Dual 𝕜 (Dual 𝕜 E)) ▼
          [tryResolve] ✅ SeminormedAddCommGroup' (Dual 𝕜 (Dual 𝕜 E)) ≟ SeminormedAddCommGroup' (Dual 𝕜 E →z 𝕜) ▼
            [] ❌ SeminormedAddCommGroup' (Dual 𝕜 E) ▼
              [] new goal SeminormedAddCommGroup' (Dual 𝕜 E) ▶
              [] ❌ apply inst✝ to SeminormedAddCommGroup' (Dual 𝕜 E) ▶
              [] ❌ apply @ContinuousLinearMap'.toSeminormedAddCommGroup' to SeminormedAddCommGroup' (Dual 𝕜 E) ▼
                [tryResolve] ❌ SeminormedAddCommGroup' (Dual 𝕜 E) ≟ SeminormedAddCommGroup' (?m.8308 →z ?m.8309)

2) Later, on `inferInstance`

[Meta.synthInstance] ❌ SeminormedAddCommGroup' (Dual 𝕜 E) ▼
  [] result <not-available> (cached)

-/

Mathlib-free! Should I post this on the github issue or are the names distasteful and I should replace them with proper computer science name like foo and bar?

[Patrick Massot]

I think those names are allowed.

[Kevin Buzzard]

The example is extremely fragile (this was one reason that minimisation was hard). If you tinker with random things then all of a sudden the failing [tryResolve] ❌ SeminormedAddCommGroup' (Dual 𝕜 E) ≟ SeminormedAddCommGroup' (?m.8308 →z ?m.8309) magically turns into a succeeding SeminormedAddCommGroup' (Dual 𝕜 E) ≟ SeminormedAddCommGroup' (E →z 𝕜). I have no understanding of what is going on here. Similarly the topological space structure has to have a field or else the problem goes away, and you have to extend Norm' twice or the problem goes away.

[Kevin Buzzard]

class Norm' (E : Type) where
  norm : E → Nat

export Norm' (norm)

class TopologicalSpace' (α : Type) where
  random : α -- need something here for some reason

class SeminormedAddCommGroup' (α : Type) extends Norm' α, TopologicalSpace' α where

-- need to extend Norm' again for some reason; note that this doesn't seem to cause a diamond
class NonUnitalSeminormedRing' (α : Type) extends Norm' α, SeminormedAddCommGroup' α where

variable (𝕜 : Type) [NonUnitalSeminormedRing' 𝕜]

-- no diamond
example : (NonUnitalSeminormedRing'.toNorm' : Norm' 𝕜) =
    @SeminormedAddCommGroup'.toNorm' 𝕜 (@NonUnitalSeminormedRing'.toSeminormedAddCommGroup' 𝕜 _) := rfl