[ deprecate ] Relation/Binary.PropositionalEquality.inspect (#1580 / #1630 / #1930 redux)

[jamesmckinna]

Fixes #1580 see the discussion there and on the previous attempts #1630 #1930.
CHANGELOG based on text from #1930

NB

• This does not touch the Relation/Binary.HeterogeneousEquality.* modules, which should be tackled in a separate PR, once we can agree how best to deal with them.
• As with [ deprecate ] README.Inspect #2928 (on which this PR is blocking ;-)) forward pointers to documentation of the Agda v2.9.0 release.

UPDATED: added CHANGELOG, but cancelled most recent make test to save cycles.

[jamesmckinna]

I further experimented with the following 'alternative' (well: hardly!) design, which is less dramatic, but does achieve (by the back door) deprecation of the bugbear [_] constructor:

module Graph {A : Set a} {B : A → Set b} (f : (x : A) → B x) (x : A) where

  record View (y : B x) : Set (a ⊔ b) where
    field fx≡y : f x ≡ y

  view : View (f x)
  view .View.fx≡y = refl

  pattern [_] eq = record { fx≡y = eq } -- can be omitted?

-- Version 2.4

module _ {A : Set a} {B : A → Set b} where

  Reveal_·_is_ : (f : (x : A) → B x) (x : A) (y : B x) → Set (a ⊔ b)
  Reveal f · x is y = Graph.View f x y

  inspect : (f : (x : A) → B x) (x : A) → Reveal f · x is f x
  inspect = Graph.view
  {-# WARNING_ON_USAGE inspect
  "Warning: inspect was deprecated in v2.4.
  Please use Graph.view instead. "
  #-}
  {-# WARNING_ON_USAGE Reveal_·_is_
  "Warning: Reveal_·_is_ was deprecated in v2.4.
  Please use Graph.View instead. "
  #-}

That way we still retain a useful notion (the graph relation associated with a function, cf. my comment on #2909; this is Conor's Im f family from their later papers about DTFP/views/Epigram, in disguise), while omitting

• the problematic constructor (well, not at present with the pattern synonym?)
• the mumbo-jumbo associated with the names Reveal and inspect, which I have always considered part of a different, cognitive/discoverability, problem.

Perhaps the thing to do is to lift this out to a separate module, or else in Relation.Binary.Definitions?