[Agda] function application in index positions

[Andreas Abel]

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

> emptinessProof : ¬ Even 1
> emptinessProof e = {!!}
>
> it is not trivial to fill in the hole.

Then you get the goal

   emptynessProof (double n p) = ?

of deriving a contradiction from

   p : n + n == 1

which can be done as Alan showed.

> Is it possible to improve to compiler to make this task simpler?
> I don't want to change the data definition.
>
> 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"

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/