[Agda] no longer type checks

[Nils Anders Danielsson]

On 2012-12-14 11:42, Andreas Abel wrote:
> Nisse's rectification of the situation was to treat *all* parameters
> as indices, to reveal hidden non-linearity situations.

I don't think this is correct. If the /indices/ contain constructors,
then the constructor parameters are reconstructed and treated as part of
the index expressions. (Constructor parameters are usually not part of
terms.)

The full rule, as described in the release notes for Agda 2.3.2:

   If the flag is activated, then Agda only accepts certain
   case-splits. If the type of the variable to be split is D pars ixs,
   where D is a data (or record) type, pars stands for the parameters,
   and ixs the indices, then the following requirements must be
   satisfied:

   * The indices ixs must be applications of constructors (or literals)
     to distinct variables. Constructors are usually not applied to
     parameters, but for the purposes of this check constructor
     parameters are treated as other arguments.

   * These distinct variables must not be free in pars.

-- 
/NAD