test: add test to demonstrate why it is useful to include instances in the PersistentHashMap type

tests/lean/phashmap_inst_coherence.lean

@@ -0,0 +1,11 @@
+import Init.Data.PersistentHashMap
+
+def m : PersistentHashMap Nat Nat :=
+let m : PersistentHashMap Nat Nat := {};
+m.insert 1 1
+
+def natDiffHash : Hashable Nat :=
+⟨fun n => USize.ofNat $ n+10⟩
+
+-- The following example should fail since the `Hashable` instance used to create `m` is not `natDiffHash`
+#eval @PersistentHashMap.find Nat Nat _ natDiffHash m 1

tests/lean/phashmap_inst_coherence.lean.expected.out

@@ -0,0 +1,8 @@
+phashmap_inst_coherence.lean:11:0: error: type mismatch at application
+  PersistentHashMap.find m
+term
+  m
+has type
+  @PersistentHashMap Nat Nat Nat.Hashable (@beqOfEq Nat Nat.DecidableEq)
+but is expected to have type
+  @PersistentHashMap Nat Nat natDiffHash (@beqOfEq Nat Nat.DecidableEq)