To be frank, my initial reaction to the modifiers proposal was not dissimilar to Joachim's. But I mellowed up to the type-based approach because of things like linear types (which need to be type-level values) and matchability (which also needs to for inference). As I understand it, adding arguments to the functional arrow (and, correspondingly, to binders) was one of the prime motivations for the design of modifiers. And as long as you annotate within expression, it seems to be a pretty reasonable design. Where maybe the proposal is overly enthusiastic (and I say “maybe” quite honestly: I don't really have an opinion) is to apply type-based modifiers to whole declarations (overlappable instance, or deactivating warnings), where the benefits of types are less clear, and we run into situation like Joachim's pointing out where we want to change the behaviour of the renamer. We may very well want to treat the definition granularity and the expression granularity very differently.
In the prior art in this space, there are also Rust's attributes, which are at the definition granularity (they are essentially just strings).