[Agda] no longer type checks

[Andreas Abel]

On 19.12.12 6:30 PM, Nils Anders Danielsson wrote:
> 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.)

Right.  But what I meant is that not all these constructor parameters 
should be taken into account, only those that share common variables 
with indices in the type of the constructor.

So 1. we analyze the situation at the time of a data definition (which 
constructor parameters are to be treated as indices in 2. the pattern 
matching situation), and at 2. pattern matching time we analyse the 
index expressions taking into account constructor indices and 
constructor parameters counted as indices according to 1.

Almost a legal document now...

> 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.
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/