Yeah, It's not that I don't see the advantages. I wish that there was a way to get our cake and eat it too. Maybe we can dependently typed eat our way through

Yeah, It's not that I don't see the advantages. I wish that there was a way to get our cake and eat it too. Maybe we can dependently typed eat our way through to the other end, where while we do have monomorphization errors, having constraints on generic types feel natural and ergonomic, much more like in a system like Lean. I think what it boils down to at the end is where you want your pain to be, pains from constantly hitting limitations and providing an escape hatch like macros, or pains from having a system that is too powerful and all the chaos that brings. I'd rather reign in the chaos, after all we also choose to be Turing-complete, and not always terminating like Coq, but mmv.