Shouldn’t the type constraint on multiplication be existence of an operator:
(*) : ^c * ^c -> ^b ? (*) : ^c * ^c -> ^b ? ^x * ^y -> ^z
because you could technically define a static member (*) (a: int) (b: float): double = ...
and there's nothing saying that you can't. in that case: (*) : ^a * ^c -> ^b //^a = int, ^c = float, ^b = double
(*) : ^c * ^c -> ^b //^c = int, ^c = float, ^b = double.
and the second one won't work, because ^c =/= ^c