Have you got an example of a more sane and easier to understand notation for type inference rules? I find the horizontal-bar notation quite readable.