problem with module

[kbuzzard]

There is a problem with module, due to the fact that a module is a module over a ring.

Here's a minimised example, due to Mario.

class ring' (α : Type*).

class module' (α : out_param $ Type*) (β : Type*) [out_param $ ring' α].

class normed_field' (α : Type*) extends ring' α.

class normed_space' (α : out_param $ Type*) (β : Type*) [out_param $ normed_field' α] extends module' α β.

instance pi.module' {I : Type*} {f : I → Type*}
 {α : out_param Type*} [out_param $ ring' α] [∀ i, module' α $ f i] : module' α (Π i : I, f i) :=
sorry

instance loop (α) [ring' α] : ring' (option α) := sorry

set_option trace.class_instances true

instance fintype.normed_space' {α} [normed_field' α]
  {ι : Type*} {E : ι → Type*} [∀i, normed_space' α (E i)] :
  normed_space' α (Πi, E i) :=
⟨_, _⟩

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_2 : @module' ?x_0 (Π (i : ι), E i) ?x_1 := @pi.module' ?x_3 ?x_4 ?x_5 ?x_6 ?x_7
[class_instances] (1) ?x_6 : out_param (ring' ?x_5) := @loop ?x_8 ?x_9
[class_instances] (2) ?x_9 : ring' ?x_8 := @loop ?x_10 ?x_11
[class_instances] (3) ?x_11 : ring' ?x_10 := @loop ?x_12 ?x_13
[class_instances] (4) ?x_13 : ring' ?x_12 := @loop ?x_14 ?x_15
...

Sebastian suggested

instance pi.module' {I : Type*} {f : I → Type*}
 {α : Type*} {r : ring' α} [∀ i, module' α (f i)] : module' α (Π i : I, f i) :=

[note {r : ring' α} ]

Some chat about this is here:

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/tc.20loop.20again

I am making this an issue despite not understanding most of the above, because I just want a place where we can collect our thoughts. I am unclear about whether anything can be done without changing core Lean. I am unclear about whether anything can be done even if we change core Lean. I am unclear about how serious the problem is. Perhaps others would like to jot down some thoughts here; currently what is happening that there is occasional zulip chat which gets lost and this issue is an attempt to have a central point where experts can explain the problem and what can and can't be done about it.

[kbuzzard]

I used module seriously for pretty much the first time yesterday. Type class inference struggled to work out the ring sometimes. But this wasn't a problem really, I just used @ and filled the rings in (even though they were obvious). Somehow the problem seemed to be that there were so many {}s that the ring seemed to have no chance of being inferred :-/ The problems must be deeper than that...

Question: is the problem nothing more than "there is some technical issue which means type class inference doesn't always work; however we can just solve this easily in practice by using @ a lot?"

Aah -- presumably the question is "type class inference doesn't work with modules sometimes, because we have to guess the ring. There is an easy workaround for this. But how do we get it to work". Am I finally there?

[kbuzzard]

Here is an example of something that I was struggling with:

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/semimodules.20nein.20danke/near/133939719

I believe that Mario's module refactoring will completely change the behaviour of that sort of thing. What is going on here is that I want polynomial R to be both a module over R and a module over polynomial R, and currently type class inference does not like this.

[jcommelin]

I think this can now be closed. Do you agree @kbuzzard ?

[kbuzzard]

I think we should ask @PatrickMassot .

[PatrickMassot]

I agree.