[Agda] no longer type checks

Nils Anders Danielsson nad at chalmers.se
Wed Dec 19 18:30:02 CET 2012


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


More information about the Agda mailing list