First off I think you have exposed a bug here.
Second I think I can offer some insight in to why this is happening, keeping in mind my knowledge of the internals of mathematica are limited.
A statement like: f[z_] := 2 z in Full form is:
SetDelayed[f[Pattern[z, Blank[]]], 2 z]
This sets the DownValue[f] to:
{HoldPattern[f[z_]] :> 2 z}
Then later when an expression, like f[2], is later is evaluated something like following is being preformed:
f[2] /. HoldPattern[f[z_]] :> 2 z
Which would evaluate to 4. Now this is all possible because pattern matching is happening with Pattern[z, Blank[]] from the first code block. This works even if you have perviously set z to a number. In other words.
z = 5;
f[z_] := 2*z
Still produces the same downvalues for f:
{HoldPattern[f[z_]] :> 2 z}
This is possible because Pattern has the HoldFirst Attribute.
The HoldFirst Attribute is not enough protection if you evaluate this inside a Module.
Example:
SetAttributes[tmp, HoldFirst];
Module[{expr},
expr = 2 z;
tmp[expr]
]
outputs:
tmp[expr$8129]
I propose that because HoldFirst Attribute does not provide immunity to Module's variable rewrite rule that any Pattern in a Rule that contains a local variable have their Pattern variables rewritten. sym->Symbol[SymbolName[sym]~~"$"]
Module[{expr},
Hold[z_ -> (z; expr)]
]
(*Hold[z$_ -> (z$; expr$1391)]*)
z has be rewritten on both sides of the rule in a simple alpha conversion.
If the rule does not contain a local variable no rewrite happens:
Module[{expr},
Hold[z_ -> (z)]
]
(*Hold[z_ -> z]*)
Rather then searching to see if a local variable matches a rule variable the above blanket rule is applied.
So the problem is that the local expr is not evaluated before the alpha conversion takes place. Or perhaps even better would be to have expr wrapped in a lazily evaluated alpha conversion which would be required for a RuleDelayed.
This does not happen in Block because Block does not rewrite any of the local variables.
Any other ideas?
Any one see any holes in my logic?