[Agda] no longer type checks
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Dec 14 11:42:40 CET 2012
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/
More information about the Agda
mailing list