[Agda] Eta reduction of a function argument in a where block

[Wojciech Jedynak]

Hello everybody!

I have been playing with Martin-Loef's W-types and I noticed a strange
Agda behavior while using the recursor for W-flavored naturals.
I think that in one of the cases in the code below, a function defined
in a where block receives an additional parameter when it's not
supposed to.

I'm sorry that the code is a big long.
The gist is that the function toℕ defined in modules Inside behaves
differently from the one from the InsideEta and Outside modules.

Greetings,
Wojciech Jedynak

\begin{code}

module WTypes where

open import Data.Nat
open import Data.Empty
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality

-- We define W-types and a recursor on them.

data W : (A : Set) → (B : A → Set) → Set₁ where
  sup : {A : Set} {B : A → Set}
      → (a : A) → (B a → W A B) → W A B

wrec : {A : Set}
     → {B : A → Set}
     → (C : W A B → Set)
     → (d : (x : A)
          → (y : B x → W A B)
          → ((z : B x) → C (y z))
          → C (sup x y))
     → (w : W A B)
     → C w
wrec C d (sup a b) = d a b (λ z → wrec C d (b z))

-----------------------
--  Natural numbers  --
-----------------------

data nat-cs : Set where
  Z S : nat-cs

nat-record : nat-cs → Set
nat-record Z = ⊥
nat-record S = ⊤

nat : Set₁
nat = W nat-cs nat-record

n-zero : nat
n-zero = sup Z ⊥-elim

n-suc : nat → nat
n-suc n = sup S (λ top → n)

\end{code}

To see if the above definition is "correct" we want to
write convertions between ℕ and nat types, and prove them correct.

Whether we can actually do the proof seems to depend on
some cosmetic changes!

Suppose we write:

\begin{code}

fromℕ : ℕ → nat
fromℕ zero    = n-zero
fromℕ (suc n) = n-suc (fromℕ n)

-- with iter in a where block

module Inside where

  toℕ : nat → ℕ
  toℕ n = wrec _ iter n module TN where
    iter : (x : nat-cs)
         → (nat-record x → nat)
         → (nat-record x → ℕ)
         → ℕ
    iter Z _ rec = 0
    iter S _ rec = 1 + rec tt

module InsideEta where

  toℕ : nat → ℕ
  toℕ = wrec _ iter module TN where
    iter : (x : nat-cs)
         → (nat-record x → nat)
         → (nat-record x → ℕ)
         → ℕ
    iter Z _ rec = 0
    iter S _ rec = 1 + rec tt

module Outside where
  iter : (x : nat-cs)
       → (nat-record x → nat)
       → (nat-record x → ℕ)
       → ℕ
  iter Z _ rec = 0
  iter S _ rec = 1 + rec tt

  toℕ : nat → ℕ
  toℕ n = wrec _ iter n

\end{code}

We want to prove that toℕ (fromℕ n) ≡ n, for all n : ℕ,
but it seems possible only in the second and third case!

\begin{code}

lem : ∀ (n : ℕ) → Inside.toℕ (fromℕ n) ≡ n
lem zero = refl
lem (suc n) with lem n
... | rec = {!!} --cong suc rec

lem2 : ∀ (n : ℕ) → InsideEta.toℕ (fromℕ n) ≡ n
lem2 zero = refl
lem2 (suc n) with lem2 n
... | rec = cong suc rec

lem3 : ∀ (n : ℕ) → Outside.toℕ (fromℕ n) ≡ n
lem3 zero = refl
lem3 (suc n) with lem3 n
... | rec = cong suc rec

\end{code}

When we write 'cong suc rec' in the goal in lem, we get an error:

  fromℕ n != sup S (λ top → fromℕ n) of type W nat-cs nat-record
  when checking that the expression cong suc rec has type
  suc (wrec (λ n → ℕ) (TN.iter (sup S (λ top → fromℕ n))) (fromℕ n)) ≡ suc n

the context in the goal is:

  Goal: suc (wrec (λ n' → ℕ) (TN.iter (sup S (λ top → fromℕ n))) (fromℕ n))
      ≡ suc n
  ————————————————————————————————————————————————————————————
  rec : wrec (λ n' → ℕ) (TN.iter (fromℕ n)) (fromℕ n) ≡ n
  n   : ℕ

The strange thing is that Agda thinks that TN.iter from Inside depends on
the nat argument of toℕ.

Everything works in lem2 and lem3. The context is

  Goal: suc (wrec (λ w → ℕ) TN.iter (fromℕ n)) ≡ suc n
  ————————————————————————————————————————————————————————————
  rec : wrec (λ w → ℕ) TN.iter (fromℕ n) ≡ n

EOF