Level mismatch in Agda

Question

Some inputs:

module error where
  open import Data.Nat as ℕ
  open import Level
  open import Data.Vec
  open import Data.Vec.N-ary

This function constructs a function type from vector of types and result type:

N-Ary-from-Vec : {α γ : Level} {l : ℕ} -> Vec (Set α) l -> Set γ -> Set (N-ary-level α γ l)
N-Ary-from-Vec   []      Z = Z
N-Ary-from-Vec  (X ∷ Xs) Z = X -> N-Ary-from-Vec Xs Z

This is two combinators from the Arity-Generic Datatype-Generic Programming paper:

v∀⇒ : {n : ℕ} {α β : Level} {A : Set α} 
    -> (Vec A n -> Set β) 
    -> Set (N-ary-level α β n)
v∀⇒ {0}       B = B []
v∀⇒ {ℕ.suc n} B = ∀ {x} -> v∀⇒ (λ xs -> B (x ∷ xs))

vλ⇒ : {n : ℕ} {α β : Level} {A : Set α} {B : Vec A n -> Set β} 
    -> ((xs : Vec A n) -> B xs) 
    -> v∀⇒ B
vλ⇒ {0}       f = f []
vλ⇒ {ℕ.suc n} f = λ {x} -> vλ⇒ (λ xs -> f (x ∷ xs))

Some valid definitions:

ok₁ : {α γ : Level} {Z : Set γ} {l : ℕ}
    -> (Xs : Vec (Set α) l)
    -> N-Ary-from-Vec Xs Z
    -> N-Ary-from-Vec Xs Z
ok₁ = {!!}

ok₁' : {α γ : Level} {Z : Set γ}
     -> (l : ℕ)
     -> v∀⇒ (λ (Xs : Vec (Set α) l)
               -> N-Ary-from-Vec Xs Z
               -> N-Ary-from-Vec Xs Z)
ok₁' l = vλ⇒ {l} ok₁

ok₂ : {α γ : Level} {Z : Set γ} {l : ℕ}
    -> (Xs : Vec (Set α) l)
    -> N-Ary-from-Vec Xs (N-Ary-from-Vec Xs Z)
ok₂ = {!!}

ok₂' : {α γ : Level} {Z : Set γ}
     -> (l : ℕ)
     -> v∀⇒ (λ (Xs : Vec (Set α) l)
               -> N-Ary-from-Vec Xs (N-Ary-from-Vec Xs Z))
ok₂' l = vλ⇒ {l} ok₂

And even:

ok₃ : {α γ : Level} {Z : Set γ} {l : ℕ}
    -> (Xs : Vec (Set α) l)
    -> N-Ary-from-Vec Xs Z
    -> N-Ary-from-Vec Xs (N-Ary-from-Vec Xs Z)
ok₃ = {!!}

ok₃' : {α γ : Level} {Z : Set γ}
     -> (l : ℕ)
     -> {x1 x2 x3 : Set α}
     -> N-Ary-from-Vec (x1 ∷ x2 ∷ x3 ∷ []) Z
     -> N-Ary-from-Vec (x1 ∷ x2 ∷ x3 ∷ []) (N-Ary-from-Vec (x1 ∷ x2 ∷ x3 ∷ []) Z)
ok₃' l = vλ⇒ {3} ok₃

But this doesn't typecheck:

error' : {α γ : Level} {Z : Set γ}
       -> (l : ℕ)
       -> v∀⇒ (λ (Xs : Vec (Set α) l)
               -> N-Ary-from-Vec Xs  Z
               -> N-Ary-from-Vec Xs (N-Ary-from-Vec Xs Z))
error' l = vλ⇒ {l} ok₃

Error:

N-ary-level .α (_γ_183 l) l != .γ of type Level
when checking that the expression vλ⇒ {l} ok₃ has type
v∀⇒
 (λ Xs →
    N-Ary-from-Vec Xs .Z → N-Ary-from-Vec Xs (N-Ary-from-Vec Xs .Z))

What's the problem?

Answer 1

There's no problem, the code you wrote is actually valid. Looks like older versions of Agda have trouble accepting it (development version from November certainly does), but it works fine in current development version.

It seems that unifications can't quite figure out what goes where, so if you are willing to help it a bit, you can get it to type check even in the older versions:

error' : {α γ : Level} {Z : Set γ}
       -> (l : ℕ)
       -> v∀⇒ (λ (Xs : Vec (Set α) l)
               -> N-Ary-from-Vec Xs  Z
               -> N-Ary-from-Vec Xs (N-Ary-from-Vec Xs Z))
error' {_} {γ} l = vλ⇒ {l} (ok₃ {_} {γ})