意外的宇宙级

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报告此问题。