RFC: deriving for single field structures

[hargoniX]

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.

[Kha]

RFC accepted!

Note that very much unlike def, we can't just rely on definitional equality but have to transform the existing instance, which in the case of dependencies might not even be possible in general. So this is a pretty complex task and it will likely take some time for us to get to it.