Clueless suggestion: What about the programmer (who implements the semigroup) also providing a proof (that can be automatically checked) that it satisfies associativity? Is that method perhaps already covered by one of the examples you mentioned?
That is the dependent typed aspect mentioned. This is actually done in Idris with VerifiedSemigroup and other verified instances.
OK. I'm afraid I don't know enough to make the connection. Actually, I never understood the point of dependent types. They seem to do away with the neat order that types introduce. ¯\_(ツ)_/¯