<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Dear all,<br><div> 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:</div><div>```</div><div>filter : ∀ {a} {A : Set a} {P : Pred A p} → Decidable P → List A → List A<br></div><div>```</div><div>My attempt at doing so is as follows:</div><div><div>```</div><div>variable</div><div>  a p : Level</div><div>  A : Set a</div><div>  P : Pred A p</div></div><div><br></div><div><div>filter : Decidable P → List A → List A</div><div>filter P? [] = []</div><div>filter P? (x ∷ xs) with P? x</div><div>... | no  _ = filter P? xs</div><div>... | yes _ = x ∷ filter P? xs</div></div><div>```</div><div>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</div><div>```</div><div><div>A !=< P.A of type (Set A.a) when checking that the expression x has type P.A</div></div><div>```</div><div>at `with P? x` in the definition.</div><div><br></div><div>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.</div><div><br></div><div>Is there a way of doing this?</div><div>Many thanks,<br>Matthew</div></div></div></div></div></div>