[Agda] eta-equality for records and metavar resolution

[Andreas Abel]

Hi Christian,

I implemented the feature.  Please test and publish a self-contained 
medium-sized test case (on the mailing list of as patch in test/succeed)!

Let me know if this solved your issue.

Cheers,
Andreas

On 28.12.13 1:44 PM, Christian Sattler wrote:
> Hi Andreas,
>
> Good to know a fix has been proposed! The type of situations where I
> encounter this issue is actually fairly common when reasoning about
> dependent sums or products where the first type parameter is itself a
> Σ-type. One example is associativity of Σ (when the right-hand side is
> left implicit):
>
> Σ (Σ A B) (λ {(a , b) → C a b}) ≃ Σ A (λ a → Σ (B a) (C a))
>
> Cheers,
> Christian
>
>
> On 2013-12-28 13:11, Andreas Abel wrote:
>> 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/