Update STYLE, incorporating wiki; close #468

This isn't quite accurate; we use dummy typeclasses to track the use of actual axioms, because this results in fewer universes and faster code (and polymorphic axioms).