[Agda] function application in index positions

[Peter Divianszky]

On 02/04/2013 06:17 PM, Andreas Abel wrote:
> On 01.02.2013 21:32, Peter Divianszky wrote:
>
>> data Even : ℕ → Set where
>>    double : ∀ n → Even (n + n)
>
> I think non-pattern indices like this one should be forbidden in the
> first place.  Instead you should have to write
>
>    data Even (m : N) : Set where
>      double : forall n -> (n + n == m) -> Even m

 From a practical viewpoint, isn't the first data definition is more 
compact having exactly the same semantics?


>> Is this documented / should I open a ticket?
>
> I think the current liberty leads people to believe the type checker
> could handle arbitrary indices, which is not true and leads to error
> messages which are harder to understand than an outright
>
>    "double's type is illegal because the unification problem
>
>       n + n == expression
>
>     is not solvable in general"

A better error message would help a lot!


Cheers,

Peter