[Agda] Weird behaviour with record normalisation

[Andreas Abel]

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