[Agda] How to enforce dependencies between generalised variables

[Matthew Daggitt]

Dear all,
 I'm trying out the new `variable` feature and am having some trouble
enforcing dependencies between generalised variables. I'm trying to
generalise the implicit variables in the following function type:
```
filter : ∀ {a} {A : Set a} {P : Pred A p} → Decidable P → List A → List A
```
My attempt at doing so is as follows:
```
variable
  a p : Level
  A : Set a
  P : Pred A p

filter : Decidable P → List A → List A
filter P? [] = []
filter P? (x ∷ xs) with P? x
... | no  _ = filter P? xs
... | yes _ = x ∷ filter P? xs
```
The problem is that slightly confusingly the `A` used implicitly in `P :
Pred A p` is generalised separately from the `A` used in `List A` and so
you get the following error
```
A !=< P.A of type (Set A.a) when checking that the expression x has type P.A
```
at `with P? x` in the definition.

Removing `A : Set a` from the `variable` declaration obviously doesn't work
as then the `A` in the variable declaration for `P` isn't defined.

Is there a way of doing this?
Many thanks,
Matthew
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190326/46c6957c/attachment.html>