How to define free monad and cofree comonad?

Stream: lean4

[André Muricy Santos]

Hi all, in Haskell we can define both of these in this way:

data Free (f :: Type -> Type) (a :: Type) = Pure a | Free (f (Free f a))
data Cofree (f :: Type -> Type) (a :: Type) = Cofree a (f (Cofree f a))

But attempting the same definition in lean4 gives some kernel errors which I don't understand. I suspect it has something to do with the termination checker but can't be sure because the errors are not clear:

-- error: (kernel) arg #3 of 'Free.free' contains a non valid occurrence of the datatypes being declared
inductive Free (f : Type → Type) (α : Type) where
  | pure : α → Free f α
  | free : f (Free f α) → Free f α

-- (kernel) arg #4 of 'Cofree.cofree' contains a non valid occurrence of the datatypes being declaredLean 4
inductive Cofree (f : Type → Type) (α : Type) where
  | cofree : α → f (Cofree f α) → Cofree f α

Is there something similar to Agda's TERMINATING pragma? Or is this error related to something else?

[André Muricy Santos]

I got a wonderful answer to this question on stackoverflow :) https://stackoverflow.com/a/78275159/4808450