[Agda] eta-equality for records and metavar resolution
Andreas Abel
andreas.abel at ifi.lmu.de
Sat Dec 28 13:11:15 CET 2013
Hi Christian,
good for bringing this up! This is a known issue:
http://code.google.com/p/agda/issues/detail?id=376
With Brigitte did the necessary research to fix this, see our TLCA 2011
paper.
However, I was wondering if this issue shows up in practice. (See
comment #6.) Apparently, you got stuck on it, so it seems worthwhile
fixing.
A fix seems to be: Whenever we see a meta-variable applied to a
projected variable, we rewrite the context such that the projected
variable is replaced by a "tuple" of fresh variables of the appropriate
types. More precisely, we solve the meta-variable by a new one which
lives in the thus expanded context.
Cheers,
Andreas
On 26.12.13 10:19 PM, Christian Sattler wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list