gistfile1.txt

data Trampoline : (m : Type -> Type) -> (r : Type) -> Type where
  MkTram : m (Either (Trampoline m r) r) -> Trampoline m r

partial
Functor m => Functor (Trampoline m) where
  map f (MkTram x) = MkTram (map (either (Left . map f) (Right . f)) x)

   |
40 |   map f (MkTram x) = MkTram (map (either (Left . map f) (Right . f)) x)
   |   ~~~~~~~~~~~~~~~~~
Prelude.Functor.Stream.Trampoline m implementation of Prelude.Functor.Functor, method map is possibly not total due to: Stream.MkTram

------------------------------

data Trampoline : (m : Type -> Type) -> (r : Type) -> Type where
  MkTram : m (Either (Trampoline m r) r) -> Trampoline m r

partial
tmap : Functor m => (a -> b) -> Trampoline m a -> Trampoline m b
tmap f (MkTram x) = MkTram (map (either (Left . tmap f) (Right . f)) x)

partial
Functor m => Functor (Trampoline m) where
  map f x = tmap f x

45 |   map f x = tmap f x
   |   ~~~~~~~~~~~~~~~~~~
Prelude.Functor.Stream.Trampoline m implementation of Prelude.Functor.Functor, method map is possibly not total due to: Stream.tmap