Is there a formalism of "coinductive" data types with negative occurrences?

Question

Consider the following program in Haskell:

data T = T { num :: Int, fun :: (T -> T), tl :: T }

repeat' :: (T -> T) -> T
repeat' f = T 0 f (repeat' f)

check :: Int -> T -> Bool
check 0 t = even (num t)
check n t = not (check (n-1) (tl t))

good :: T -> T
good t
  | check 2 t = T 0 (\_ -> t') t'
  | otherwise = T 1 good (fun t t')
  where t' = tl t

bad :: T -> T
bad t
  | check 2 (fun t t) = T 0 (\_ -> t') t'
  | otherwise         = T 1 bad (fun t t')
  where t' = tl t

-- main = print $ num (tl (tl (good (repeat' good))))
main = print $ num (bad (repeat' bad))

(test with: runghc test.hs)

T is "nearly" a plain coinductive Stream of Ints, except for an infamous negative occurrence in the fun field.

good and bad are functions that differ only in what check (implementation quite irrelevant, other than it looks at the supplied T) is passed.

Both are "nearly" defined by guarded recursion if you ignore the unapplied occurrences in the otherwise clauses.

Of course, "nearly" is not quite good enough for a well-defined definition and bad goes into infinite regress while good is productive. Although both call the fun field of the input with (part of) its input, the red flag is that bad calls the fun of its input before producing a constructor, I believe.

As the call to check demonstrates (and as is compatible with the definition of guarded recursion I found here), it is OK to look at num or tl before producing. Of course, the definition of guarded recursion is not concerned about a "nearly" coinductive type like T; plus the unapplied recursive occurrence would likely be rejected anyway.

I have a function like good in practice and would like to wiggle around the domain theory excursion that's necessary to prove its well-definedness on well-defined inputs (e.g., all funs must be productive rather than otherwise continuous/partial in a weird way).

So my questions are:

1. Is there literature on "nearly" coinductive data types such as T together with a refined definition of what constitutes a definition by guarded recursion on these types? E.g., allow unapplied guarded recursive occurrences and conservatively reject unguarded uses of fields like fun with negative occurrences.
2. Perhaps one that is a compositional extension of the usual definition of coinductive data types+guarded recursion?
3. And that allows good (unless it is not as well-defined as I think) and rejects bad, of course?

Answer 1

I found my answer in Guarded Domain Theory and its implementation in Guarded Cubical Agda (implementing Ticked Cubical Type Theory).

The following program type-checks good but rejects bad at the place I indicated:

{-# OPTIONS --cubical --guarded #-}

module SO where

-- This prelude is from the "trusted kernel" 
-- https://github.com/agda/agda/blob/3d393d65baefa07b70f4d3e55475b7852cbe12e5/test/Succeed/LaterPrims.agda

open import Agda.Primitive
open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

module Prims where
  primitive
    primLockUniv : Set₁

open Prims renaming (primLockUniv to LockU) public

private variable
  l : Level
  A B : Set l

postulate Tick : LockU

▹_ : ∀ {l} → Set l → Set l
▹ A = (@tick x : Tick) -> A

next : A → ▹ A
next x _ = x

postulate fix : ∀ {l} {A : Set l} → (▹ A → A) → A

-- Now the actual payload

open import Data.Nat
open import Data.Bool

{-# NO_POSITIVITY_CHECK #-} -- needed because of https://github.com/agda/agda/issues/6587
record Ty : Set where
  inductive
  field 
    num : ℕ
    fun : (▹ Ty -> ▹ Ty)
    tl : ▹ Ty

postulate check : ℕ -> Ty -> Bool
-- A postulate, because I don't know how to faithfully define 
-- Barr's tick constant ◇ from http://www.itu.dk/people/mogel/papers/lics2017.pdf
-- We'd need this constant to apply it to `tl t` below.
-- check 0 t = even (num t)
-- check n t = not (check (n-1) (tl t))

good : Ty -> Ty
good = fix aux
  where
    aux : ▹ (Ty -> Ty) -> Ty -> Ty
    aux rec t with check 2 t
    ... | true  = record { num = 0; fun = (λ _ -> Ty.tl t); tl = Ty.tl t }
    ... | false = record { num = 1; fun = (λ t α -> rec α (t α)); tl = Ty.fun t (Ty.tl t) }

-- bad : Ty -> Ty
-- bad = fix aux
--   where
--     aux : ▹ (Ty -> Ty) -> Ty -> Ty
--     aux rec t with check 2 (Ty.fun t t) 
--                         -- ^^^^^^^^^^^^
--                         -- type error!
--                         -- Ty !=< (Tick → Ty)
--                         -- when checking that the expression t has type ▹ Ty   
--     ... | true  = record { num = 0; fun = (λ _ -> Ty.tl t); tl = Ty.tl t }
--     ... | false = record { num = 1; fun = (λ t α -> rec α (t α)); tl = Ty.fun t (Ty.tl t) }

Specifically, there is no way to tweak Ty.fun t t such that it returns an unguarded Ty, thus we can't pass the result to check.

An ingenious abstraction!

Answer 2

Your datatype is a variant of the domain equation for the untyped lambda calculus. Verifying that an arbitrary untyped lambda term is normalizing is an undecidable problem, but there are undecidable type systems that can be used, specifically intersection types in the sense of Coppo and Dezani. For instance see here for how it relates to strong normalization.