Pretty often I'll investigate a garden-variety Agda issue and end up revealing a lovecraftian Agda issue lurking right beneath
Normally when user code breaks with f ≠ g, and f, g are two adjacent variables in the context, it's because you messed up de Bruijn indices somewhere. Garden variety.
In this case it was the positivity checker just casually deciding to break transitivity of conversion by not using the polarity associated with the data type name, but with some secret info from god-knows-where. Lovecraftian
Follow
though I will say it's very unusual to break user code and go "Is my patch bad? No, it is the users who are wrong"
@amy That happens to us every so often. We fix a bug in the typechecker, and as a result code that should never have typechecked gets rejected. Which is usually fine if the code is actively maintained, but sometimes it's a dependency that nobody has touched in years, the person who wrote it has left the company, etc.