Change in definition of Data.List.Base.filter etc. result in new unsolved metas in proofs

[MatthewDaggitt]

The definition of filter etc got changed to be defined in terms of the boolean test rather than a decidable predicate. Several problems have resulted:

1. Firstly this is not documented in the CHANGELOG
2. This has lead to many of the proofs not being able to infer their list argument. In particular filter-accept and filter-reject in Data.List.Properties now need their xs parameter to be passed explicitly.

We should check all functions which have been redefined similarly.

[jamesmckinna]

git blame offers this commit as the offending one, which seems to have touched all the functions in the same way.

[jamesmckinna]

Do you have examples of eg failing client code/tests? The usual make test cycle (locally, and on GitHub) doesn't show this issue up, it seems.

[MatthewDaggitt]

For example, these two are failing in my own code base:

https://github.com/MatthewDaggitt/agda-routing/blob/ee065c039ee0b677ff5651f433d2dcf20311d044/RoutingLib/lmv34/Synchronous/Gamma_one/Properties.agda#L230

https://github.com/MatthewDaggitt/agda-routing/blob/ee065c039ee0b677ff5651f433d2dcf20311d044/RoutingLib/lmv34/Synchronous/Gamma_one/Properties.agda#L233

The usual make test cycle (locally, and on GitHub) doesn't show this issue up, it seems.

Yes, I suspect we don't actually ever use any of the filter lemmas in the library? I can't think of anywhere we do.

[jamesmckinna]

Indeed, there are no uses in the library. I'm curious as to how they might have typechecked under the old definitions, unless those had explicit quantification, and somewhere along the line, we made the explicit->implicit 'mistake'...?

A better/more precise question: what is the last version of the library that those proofs did check under?

[MatthewDaggitt]

Ah I remember why I defined the predicate versions in terms of the boolean ones. Because in order to convert from boolean to decidable predicates you need to use T? from Data.Bool.Properties in Data.List.Base, which violates our dependency management convention that we never import Properties modules from Base modules....

[jamesmckinna]

Well... see previous discussion about moving that operator to Relation.Nullary.Decidable.Core... ;-)

[jamesmckinna]

Re: your opening comment

Has the behaviour of filter-accept and filter-reject now reverted to the previous (implicit quantification) behaviour as a consequence of #2186 ?

Apologies: I suppose that it must be the case, because the tests pass (sic)...?

[MatthewDaggitt]

Yes, that is the case 👍