Eta-short and Eta-expanded records not typechecked at the same type

Vector.agda

-- Cf. this discussion for an explanation of what happens:
-- http://code.google.com/p/agda/issues/detail?id=1526

module Vector where

open import Data.Bool
open import Data.Nat
open import Data.Fin as Fin
open import Data.Unit
open import Data.Product
open import Function
open import Relation.Nullary


-- we start by defining an heterogeneous vector
[vector] : (n : ℕ) (ρ : Fin n → Set) → Set
[vector] zero    ρ = ⊤
[vector] (suc n) ρ = ρ Fin.zero × [vector] n (ρ ∘ Fin.suc)

-- having a record wrapping the computation helps the type
-- inference engine.
record vector (n : ℕ) (ρ : Fin n → Set) : Set where
  constructor [_]
  field
    content : [vector] n ρ
open vector public

-- It is possible to change the type of an element in a specific
-- position.
update : {n : ℕ} (k : Fin n) (A : Set) (ρ : Fin n → Set) → Fin n → Set
update zero    A ρ zero    = A
update zero    A ρ (suc l) = ρ (suc l)
update (suc k) A ρ zero    = ρ zero
update (suc k) A ρ (suc l) = update k A (ρ ∘ Fin.suc) l

-- from this we can define an update operation filling a position
-- k with a new element no matter what its type is
infixr 5 [_∷=_⟨]_ _∷=_⟨_
[_∷=_⟨]_ : {n : ℕ} {ρ : Fin n → Set} (k : Fin n) {A : Set} (a : A) →
           [vector] n ρ → [vector] n (update k A ρ)
[ zero  ∷= a ⟨] (_ , v) = a , v
[ suc k ∷= a ⟨] (w , v) = w , [ k ∷= a ⟨] v

_∷=_⟨_ : {n : ℕ} (k : Fin n) {A : Set} (a : A)
         {ρ : Fin n → Set} → vector n ρ → vector n (update k A ρ)
b ∷= a ⟨ [ p ] = [ [ b ∷= a ⟨] p ]

-- we can always generate a dummy vector full of proofs of unit
[⟨⟩] : (n : ℕ) → [vector] n (const ⊤)
[⟨⟩] zero    = tt
[⟨⟩] (suc n) = tt , [⟨⟩] n

⟨⟩ : {n : ℕ} → vector n (const ⊤)
⟨⟩ = [ [⟨⟩] _ ]

-- from this we can build a vector by successively updating
-- a dummy one until we're happy with the result.
-- That's where the trouble is: Agda rejects the type annotation
-- so we need to define the vector by successive updates first
-- and then eta-expand it to assign it the type we want!

0⋯4 : vector 5 (const ℕ)
0⋯4 = [ content r ] where
-- The type annotation
--   r : vector 5 (const ℕ)
-- fails to typecheck
  r : vector 5 _
  r = (# 0) ∷= 0 ⟨
      (# 1) ∷= 1 ⟨
      (# 2) ∷= 2 ⟨
      (# 3) ∷= 3 ⟨
      (# 4) ∷= 4 ⟨
      ⟨⟩

-- these two things are deemed equal judgmentally though:

open import Relation.Binary.PropositionalEquality

eta : {n : ℕ} {ρ : Fin n → Set} {v : vector n ρ} → v ≡ [ content v ]
eta = refl