[Agda] no longer type checks

[Martin Escardo]

Thanks, Andreas. This is a helpful explanation.

I think that maybe it is an open research question what kind of pattern 
matching corresponds to (intensional) MLTT (without the K axiom). That 
should be interesting to know for sure. But I am glad that there is some 
preliminary experimental work in Agda going on.

Best,
Martin

On 14/12/12 10:42, 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
>>
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe