test.idr

-- code based on https://www.youtube.com/watch?v=umiUJNcvPl0

data Command : Type -> Type where
  PutStr : String -> Command ()
  GetStr : Command String

data InfIO : Type where
  Do : Command a -> (a -> Inf InfIO) -> InfIO

(>>=) : Command a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do

runCommand : Command a -> IO a
runCommand (PutStr x) = putStr x
runCommand GetStr = getLine

-- a run function:
run : InfIO -> IO ()
run (Do command rest) = do res <- runCommand command
                           run (rest res)

-- expanding `do` notation and doing eta reduction fails:
run (Do command rest) = runCommand command >>= run . rest

-- `-- test.idr line 17 col 51:
--     When checking right hand side of run with expected type
--             IO ()
--     
--     When checking an application of function Prelude.Basics..:
--             Type mismatch between
--                     a -> Inf InfIO (Type of rest)
--             and
--                     a -> InfIO (Expected type)
--             
--             Specifically:
--                     Type mismatch between
--                             Inf InfIO
--                     and
--                             InfIO


-- inserting a `Force` fixes it:
run (Do command rest) = runCommand command >>= run . Force . rest