mystic linter message

Stream: general

[Kenny Lau]

import algebra.group_ring_action

universes u v w u₁

variables (M : Type u) [monoid M]
variables (X : Type v) [mul_action M X]
variables (Y : Type w) [mul_action M Y]
variables (A : Type v) [add_monoid A] [distrib_mul_action M A]
variables (B : Type w) [add_monoid B] [distrib_mul_action M B]

set_option default_priority 100 -- see Note [default priority]
set_option old_structure_cmd true

/-- Equivariant functions. -/
@[nolint has_inhabited_instance]
structure mul_action_hom :=
(to_fun : X → Y)
(map_smul' : ∀ (m : M) (x : X), to_fun (m • x) = m • to_fun x)

notation β ` →[`:25 α:25 `] `:0 γ:0 := mul_action_hom α β γ

namespace mul_action_hom

instance : has_coe_to_fun (X →[M] Y) :=
⟨_, λ c, c.to_fun⟩

end mul_action_hom

/-- Equivariant additive monoid homomorphisms. -/
@[nolint has_inhabited_instance]
structure distrib_mul_action_hom extends A →[M] B, A →+ B.

/-- Reinterpret an equivariant additive monoid homomorphism as an additive monoid homomorphism. -/
add_decl_doc distrib_mul_action_hom.to_add_monoid_hom

/-- Reinterpret an equivariant additive monoid homomorphism as an equivariant function. -/
add_decl_doc distrib_mul_action_hom.to_mul_action_hom

notation β ` →+[`:25 α:25 `] `:0 γ:0 := distrib_mul_action_hom α β γ

namespace distrib_mul_action_hom

instance has_coe : has_coe (A →+[M] B) (A →+ B) :=
⟨to_add_monoid_hom⟩

instance : has_coe_to_fun (A →+[M] B) :=
⟨_, λ c, c.to_fun⟩

end distrib_mul_action_hom

#lint

[Kenny Lau]

/- INVALID/MISSING `has_coe_to_fun` instances.
You should add a `has_coe_to_fun` instance for the following types.
See Note function coercions].: -/
#print distrib_mul_action_hom /- `has_coe_to_fun` instance is definitionally equal to a transitive instance composed of:
  @add_monoid_hom.has_coe_to_fun.{v w} A B _inst_4 _inst_6
and
  @coe_base_aux.{(max (v+1) (w+1)) (max (v+1) (w+1))}
    (@distrib_mul_action_hom.{u v w} M _inst_1 A _inst_4 _inst_5 B _inst_6 _inst_7)
    (@add_monoid_hom.{v w} A B _inst_4 _inst_6)
    (@distrib_mul_action_hom.has_coe.{u v w} M _inst_1 A _inst_4 _inst_5 B _inst_6 _inst_7) -/

[Kenny Lau]

what does this linter message mean?

[Kenny Lau]

I already have a has_coe_to_fun instance for that type

[Kenny Lau]

also there is no Note [function coercions]

[Kenny Lau]

or at least I cannot find it

[Gabriel Ebner]

I think you should remove the set option default priority.

[Kenny Lau]

ok, but the mystic message is still here

[Gabriel Ebner]

@Kenny Lau Removing the set_option fixes the linting error for me. And the library note is a typo, it's called "function coercion" (singular).

[Kenny Lau]

import algebra.group_ring_action

universes u v w u₁

variables (M : Type u) [monoid M]
variables (X : Type v) [mul_action M X]
variables (Y : Type w) [mul_action M Y]
variables (A : Type v) [add_monoid A] [distrib_mul_action M A]
variables (B : Type w) [add_monoid B] [distrib_mul_action M B]

-- set_option default_priority 100 -- see Note [default priority]
set_option old_structure_cmd true

/-- Equivariant functions. -/
@[nolint has_inhabited_instance]
structure mul_action_hom :=
(to_fun : X → Y)
(map_smul' : ∀ (m : M) (x : X), to_fun (m • x) = m • to_fun x)

notation β ` →[`:25 α:25 `] `:0 γ:0 := mul_action_hom α β γ

namespace mul_action_hom

instance : has_coe_to_fun (X →[M] Y) :=
⟨_, λ c, c.to_fun⟩

end mul_action_hom

/-- Equivariant additive monoid homomorphisms. -/
@[nolint has_inhabited_instance]
structure distrib_mul_action_hom extends A →[M] B, A →+ B.

/-- Reinterpret an equivariant additive monoid homomorphism as an additive monoid homomorphism. -/
add_decl_doc distrib_mul_action_hom.to_add_monoid_hom

/-- Reinterpret an equivariant additive monoid homomorphism as an equivariant function. -/
add_decl_doc distrib_mul_action_hom.to_mul_action_hom

notation β ` →+[`:25 α:25 `] `:0 γ:0 := distrib_mul_action_hom α β γ

namespace distrib_mul_action_hom

instance has_coe : has_coe (A →+[M] B) (A →+ B) :=
⟨to_add_monoid_hom⟩

/- instance : has_coe_to_fun (A →+[M] B) :=
⟨_, λ c, c.to_fun⟩ -/

end distrib_mul_action_hom

#lint

[Kenny Lau]

@Gabriel Ebner this still has the linting error

[Gabriel Ebner]

Ugh, you commented out too much. You need to put the has_coe_to_fun instance back in.

[Kenny Lau]

oh ok that works

[Kenny Lau]

but why?