[Agda] Weird behaviour with record normalisation

[Simon Foster]

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.

Thanks,

-Si.