Comment by antonvs

There's a reason I mentioned Haskell and Rust specifically. You're right, OCaml's type system is simpler in some relevant respects, and may avoid the issues that I was alluding to. I haven't worked with OCaml for a number of years, since before the LLM boom.

The presence of type classes in Haskell and traits in Rust, and of course the memory lifetime types in Rust, are a big part of the complexity I mentioned.

(Edit: I like type classes and traits. They're a big reason I eventually settled on Haskell over OCaml, and one of the reasons I like Rust. I'm also not such a fan of the "O" in OCaml.)

> All possible runs of a program is exactly what HM type systems type check for.

Yes, my point was this can be a more difficult goal to achieve.

> This fed into the coding model automatically iterates until it finds a solution that doesn't violate any possible run of the program.

Only if the model is able to make progress effectively. I have some amusing transcripts of the opposite situation.