Equality testing without explicit proof that data constructors are injective

Question

Is it possible to define a simple syntactic notion of equality (similar to what GHC might automatically derive as the Eq instance for a Haskell 98 type), without either explicitly proving that each data constructor is injective, or doing something analogous, such as defining the retraction of each constructor and using cong?

In other words, is it possible to exploit the injectivity of data constructors more directly, rather than having to introduce one auxiliary function per constructor?

The following uses the natural numbers as an example.

module Eq where

   open import Function
   open import Relation.Binary
   open import Relation.Binary.PropositionalEquality
   open import Relation.Nullary

   data ℕ : Set where
      zero : ℕ
      suc : ℕ → ℕ

   -- How to eliminate these injectivity proofs?
   suc-injective : ∀ {n m} → suc n ≡ suc m → n ≡ m
   suc-injective refl = refl

   _≟_ : Decidable {A = ℕ} _≡_
   zero ≟ suc _ = no (λ ())
   suc _ ≟ zero = no (λ ())
   zero ≟ zero = yes refl
   suc n ≟ suc m with n ≟ m
   suc n ≟ suc .n | yes refl = yes refl
   ... | no n≢m = no (n≢m ∘ suc-injective)

One could replace suc-injective by cong (λ { zero → zero ; (suc x) → x }), i.e. by defining a function which inverts suc, but that still requires boilerplate of one auxiliary function per constructor, and such functions are somewhat ugly to define because of the need to be total.

(Usual caveats re. missing something obvious apply.)

Answer 1

Ulf Norell's prelude for Agda contains a mechanism for automatically deriving decidable equality for a given datatype. The code is based on Agda's reflection mechanism and automatically generated extended lambdas for proving injectivity of constructors. I recommend taking a look at the code, even though it's not always as simple as it could be.