[Agda] eta-equality for records and metavar resolution

[Andreas Abel]

Hi Christian,

thanks for the test case and for finding this bug!  It was just a stupid 
glitch in the implementation, easily fixed.  Agda does recognize 
unguarded recursive records like the one below and switches of 
eta-equality for these, thus, there is no problem in principle.

Congrats to your first contribution to the Agda code base!
(darcs show authors)

Cheers,
Andreas

On 31.12.13 4:24 AM, Christian Sattler wrote:
> Uh oh, I just tried (didn't even know we had recursive records) and the
> following makes Agda loop now:
>
> record R : Set where
>    constructor cons
>    field
>      r : R
>
> module _ (F : (R → Set) → Set) where
>    q : (∀ f → F f) → (∀ f → F f)
>    q h _ = h (λ {(cons _) → _})
>
> Cheers,
> Christian
>
> PS: I had a small, but important omission in my test case, please
> obliterate the old patch.
>
>
> On 2013-12-31 03:41, Christian Sattler wrote:
>> Hi Andreas,
>>
>> Yes, that solves my issue. Your development pipeline sure is pretty
>> short! I hope there are no unintended consequences in the form of
>> non-termination of metavar resolution in the context of recursive
>> records or things like that.
>>
>> I have attached a test case patch.
>>
>> Thanks!
>> Christian
>>
>> On 2013-12-30 14:07, Andreas Abel wrote:
>>> 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/