Agda 2.6.4

[jkopanski]

Intro

With this Agda version there were changes [1] to instance resolution
algorithm, from agda changelog:

[Breaking] The algorithm for resolution of instance arguments has been
simplified. It will now only rely on the type of instances to
determine which candidate it should use, and no longer on their
values.

I've found this thread [2] at zulip, which might be helpful. It
wasn't for me;)

Solution

In the end I've removed the opening of the Equivalent record module
straight after its definition. With this version Agda won't be able
to figure out definitions like this:

F-cong : ∀ {a b} {f g : a ⇨ b} → f ≈ g → Fₘ f ≈ Fₘ g

where each _≈_ belongs to a different instance. That's why now one
have to manually open appropriate instance. However if we have only
single Equivalent in the context using an open Equivalent ⦃ … ⦄
will suffice.

Additional comments around design

Furthermore I've added explicit implicit ;) arguments to Equivalent
fields. Those are actually important and it is impossible to follow
hint that was stated in the TODO comment, that used to said:

TODO: move a and b arguments from methods to record.

Without those implicit args, definitions like:

∘≈ : ∀ {f g : a ⇨ b} {h k : b ⇨ c} → h ≈ k → f ≈ g → h ∘ f ≈ k ∘ g

wouldn't typecheck as the Equivalent would lock it's variables
during instantiation and we could use only those two (a & b in
this case). _≈_ would reject morphisms h & k here as it's
objects would be different.

There is additional TODO comment that says:

TODO: Replace Equivalent by Setoid?

Actually moving variables mentioned above would almost turn Equivalent
into Setoid (minus Carrier as a field). Which isn't really feasible
for the reasons already mentioned.

How others do it

I've took a peek how agda-categoris does it [3] and they basically put
Equivalent into definition of Category and call it Setoid
enriched. I've played with that for a bit. Initially putting _≈_
into lawful category. That didn't work out however because we need
_≈_ for defining different kinds homomorphisms, where we don't have
lawful classes in scope. So I've moved it to the raw Category, but
the problem with definitions that use multiple equalities still
persists. I think that restricting the opening of Category class
would be too cumbersome. So I think this split to Equivalent works
nice. I do wonder however if it's worth doing the instance search, if
most of the time one has to manually open appropriate one?

[1] https://github.com/agda/agda/blob/master/doc/release-notes/2.6.4.md#language
[2] https://agda.zulipchat.com/#narrow/stream/238741-general/topic/Issue.20with.20instance.20search.20changes.20in.202.2E6.2E4/near/384560563
[3] https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Core.agda#L21

[conal]

With this version Agda won't be able to figure out definitions like this:

F-cong : ∀ {a b} {f g : a ⇨ b} → f ≈ g → Fₘ f ≈ Fₘ g

where each _≈_ belongs to a different instance.

Do you understand how it is that the new restriction on instance selection applies to this F-cong signature? Doesn't this code rely on the morphism types rather values to determine each of the two Equivalent instances needd?

[jkopanski]

With this version Agda won't be able to figure out definitions like this:

F-cong : ∀ {a b} {f g : a ⇨ b} → f ≈ g → Fₘ f ≈ Fₘ g

where each _≈_ belongs to a different instance.

Do you understand how it is that the new restriction on instance selection applies to this F-cong signature? Doesn't this code rely on the morphism types rather values to determine each of the two Equivalent instances needd?

just a caveat that my understanding of this is very limited!

But the _≈_ type itself sits inside a record and now Agda won't look inside of that record.

I think we should look into the change PR for more clues. Specifically take a look at test cases: Issue1952 they seem to contain some similar signatures that we would like to have.

[conal]

But the _≈_ type itself sits inside a record and now Agda won't look inside of that record.

Thank you. I'll do some experimenting also.

[conal]

What motivated introducing and using this synonym for sym? Is it related to the other changes in this PR?

[jkopanski]

Ok, this pointed out that I didn't spell out my bigger questions here. Right now the we open Equiv publicly, under the Equivalent. Using sym (and refl, trans) directly will have the problems we are seeing. I think that we shouldn't reexport those functions publicly, but I didn't want to change that without discussing.

That's why I introduced alias for sym which comes from ≈-Reasoning module and can have Equivalent instance passed explicitly.

Alias itself and its fixity declarations come from agda- categories and I don't know the answer to the fixity question.

Another approach would be to reexport familiar names from the reasoning module instead.

[conal]

Thank you for the context. I had not noticed that you moved _;_ and _•_ under ≈-Reasoning. Nice trick!

I agree with you about reexporting refl, sym, and trans from ≈-Reasoning instead of from Equivalent. Thanks for the suggestion.

[conal]

What is the effect of an infix declaration for an operator without one or more underscores in its name?

[conal]

The single essence of this PR is to open ≈-Reasoning with an explicit Equivalence argument, in order to disambiguate refl, sym, and trans (and their synonyms), right?

[jkopanski]

The single essence of this PR is to open ≈-Reasoning with an explicit Equivalence argument, in order to disambiguate refl, sym, and trans (and their synonyms), right?

yes, although only synonyms will be disambiguated, because refl, sym, and trans are opened publicly outside of the ≈-Reasoning.

[conal]

Thank you, @jkopanski, for all your effort in adapting Felix to Agda 2.6.4. I'm delighted with the result! We're back in the mainstream of Agda progress, while retaining readability, especially in the signatures/theorems, where it matters most!