Using the standard encoding of a free monad in Haskell and its
data Free f a = Pure a
| Roll (f (Free f a))
Writing an equivalent to this in a dependently typed theory gets rejected because of the strict positivity condition.
Is it possible to cause non-termination with this encoding of a
If this isn't the case does it point to some known relaxation of the strict positivity condition?
If this is the case is there a strictly positive datatype which acts as Free for strictly positive functors?
I don't specify the exact type theory I am working in, as some might allow addition of features to allow this. The base theory might be something like Coq's CoC.