From a user's perspective, I think pyright's behaviour on the first one (keep around both types, use the broader type for future assignments) is the friendliest.

In general, I think it's surprising when x: T = ... differs from x: T; x = ...

I think the Any examples should be consistent in this respect, and beyond that it matters less. I don't think narrowing is bad (assuming all future assignments are allowed), since you can always cast your value to Any (arguably the clearest way of making a type disappear for a value).