Sneak Peek: Bolt Math

It seems to me that you might be able to get the flexibility that you need and preserve type inference in the common case, if you use the operators as constrained aliases for the heterogeneous word form: class Addition a b where type Sum a b :: Type plus :: a -> b -> Sum a b -- | Constrained version of 'plus', for arithmetic convenience. (+) :: (Addition a a, Sum a a ~ a) => a -> a -> a (+) = plus