From 6d358a5deec6ee44106e1c3e113a321925db9dc5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 8 Nov 2019 08:23:10 -0800 Subject: [PATCH] test: add test to demonstrate why it is useful to include instances in the PersistentHashMap type --- tests/lean/phashmap_inst_coherence.lean | 11 +++++++++++ tests/lean/phashmap_inst_coherence.lean.expected.out | 8 ++++++++ 2 files changed, 19 insertions(+) create mode 100644 tests/lean/phashmap_inst_coherence.lean create mode 100644 tests/lean/phashmap_inst_coherence.lean.expected.out diff --git a/tests/lean/phashmap_inst_coherence.lean b/tests/lean/phashmap_inst_coherence.lean new file mode 100644 index 0000000000..284fdcbe68 --- /dev/null +++ b/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 diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out new file mode 100644 index 0000000000..213a41dd01 --- /dev/null +++ b/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)