RFC: improving performance of `deriving Hashable` on single-field structures

[math-fehr]

Proposal

The hash produced by deriving Hashable on a single-field structure should be the same as the hash of the field type.

Currently, these two types have very different hashes, where the structure hash has a large slowdown compared to the other one:

abbrev T := Nat

structure U where
  value: Nat
deriving Hashable

On our benchmarks that rely a lot on hashmaps, going from U to T lead to a 2x slowdown overall, whereas the two types are representing exactly the same thing.

Manually deriving the Hashable removes that slowdown, and I believe this implementation should be the one generated by deriving Hashable

instance : Hashable U where
  hash u := hash u.value

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.