`calc` for isomorphisms involving typeclasses

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

I can't work out how to use calc for calculations involving isomorphisms between objects which have typeclasses attached to them.

Steps to Reproduce

structure MulEquiv (M N : Type _) [Mul M] [Mul N] where -- group isomorphism

infixl:25 " ≃* " => MulEquiv

def MulEquiv.trans [Mul A] [Mul B] [Mul C] (hAB : A ≃* B) (hBC : B ≃* C) : A ≃* C := sorry

instance : Trans (@MulEquiv A B) (@MulEquiv B C) (@MulEquiv A C) where
  trans := MulEquiv.trans

example (A B C : Type) [Mul A] [Mul B] [Mul C] (hAB : A ≃* B) (hBC : B ≃* C) : A ≃* C := by calc
  A ≃* B := hAB
  _ ≃* C := hBC

/-
scratch4.lean:12:2
invalid 'calc' step, left-hand-side is
  Type : Type 1
previous right-hand-side is
  inst✝¹ : Mul B

scratch4.lean:10:92
application type mismatch
  MulEquiv ?m.8550
argument
  ?m.8550
has type
  Mul B : Type
but is expected to have type
  Type ?u.8548 : Type (?u.8548 + 1)
-/

Versions

Lean (version 4.0.0-nightly-2023-03-31, commit 742d053a97bd, Release)

Additional Information

The issue is that Lean wants Trans, which powers calc behind the scenes, wants to eat two types and return a type (in this case the type of group isomorphisms between the two types) but I can't figure out where to insert the group structure. Of course this can be worked around by just applying MulEquiv.trans directly so this is not blocking anything important, I just thought it was worth observing this potential limitation of calc (there is currently a push to introduce more calc blocks into mathlib and this came up there).

Start with the reproducible example in scratch4.lean and trace how calc elaborates its Trans instance for MulEquiv.trans. Read the reported invalid calc step and application type mismatch alongside the Trans declaration. Done means the shown calc expression typechecks while preserving the typeclass parameters for A, B, and C.