[Agda] without-K problem

[Andreas Abel]

On 22.06.12 12:43 AM, Nils Anders Danielsson wrote:
> On 2012-06-20 14:00, Andreas Abel wrote:
>> On 20.06.2012 12:32, Altenkirch Thorsten wrote:
>>> On 20/06/2012 08:39, "Andreas Abel"<andreas.abel at ifi.lmu.de> wrote:
>>>> On 18.06.12 9:18 PM, Guillaume Brunerie wrote:
>
>>>>> For what it’s worth, I cannot reproduce the bug using the following
>>>>> definition of the identity types:
>>>>>
>>>>> data _≡_ {A : Set} : A → A → Set where
>>>>> refl : {x : A} → x ≡ x
>>>>>
>>>>> But I can reproduce it using the following definition (which is the
>>>>> one
>>>>> used in the standard library):
>>>>>
>>>>> data _≡_ {A : Set} (x : A) : A → Set where
>>>>> refl : x ≡ x
>>>>
>>>> Yes, it seems --without-K should also forbid data definitions where a
>>>> parameter variable ("x") is free in a index position.
>>>>
>>>> Otherwise, index variables can be "hidden" in parameter positions and
>>>> are not spotted by --without-K when it checks whether a split is legal.
>
> Yes, the problem is that constructors are not applied to their
> parameters. We can fix the problem in several ways:
>
> * Don't allow any constructors: force the indices to be distinct
> variables that are not free in the parameters. I tried this once, and
> found it rather crippling.
>
> * Only allow constructors from parameter-free data types (natural
> numbers but not lists). This is easy to implement, but also quite
> annoying.
>
> * Reconstruct the parameters when applying the check. This sounds like
> the way to go. Is there some kind of parameter-reconstructing function
> somewhere in the code base?

You need to know the type t of the constructor application c vs 
(basically a pattern), then you can get hold of the parameters quite easily.

In your case t is the split type, and it must be of the form d us.  Thus 
you have typing

    c vs : d us

and the parameters of c are just

   take conPars us.

Further, you can without much effort determine the types ti of the 
regular constructor arguments vi to continue recursively.

It should not be hard to extend your function wellformedIndices to 
incorporate the type t of the pattern.

Cheers,
Andreas

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