structure unification fails

Stream: general

[Yury G. Kudryashov]

Yet another unification problem. I'm trying to define subsemiring reusing submonoid. The following code fails in the definition of comap. It fails to unify different carriers coming from to_submonoid and to_add_submonoid.

import group_theory.submonoid algebra.ring

universes u v

variables {R : Type u} {S : Type v} [semiring R] [semiring S]

set_option old_structure_cmd true

structure subsemiring (R : Type u) [semiring R] extends submonoid R, add_submonoid R

namespace subsemiring

instance : has_coe (subsemiring R) (set R) := ⟨subsemiring.carrier⟩

instance : has_coe_to_sort (subsemiring R) := ⟨Type*, λ S, S.carrier⟩

instance : has_mem R (subsemiring R) := ⟨λ m S, m ∈ (S:set R)⟩

@[simp, norm_cast]
lemma mem_coe {S : subsemiring R} {m : R} : m ∈ (S : set R) ↔ m ∈ S := iff.rfl

@[simp, norm_cast]
lemma coe_coe (s : subsemiring R) : ↥(s : set R) = s := rfl

/-- The preimage of a subsemiring along a monoid homomorphism is a subsemiring. -/
def comap (f : R →+* S) (s : subsemiring S) : subsemiring R :=
{ carrier := (f ⁻¹' s),
  .. s.to_submonoid.comap ↑f, .. s.to_add_submonoid.comap ↑f }

end subsemiring

[Yury G. Kudryashov]

Ping here

[Yury G. Kudryashov]

Solved by using (f : R →* S) instead of coe f.

[Kevin Buzzard]

the randomness of Lean

[Kenny Lau]

magic doesn't work in Lean

[Chris Hughes]

It's the wrong sort of arrow right? It should be \u=

[Yury G. Kudryashov]

No, it is a conversion to monoid_hom / add_monoid_hom, so it is a correct type of arrow. I guess that Lean failed to figure out the target type of this coercion.