Encourage unticked promoted constructors

At the moment, GHC encourages the use of ticks to mark promoted data constructors when using DataKinds. In particular:

The -Wunticked-promoted-constructors warning, included in -Wall, complains about the absence of ticks.
When pretty-printing promoted data constructors, GHC shows a tick even if it is not needed for disambiguation.
The user's guide encourages the use of ticks:

As a convenience, GHC allows you to omit the quote mark when the name is unambiguous. However, our experience has shown that the quote mark helps to make code more readable and less error-prone.

However, it is far from clear that using ticks by default is a good idea:

They introduce additional syntactic clutter.
Some library authors wish to use DataKinds without their users needing to understand datatype promotion, and without the aesthetic impact of ticks, and hence would rather ticks were not mandated (e.g. the optics library avoids DataKinds for this reason).
They do not help explain what is going wrong when a promotion-related error occurs, because the warning is not displayed.
They are an obstacle in the way of bringing the type and term levels closer together, as part of the long term plan for DependentHaskell.

I propose that instead:

-Wunticked-promoted-constructors should be removed from -Wall (but remain supported and part of -Weverything).
When pretty-printing promoted data constructors, GHC should insert a tick only if doing so is necessary to disambiguate (i.e. there is a type with the same name in scope).
The user's guide should be modified to explain ticks as an option for disambiguation, rather than a preferred default.