(kernel) application type mismatch using HashMap

Stream: lean4

[Valentin Robert]

This is simplified from my actual use case, but I can't seem to put a hash map whose target type is the type being defined in an inductive type:

import Std.Data.HashMap.Basic

inductive MyType (K : Type k) (V : Type v) [BEq K] [Hashable K] : Type (max k v) where
  | NodeThing : Std.HashMap K (MyType K V) → MyType K V
  | LeafThing : MyType K V

Error message:

(kernel) application type mismatch
  Std.DHashMap.Raw.WF inner
argument has type
  @_nested.Std.DHashMap.Raw_3 K V inst✝¹ inst✝
but function has type
  (Std.DHashMap.Raw K fun x => @MyType K V inst✝¹ inst✝) → Prop

Note that the simpler case where the hashmap target is just V works:

import Std.Data.HashMap.Basic

inductive MyType (K : Type k) (V : Type v) [BEq K] [Hashable K] : Type (max k v) where
  | NodeThing : Std.HashMap K V → MyType K V
  | LeafThing : MyType K V

This is on Lean 4.22.0-rc3.

[Johannes Tantow]

You have to use Std.HashMap.Raw in this case.

[Robin Arnez]

If you read the documentation of Std.HashMap, at the end is says:

These hash maps contain a bundled well-formedness invariant, which means that they cannot be used in nested inductive types. For these use cases, Std.Data.HashMap.Raw and Std.Data.HashMap.Raw.WF unbundle the invariant from the hash map. When in doubt, prefer HashMap over HashMap.Raw.

In other words, because of limitations of Lean, Std.HashMap cannot be used for nested inductives; but Std.HashMap.Raw does.

[Markus Himmel]

There is more information about this in the reference manual: https://lean-lang.org/doc/reference/latest//Basic-Types/Maps-and-Sets/#raw-data It also contains an example of how to use the Raw variant.