vector bundles -- typeclass inference issue

Stream: maths

[Heather Macbeth]

Here is a toy example for an issue I am hitting while constructing the vector bundle of continuous linear maps, cc @Sebastien Gouezel @Patrick Massot

import topology.vector_bundle.basic
import analysis.normed_space.basic

variables {B : Type*} {R : Type*} (F₁ : Type*) (F₂ : Type*)
  (E₁ : B → Type*) [Π x, add_comm_monoid (E₁ x)]
  (E₂ : B → Type*) [Π x, add_comm_monoid (E₂ x)]

section defs
variables [comm_semiring R] (σ : R →+* R) [Π x, module R (E₁ x)] [Π x, module R (E₂ x)]
include F₁ F₂

def fibrewise_clm (x : B) := E₁ x →ₛₗ[σ] E₂ x

instance : Π x, add_comm_monoid (fibrewise_clm F₁ F₂ E₁ E₂ σ x) := λ x, linear_map.add_comm_monoid

example : Π x, add_comm_monoid (fibrewise_clm F₁ F₂ E₁ E₂ σ x) := by apply_instance -- works

end defs

variables [normed_field R] (σ : R →+* R) [Π x, module R (E₁ x)] [Π x, module R (E₂ x)]

example : Π x, add_comm_monoid (fibrewise_clm F₁ F₂ E₁ E₂ σ x) := by apply_instance --fails

[Heather Macbeth]

I think this is the fairly-common issue of typeclass inference with pi-types? An instance Π x, add_comm_monoid (fibrewise_clm F₁ F₂ E₁ E₂ σ x) can't be picked up if some kind of typeclass inference (here from normed_field to comm_semiring) is needed separately on each fibre.

[Heather Macbeth]

I have work-in-progress for one workaround at branch#vb-hom-2 : to defer for as long as possible working over a normed_field, which here requires assuming the additional data of a topology on F₁ →SL[σ] F₂ (which will presumably require a bunch of Prop hypotheses to complete the construction). This seems more elegant, but it's possible that it's kicking the can down the road (eventually the construction will need to be applied over a normed field).

[Heather Macbeth]

And here is a second workaround, at branch#vb-hom, where I require for the type synonym that the rings already be normed fields. Less elegant in my opinion, but perhaps less likely to fail down the road?

[Patrick Massot]

