Caveat emptor, I'm not a Haskeller, just an admirer. But Haskell let's you run functions over the type system itself very elegantly, so you can have a type that is derived from a type that composes three types that are derived from several functions' declared runtime behavior. This kind of type inference can provide arbitrarily rich information about anything in the entire program, letting you encode more than just range-types etc at compile time.

This comes with some design drawbacks. I think Rust's borrow checker would be implementable but unreasonable in Haskell: Haskell already does lazy-evaluation on types to enable its arbitrary depth of type expressivity. But the borrow checker also wouldn't really make sense for Haskell because the default programming model uses a GC. I think Linear Haskell might be a kind of Rust-in-Haskell, though.

Again, caveat emptor.

I've spent long time writing Haskell and now write Rust professionally, so let me tell you something. The stuff where you really want to "program in types" lives beyond Haskell, in languages like Agda, Idris, some HoTT stuff etc. anyways.

In principle the more developed the type system is – the closer it to not distinct between types and values. Caviat is that its "type inference" gets worse.

So, in those more developed languages, you could have type-level proofs (guarantees) that your calculator produces correct results, as a proof, as theorems. That 2+3 will be 5, not as runtime test assertion, but as a theorem, that no other result is possible no matter what happens. Or that your parser will never fail on valid JSON etc. but nobody guarantees it's going to be a pleasant thing to write, maintain, and debug. And compile times will probably be terrible.