[Agda] How to enforce dependencies between generalised variables

[Ulf Norell]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190326/d0eb06d6/attachment.html>