agda/agda#7674 eta-expand fields in record expression

[andreasabel]

agda/agda#7674 eta-expand fields in record expression

Agda PR #7674 requires some implicit arguments explicitly in some record expression given since variance info got refined (invariant to non-variant) and hence solutions are no longer unique.

Fixing Agda to commit 2ffb002 now in agda/agda#7674.
If this PR is rebased or squashed (rather than merged with merge commit) the commit hash there needs to be updated accordingly.

[andreasabel]

This checks with Agda master (2.8.0) but not with 2.7.0.1:

_x_48 ≈ y → _u_49 ≈ v → _x_48 ∙ _u_49 ≈ y ∙ v !=
{v = v₁ : Carrier} → x ≈ y → v ≈ v₁ → x ∙ v ≈ y ∙ v₁ because one is
an implicit function type and the other is an explicit function type
when checking that the expression
λ {y} {v} → ∙-cong {y = y} {v = v} has type Congruent₂ _≈_ _∙_

Apparently, in 2.8.0 we have fixed another bug but I could not find it now.

[jamesmckinna]

@andreasabel IIUC, as this is an upstream change to a not-yet-released agda-2.8.0, should this PR not be merged into targeted at the experimental branch of stdlib, and not at master?

[andreasabel]

@andreasabel IIUC, as this is an upstream change to a not-yet-released agda-2.8.0, should this PR not be merged into targeted at the experimental branch of stdlib, and not at master?

Formally, yes.

However, in this case the change is in its present form compatible both with current Agda and 2.8.0, and it does not change the value of any definition, only makes some arguments explicit, so I thought we could just merge this into master.
Let me know if you think otherwise.

[jamesmckinna]

@andreasabel your definition of "Current Agda" is v2.7.0, or v2.7.0.1?

If the former, then the module continues to typecheck as-was under 2.7.0, and IIUC from @MatthewDaggitt 's v2.2rc1, also under 2.7.0.1.

It may very well be that v2.8.0 fixes bugs which mean that eta-expansion of implicit functions is required in record field bindings, but in my own (not so very) humble opinion, this should be regarded as a major UX failure. The changes in this PR concern a single module within which it will no longer be possible, IIUC (please correct if otherwise) to exploit record subtyping in order to construct the relevant instantiations of the various initial Algebra structures... by writing

name : type
name = defn
... = record { name = name }

when the shared type type of defn and field name name involves implicit quantification.

How can this make sense to users?

And FTR, there are other examples in the stdlib (I can't identify them off the top of my head) where we have had to eta-expand to accommodate this style, and it's exasperating! (to me, at least)

One reason I nudged towards experimental is in the hope that this UX failure might be reconciled with the type-theoretical sophistication around the issues fixed by agda/agda#7674 without having to disturb either the v2.2 point release, and our plans for the subsequent breaking v3.0... until such time as we can revisit this?

[jamesmckinna]

For trans alone, we already have (at least) the following apparently needing eta-expansion, when I wish we didn't:

• Algebra.Properties.Monoid.Divisibility
• Data.Container.Indexed.WithK
• Data.Float.Properties
• Data.String.Properties
• Data.Word64.Properties
• Function.Related.Propositional
• Function.Relation.Binary.Setoid.Equality
• Relation.Binary.HeterogeneousEquality.Quotients.Examples

[MatthewDaggitt]

My feeling is that this should also go on experimental. As @jamesmckinna says this seems like a downgrade in the library code (even if backwards compatible). Furthermore, if Agda 2.8.0 is released, it'll make creating a clean release of the standard library much easier than if this is buried on master somewhere.

[JacquesCarette]

Adding my voice to the chorus in favour of experimental.

[andreasabel]

Ok, I merged this into experimental.

@jamesmckinna wrote:

that eta-expansion of implicit functions is required in record field bindings, but in my own (not so very) humble opinion, this should be regarded as a major UX failure

Here is some background on this PR:

1. Agda does not have a special checker for record expressions. What is checked is the application of the record constructor (having an iterated Pi-type) to the expressions given for the record fields.

   IsMagma.constructor isEquivalence \bullet-cong

2. Agda does eager insertion of implicit lambdas and applications, so what you get there is

    ... (\ {x y u v} -> \bullet-cong {_} {_} {_} {_})
   

   Agda's implicit arguments are akin to type-quantification in F-sub, which is known to have undecidable subtyping.
   So, please do not forget, Agda's (surface) typing is undecidable.
3. If Agda cannot solve one of the underscores, you get yellow and have to provide it (that is happening in this PR).
   Agda will only solve underscores for you that have a unique solution, which is not the case (any longer) in this example.
4. Before Fix #7669: positivity checker: compute function arity up to def. eq. agda#7674, the underscores could be filled thank to a bug in Agda's polarity inference.

We are all aware that eager insertion of implicits leads often to annoying eta expansions like \ {x} -> f {x}, and I have worked in the past on some heuristics to prevent this. E.g., if you write an alias g = f, then no implicit insertion takes place because this is usually not what the user would want.
A similar heuristics could be tried for record expressions, but this is a new feature of Agda, we are discussing then. (It is not that agda/agda#7674 would introduce a regression.) Implementing the new feature is an enterprise independent of fixing existing bugs. Note that this new feature could introduce regressions as well, so it is not a clear shot.

A final note: Not having eager insertion of implicits would be annoying as well, e.g. for the standard map and polymorphic identity id, this code would fail to type check: map id xs. The error would then be "forall {A} -> A -> A is not a subtype of _ -> _".

[jamesmckinna]

@andreasabel thanks for the detailed account of what is going on under the hood regarding eta-expansion in the setting of (undecidable!) typechecking of Agda's surface syntax.

Once v2.8.0 gets released, I'd be happy to revisit this for master, but via a more comprehensive/systematic refactoring of Algebra.Construct.Initial, perhaps even by removing the delegation to the ℤero module...

[andreasabel]

Rebased experimental onto master to get GHC 9.12-compatibility in.