[Agda] How to enforce dependencies between generalised variables

[Guillaume Allais]

Alternatively you can pass `A` explicitly to `Decidable` like we often
do for `Decidable _≡_`. This way you tell Agda that P's domain and A
should be the same. This gives us:

```
open import Level
open import Data.List.Base hiding (filter)
open import Relation.Unary
open import Relation.Nullary

variable
  a p : Level
  A : Set a
  P : Pred A p

filter : Decidable {A = A} P → List A → List A
filter P? [] = []
filter P? (x ∷ xs) with P? x
... | no  _ = filter P? xs
... | yes _ = x ∷ filter P? xs
```

Cheers,
gallais

On 26/03/2019 12:27, Ulf Norell wrote:
> 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.
> 
> See this section of the user manual for more details:
> 
> https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html#nested-generalization
> 
> / Ulf
> 
> On Tue, Mar 26, 2019 at 1:07 PM Matthew Daggitt <matthewdaggitt at gmail.com>
> wrote:
> 
>> 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
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190326/7b68a23d/attachment.sig>