Fragile `NonZero` and implementation-dependent luck

[JacquesCarette]

A quite thorough description of the issue is already written so I won't repeat it all here.

Basically some of our NonZero instances resolve through sheer luck of the details of the current implementation and changes to make the upstream algorithm less ad hoc break stdlib. The issue boils down to some non-injective functions (like / and %) having accompanying cong functions with implicits that should be explicit as they can't in general be inferred [see details at above post.]. So we should fix those cong routines to not be so fragile.

This will be a breaking change, but one that we are forced to do, as our current implementation should be regarded as buggy because it relies on 'sheer luck' to work.

While I am intending to fix this myself, I'm not sure how fast I'll be, so I would be very happy to collaborate with others on that.

[jamesmckinna]

Unfortunately, I didn't understand the discussion on the main Agda Zulip, but get your outline of what might be required. What's not clear is how many of these lemmas (all?) regarding the affected functions are touched by the change. is it 'simply' a case of the cong proofs being faulty (when proved, or when deployed, etc.), or all uses?

[plt-amy]

@jamesmckinna The heart of the issue is that (without lossy-unification) Agda will not generally solve for _0 := y based on a constraint like f x _0 = f x y — practically, this means that if you have an argument that's only mentioned "in a return type, under a function" it'll often fail to be inferred— taking one of the affected functions as an example,

%-congˡ : ∀{m n o} .⦃ _ : NonZero o ⦄ → m ≡ n → m % o ≡ n % o

here the variables m and n appear as arguments to _≡_, which, as a data type, is definitionally injective; so they can be solved by looking at the type of the explicit argument to %-congˡ. This isn't unique to instances: lemmas like +-assoc generally need to have all of their arguments specified, because in general we can't definitionally invert addition. But here the argument o only appears under _%_, which is not injective, and so it'd go unsolved.

(It currently works by coincidence: at the use sites I inspected, the correct NonZero instance happens to be the first one tried, and (even though this is an unforced choice) Agda will simply choose that first instance because NonZero instances are always used irrelevantly.)

So, to summarize, the cong proofs have very "hopeful" types, which currently work by relying on details of instance search (that I would rather change); and there's not really a guarantee that the use sites will keep working. The easiest fix is to make any argument fitting that heuristic ("only under a function") explicit, which will cause a bit of churn.

[plt-amy]

(P.S. I'd be happy to hold back on my instance search work/have it under a flag for a while/etc so these functions can have a proper deprecation cycle, since I'm not sure what the stdlib policy here is)

[jamesmckinna]

Thanks @plt-amy ! for:

• the more explicit guidance regarding how to localise the problem
• the concern about how agda and agda-stdlib development cycles might interact

Regarding the second, I'm guessing your changes to instance inference/lossy unification will be v2.8.0, and since we're currently in a v2.7.0.* test/release cycle, I think these things could be considered 'non-interfering' (notwithstanding other changes to agda such as #2476 which have required changes to experimental rather than master). That said, maybe pushing to experimental would be the right thing to do? Shoutouts to @JacquesCarette @MatthewDaggitt and @gallais for rulings on this...

[plt-amy]

Yes, getting rid of the unforced choices by 2.8.0 sounds like a good plan on the compiler end.

[MatthewDaggitt]

Yes, I think these changes should be pushed to experimental with the aim of releasing them as compatibility changes with whatever release we make to coincide with v2.8.0.