Изоморфизм спешит на помощь

Как уже отмечали, такие компиляторы существуют, и в них можно формализовать изоморфизмы для многих типов:
github.com/idris-lang/Idris-dev/blob/master/libs/base/Control/Isomorphism.idr
github.com/idris-lang/Idris-dev/tree/master/libs/contrib/Control/Isomorphism
А с переходом к гомотопическим типам можно полноценно формализовать и изоморфизмы для функций:
github.com/clayrat/redtt/blob/isos/library/cool/isos.red#L60