■

module Free

data Free : (Type -> Type) -> Type -> Type where
  Pure   : a -> Free f a
  Impure : f (Free f a) -> Free f a

bind : Functor f => (a -> Free f b) -> Free f a -> Free f b
bind k (Pure x)   = k x
bind k (Impure x) = Impure (fmap (bind k) x)

instance Functor f => Functor (Free f) where
  fmap g = bind (\x => Pure (g x))

instance Functor f => Applicative (Free f) where
  pure  = Pure
  f <$> x = bind (\f' => bind (\x' => Pure (f' x')) x) f

instance Functor f => Monad (Free f) where
  return  = Pure
  m >>= k = bind k m

$ idris --check --total free.idr
free.idr:8:Free.bind is possibly not total due to recursive path Free.bind --> Free.bind

うまくいかないなー