[Agda] function application in index positions

[Peter Divianszky]

Hi,

Currently it is not easy to deal with function application in index 
positions.

For example, given

\begin{code}
open import Data.Nat
open import Relation.Nullary

data Even : ℕ → Set where
   double : ∀ n → Even (n + n)

emptinessProof : ¬ Even 1
emptinessProof e = {!!}
\end{code}

it is not trivial to fill in the hole.

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?

Thanks,

Peter