varying in idris

varying.idr

record VaryingT (input : Type) (m : Type -> Type) (output : Type)  where
  constructor VT
  runVarT : input -> m (output, Inf $ VaryingT input m output)

Monad m => Functor (VaryingT a m) where
  map f v = assert_total $ VT $ \ x => do
    (b, v2) <- runVarT v x
    pure (f b, map f v2)

Melvar (irc.freenode.net #idris): The problem is that as you define VT, m could be contravariant or invariant, meaning VT is not strictly positive and thus counts as nontotal.