Attempt at deprecating inspect idiom

[MatthewDaggitt]

Attempts to fix #1580.

There's one small fly in the ointment and that's the following use in Data.List.NonEmpty

agda-stdlib/src/Data/List/NonEmpty.agda

Line 68 in 5ac8015

with p x | P.inspect p x | split p xs | flatten-split p xs

where I get the dreaded != w error below if I try and use with ... in instead. Had a hack at it for the last 15 minutes but no matter what I try, I can't seem to get rid of it. @gallais if you have a spare 10 minutes at some point any chance you could take a look?

p x != w of type Bool
when checking that the type
{A.a.1 : Level} {A : Set A.a.1} (p : A → Bool) (x : A)
(xs : List A) (w : Bool)
(w₁
 : List
   (List⁺ (Prod.Σ A (λ x₁ → T (p x₁))) ⊎
    List⁺ (Prod.Σ A (λ x₁ → T (not (p x₁)))))) →
List.foldr List._++_ []
(List.map
 Sum.[ (λ x₁ → proj₁ (head x₁) ∷ List.map proj₁ (tail x₁)) ,
 (λ x₁ → proj₁ (head x₁) ∷ List.map proj₁ (tail x₁)) ]
 w₁)
≡ xs →
List.foldr List._++_ []
(List.map
 Sum.[ (λ x₁ → proj₁ (head x₁) ∷ List.map proj₁ (tail x₁)) ,
 (λ x₁ → proj₁ (head x₁) ∷ List.map proj₁ (tail x₁)) ]
 (split p (x ∷ xs) | w | refl | w₁))
≡ x ∷ xs
of the generated with function is well-formed

If we can't fix it, then I'll have a go at rewriting the functions. They're currently not very compliant with the standard library style anyway as they mix both computations and proofs.

[gallais]

I think it's an upstream problem: it looks like the code doing abstraction is not handling with-in properly.
Self-contained:

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Sigma

filter : {A : Set} (p : A → Bool) →
         (xs : List A) → List (Σ A λ a → p a ≡ true)
filter p [] = []
filter p (x ∷ xs) with p x in eq
... | false = filter p xs
... | true  = (x , eq) ∷ filter p xs

map : {A B : Set} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

filter-filter : {A : Set} (p : A → Bool) → (xs : List A) →
                filter p (map fst (filter p xs)) ≡ filter p xs
filter-filter p [] = refl
filter-filter p (x ∷ xs) with p x
... | b = {!!}

[MatthewDaggitt]

Yet another bug found while trying to get this working: agda/agda#5818

In conclusion this definitely shouldn't be merged until these upstream issues are fixed...

[jamesmckinna]

Moving to Agda-2.6.2.2 appears to have fixed this.
Superseded by #1930 including renamed README.WithIn in place of README.Inspect.