[ 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?

[JacquesCarette]

I rather like the Graph relation. Yes, I think that should be available in stdlib somewhere (without the [_]).

[jamesmckinna]

I rather like the Graph relation. Yes, I think that should be available in stdlib somewhere (without the [_]).

Thanks for the endorsement. I realised that to try and work out a 'proper' design wrt arbitrary (indexed!) relations, and naming, was a bit beyond me (I have yet another wicked chest/throat infection atm after what seems like 7 continuous weeks of freezing rain here), so I'll make some rearrangements to the above code, and then leave it be... but I'd be happy either way if the most recent commit b23264e were reverted.

I think it's time to stop picking at this particular wart!