[Agda] Weird behaviour with record normalisation

[Andreas Abel]

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/