Only constants and Pi types are supported

Stream: new members

[Nicolò Cavalleri]

If I change the following instance in mathlib

instance continuous_map_semimodule {α : Type*} [topological_space α]
{R : Type*} [semiring R] [topological_space R]
{M : Type*} [topological_space M] [add_comm_group M] [topological_add_group M]
[semimodule R M] [topological_semimodule R M] :
  semimodule R C(α, M) :=
  semimodule.of_core $
{ smul     := (•),
  smul_add := λ c f g, by ext x; exact smul_add c (f x) (g x),
  add_smul := λ c₁ c₂ f, by ext x; exact add_smul c₁ c₂ (f x),
  mul_smul := λ c₁ c₂ f, by ext x; exact mul_smul c₁ c₂ (f x),
  one_smul := λ f, by ext x; exact one_smul R (f x) }

to

instance continuous_map_semimodule {α : Type*} [topological_space α]
{R : Type*} [semiring R] [topological_space R]
{M : Type*} [topological_space M] [add_comm_monoid M] [has_continuous_add M]
[semimodule R M] [topological_semimodule R M] :
  semimodule R C(α, M) :=
  semimodule.of_core $
{ smul     := (•),
  smul_add := λ c f g, by ext x; exact smul_add c (f x) (g x),
  add_smul := λ c₁ c₂ f, by ext x; exact add_smul c₁ c₂ (f x),
  mul_smul := λ c₁ c₂ f, by ext x; exact mul_smul c₁ c₂ (f x),
  one_smul := λ f, by ext x; exact one_smul R (f x) }

(which I was planning to do before the PR but I forgot) I get

/-
only constants and Pi types are supported: ?m_1
state:
α : Type ?,
_inst_1 : topological_space α,
R : Type ?,
_inst_2 : semiring R,
_inst_3 : topological_space R,
M : Type ?,
_inst_4 : topological_space M,
_inst_5 : add_comm_monoid M,
_inst_6 : has_continuous_add M,
_inst_7 : semimodule R M,
_inst_8 : topological_semimodule R M,
c : ?m_1,
f g : ?m_2
⊢ c • (f + g) = c • f + c • g
-/

What is going wrong?

[Sebastien Gouezel]

semimodule.of_core requires an add_comm_group M, but you have an add_comm_monoid. It means you should not use semimodule.of_core here, but give a direct proof for all the fields.

[Nicolò Cavalleri]

Oh again weird error message

[Nicolò Cavalleri]

Moreover when I did PR that I copied the proof of the subtype. Weird that it was not already in greatest generality

[Sebastien Gouezel]

Yes, we are improving things slowly by pushing things to the right generality when someone notices that things are not as general as they could be, just like you just did!

[Sebastien Gouezel]

And yes, the error messages are often pretty bad!