> If you're too strict about what counts as equivalent (including performance in the type system, say) it would be harder to make local changes since fewer substitutions would be possible.

I think this is avoidable if your types/effects can decompose properly into orthogonal factors. E.g. with a Future type and a generic monad abstraction it's fairly easy to substitute a sync call for an async call - you have to be explicit about the change you're making, but only very slightly, and you'd never get confused between changing sync/async and changing the "actual" type that's returned.