Preventing $-renaming of pattern names in lexically-scoped constructs

Question

When you use a lexically-scoped construct like With or Function to perform replacements in an expression, Mathematica might rename pattern names in that expression. It does so if the patterns appear on the lhs of a lexical scoping construct (such as Rule) whose rhs is altered by performing the replacement.

For example, we have

With[{s = c}, {t_ -> s, t_ -> 1}]

(* Out: {t$_ -> c, t_ -> 1} *)

Mathematica does this (I'm guessing) to prevent binding conflicts; if t_ lexically scopes the rhs of -> in t_ -> s, then we don't want to accidentally bind any t's that might occur in c once we substitute it in. For example, if we instead had s = f[t], we might accidentally create t_ -> f[t].

How do I prevent this? Since I'm trying to extract and manipulate pattern names from expressions, this is a bit of an issue for me! So far I've found two possibilities, but I don't know if I can trust them or why.

I'd be any sort of lexical replacement mechanism; but it would be cool to see a general-purpose way to prevent things from being renamed! :)

Work so far

1. The first possibility comes from noticing that Function only seems to rename variables when using a symbol as a formal parameter, and that e.g.

(t_ -> # &)[c]

(* Out: t_ -> c *)

might not ever rename anything. However, this makes replacements which require formal parameters (e.g. when having functions within functions and no other way to eliminate the ambiguity between which argument belongs to which function) difficult. So, I'd say this is only a partial solution without some other technique.

2. The second possibility comes from the sense that maybe we can "freeze" the expressions on the lhs's and prevent them from being touched by the renaming mechanism. Unfortunately, Hold (and all its evaluation-controlling variations, like Unevaluated and Inactivate) don't get in the way. However, Verbatim seems to, at least when surrounding (only) the scoping pattern:

With[{s = c}, {Verbatim[t_] -> s, Verbatim[t_ -> s]}]

(* Out: {Verbatim[t_] -> c, Verbatim[t$_ -> c]} *)

Is this robust? I couldn't see anything in the docs about it (but I could have missed it). This seems to work, but I have no guarantee that it does. So, that would also be useful as an answer, even if not the "holy grail" of turning off/reverting all $-renaming. :)

Further Background

In With[{s = c}, {t_ -> s, t_ -> 1}], since the rhs of t_ -> 1 is not touched by the replacement, there's no need to rename patterns on its lhs. In general, though, any touching of the rhs causes all variables that scope it on the lhs to be renamed:

With[{s = 1}, {a_, b_} -> s]

(* {a$_, b$_} -> 1 *)

At the top I said MMA renames "patterns which appear on the lhs of a lexical scoping construct...", but to be more precise I should have said something like "which are bound by a lexical scoping construct...", as being on the "lhs" is not always the criterion for being bound (and thus having a scope).

So, replacement happens provided the pattern names on the lhs actually do scope the part of the expression the replacement touched! If the scope of a given pattern name does not actually include the replacement, e.g. if the lhs is bound by some outer Rule instead, it is not renamed. Compare the two elements of the list output below:

With[{s = 1}, {(t_ -> s) -> 2, (t_ -> 2) -> s}]

(* Out: {(t_ -> 1) -> 2, (t$_ -> 2) -> 1} *)

The scope of t_ in (t_ -> s) -> 2 is 2, not s, as the outer -> binds it first (as far as I can tell).

There's also a discussion of this at this question, but it doesn't answer the question here. It's also discussed in the docs here.

Aside

If you try to "anticipate" the renaming by using e.g. t$ in your replacement expression, you can get away with inducing a binding:

With[{s = f[t$]}, t_ :> s]

(* Out: t$_ :> f[t$] *)

w /. With[{s = f[t$]}, t_ :> s]

(* Out: f[w] *)

This seems like an oversight—or maybe it's in the name of efficiency, and we just trust no one would ever feel ok ending a variable with $ in the first place?

If you're not careful, even two expressions where everything's the same, but you chose to write in the With constant explicitly, can wind up different:

3 /. {With[{d = 1}, With[{s = (e[t_] :> d)}, {t_ :> s}]], 
      With[{d = 1}, With[{s = (e[t_] :> 1)}, {t_ :> s}]]}

(* Out: {e[Pattern[3, _]] :> 1, e[t_] :> 1} *)

Mathematica warns you something's weird with RuleDelayed::rhs, but still. Can anyone find any other exploits?