[Agda] Weird behaviour with record normalisation

[Simon Foster]

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.