Using unification hints to find bundled homs

Stream: general

[Eric Wieser]

I was hoping something like this would be possible, but it seems not to work:

import algebra.group.pi
import data.finset.basic
import algebra.big_operators.basic

def monoid_hom.coe_monoid_hom (α β : Type*) [monoid α] [comm_monoid β] : (α →* β) →* (α → β) :=
{ to_fun := λ g, g,
  map_one' := rfl,
  map_mul' := λ x y, rfl, }

/-- Tell the unifier where to find a monoid_hom that matches a coercion -/
@[unify] def monoid_hom.coe_hint {M N : Type*} [monoid M] [comm_monoid N]
  (f : M →* N) (coe_fn_hom : (M →* N) →* has_coe_to_fun.F f) : unification_hint :=
{ pattern     := ⇑f ≟ coe_fn_hom f,
  constraints := [coe_fn_hom ≟ monoid_hom.coe_monoid_hom M N] }

open_locale big_operators

example  {ι M N : Type*} [comm_monoid M] [comm_monoid N] (s : finset ι) (fs : ι → M →* N) :
  ⇑(∏ i in s, fs i) = (∏ i in s, fs i) := begin
    -- convert (monoid_hom.coe_monoid_hom M N).map_prod _ _, -- works
    convert monoid_hom.map_prod _ fs _, -- leaves unsolved goals, unifier can't guess the hom
  end

My understanding was that unification hints are for telling the elaborator how to fill in metavariables automatically - but despite the goal matching pattern exactly, it doesn't appear to use my hint.

Am I missing something here?