Agda – difference between type args on the left and right side of the colon

Question

Following definition compiles and behaves well:

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

However this one does not compile:

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

because

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

I don't understand why they aren't equivalent. What's the difference and why the second variant is not correct?

Answer 1

The arguments on the left of the colon are called parameters; those on the right are called indices. The difference between the two is this: In the return type of the data type's constructors, the parameters must always be exactly the variables from the type declaration. The indices, on the other hand, can be arbitrary terms (of the correct type).

In your second example, the return type of refl is Eq x x. However, y is a parameter, so the return type would have to be Eq x y. In your first example, the type of refl is legal because y is an index and x is a term of type A.

By 'return type' I mean the expression to the right of the last arrow in a constructor's type. To illustrate, here is the definition of length-indexed lists aka vectors:

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

data Vec (A : Set) : ℕ → Set where
  [] : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

The return type of _∷_ is Vec A (suc n). Again, suc n is an arbitrary expression of type ℕ. If the data type occurs in the type of an argument of a constructor, as with the Vec A n argument to _∷_, both the parameters and the indexes can be arbitrary terms (though we use the same parameter here).

When you pattern match on an indexed data type, the constructor's index can give you additional information. Consider head on vectors:

head : ∀ {A n} → Vec A (suc n) → A
head (x ∷ xs) = x

We don't need to write an equation for the constructor [] because its type is Vec A zero whereas the type of the pattern is Vec A (suc n) and these types cannot be equal. Similarly, consider the following proof that your equality is symmetric:

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

sym : {A : Set} (x y : A) → Eq x y → Eq y x
sym x .x refl = refl

By pattern matching on refl, we learn that y is, in fact, x. This is indicated by the dot pattern .x. Thus, our goal becomes x ≡ x, which can be proven with refl again. More formally, x is unified with y when we match on refl.

You might wonder whether you should simply declare all arguments of a data type as indices. I believe that in Agda, there's no downside to doing so, but it's good style to declare arguments as parameters if possible (since these are simpler).

Related: section of the Agda manual; SO question with more examples.