I have the following situation, given two types MA and MB, I would like to be able to prove that they both not only have an Applicative but also that they both have the same underlying shape. I tried doing the following:
type UnapplyM[TC[_[_]], MA, M0[_]] = Unapply[TC, MA]{ type M[X] = M0[X] }
implicit def thing[MA, MB, M[_]](implicit un: UnapplyM[Applicative,MA,M], un2: UnapplyM[Applicative,MB,M]) = ...
but keep running into diverging implicits (i.e. this doesn't work.) Similar things can be done with a type projection on the A type param of Unapply and work.
This there a way to take these two types and be able to prove they are, in fact, supported by the same type class instance?