Eta-reduction for records buggy [Re: [Agda] Weird behaviour with record normalisation]

[Andreas Abel]

Ok, I had only tested the normalization of R.p {b} (c {b} (R.p {a} r))
and this was correct after my fix.  Which I withdrew now.

But I found a way to expose the eta-reduction bug in form of an 
unjustified error message.

module Issue361 where

data _==_ {A : Set}(a : A) : A -> Set where
   refl : a == a

postulate
   A : Set
   a b : A
   F : A -> Set

record R (a : A) : Set where
   constructor c
   field
     p : A

beta : (x : A) -> R.p {b} (c {b} x) == x
beta x = refl

lemma : (r : R a) -> R.p {b} (c {b} (R.p {a} r)) == R.p {a} r
lemma r = beta (R.p {a} r)

{-
     a != b of type A
     when checking that the expression beta (R.p {a} r) has type
     _==_ {A} (R.p {b} r) (R.p {a} r)
-}

This code should clearly type-check.

Cheers,
Andreas
On 11/15/10 12:48 PM, Simon Foster wrote:
> 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/
>
>

-- 
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/