This is pretty frustrating because the correct instance is the third thing it tries. If you name that instance good (the only instance in Heather's code) then the failing search trace first tries two instances from the local contact and then:

@good (?x_3 x) (?x_4 x) (?x_5 x) (?x_6 x) (?x_7 x) (?x_8 x) (?x_9 x) (?x_10 x) (?x_11 x) (?x_12 x) (?x_13 x) (?x_14 x)
  (?x_15 x)
failed is_def_eq

[Patrick Massot]

Whereas replacing by apply_instance with @good _ _ _ _ _ _ _ _ _ _ _ _ works

[Heather Macbeth]

I heard a rumour that these typeclass-inference-with-pi-types issues are fixed in Lean 4?

[Patrick Massot]

For the record, the solution to this search is:

@good B R F₁ F₂ E₁ (λ (x : B), _inst_1 x) E₂ (λ (x : B), _inst_2 x)
    (@comm_ring.to_comm_semiring R
       (@semi_normed_comm_ring.to_comm_ring R
          (@normed_comm_ring.to_semi_normed_comm_ring R (@normed_field.to_normed_comm_ring R _inst_3))))
    σ
    (λ (x : B), _inst_4 x)
    (λ (x : B), _inst_5 x)

[Patrick Massot]

Note that @good _ _ _ _ _ (by apply_instance) _ (by apply_instance) _ _ _ _ also fails.

[Heather Macbeth]

Here's an earlier commit of one of those branches, in which I "do typeclass inference by hand" over and over again ...
https://github.com/leanprover-community/mathlib/blob/a20b9ddaf58eb95e1fd06b59028f53d4def16206/src/topology/vector_bundle/hom.lean

[Patrick Massot]

and it fails with saying tactic.mk_instance failed to generate instance for Π (x : ?m_1), add_comm_monoid (?m_2 x) where E₁ (or E₂) is not guessed

[Patrick Massot]

The workaround at branch#vb-hom seems good to me.

[Patrick Massot]

Hopefully we won't need topological module bundle over non field rings before Lean 4 fixes this type class issue.

[Heather Macbeth]

I like the other one (at branch#vb-hom-2) better in principle, but do you think it's likely that it will cause pain later when one tries to apply it to normed fields?

[Sebastien Gouezel]

It would be good to have a real fix for this issue, which has been biting us again and again and again, but I understand perfectly that this is low priority in Lean 3 -- it is not completely clear to me if this is really fixed in Lean 4, but to check this we need to get a working mathlib there first!

[Patrick Massot]

Hopefully we can build a toy example which is completely independent of mathlib

[Sebastien Gouezel]

Is it enough to fix your issues to register another instance assuming the stronger assumption on R?

[Sebastien Gouezel]

I have tried several times to build a toy example, but I have always failed :-(

[Heather Macbeth]

Maybe we can at least make a collection of examples. Here's one from last week:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Completeness.20of.20direct.20sums.20of.20Hilbert.20spaces.3F

[Patrick Massot]

I tried to minimize but failed. The following code mimics the type class setup in what feels to be a very faithful way, but the mock up version works perfectly.

import topology.vector_bundle
import analysis.normed_space.basic

section
variables {B : Type*} {R : Type*} (F₁ : Type*) (F₂ : Type*)
  (E₁ : B → Type*) [Π x, add_comm_monoid (E₁ x)]
  (E₂ : B → Type*) [Π x, add_comm_monoid (E₂ x)]

section defs
variables [comm_semiring R] (σ : R →+* R) [Π x, module R (E₁ x)] [Π x, module R (E₂ x)]
include F₁ F₂

def fibrewise_clm (x : B) := E₁ x →ₛₗ[σ] E₂ x

instance good : Π x, add_comm_monoid (fibrewise_clm F₁ F₂ E₁ E₂ σ x) := λ x, linear_map.add_comm_monoid

example : Π x, add_comm_monoid (fibrewise_clm F₁ F₂ E₁ E₂ σ x) := by apply_instance -- works

end defs

variables [normed_field R] (σ : R →+* R) [Π x, module R (E₁ x)] [Π x, module R (E₂ x)]

def bar : Π x, add_comm_monoid (fibrewise_clm F₁ F₂ E₁ E₂ σ x) :=
sorry -- by apply_instance -- fails

end

class monoide (M : Type*) :=
(add : M → M → M)

class anneau (R : Type*) :=
(mul : R → R → R)

structure mph (R : Type*) [anneau R] (R' : Type*) [anneau R'] :=
(map : R → R)

class corps (R : Type*) extends anneau R :=
(inv : R → R)

class modul (R : Type*) [anneau R] (M : Type*) [monoide M] :=
(smul : R → M → M)

section
variables {B : Type*} {R : Type*}  (F₁ : Type*) (F₂ : Type*)
(E₁ : B → Type*) [Π x, monoide (E₁ x)] (E₂ : B → Type*) [Π x, monoide (E₂ x)]
[anneau R] (σ : mph R R) [Π x, modul R (E₁ x)] [Π x, modul R (E₂ x)]

include F₁ F₂ σ

def foo (x : B) := E₁ x → E₂ x

instance baz  : Π x : B, monoide (foo F₁ F₂ E₁ E₂ σ x) :=
sorry

/-
fibrewise_clm :
  Π {B : Type u_5} {R : Type u_6},
    Type u_7 →
    Type u_8 →
    Π (E₁ : B → Type u_9) [_inst_1 : Π (x : B), add_comm_monoid (E₁ x)] (E₂ : B → Type u_10)
    [_inst_2 : Π (x : B), add_comm_monoid (E₂ x)] [_inst_3 : comm_semiring R],
      (R →+* R) →
      Π [_inst_4 : Π (x : B), module R (E₁ x)] [_inst_5 : Π (x : B), module R (E₂ x)], B → Type (max u_9 u_10)
-/

/-
foo :
  Π {B : Type u_7} {R : Type u_8},
    Type u_9 →
    Type u_10 →
    Π (E₁ : B → Type u_11) [_inst_1 : Π (x : B), monoide (E₁ x)] (E₂ : B → Type u_12)
    [_inst_2 : Π (x : B), monoide (E₂ x)] [_inst_3 : anneau R],
      mph R R →
      Π [_inst_4 : Π (x : B), modul R (E₁ x)] [_inst_5 : Π (x : B), modul R (E₂ x)], B → Type (max u_11 u_12)
-/

/-
good :
  Π {B : Type u_7} {R : Type u_8} (F₁ : Type u_9) (F₂ : Type u_10) (E₁ : B → Type u_11)
  [_inst_1 : Π (x : B), add_comm_monoid (E₁ x)] (E₂ : B → Type u_12)
  [_inst_2 : Π (x : B), add_comm_monoid (E₂ x)] [_inst_3 : comm_semiring R] (σ : R →+* R)
  [_inst_4 : Π (x : B), module R (E₁ x)] [_inst_5 : Π (x : B), module R (E₂ x)] (x : B),
    add_comm_monoid (fibrewise_clm F₁ F₂ E₁ E₂ σ x)
-/

/-
baz :
  Π {B : Type u_7} {R : Type u_8} (F₁ : Type u_9) (F₂ : Type u_10) (E₁ : B → Type u_11)
  [_inst_1 : Π (x : B), monoide (E₁ x)] (E₂ : B → Type u_12) [_inst_2 : Π (x : B), monoide (E₂ x)]
  [_inst_3 : anneau R] (σ : mph R R) [_inst_4 : Π (x : B), modul R (E₁ x)] [_inst_5 : Π (x : B), modul R (E₂ x)]
  (x : B), monoide (foo F₁ F₂ E₁ E₂ σ x)
-/


example [Π x, modul R (E₁ x)] [Π x, modul R (E₂ x)] : Π x : B, monoide (foo F₁ F₂ E₁ E₂ σ x) :=
by apply_instance

end

variables (K : Type*) [corps K] {B : Type*} (σ : mph K K) (F₁ F₂ : Type*)
(E₁ : B → Type*) [Π x, monoide (E₁ x)] (E₂ : B → Type*) [Π x, monoide (E₂ x)]

example [Π x, modul K (E₁ x)] [Π x, modul K (E₂ x)] : Π x : B, monoide (foo F₁ F₂ E₁ E₂ σ x) :=
by apply_instance

[Patrick Massot]

Maybe @Gabriel Ebner will pity us and explain what's going on.

[Kevin Buzzard]

I ported a huge amount of the bottom of the algebra heirarchy to mathlib4 last year precisely to see if a certain Lean 3 issue was fixed in Lean 4 (it was), and also because I thought it would be a neat way to learn some Lean 4. Maybe someone wants to try the same thing here?

[Gabriel Ebner]

My general impression is that this class of bugs requires a couple of ingredients (did not check if this is indeed the case here as well):

1. Quantified instances
2. Type classes with type class parameters (in this case the add_comm_monoid parameter of module).
3. "Non-obviously" commuting diamonds, i.e. the instance normed_field→add_comm_monoid looks different than the comm_semiring→add_comm_monoid instance.

[Gabriel Ebner]

Particularly 3) I think means that this kind of bug is very sensitive as to whether old_structure_cmd is used or not, how the instances are constructed syntactically (i.e. comm_semiring.to_add_comm_monoid might work while { .. ‹normed_field A› } could fail spectacularly).

[Gabriel Ebner]

Lean 4 changes some of these ingredients, but it's not clear to me how much of the issue that fixes.

[Gabriel Ebner]

For example, the structure encoding is different, a mix between old_structure_cmd and "new_structure_cmd". But for the algebraic hierarchy the mix looks very much like old_structure_cmd.

[Gabriel Ebner]

Another difference is the order type-class parameters are searched for. Lean 3 used to be left-to-right. Then Lean 4 switched to right-to-left. We then backported right-to-left to Lean 3. Lean 4 then switched back. (In other words, nobody knows what they're doing.)

The left-to-right order has some advantages though with these kinds of type classes. Look at this excerpt of a type class trace in Lean 3:

[class_instances] (5) ?x_1403 : @normed_space ℂ β complex.normed_field (@normed_group.to_semi_normed_group β ?x_1402) := ...

Note that the semi_normed_group parameter of normed_space contains a metavariable (this is because of the right-to-left order!). Such a metavariable is a huge problem during unification. If we need to unify e.g. @normed_group.to_semi_normed_group β ?x_1402 and real.normed_group, then Lean needs to find a semi_normed_group ℝ instance during unification. These nested type class problems furthermore do not have caching in Lean 3 for technical reasons.