Both in school and out, I have only ever encountered dynamic scoping paired with dynamic typing. Is there any published work (even if just academic, not yet implemented in a "real" programming language) on doing static type verification with dynamic scoping?
It seems to me that it should be possible if the type checker can build a static call graph for the program, and then check that all accessed variables are defined somehow in all possible traversals, and unify types between different traversals that lead to the same access point. While doable, though, that's potentially a very expensive operation, so I'd be interested to see if there is any way to significantly optimize it.
For reference, Scala seems like a decent proof-of-concept for some first steps towards such a dynamically-scoped type system with its concept of "implicit arguments"; it just requires that all usable edges in the dynamic call graph through which dynamically-scoped values can pass be manually type-annotated by the programmer, rather than assuming that all edges in the call graph are usable and having the compiler figure out the types automatically.