Why won't the following Agda code typecheck?

Question

I'm new to Agda and am puzzled by this one.

open import Data.Vec
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Fin hiding (_+_ ; splitAt)
open import Data.Product
open import Relation.Binary.PropositionalEquality

difference : ∀ m (n : Fin m) → ∃ λ o → m ≡ toℕ n + o
difference zero ()
difference (suc m) zero = suc m , refl
difference (suc m) (suc n) with difference m n
difference (suc m) (suc n) | o , p1 = o , cong suc p1

takeFin : ∀ {A : Set} {m : ℕ} (n : Fin m) → Vec A m → Vec A (toℕ n)
takeFin {A} {m = m} n vec with difference m n
... | o , p rewrite p with splitAt (toℕ n) vec
... | xs , _ , _ = xs

The takeFin function gives the error message: m != lhs of type ℕ when checking that the type {m : ℕ} (n : Fin m) (o : ℕ) (p : m ≡ toℕ n + o) (lhs : ℕ) → lhs ≡ toℕ n + o → {A : Set} (vec : Vec A lhs) → Vec A (toℕ n) of the generated with function is well-formed

but the following functions do compile

takeFin' : ∀ {A : Set} {m : ℕ} (n : Fin m) → Vec A m → Vec A m
takeFin' {A} {m = m} n a vec with difference m n
... | o , p rewrite p with splitAt (toℕ n) vec
... | xs , ys , _ = xs ++ ys

takeFin'' : ∀ {A : Set} {m : ℕ} (n : Fin m) → A → Vec A m → Vec A (toℕ n)
takeFin'' {A} {m = m} n a vec = replicate a

Can anyone help me out?

user_8988486 · Answer

As new Agda users tend to do, you did complicate matters a lot more than you needed to. What you intend to prove can actually be done in a much simpler way, as follows:

open import Data.Vec
open import Data.Fin

takeFin : ∀ {a} {A : Set a} {m} {n : Fin m} → Vec A m → Vec A (toℕ n)
takeFin {n = zero} (x ∷ v) = []
takeFin {n = suc _} (x ∷ v) = x ∷ takeFin v

You should always try to write simple inductive proofs rather than using unnecessary intermediate lemmas.

As to why your version does not typecheck (it's not compilation, it's type checking) the reason lies in your rewrite call which is made on an element of m ≡ toℕ n + o while your goal is of type Vec A (toℕ n) and does not contain any occurrence of m. What you want to do instead is to transform the type of vec in your context, while rewrite only acts over the goal. Here is how I would make it work:

takeFin : ∀ {A : Set} {m} {n : Fin m} → Vec A m → Vec A (toℕ n)
takeFin {m = m} {n} vec with difference m n
... | _ , p = proj₁ (splitAt (toℕ n) (subst (Vec _) p vec))

It works but as you can see it is far less elegant (and it also requires the difference function that you defined) and, more importantly, it uses subst which is often discouraged.

As a side note, and mostly for fun, it's possible to make the function a bit more concise and elegant (but less understandable) as follows:

open import Function

takeFin : ∀ {A : Set} {m} {n : Fin m} → Vec A m → Vec A (toℕ n)
takeFin {n = n} = proj₁ ∘ (splitAt (toℕ n)) ∘ (subst (Vec _) (proj₂ (difference _ n)))

This version, while a lot more complicated to read, shows how powerful Agda is in inferring the values of parameters, as only n is explicitly given.

Why won't the following Agda code typecheck?

1 Answers