RFC: `deriving` for single field `structure`s

Proposal

Currently the following program from our time library works and correctly derives all the instances:

def Offset : Type := UnitVal 1
  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString

However if we wanted to refactor this to a single field structure to make writing instances such as Decidable for LT easier:

structure Offset : Type where
  val : UnitVal 1
  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString

The following deriving handlers:

Add, Sub, Neg, LE, LT, ToString

all fail with:

default handlers have not been implemented yet, class: 'Add' types: [Std.Time.Second.Offset]

Based on some preliminary reading of the deriving framework it seems to me that we have an automated deriving mechanism for all classes for just def but this just gives up on single field structures right away. I propose that we improve this mechanism to allow such automated deriving for all single field structure's as well.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reading the deriving framework and reproducing the reported single-field structure example with Add, Sub, Neg, LE, LT, and ToString. Done means those handlers derive successfully for the Offset structure while preserving the existing behavior shown in the issue.