Many times, Decidable assumptions are added simply because they appear in the terms in a theorem statement, and doing so makes applying such a theorem easier. There's the technical annoyance that Decidable instances are equal but not necessarily defeq, so if the wrong instances are present (such as the classical ones) then you need simp-like automation to rewrite instances before unifying. Maybe this is what you're seeing?

There have also been attempts to make polynomials computable, which peppers everything with decidability, but it's not a good data type for real large-scale computations, so it's not clear what the future is there. Maybe the defeqs are worth it, I don't know.

Re constructibility, this is all at too high of a level to really know what you're talking about, or why it's beneficial to write proofs themselves in a certain way. I'm not really even sure what you mean by "constructive". To me, I see no problem with writing a recursive definition that requires a non-constructive proof of termination by well-founded recursion -- is that constructive to you?