[Agda] eta-equality for records and metavar resolution

[Christian Sattler]

Hi everyone,

Given (A B : Set), abbreviate

T = {C : A → B → Set} → Σ (A × B) (λ {(a , b) → C a b}).

Given an occurrence of a variable (t : T), one would like the implicit 
parameter C to be resolvable from a given value for the resulting type Σ 
(A × B) (λ {(a , b) → C a b}) of the same shape: records are specified 
to have eta-conversion after all. We can test this hypothesis as follows:

f : T → T
f t = t

Alas, the implicit argument C of t will be marked unresolved: the 
contraint resolver gets stuck at

_C_11 (π₁ x) (π₂ x) =< .C (π₁ x) (π₂ x) : Set.

Why is that? Should eta-expansion not allow us to regard x as a pair (a 
, b), which would simplify the contraint to _C_11 a b =< .C a b?

Ironically, the situation changes if we choose

T = {C : A × B → Set} → Σ (A × B) (λ {(a , b) → C (a , b)})

(but not with B × A!) - because of eta!

Cheers,
Christian