Fix #7669: positivity checker: compute function arity up to def. eq.

[andreasabel]

Closes #7669.

[andreasabel]

The change here improves polarity inference, which seems to make solutions of unification problems less unique.
https://github.com/agda/agda-stdlib/blob/d85cd7e5cc9d990c103be625e52331b6e7f125b9/src/Algebra/Construct/Initial.agda#L78
https://github.com/agda/agda/actions/runs/12603074122/job/35127852387?pr=7674#step:8:158

Unsolved metas at the following locations:
/home/runner/work/agda/agda/std-lib/src/Algebra/Construct/Initial.agda:78.17-32
/home/runner/work/agda/agda/std-lib/src/Algebra/Construct/Initial.agda:81.61-67

[szumixie]

Here's a minimized example for the difference in unification behavior:

data Unit : Set where
  tt : Unit

postulate
  A B : Set

FUN : Set₁
FUN = Set → Set

ConstA : Unit → FUN
ConstA tt _ = A

postulate
  x : Unit
  f : (Z : Set) → ConstA x Z

a : ConstA x B
a = f _

With the old behavior, the code above typechecks even though the hole in a can be solved with any type, inlining FUN in the type of ConstA results in an unsolved meta. With the new behavior, it always results in an unsolved meta.

[nad]

With the old behavior, the code above typechecks even though the hole in a can be solved with any type

That sounds like a bug to me.

[szumixie]

Yes it is a bug, the new behavior is the correct one. With the old behavior, the positivity checker fails to infer that the second argument of ConstA is nonvariant, which causes the unifier to treat it as definitionally injective in that argument.

[andreasabel]

Updating std-lib in

• agda/agda#7674 eta-expand fields in record expression agda-stdlib#2546