<div dir="ltr"><div dir="ltr"><div dir="ltr"><br></div><div>No, there is no way to enforce this dependency, so you have bind P manually. Generalisable variables would be quite awkward to use if they weren't generalised in type signatures for other variables.<br></div><div dir="ltr"><br></div><div>See this section of the user manual for more details:</div><div><br></div><div dir="ltr"><a href="https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html#nested-generalization">https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html#nested-generalization</a><br></div></div><div><br></div><div>/ Ulf<br></div><div dir="ltr"><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Mar 26, 2019 at 1:07 PM Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com">matthewdaggitt@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><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>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div></div></div>