Use case for ∷-dec

Rose.agda

open import Data.List using (List); open List
open import Data.List.Properties
open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

private variable A : Set

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

node-injective : {xs ys : List (Rose A)} → node xs ≡ node ys → xs ≡ ys
node-injective refl = refl

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

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

-- _≟s_ = ≡-dec _≟_ -- termination error

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

  where

    ∷-dec : ∀ {x y : A} {xs ys} → 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)