Deriving instances for newtypes and enums

[qsctr]

Newtypes currently do not work with any of the typeclasses which means you can't even check if two things are the same.

newtype T = { val : Integer }

Main> T { val = 1 } == T { val = 1 }

[error] at <interactive>:2:1--2:31:
  • Type `T` does not support equality.
      arising from
      use of expression (==)
      at <interactive>:2:1--2:31

It would be nice if the user could derive instances for classes based on the underlying type.

[RyanGlScott]

A similar issue exists for enums (#1602). It might be nice to make certain classes derivable for enums (e.g., Eq).

[RyanGlScott]

Here is a more detailed proposal. Throughout the example, I'll reference enum Maybe a = Nothing | Just a.

1. Newtype and enum declarations can have an optional deriving (C_1, ..., C_n) clause attached to the end, where each of C_1 through C_n is a type of kind * -> Prop. Unlike Haskell, it is not valid to say deriving C; you must instead wrap it in parentheses, i.e., deriving (C).

2. For enums, the only derivable constraints are Eq, Cmp, and SignedCmp.

   A derived Eq instance will consider two values of the same constructor to be equal iff their fields are also equal, and it considers two values of different constructors to be unequal. For example, Nothing == Nothing ~> True, Nothing == Just 0b0 ~> False, Just 0b0 == Just 0b0 ~> True, and Just 0b0 == Just 0b1 ~> False.

   Derived Cmp and SignedCmp instances obey a lexicographic ordering where earlier constructors are less than later constructors, and comparing two values of the same constructor will compare the fields pointwise. For instance, Nothing < Just 0b0 ~> True, Just 0b0 < Nothing ~> False, Just 0b0 < Just 0b0 ~> False, and Just 0b0 < Just 0b1 ~> True.

3. For newtypes, one can derive any class for which the underlying record type has a valid instance. This means that in addition to deriving Eq, Cmp, and SignedCmp instances, one could also derive Zero, Logic, and Ring instances.
4. The generated instances may have other conditions that need to be met in order to be valid. For instance, a derived Eq (Maybe a) instance would also require Eq a.

In order to support derived Cmp and SignedCmp instances, we will need to record the order in which constructors are defined, which will likely require some changes to the way enums are represented in the Cryptol AST.