[Agda] refusal to construct infinite term

[Martin Escardo]

Why does Agda think it would have to construct an infinite term?

In the attached short(ened) Agda file, I have two different 
implementations of vectors, in two modules FinitePowers and FinitePowers'.

(1) If I open FinitePowers, the whole file type checks.

(2) If I instead open FinitePowers', I get

-- AgdaQuestion.agda:84,11-13
-- Refuse to construct infinite term by instantiating _125 to (_Γ_125
-- [ succ (succ zero) ] ⇒ _τ_127)
-- when checking that the expression ν₁ has type
-- T _Γ_125 (_Γ_125 [ succ (succ zero) ] ⇒ _τ_127)

This is in the definition of η. (Search for "Refuse" in tghe attached file.)

(3) If I still keep FinitePowers', but replace the definition by 
supplying all implicit parameters explicitly (with the help of ctrl-C 
ctrl-A), then the whole file type checks.

(4) If I still keep FinitePowers', but in the original offending 
definition of η, I replace the offending subterm term by a hole, I still 
get the same error as in (2).

Clarifications are welcome.

It is unfortunate that I can't use FinitePowers': it makes my proof (not 
included in this attachment) much more cumbersome (in particular, I lose 
some definitional equalities and have to use subst). The interesting 
thing is that I can prove what I want with FinitePowers', but then I 
can't use the proof for particular examples without supplying the (huge) 
implicit parameters.

Thanks,
Martin

-------------- next part --------------
-- Martin Escardo 31 May 2013.

-- Why does Agda think it needs to construct an infinite term?
--
-- Moreover, why does one abstract type work but not the other?

module AgdaQuestion where

data ℕ : Set where 
  zero : ℕ              
  succ : ℕ → ℕ 

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC succ #-}      

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin(succ n)
  succ : {n : ℕ} → Fin n → Fin(succ n) 

-- Vector which notationally grow at the end:

module FinitePowers where

  data _^_ (X : Set) : ℕ → Set where
    〈〉  : X ^ zero
    _’_ : {n : ℕ} → X ^ n → X → X ^ (succ n)

  infixl 6  _’_

  _[_] : {X : Set} {n : ℕ} → X ^ n → Fin n → X
  (xs ’ x) [ zero ] = x
  (xs ’ x) [ succ i ] = xs [ i ]

-- Alternative implementation:

module FinitePowers' where

  _^_ : Set → ℕ → Set
  X ^ n = Fin n → X

  〈〉 : {X : Set} → X ^ zero
  〈〉 () 

  _’_ : {n : ℕ} {X : Set} → X ^ n → X → X ^ (succ n) 
  (xs ’ x) zero = x
  (xs ’ x) (succ i) = xs i

  infixl 6  _’_

  _[_] : {X : Set} {n : ℕ} → X ^ n → Fin n → X
  xs [ i ] = xs i


open FinitePowers -- fine with this, but failure with FinitePowers' (see below)

data type : Set where
 ι    : type
 _⇒_ : type → type → type

infixr 6 _⇒_

Cxt : ℕ → Set
Cxt n = type ^ n

-- Terms in context, using de Bruijn indices:

data T : {n : ℕ} (Γ : Cxt n) (σ : type) → Set where
 ν    : {n : ℕ}{Γ : Cxt n} → (i : Fin n)  → T Γ (Γ [ i ])
 ƛ    : {n : ℕ}{Γ : Cxt n} → {σ τ : type} → T (Γ ’ σ) τ → T Γ (σ ⇒ τ) 
 _·_  : {n : ℕ}{Γ : Cxt n} → {σ τ : type} → T Γ (σ ⇒ τ) → T Γ σ → T Γ τ

infixl 6 _·_

-- Example

ν₀ : {n : ℕ}{Γ : Cxt(succ n)} → T Γ (Γ [ zero ])
ν₀ = ν zero
ν₁ : {n : ℕ}{Γ : Cxt(succ(succ n))} → T Γ (Γ [ succ zero ])
ν₁ = ν (succ zero)
ν₂ : {n : ℕ}{Γ : Cxt(succ(succ(succ n)))} → T Γ (Γ [ succ(succ zero) ])
ν₂ = ν (succ(succ zero))

D : type → type → type → type → type
D X Y Z A = (Z ⇒ A) ⇒ ((Y ⇒ A) ⇒ X ⇒ A) ⇒ A

η : {X Y Z A : type} {n : ℕ} {Γ : Cxt n} → T Γ (Z ⇒ D X Y Z A)
η = ƛ(ƛ(ƛ(ν₁ · ν₂)))

-- Now I write the same with all implicit parameters explicitly given
-- (thanks to ctrl-C ctrl-A):

η' : {X Y Z A : type} {n : ℕ} {Γ : Cxt n} → T Γ (Z ⇒ D X Y Z A)
η' {X} {Y} {Z} {A} {n} {Γ} = ƛ {n}{Γ}{Z}{(Z ⇒ A) ⇒ ((Y ⇒ A) ⇒ X ⇒ A) ⇒ A}(ƛ {succ n}{Γ ’ Z}{Z ⇒ A}{((Y ⇒ A) ⇒ X ⇒ A) ⇒ A}(ƛ{succ (succ n)}{Γ ’ Z ’ (Z ⇒ A)}{(Y ⇒ A) ⇒ X ⇒ A}(ν {succ (succ (succ n))}{Γ ’ Z ’ (Z ⇒ A) ’ ((Y ⇒ A) ⇒ X ⇒ A)}(succ zero) · ν {succ (succ (succ n))} {Γ ’ Z ’ (Z ⇒ A) ’ ((Y ⇒ A) ⇒ X ⇒ A)} (succ (succ zero)))))

-- To be sure:

data _≡_ {X : Set} : X → X → Set where
  refl : {x : X} → x ≡ x

η-η'-the-same : {X Y Z A : type} {n : ℕ} {Γ : Cxt n} → η {X} {Y} {Z} {A} {n} {Γ} ≡ η'  {X} {Y} {Z} {A} {n} {Γ}
η-η'-the-same = refl


-- This works fine. Now change the above import to FinitePowers'.

-- Then everything up to η type-checks, but the definition of η
-- fails with:

-- AgdaQuestion.agda:84,11-13
-- Refuse to construct infinite term by instantiating _125 to (_Γ_125
-- [ succ (succ zero) ] ⇒ _τ_127)
-- when checking that the expression ν₁ has type
-- T _Γ_125 (_Γ_125 [ succ (succ zero) ] ⇒ _τ_127)

-- If I replace:
--
-- η : {X Y Z A : type} {n : ℕ} {Γ : Cxt n} → T Γ (Z ⇒ D X Y Z A)
-- η = ƛ(ƛ(ƛ(ν ? · ν₂)))
--
-- I get the same error. Why?

-- If I delete η (and hence η-η'-the-same), then η' and the whole file type check.