Type inference doesn't somehow fail if we go beyond Haskell's type system. The inferable subset of the language remains inferable. Haskell already has inferable

Type inference doesn't somehow fail if we go beyond Haskell's type system. The inferable subset of the language remains inferable. Haskell already has inferable (Hindley-Milner) and uninferable (higher-rank polymorphism, GADTs) parts. If we go beyond Haskell's type system, it actually becomes crucial for productivity to have powerful type (and term) inference. Agda and Coq both have much more powerful inference than Haskell; it's just that don't bother with using it to realize Hindley-Milner-style annotation-free bindings, because there's little use for it in proof assistants.