[Agda] Weird behaviour with record normalisation

[Andreas Abel]

Hi Simon,

the behavior may be strange, but it is perfectly sound.  By looking at 
the hidden arguments you have almost answered your question yourself. 
Looking at the terms and their types, we have

   r2 : R2 r1
   mg r2 : R2 (mf r1)
   mg {mf r1} r2 = R2C {mf r1} (R2.g {mf r1} r2)
   g (mg r2) = R2.g {mf r1} r2
            != R2.g {r1}    r2

While the terms differs only in their hidden argument, they are 
nontheless unequal.  Hidden arguments are not irrelevant.

Of course, without option --show-implicit

Goal: Fin (R2.g r2)
————————————————————————————————————————————————————————————
x  : Fin (R2.g r2)
r2 : R2 r1
r1 : R1

not being able to fill the hole with x is alienating.

Cheers,
Andreas

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.