A role stays default even if it's revoked from the user or even dropped

Currently if a role is set as default for a user, and then revoked or dropped, the default setting is preserved; and if the role is later re-created and/or re-granted, it immediately becomes default again. I assume it's because the value is kept in mysql.user.

It's a bit counter-intuitive, not how things are usually done in MySQL when stuff gets dropped. However, it's nor really critical, so if it works so "by design", I don't insist on changing it, please just document it explicitly in the KB.