意外的宇宙級

Question

這裏是一個類似於在Data.List.All一個定義：

open import Data.Vec 

data All {α π} {A : Set α} (P : A -> Set π) : ∀ {n} -> Vec A n -> Set π where 
    []ₐ : All P [] 
    _∷ₐ_ : ∀ {n x} {xs : Vec A n} -> P x -> All P xs -> All P (x ∷ xs) 

爲什麼All在於Set π？

Agda版本2.4.3。

Answer 1

Agda 2.4.2.4和Agda 2.4.2.5（維護分支）報告All住在Set π時的預期錯誤，但它被Agda 2.4.3（主分支）接受。

請在Agda bug tracker報告此問題。