Несоответствие уровня в Агде

Question

Некоторые входы:

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

Эта функция создает тип функции из вектора типов и типа результата:

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

Это два комбинатора из статьи Arity-Generic Datatype-Generic Programming:

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))

Некоторые действительные определения:

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₂

И даже:

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₃

Но это не проверка типа:

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₃

Ошибка:

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))

В чем проблема?

Answer 1

Нет проблем, код, который вы написали, действительно действителен. Похоже, что более старые версии Agda испытывают трудности с его принятием (конечно, ноябрьская версия разработки), но в текущей версии разработки она работает нормально.

Кажется, что унификации не совсем могут понять, что и где, поэтому, если вы захотите немного помочь, вы можете заставить их проверять тип даже в старых версиях:

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₃ {_} {γ})