Make `@[trans]`/`calc` work with `homeomorph` etc

Here is a minimal non-working example. See also homeomorph.trans in mathlib. It seems that calc makes very strict assumptions on the meaning of implicit arguments preceding the explicit arguments of the @[trans] lemma, and we can't satisfy these assumptions with homeomorph, local_homeomorph, monoid_hom etc, see Zulip chat.

structure inhabited_hom (α β : Type*) [inhabited α] [inhabited β] :=
(to_fun : α → β)
(map_default : to_fun (default α) = default β)

notation α `→'`:25 β := inhabited_hom α β

@[trans] def inhabited_hom.trans {α β γ : Type*} [inhabited α] [inhabited β] [inhabited γ]
  (f : α →' β) (g : β →' γ) :
  α →' γ :=
{ to_fun := λ x, g.to_fun (f.to_fun x),
  map_default := by rw [f.map_default, g.map_default] }

example {α β γ : Type*} [inhabited α] [inhabited β] [inhabited γ]
  (f : α →' β) (g : β →' γ) : α →' γ :=
calc α →' β : f
... →' γ : g

Start by reproducing the minimal inhabited_hom example and reading how calc resolves @[trans] lemmas. Compare this behavior with homeomorph.trans and the linked Zulip discussion; done means the example and analogous homomorphism cases elaborate successfully without breaking existing calc behavior.