I mean we're talking about definitions here so ultimately there isn't a definitive answer, but I think your definition of dependent types excludes a lot of thin

I mean we're talking about definitions here so ultimately there isn't a definitive answer, but I think your definition of dependent types excludes a lot of things that are commonly referred to as "some dependent typing" or "lightweight dependent types" (this includes things like GADTs and singletons, Liquid Haskell, etc.). It's important to note that what is going on in that TS example isn't just flow typing (otherwise something like Kotlin would count as a dependently typed language). The `typeof` operator is playing a crucial role here. That's what makes this really a case of a type depending on a runtime value. If it was really just flow typing, then you could still replicate it in something like Scala by just introducing additional layers of types and folding over them (this is also why I would agree flow typing by itself is not dependent types). But that's insufficient to replicate the full TS example. Idris doesn't want to make its soundness situation any worse than it already it is because the community does eventually want it to be completely sound. But like I said, that's not at the top of its priority list. EDIT: Removed "Flow-sensitive typing isn't really all that different from dependent pattern matching (the main difference is on the other side of the coin, where you need some way of generating those dependent patterns and of cascading the flow "down" so to speak, so indeed by itself flow-sensitive typing isn't dependent typing). " as the first line because it didn't seem all that relevant in retrospect.