Less restrictive --without-K [Re: [Agda] no longer type checks]

[Andreas Abel]

I implemented the ideas below to make --without-K less restrictive. 
Maybe the pendulum has to swing back after this once more.

1. Big parameters are now ignored.

    Big are those that are in the same universe than the data type or 
higher.  Size prevents information to flow from these parameters into 
the type.

2. Non-linear parameters are treated just as indices.

   This means that Id1 and Id2 are no longer distinguished in the analysis.

Hope this helps.

Cheers,
Andreas

On 14.12.12 11:42 AM, Andreas Abel wrote:
> For background on the new implementation of --without-K, see the thread
>
>    without-K problem
>
> on this list.  Thorsten had observed that with Agda 2.3.0, a weak
> version of K was provable for the identity type given by
>
>    data Id1 (X : Set)(x : X) : X -> Set where
>      refl : Id1 X x x
>
> Guillaume Brunerie observed that this is not possible for the version
>
>    data Id2 (X : Set) : X -> X -> Set where
>      refl : (x : X) -> Id2 X x x
>
> The difference between Id1 and Id2 is that for Id2, there is only one
> index (x) and two parameters (X,x), but Id2 has one parameter (X) and
> two indices (x,x).  The old --without-K check was that during matching,
> the indices should not have common free variables, because by the
> non-linearity one could get K.  For Id1, the non-linear nature of
> indices is hidden by the fact that only the second argument of type X is
> declared as an index.  For Id2, the non-linearity is obvious.
>
> Nisse's rectification of the situation was to treat *all* parameters as
> indices, to reveal hidden non-linearity situations.  I think he went one
> step to far, as your example shows.  Your lemma gets rejected because it
> uses two constructors of the disjoint sum type which naturally share the
> type parameters of the disjoint sum type.
>
> I think in the calculation of the "critical variables", i.e., those that
> need to be all distinct, only those parameters of a constructor should
> be taken into account that have common variables with one of the
> indices.  To state that in the mentioned examples,
>
>    - for the disjoint sum type, no parameter should be counted as index
>
>    - for the type Id1, only x, but not X should be counted as index
>
> Might be worth to add this to the bug tracker...
>
> Cheers,
> Andreas
>
>
> On 13.12.12 10:16 PM, Martin Escardo wrote:
>> This
>>
>> lemma : in₀ x ≡ in₁ y → ⊥
>> lemma ()
>>
>> used to compile, where "in" are the injections into X + Y.
>>
>> Now I get, in 2.3.2,
>>
>> "The variables
>>    .X₁
>>    .Y₁
>>    x₁
>>    .X₁
>>    .Y₁
>>    y₁
>> in the indices
>>    in₀ x₁
>>    in₁ y₁
>> are not distinct (note that parameters count as constructor
>> arguments)
>> when checking that the clause lemma () has type in₀ x ≡ in₁ y → ⊥"
>>
>> Is that intended behaviour?
>>
>> What would be the easiest solution to make this lemma work?
>>
>> Thanks,
>> Martin
>>
>

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