cannot synth IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜)

Stream: mathlib4

[Jireh Loreaux]

Well, this is fun ...

import Mathlib.Topology.ContinuousFunction.Algebra
import Mathlib.Data.IsROrC.Basic

variable {R : Type*} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R]

variable {𝕜 : Type*} [IsROrC 𝕜]

#synth Algebra R C(R, R) -- ContinuousMap.algebra
#synth IsScalarTower R C(R, R) C(R, R) -- IsScalarTower.right

#synth Algebra 𝕜 C(𝕜, 𝕜) -- ContinuousMap.algebra

set_option trace.Meta.synthInstance true
set_option trace.Meta.isDefEq true
#synth IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜) -- failed
/-
[Meta.synthInstance] ❌ IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜) ▼
  [] new goal IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜) ▶
  [] ❌ apply @ContinuousMap.instIsScalarTowerContinuousMapInstSMulInstSMul to IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜) ▶
  [] ❌ apply @IsScalarTower.right to IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜) ▼
    [tryResolve] ❌ IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜) ≟ IsScalarTower ?m.8431 ?m.8432 ?m.8432 ▼
      [isDefEq] ❌ IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜) =?= IsScalarTower ?m.8431 ?m.8432 ?m.8432 ▼
        [] ✅ 𝕜 =?= ?m.8431 ▶
        [] ✅ C(𝕜, 𝕜) =?= ?m.8432 ▶
        [] ✅ C(𝕜, 𝕜) =?= C(𝕜, 𝕜)
        [synthInstance] 💥 Algebra 𝕜 C(𝕜, 𝕜) ▶
        [] ❌ ContinuousMap.instSMul =?= Algebra.toSMul ▼
          [] ❌ { smul := fun r f => { toFun := r • ⇑f, continuous_toFun := ⋯ } } =?= Algebra.toSMul ▼
            [] ❌ { smul := fun r f => { toFun := r • ⇑f, continuous_toFun := ⋯ } } =?= ?m.8435.1 ▼
              [] ✅ SMul 𝕜 C(𝕜, 𝕜) =?= SMul 𝕜 C(𝕜, 𝕜) ▶
              [] ❌ SMul.smul =?= fun r f => { toFun := r • ⇑f, continuous_toFun := ⋯ } ▼
                [] ❌ fun r f => { toFun := r • ⇑f, continuous_toFun := ⋯ } =?= fun a => SMul.smul a ▼
                  [] ✅ 𝕜 =?= 𝕜
                  [] ❌ fun f => { toFun := r • ⇑f, continuous_toFun := ⋯ } =?= SMul.smul r ▼
                    [] ❌ fun f => { toFun := r • ⇑f, continuous_toFun := ⋯ } =?= fun a => SMul.smul r a ▼
                      [] ✅ C(𝕜, 𝕜) =?= C(𝕜, 𝕜)
                      [] ❌ { toFun := r • ⇑f, continuous_toFun := ⋯ } =?= SMul.smul r f ▼
                        [] ❌ { toFun := r • ⇑f, continuous_toFun := ⋯ } =?= ?m.8435.1.1 r f ▼
                          [] ✅ C(𝕜, 𝕜) =?= C(𝕜, 𝕜)
                          [] ❌ (?m.8435.1.1 r f).toFun =?= r • ⇑f ▶
                          [] ❌ @ContinuousMap.mk =?= ?m.8435.1.1 ▶
                          [onFailure] ❌ { toFun := r • ⇑f, continuous_toFun := ⋯ } =?= ?m.8435.1.1 r f ▶
                          [onFailure] ❌ { toFun := r • ⇑f, continuous_toFun := ⋯ } =?= ?m.8435.1.1 r f ▶
              [onFailure] ❌ { smul := fun r f => { toFun := r • ⇑f, continuous_toFun := ⋯ } } =?= ?m.8435.1 ▶
        [onFailure] ❌ IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜) =?= IsScalarTower ?m.8431 ?m.8432 ?m.8432
        [onFailure] ❌ IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜) =?= IsScalarTower ?m.8431 ?m.8432 ?m.8432
  [] ❌ apply IsScalarTower.left to IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜) ▶
  [] ❌ apply @Semigroup.isScalarTower to IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜) ▶
  [] ❌ apply @IsScalarTower.of_algHom to IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜) ▶
-/

[Matthew Ballard]

Is pasting this into scratch.lean file at the root of mathlib supposed to bork the server?

[Jireh Loreaux]

oh, that's even worse. I didn't even notice that. I get that it prints this error:

4
54
46
96
146
44
94
144

[Jireh Loreaux]

The borking of the server is somehow due to the tracing (of the instances, not of the defeq), which seems very bad.

[Matthew Ballard]

It’s not the problem but ContinousMap.C should be reducible

[Matthew Ballard]

I am guessing metavariable depth is the culprit here

[Matthew Ballard]

[] 💥 ?m.18092 =?= ContinuousMap.instSemiringContinuousMap ▼
                  [] ?m.18092 [nonassignable] =?= ContinuousMap.instSemiringContinuousMap [nonassignable]

it fails to get the algebra structure here and just continuous with a metavariable

[Matthew Ballard]

Do we need Algebra R A for IsScalarTower.right?

[Jireh Loreaux]

But it gets the algebra structure fine when you ask it, see above.

[Matthew Ballard]

Right, for some reason it goes deeper into the docs#Lean.MetavarContext.depth and tries to assign it there (is my theory)

[Jireh Loreaux]

It succeeds if you replace 𝕜 with ℝ, but not with ℂ.

[Jireh Loreaux]

Your idea about metavariable context depth seems likely because of the unassignable, but also note that this succeeds:

example : IsScalarTower 𝕜 C(𝕜, 𝕜) C(𝕜, 𝕜) := @IsScalarTower.right _ C(𝕜, 𝕜) _ _ _