[Agda] no longer type checks

[Andreas Abel]

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/