I used to really hype over MLsub but eventually moved on to hype over type theory and category theory. The MLsub inference algorithm was indeed quite complex. I guess I’ll take a look at this and review the paper in my blog.
MLsub is still interesting but for a different reason though. When I’m coding Idris or Haskell, awful often it seems like everything should be a typeclass. This is also presenting up in category theory. Adjoint functors seem to form “arguments” that introduce evaluation rules as well, resembling typeclasses. MLsub constraints resemble typeclasses.