perf: better derived Hashable for single field structures

[hargoniX]

This PR changes the deriving handler for Hashable to simply call hash x instead of
mixHash 0 (hash x) for single field structures.

Closes: #11818

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for d2b44d6 against b81608d are in! @hargoniX

Warnings (2)

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Runner for run build has different system configurations between commits.
• Runner for run other has different system configurations between commits.

Large changes (1✅)

• ✅ big_do//instructions: -155.0M (-0.5%)

Small changes (280✅, 3🟥)

Too many entries to display here. View the full report on radar instead.

[georgerennie]

With these, rather than just special casing single field structures you can just make the first case (hash a) instead of (mixHash 0 (hash a)) i think? The Hashable instance already does this for Prod, saving a mixHash:

structure MyProd where
  a : Nat
  b : Nat
deriving Hashable

#print instHashableMyProd.hash
-- | { a := a, b := a_1 } => mixHash (mixHash 0 (hash a)) (hash a_1)

#print instHashableProd
-- mixHash (hash a) (hash b)

edit: Actually with inductives this doesn't work so well because if the hash for the first case is equivalent to (mixhash 0 _) of the same type in the second case then both have the same path of mix hashes so are more likely to collide.

You can do similarly with inductives, currently you get:

inductive MySum where
| a : Nat -> MySum
| b : Nat -> MySum
deriving Hashable

#print instHashableMySum.hash
-- match x with
-- | MySum.a a => mixHash 0 (hash a)
-- | MySum.b a => mixHash 1 (hash a)

but this could be (although this is arguably less useful given it only saves work in the first case)

match x with
| MySum.a a => hash a
| MySum.b a => mixHash 0 (hash a)