CODEWITHSUNDEEP
agdadependent-type
while1fork
while1fork

Reputation: 374

Why does Agda give error "expected: ℕ, actual: ℕ"

When I write the following function is agda,

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

I expect the error to say that I have not specified all cases.

Instead, I get this error:

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

What is going on here?

Upvotes: 1

Views: 233

Answers (1)

Jesper
Jesper

Reputation: 2965

With a more recent version of Agda (I'm using 2.5.4) you get a more informative error:

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

The problem is that the pattern of a function definition (on the left of the equals sign) can consist of only constructors, variables, and dot patterns, but not types such as ℕ. Since ℕ is not a valid pattern, Agda assumes (perhaps confusingly) that it is a new variable called ℕ of type Set, thus shadowing the actual type ℕ of natural numbers. Now the error makes sense, since the type of n (which is ℕ the variable) is not equal to the expected return type (which is the type ℕ of natural numbers).

Upvotes: 6

Related Questions