Are there any Forth variants that have static typing? Or more generally, are there any interesting type systems that target stack-based machines?
https://www.stephan-becher.de/strongforth/
FORTH compilation is typically minimal (bit of a defining feature really), so there is no static (i.e. compile-time) type verification or much any optimization.
O.t.o.h., the JVM is stack-based and has been used for a plethora of programming languages, many statically typed.
The JVM is stack-based and static typing rather common in the languages that runs on it.
Factor has dynamic typing, though I haven't thought much about that, it kind of stays in the background. It's more a tool for problem solving than a description of some type theory: https://factorcode.org/
Don't really see the point, though. Static on-the-nose typing tends to shine when a lot of people need to do quick edits to large amounts of code, settings where code is never done, and that's not exactly where Forth-like languages are a good fit. They're more for settings where few people think long and hard and experiment a lot until the right solution is found and then it's done, I think.
In practice I often find the shape of data to be good enough and don't feel a need to also put names to it. It might be convenient to invent a type to carry some constraint, like UserNicknameString that can only be up to 200 4 byte characters (or whatever the big emoji chars in Unicode are) and no more, but that can also be solved functionally. As far as I'm aware no one has yet created a serious ERP or social media product in a Forth-like language, so maybe the perks that come with having an ontology of ten thousand types keeping things in check are still illusory for the hardcore forthers.