test.idr

module Main

import Data.List

data Creep : Type where [external]

data Flag : Type where [external]

moveTo : (HasIO io) => Creep -> Flag -> io ()
moveTo creep flag = pure ()

simpleMove: IO ()
simpleMove = do
  creeps <- pure []
  flags <- pure []
  let firstCreep = head' creeps
  let firstFlag = head' flags
  -- NOTE: this works
  -- let result = (the (Maybe $ IO ()) (moveTo <$> firstCreep <*> firstFlag))
  -- pure ()

  -- NOTE: this doesn't work because it can't find an implementation for Applicative ?f
  let result = (the (Maybe $ IO ()) [| moveTo firstCreep firstFlag |])
  pure ()

  -- NOTE: this works
  -- case (the (Maybe $ IO ()) [| moveTo firstCreep firstFlag |]) of
  --      Just _ => pure ()
  --      Nothing => pure ()

main : IO ()
main = simpleMove