Maybe this should be a diagnostic? But it isn't in pyright (which has the same behavior you implemented here).

It is in mypy, but for different reasons than it would be for us, since mypy just generally prohibits re-declaration.

Not sure, don't feel clear enough about it to even suggest a TODO comment. We can always add this diagnostic if we decide we need it.

The "currently" was my way to try and describe that this is probably an open design decision. It feels to me like a not very common edge case, so in spirit of "every lint rule generates maintenance work", I'll leave this as-is for now, but it should be straightforward to add a lint for this later if we want to.

nit: is it valuable to maintain an invariant that a variable named *_ty contains a Type, and a function named *_ty returns a Type? If so, should we establish a suffix like *_tyq for a "type and qualifiers"? Or is this all too pedantic and veering unnecessarily into Hungarian notation? (I don't feel strongly.)

I'm afraid I broke this invariant before, and never cleaned it up. For example, bindings_ty returns a Symbol. Most call sites that call functions returning Symbol/TypeAndQualifiers are only interested in the contained type, but it's probably still better to clean up those names. I opened #15569 as a follow-up task for me.

We're already inside a match arm for ctx being Store, why do we need to match on ctx again?

Thanks for catching that. I previously had this code block in an entirely different place (where the match on ctx was necessary) and forgot to remove it when I moved it here.

With type narrowing, clippy could have been able to catch this 😄