Typeclass Inference Failure on HashMap

Stream: lean4

[Yicheng Qian]

(deleted)

[Yicheng Qian]

(deleted)

[Yicheng Qian]

Lean fails to synthesize typeclass instances in the following code:

set_option trace.Meta.isDefEq true
def foo (a : List (Nat × Nat)) : Option Nat := (HashMap.ofList a).find? 0

error messages:

don't know how to synthesize implicit argument
  @HashMap.ofList Nat Nat (?m.3770 a) (?m.3771 a) a
context:
a : List (Nat × Nat)
⊢ Hashable Nat

don't know how to synthesize implicit argument
  @HashMap.find? Nat Nat (?m.3770 a) (?m.3771 a) (HashMap.ofList a) 0
context:
a : List (Nat × Nat)
⊢ Hashable Nat

[Chris Bailey]

If you're using the hash map in Lean.Data.HashMap, I assume this is because the instances of BEq and Hashable on HashMap.ofList are marked as regular implicits and not inst/typeclass implicits. I don't know why that is, I was surprised when I looked at the docs.

There are two implementations of HashMap, I think the one in Lean.Data.HashMap is still mostly for internal use. The other one is Batteries.Data.HashMap, where Batteries is like a standard library.

[Kim Morrison]

Fixed in lean#4248