Predicate modal logic has been controversial at least since the criticisms of Quine. While predicate modal logic is now accepted, questions remain about its formulation, which has been hampered by several myths. Among these are:
In the context of a modal operator, substitution of equals for equals fails.
In the context of a modal operator, ordinary quantifier rules such as existential generalization fail.
De re is the result of a modal operator occurring inside the scope of a quantifier or lambda.
Applying lessons from modal type theory (Bierman and de Paiva 2000, Pfenning and Davies 2001, etc.), I argue for a countervailing principle: A. In the context of a modal operator, all free variables will receive de re interpretation, and should be marked as such. Where this is implemented (e.g. Zwanziger 2017), the rules for equality and quantifiers finally become unproblematic (as demanded by Quine), and de re is more evidently decoupled from scope-taking operators. Further refinements are needed, but should avoid Myths 1-3 by adhering to Principle A, roughly speaking.