Miss Dada  🏳️‍⚧️

right but I'm specifically talking about a world where everyone wants you to interoperate with dozens of (potentially adhoc) effects. Every effect you incidentally satisfy that you refuse to document makes your library less useful.

Yup, this is the world I live in. I think it's easy to over-estimate how bad it is, as long as you actively consider "what realistically could break" with every change, and take the spirit of RFC 1105 to heart.

Do you think this philosophy would be tractable in a world of pervasive dependent typing?

I don't know that I can give a better answer than "it depends". Maybe you should ask an Idris programmer. ;) For Diesel we work around this by "the public API for the result of this method is this helper type w/ the same name". Associated type values are generally private

r.e. your list of things worth encoding, I think the only one that's really worth doing is constexpr and maybe i/o purity (I generally always lean towards "this type does I/O, other types take this one as an arg" regardless so I don't care as much)

I do think that *in general* spending a lot of time considering how changes will affect your users goes a very long way. If everybody in OSS did this, we would have a lot fewer of these discussions

There's a lot of value in having a connection with your larger users, and being able to just ask "hey does this commit break your app?". Crater is nice, but ultimately the real breakage is from the servos of the world, and apps of that size are rarely open source.