'Gradual' decidable equality combinators

[gallais]

When you define decidable equality for e.g.

data Rose (A : Set) : Set where
  node : List (Rose A) → Rose A

you can't reuse Data.List.Properties' ≡-dec because it makes the
termination checker scream. However you would not have to redo all the
work if only we provided

∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x ∷ xs ≡ y ∷ ys)
∷-dec x≟y xs≟ys = map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys)

Indeed mutually defining

_≟_  : Decidable {A = Rose A} _≡_
_≟s_ : Decidable {A = List (Rose A)} _≡_

then becomes easy:

node xs ≟ node ys = map′ (cong node) node-injective (xs ≟s ys)

[]       ≟s []       = yes refl
(x ∷ xs) ≟s (y ∷ ys) = ∷-dec (x ≟ y) (xs ≟s ys)

[] ≟s (x ∷ ys) = no (λ ())
(x ∷ xs) ≟s [] = no (λ ())

I have used this trick twice in #799 to simplify decidable equality proofs
involving Arg and Abs and there are probably numerous other places where
we can define these combinators in the stdlib.

Edit: self-contained gist

[jamesmckinna]

Towards a general solution to deriving (Eq)-style automated support?
(I'm told that this is a frequently-solved problem among commercial Agda developers)

[JacquesCarette]

'commercial Agda developers' ???

[jamesmckinna]

Was this issue effectively put to bed by #811 ? If so, we should close, but perhaps document the pattern in the library design/style guide documentation?

[JacquesCarette]

Agreed. Can we even test its use internally, or would that introduce dependencies that are a bit over the top?

[jamesmckinna]

Stub content added to doc/style-guide.md in #2270, so closing this now.