I agree that the implementation is quite obvious. It's the inference—the collusion between the HM type constraints and the Prolog-like typeclass constraints—that's magical.