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

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.

@asaj @amy I'm very interested in those cases and I would love to develop a theory of "adaptable changes" where the compiler fix also provides a migration tool for users affected by the change

This is not only useful for compilers but also for breaking changes in libraries

@Andrev @amy the problem we hit is that trying to work out if the new type error is a false +ve (so the fix is to change the type annotations) or a genuine bug (so the fix is to change the code) is often non-trivial.

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.