Functions in inductive types

Stream: new members

[Virginia Senioria]

I'm working with some code like this in Lean4:

import Std.Data.HashMap

inductive T where
| tt: Std.HashMap String T -> T

And Lean complaints:

(kernel) arg #1 of 'T.tt' contains a non valid occurrence of the datatypes being declared

I inspected the definition of Std.HashMap, and found it seems not like that T.tt is not strictly positive.

---

Besides, when I tried to alter T like this:

def R (a b: Type) := a -> b

inductive T where
| tt: R String T -> T

Lean complaints something longer:

application type mismatch
  T.rec fun a a_ih => PProd (PProd ((a_1 : String) → motive (a a_1)) ((a : String) → a_ih a)) PUnit
argument has type
  R String T → (String → Sort (max 1 u)) → Sort (max (max 1 (max 1 (imax 1 u)) 1 u) 1 u)
but function has type
  ((a : R String T) → ((a_1 : String) → (fun t => Sort (max 1 u)) (a a_1)) → (fun t => Sort (max 1 u)) (T.tt a)) →
    (t : T) → (fun t => Sort (max 1 u)) t

while Idris2 seems accepting something similar:

R : Type -> Type -> Type
R a b = a -> b

data T: Type where
  Tt: R String T -> T

How can I alter my code to make such constructors work? Thanks.