等級不匹配

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 

這是從元數 - 通用數據類型 - 通用2個組合子編程紙：

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無法接受它（11月份的開發版肯定會這樣做），但它在當前的開發版本中工作正常。

似乎unifications不能完全弄清楚什麼去的地方，所以如果你願意幫助這一點，你可以把它的類型檢查，即使在舊版本：

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