> Then how do you explain the existence of e.g. Idris or Dotty?
Have fun convincing people to port their existing Haskell and Scala programs to Idris and Dotty, respectively. In particular, Idris is not even remotely similar to Haskell beyond the syntax - it even uses a different evaluation strategy!
> They don't feel like a workaround. They feel like a nice way of modelling my problems that has the properties that I want.
The trouble with Haskell and Scala-like higher-kinded type constructors is that they are merely parameterized by other type constructors, rather than by entire structures. (It is as if, in mathematics, all functors were functors from Set!) Haskell and Scala attempt to remedy this situation using type classes, i.e., identifying every type constructor `T` with a canonical structure whose carrier is `T`. But, what if you need to use two different algebraic structures, both having `T` as their carrier? For example, say you need to use maps whose keys are lexicographically ordered strings, as well as maps whose keys are colexicographically ordered strings. Do you create a `newtype` wrapper as in Haskell? Or do you use different implicits in different contexts, and risk conflating maps created in one context with maps created in the other?
This problem doesn't exist in ML, because functors allow you to parameterize entire structures by other entire structures, not just their carriers.
> Maybe there are other ways, but if those other ways work then why aren't we seeing them in industry?
What do I know. Ask the industry, not me.
> I use a combination of trusting the compiler's typechecking,
Trust is neither here nor there. Without concrete type safety theorems (“such and such doesn't happen in a typable program”), you don't even know what type checking is supposed to buy you.
> sticking to the scalazzi safe subset and enforcing with linters etc., manual review of recursion (limiting the cases where it occurs as far as possible) and fast and loose reasoning.
That's a perfectly fine set of software development practices, but it's not verification.
> I don't have a proof of soundness, but plenty of verification systems don't have that.
Then all you have is a fancy linter.
> More to the point, there's nothing fundamental about Scala that makes it impossible to incorporate linear algebra without array bounds checks at runtime into the language.
Um, the inability to statically verify array index manipulation using Scala's type system?
> "Without array bounds checks at runtime" is not a real requirement.
Not paying the runtime cost of superfluous runtime checks is absolutely a real requirement in my current job.
> More to the point, there's nothing fundamental about Scala that makes it impossible to incorporate linear algebra without array bounds checks at runtime into the language.
It can't be implemented as an ordinary library in the existing Scala language without relying on unsafe features (e.g., a C FFI). Doing this safely requiers bona fide dependent types - in spite of their name, so-called “path-dependent types” are just fancy first-class existentials.