contract is way wider than simple refinement types. Refinement types are just a very specific group of invariants.

Contracts are an attempt to include formal specification languages into the implementation languages. You can enforce valid and invalid state changes, enforce relationships across the program state, or even enforce some level of correctness in behaviour.

> around a long time and has not caught on. That's usually a good sign that better approaches are prevailing.

That is completely not true. Plenty of dumb things prevail for faar too long for no other reason than momentum. Plenty of great things remain academic forever. It took decades to get algebraic types or basic functional programming somewhat accepted.

Design by contract is in theory a good idea but suffers from being a pain to use effectively. (making actually useful invariants that help the program more than an assert already would have)

Adding them to languages not built around them also results in quite nasty boilerplate or runtime overhead which further discourage their usage.