[Agda] Weird behaviour with record normalisation

[Simon Foster]

Thanks Andreas, and yes this patch has solved both the toy example and  
my actual problem code. However, I've noticed using your example that  
whilst the following works correctly now:

problem1 : (r : R a) -> F (R.p {a} r) -> F (R.p {b} (relabel r))
problem1 r x = x

If I manually expand the definition of relabel in the function head:

problem2 : (r : R a) -> F (R.p {a} r) -> F (R.p {b} (c {b} (R.p {a} r)))
problem2 r x = {!x!}

This doesn't work, and still normalises to F (R.p {b} r).

Thanks,

-Si.

On 12 Nov 2010, at 22:59, Andreas Abel wrote:

> The weird behavior comes from eta-contraction, the definition of  
> relabel is eta-contracted to
>
>  relabel r = r
>
> In your example, mg is reduced to the identity.
>
> I pushed patches that implement less eta-contraction, so the  
> weirdness should have disappeared.
>
> Cheers,
> Andreas
>
> On 11/12/10 2:14 PM, Andreas Abel wrote:
>> Ah, ok, now I see what you mean. This seems to be a bug, subject
>> reduction is broken. Simplifying your example...
>>
>> {-# OPTIONS --show-implicit #-}
>>
>> module Issue361 where
>>
>> postulate
>> A : Set
>> a b : A
>> F : A -> Set
>>
>> record R (a : A) : Set where
>> constructor c
>> field
>> p : A
>>
>> relabel : R a -> R b
>> relabel r = c {b} (R.p {a} r)
>>
>> problem : (r : R a) -> F (R.p {a} r) -> F (R.p {b} (relabel r))
>> problem r x = {!R.p {b} (relabel r)!}
>> -- C-c C-n normalizes this expression to R.p {b} r
>>
>> Agda seems to compute
>>
>> R.p {b} (c {b} (R.p {a} r)) = R.p {b} r
>>
>> instead of
>>
>> R.p {a} r
>>
>> I filed this as bug 361.
>>
>> Cheers,
>> Andreas
>>
>>
>> On 11/12/10 9:56 AM, Simon Foster wrote:
>>> Hi,
>>>
>>>> While the terms differs only in their hidden argument, they are
>>>> nontheless unequal. Hidden arguments are not irrelevant.
>>>
>>> Sure, and I understand that's why x can't be used as the  
>>> inhabitant for
>>> "fails". What I don't understand is how function "fails" can be  
>>> given
>>> type "Fin (R2.g {R1C (R1.f1 r1) (suc (R1.f2 r1))} r2)" at all,  
>>> when Agda
>>> says this isn't a valid type (try deducing it), since r2 is not  
>>> indexed
>>> by "R1C (R1.f1 r1) (suc (R1.f2 r1))" but by r1.
>>>
>>> Fundamentally, I don't understand why "mg r2" normalises to r2  
>>> when the
>>> two have different types (even though they they contain the same
>>> fields), namely "R2 (R1C (R1.f1 r1) (suc (R1.f2 r1))})" and "R2 r1"
>>> respectively.
>>>
>>> Thanks,
>>>
>>> -Si.
>>>
>>>> On 11/11/10 5:32 PM, Simon Foster wrote:
>>>>> Hi,
>>>>>
>>>>> I'm experiencing some strange behaviour when trying to  
>>>>> manipulate the
>>>>> fields of a record parametrised over another record. Consider  
>>>>> this toy
>>>>> example:
>>>>>
>>>>> module Test where
>>>>>
>>>>> open import Data.Fin
>>>>> open import Data.Nat
>>>>>
>>>>> record R1 : Set where
>>>>> constructor R1C
>>>>> field
>>>>> f1 : ℕ
>>>>> f2 : ℕ
>>>>>
>>>>> record R2 (r1 : R1) : Set where
>>>>> constructor R2C
>>>>> open R1 r1
>>>>> field
>>>>> g : ℕ
>>>>>
>>>>> mf : R1 → R1
>>>>> mf r1 = R1C (R1.f1 r1) (suc (R1.f2 r1))
>>>>>
>>>>> mg : ∀ {r1 : R1} → R2 r1 → R2 (mf r1)
>>>>> mg r2 = R2C (R2.g r2)
>>>>>
>>>>> fails : ∀ r1 (r2 : R2 r1) → Fin (R2.g r2) → Fin (R2.g (mg  
>>>>> r2))
>>>>> fails r1 r2 x = {!x!}
>>>>>
>>>>> Under the current darcs version of Agda, the function "fails"  
>>>>> cannot be
>>>>> inhabited. The type of this function normalises to "Fin (R2.g  
>>>>> r2)",
>>>>> which it ought to be possible to inhabit with x. However on closer
>>>>> inspection of the hidden variables the actual type is "Fin (R2.g  
>>>>> {R1C
>>>>> (R1.f1 r1) (suc (R1.f2 r1))} r2)", that is r1 has been  
>>>>> instantiated to
>>>>> "R1C (R1.f1 r1) (suc (R1.f2 r1))", and therefore the output  
>>>>> doesn't
>>>>> seem
>>>>> to be a valid type since r2 is parametrised over r1.
>>>>>
>>>>> I'm not sure what's going on here, but somehow the function mg  
>>>>> seems to
>>>>> be normalising in a strange way - "mg r2" normalises to r2, but  
>>>>> has
>>>>> type
>>>>> "R2 (R1C (R1.f1 r1) (suc (R1.f2 r1)))" which is not equal to "R2  
>>>>> r1".
>>>>> Either that or there is somehow two versions of r2.
>>>
>>>
>>>
>>
>
> -- 
> 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/