Andreas, thanks for the answer, I now understand the problem.
> the index A appears as variable, so it could be treated like a parameter.
Since Agda already knows that when performing universe checking, maybe
it's not hard to implement this for positivity checking too? And
enable by something like {-# OPTIONS --indices-variance #-}.