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.

No you cannot

  > But it’s not a clear cut that Haskell type system offers more safety guarantees.

You can log operands in your implementation of Rust's Add trait, or compute running sum of one of the operands. In Haskell it is not possible unless you use unsafePerformIO from System.IO.Unsafe.

Haskell's type system controls effects available to the code. This can be used to implement programs adhering to specific formulas of Linear Temporal Logic or implementing a protocol specification, where operations on any given phase and side are restricted by type system.

I used Haskell's type system to prevent crossing of clock domains in the hardware description eDSL. Also, it was of great help in the CPU simulator description, fixing available commands and resources for different CPU models.

Even the logic of Rust's borrow checker was expressible in Haskell as early as February 2009 - there was HList, there was ParameterizedMonad and that's about what one needs for implementation of borrow checker.