Hmm, perhaps, I’ll keep succinct for this:
Not at all, that is enforced via standard HM typing, pretty trivial. The harder parts are things like enforcing not performing improper math on the values, like taking $2.53 and dividing it by 2, it is super easy to forget things like the half cents in each and that you actually need to pick a place (still can be done via HM though enforcing usage is not), and things like the move semantics (which is part of the refined typing since it linearizes the usage of a type) so you can’t do something like accidentally add a payment twice or deduct $50 from a $60 account twice in two different threads (since you can’t forget a synchronization primitive for example on your type access).
Idris on the other hand goes far far beyond. Dependently typed type systems not only hold type information (HM typing), and linearized types and all that, but far far more, including even having knowledge about the values that will be held at runtime. The prime simple example of a dependently typed language is a language that can take something like a list that you can pass into, say, a head/1 function, and it will fail to compile unless you verify that it is not empty, and that check is not a check built in to the language, those are checks you can ‘build’ on any type. In essence it lets you program in the type system, thus making check and bounds that are impossible otherwise. Why something like Idris and Coq are so useful for monetary systems is that they can absolutely prove the flow of a value through a system, ensure it is only accessed properly, that nothing is forgotten about, and I’m still only scratching what a full dependently typed language can do.
Now because the types are so powerful in dependently typed languages the programs also tend to be a good bit bigger, with type signatures that are…impressively large to put it mildly, but once it compiles you can be sure that not only your types are correct in their usage but you also aren’t breaking any potential runtime logical contracts either.
You have this ability now, but will that remain in the future? What if Scala finishes dying off (it almost has really…) and they start writing interface code in Java or Kotlin then? A small team of competent people ‘now’ does not equate the same to the maintainers in the future, and over a multi-decade timescale spoken of prior, then I’d still vote on grabbing a pre-made, very well tested and used prior-existing product instead. 
(I do like Scala, much more so than Java or Kotlin, it just doesn’t have much backing anymore…)
