The totality checker thinks `dual` the last case of makes it partial - even though I would have thought the pattern matching shrinks the argument.

channel.idr

%default total

data Channel : (result :Type ) -> Type
where
  Send     : a -> Channel a
  Receive  : a -> Channel a
  Finished : Channel ()
  (>>=)    : Channel a -> ((x:a) -> Channel b) -> Channel b

dual : Channel a -> Channel a
dual (Send x) = (Receive x)
dual (Receive x) = (Send x)
dual Finished = Finished
dual (x >>= f) = (dual x) >>= (dual . f)