Static type analysis with dynamic scoping? 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.
There is a paper titled Implicit Parameters: Dynamic Scoping with Static Types that discusses just such a system.

The implement a slightly different system from Scala under the name "implicit parameters". By having compiler automatically generate implicit parameters in any function that calls other functions with implicit parameters the problem becomes nearly identical to standard type inference. Additionally, since these implicit parameters are still part of each functions type signature they propose a syntax for declaring most of a functions signature, while still allowing the compiler to determine the types of any implicit parameters.