[zozbot234]

Something that's checked dynamically is not a "typing judgment", by definition. It's a proposition established at runtime, possibly even with non-trivial data attached describing "how" the dynamic check succeeds, and possibly affecting program operation in its own right as that proposition object gets "passed" to downstream functions that depend on that dynamic check. These are two altogether different things.

[dllthomas]

Sure. Tip: if something's true by definition, it's usually not interesting. Substitute the appropriate phrase - "observation of a property which, in the static context, might constitute a typing judgement"? Note that we're here specifically considering things that can be typed statically, as outside of that setting there is no question of whether static and dynamic are opposed.

The rest of your comment seems concerned with the fact that the tagging infrastructure typically needed to check these properties at runtime can also be used for other purposes. That's true, but I don't see the relevance.

[dllthomas]

That probably reads a little snarkier than appropriate. My apologies for the tone.