HashMap with inductive types?

Stream: lean4

[Andrés Goens]

I was trying to implement a recursive structure like the one discussed in this thread: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Recursive.20Structures but wanted to use HashMap instead of List, say something like:

inductive Package
  -- | mk : (deps : List Package) → Package -- works fine
  | mk : (deps : Std.HashMap String Package) → Package -- (kernel) arg #1 of 'Package.mk' contains a non valid occurrence of the datatypes being declared

I guess there's some reason why the code generator won't work with this. For my purpuses I can just use (the equivalent of) List (Strig × Package), but I'm curious, why doesn't this work? The error seems quite cryptic

[Jannis Limperg]

Whenever the type you're defining (here Package) appears as an argument to some type function F : Type -> Type in a constructor argument (here F = λ T, Std.HashMap String T, Lean must prove that F is "strictly positive". This is necessary to avoid paradoxes. Lean's strict positivity checker is incomplete and doesn't realise that HashMap, which is a rather complex type, is strictly positive.

If you really want, you can get the desired representation by defining Package as an unsafe inductive, though that way lies much pain.

[Andrés Goens]

is there a way to manually provide a proof of that, like for termination?

[Jannis Limperg]

Not to my knowledge.