Strict positivity for nested types

[clayrat]

Steps to Reproduce

data Cofree1 : (f : Type -> Type) -> Type -> Type where 
  Co1 : a -> f (Cofree1 f a) -> Cofree1 f a

data Cofree2 : (f : Type -> Type) -> Type -> Type where 
  Co2 : (a, f (Cofree2 f a)) -> Cofree2 f a

Expected Behavior

Both cases fail the positivity check (unless there's some way to constrain f?)

Observed Behavior

On Idris 1.2.0:

> :total Co1
Co1 is not strictly positive
> :total Co2
Co2 is Total

I suspect the root cause is missing cases in Idris.Termination.checkPositive.cp, but I'm not sure what are the correct ones for nested data, is it something starting with App?

[ahmadsalim]

Thanks for reporting the issue.

[ahmadsalim]

@clayrat Hmm, looking at the code it should be correct to rely on Bind, the question is just why allTTnames does not report the correct type.

[ahmadsalim]

@clayrat Ah nevermind, the problem is in posArg!

[ahmadsalim]

@clayrat Yes, it should check recursively in App as well.

[ivanperez-keera]

unless there's some way to constrain f?

Is there? (I'm really interested in doing this.)

[ahmadsalim]

@ivanperez-keera You have to take a look at something like generic programming.