agda - Agda – 冒号左侧和右侧类型 args 的区别

Question

以下定义编译并表现良好：

data Eq {lvl} {A : Set lvl} (x : A) : A → Set where
  refl : Eq x x

然而，这个不编译：

data Eq {lvl} {A : Set lvl} (x : A) (y : A) : Set where
  refl : Eq x x

因为

x != y of type A
when checking the constructor refl in the declaration of Eq

我不明白为什么它们不相等。有什么区别以及为什么第二个变体不正确？

Answer 1