[Agda] eta-equality for records and metavar resolution
Christian Sattler
sattler.christian at gmail.com
Thu Dec 26 22:19:10 CET 2013
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
More information about the Agda
mailing list