I mentioned in another comment, but that worse user experience is also going to exist with Idris. It's not a theorem prover, you can just use it as one.

Idris has pi and sigma types, dependent pattern matching, view patterns, totality checking, proof search, interactive case splitting, etc, etc.

It is orders of magnitude better then Haskell where the best you can do is hacky bullshit with singletons, GADTs, and type families.