Почему Agda выдает ошибку «ожидаемый: ℕ, фактический: ℕ»

Question

Когда я пишу следующую функцию - agda,

f : (A : Set) → (a : A) → ℕ
f ℕ n = n

Я ожидаю, что ошибка скажет, что я не указал все случаи.

Вместо этого я получаю эту ошибку:

Type mismatch:
expected: ℕ
actual: ℕ
when checking that the expression n
has type ℕ

Что здесь происходит?

Answer 1

В более новой версии Agda (я использую 2.5.4) вы получаете более информативную ошибку:

ℕ !=< ℕ of type Set
(because one is a variable and one a defined identifier)
when checking that the expression n has type ℕ

Проблема заключается в том, что шаблон определения функции (слева отзнак равенства) может состоять только из конструкторов, переменных и точечных рисунков, но не таких типов, как ℕ.Поскольку ℕ не является допустимым шаблоном, Agda предполагает (возможно, сбивает с толку), что это новая переменная с именем ℕ типа Set, таким образом, скрывая фактический тип ℕ натуральных чисел.Теперь ошибка имеет смысл, поскольку тип n (который является ℕ переменной) не равен ожидаемому типу возврата (который является типом ℕ натуральных чисел).