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
@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.
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.
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"