<div dir="ltr">Okay, well at least I know to stop looking! Cheers Gallais that's a neat work around (although it'll get a little cumbersome for deeper dependencies).<div><br></div><div>Thanks both for the quick reply!<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Mar 26, 2019 at 8:33 PM Guillaume Allais <<a href="mailto:guillaume.allais@ens-lyon.org">guillaume.allais@ens-lyon.org</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">Alternatively you can pass `A` explicitly to `Decidable` like we often<br>
do for `Decidable _≡_`. This way you tell Agda that P's domain and A<br>
should be the same. This gives us:<br>
<br>
```<br>
open import Level<br>
open import Data.List.Base hiding (filter)<br>
open import Relation.Unary<br>
open import Relation.Nullary<br>
<br>
variable<br>
  a p : Level<br>
  A : Set a<br>
  P : Pred A p<br>
<br>
filter : Decidable {A = A} P → List A → List A<br>
filter P? [] = []<br>
filter P? (x ∷ xs) with P? x<br>
... | no  _ = filter P? xs<br>
... | yes _ = x ∷ filter P? xs<br>
```<br>
<br>
Cheers,<br>
gallais<br>
<br>
On 26/03/2019 12:27, Ulf Norell wrote:<br>
> No, there is no way to enforce this dependency, so you have bind P<br>
> manually. Generalisable variables would be quite awkward to use if they<br>
> weren't generalised in type signatures for other variables.<br>
> <br>
> See this section of the user manual for more details:<br>
> <br>
> <a href="https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html#nested-generalization" rel="noreferrer" target="_blank">https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html#nested-generalization</a><br>
> <br>
> / Ulf<br>
> <br>
> On Tue, Mar 26, 2019 at 1:07 PM Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com" target="_blank">matthewdaggitt@gmail.com</a>><br>
> wrote:<br>
> <br>
>> Dear all,<br>
>>  I'm trying out the new `variable` feature and am having some trouble<br>
>> enforcing dependencies between generalised variables. I'm trying to<br>
>> generalise the implicit variables in the following function type:<br>
>> ```<br>
>> filter : ∀ {a} {A : Set a} {P : Pred A p} → Decidable P → List A → List A<br>
>> ```<br>
>> My attempt at doing so is as follows:<br>
>> ```<br>
>> variable<br>
>>   a p : Level<br>
>>   A : Set a<br>
>>   P : Pred A p<br>
>><br>
>> filter : Decidable P → List A → List A<br>
>> filter P? [] = []<br>
>> filter P? (x ∷ xs) with P? x<br>
>> ... | no  _ = filter P? xs<br>
>> ... | yes _ = x ∷ filter P? xs<br>
>> ```<br>
>> The problem is that slightly confusingly the `A` used implicitly in `P :<br>
>> Pred A p` is generalised separately from the `A` used in `List A` and so<br>
>> you get the following error<br>
>> ```<br>
>> A !=< P.A of type (Set A.a) when checking that the expression x has type<br>
>> P.A<br>
>> ```<br>
>> at `with P? x` in the definition.<br>
>><br>
>> Removing `A : Set a` from the `variable` declaration obviously doesn't<br>
>> work as then the `A` in the variable declaration for `P` isn't defined.<br>
>><br>
>> Is there a way of doing this?<br>
>> Many thanks,<br>
>> Matthew<br>
>> _______________________________________________<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>
>><br>
> <br>
> <br>
> _______________________________________________<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>
> <br>
<br>
</blockquote></div>