TypeScript's type system, with tagged unions, `never` type and type inference being used in an app with good Language Server support (e.g. VSCode) is probably t

TypeScript's type system, with tagged unions, `never` type and type inference being used in an app with good Language Server support (e.g. VSCode) is probably the closest I've seen to this. The biggest limitation still in place is that it can't reason very well about value ranges (e.g. numbers between 20 and 30) without you enumerating every single possibility (i.e. 20 | 21 | 22 | 23 | ... | 30) which isn't really feasible or desirable for larger ranges. We're probably very close to this level of generality, though, with the recent string template types being a major step forward in expressiveness.