How to write a type signature with two parameters?

Question

I try to learn agda and use the tutorial. I paste code for two mutally recursive sets

module MoreSets where 

data List₁ (A B : Set) : Set
data List₂ (A B : Set) : Set

data List₁ (A B : Set) where
  []  :                 List₁ A B
  _∷_ : A → List₂ A B → List₁ A B

data List₂ (A B : Set) where
  _∷_ : B → List₁ A B → List₂ A B

and get the error

MoreSets.agda:6,12-23
Unexpected type signature for parameters A B
when checking the definition of List₁

I assume a trivial error but cannot see it.

What is a simple tutorial to learn agda for a Haskell programmer which does not go deep into category theory?

Answer 1

You're not supposed to repeat the type annotations that you had in the declarations when you're defining the inductive type. So:

module MoreSets where

data List₁ (A B : Set) : Set
data List₂ (A B : Set) : Set

data List₁ A B where
  []  :                 List₁ A B
  _∷_ : A → List₂ A B → List₁ A B

data List₂ A B where
  _∷_ : B → List₁ A B → List₂ A B