AGDA如何解决错误：无法求解以下约束

Question

此代码有什么问题？

编辑： 我正在发送所有代码，包括依赖关系，导入，标志等。

我无法弄清楚该错误可能在哪里。如果有人可以指导我如何解决此错误，我将非常感激。

{-#  OPTIONS --type-in-type --without-K  #-}

module Basic where

Type = Set

data Path {A : Type} : A → A → Type where
  id : {M : A} → Path M M

_≃_ : {A : Type} → A → A → Type
_≃_ = Path

infix 9 _≃_

ap :  {A B : Type} {M N : A}
      (f : A → B) → Path{A} M N → Path{B} (f M) (f N)
ap f id = id

ap≃ : ∀ {A} {B : A → Type} {f g : (x : A) → B x} 
      → Path f g → {x : A} → Path (f x) (g x)
ap≃ α {x} = ap (\ f → f x) α

postulate 
   λ≃  : ∀ {A} {B : A → Type} {f g : (x : A) → B x}
      → ((x : A) → Path (f x) (g x)) 

我遇到了这个错误：

Failed to solve the following constraints:
  Has bigger sort: _44
  piSort _25 (λ _ → Set) = Set
  Has bigger sort: _25

有帮助吗？

Answer 1

我没有遇到完全相同的错误，但是我通过注释a使用类型type在λ≃的类型中进行检查。 ：

postulate
   λ≃  : ∀ {A : Type} {B : A → Type} {f g : (x : A) → B x}
      → ((x : A) → Path (f x) (g x))

我看到的错误是因为AGDA通常会假设您可能要使用宇宙多态性，并且在λ≃类型中碰巧没有其他约束a 到最低的Universe 类型。