[Agda] Type checker changes its mind

[Coquand]

> such as these (and other IR) definitions, at least `what goes on'.  (I
> vaguely remember Thierry saying (sometime in the late 20'th century)
> that it is in two passes, where first you check the types of the
> definitions, and then second you check the bodies -- but I would like
> something to refer to when I run into the issue.)
>

 For type-checking the system of equations

  x1 : A1 = a1(x1,...,xn)
  x2 :A2(x1) = a2(x1,...,xn)
 ...
  xn :An(x1,...,x(n-1)) = an(x1,...,xn)

first one type-check

 Gamma = x1:A1, x2:A2(x1),...,xn:An(x1,...,x(n-1))

and then

 a1:A1 [Gamma]
 ...
 an:An [Gamma]

so that the map (x1,...,xn) |--> (a1,...,an) is a map from Gamma to Gamma,
and one takes the least fixedpoint of this map to have the solution of the
system of mutual equations.

                  Thierry