{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures             #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE RebindableSyntax           #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE TypeOperators              #-}

import           Control.Monad (void, fail)
import           Control.Monad.Indexed
import           Control.Monad.Trans.Ix
import           Data.Coerce
import           Data.Kind (Type)
import           GHC.TypeLits (Nat, type (+))
import           Language.Haskell.DoNotation
import           Prelude hiding (Monad (..), pure)
import qualified System.IO as SIO
import           System.IO hiding (openFile, Handle)


------------------------------------------------------------------------------
-- | This module just exists to make sure 'iShouldCompile' actually compiles.
main :: IO ()
main = do
  pure ()


------------------------------------------------------------------------------
-- |
monadUnecessary :: Applicative m => m ()
monadUnecessary = pure ()


------------------------------------------------------------------------------
-- | Function that uses both monads and indexed monads in do blocks.
iShouldCompile :: IO ()
iShouldCompile = do
  putStrLn "hello"
  void $ runLinear $ do
    f <- openFile "not a real file" ReadMode
    closeFile f
    pure "goodbye"
  putStrLn $ do
    c <- ['a' .. 'z']
    pure c


------------------------------------------------------------------------------
-- | 'Linear' statically tracks the files you open and makes sure you close them
-- exactly one time.
newtype Linear (s :: Type)
               (i :: LinearState)
               (j :: LinearState) a = Linear
  { unsafeRunLinear :: Ix IO i j a
  }
  deriving (IxFunctor, IxPointed, IxApplicative, IxMonad)


------------------------------------------------------------------------------
-- | Run the underlying IO action if you've closed all the files you opened.
runLinear
    :: (forall s. Linear s ('LinearState 0 '[])
                           ('LinearState n '[]) a)
    -> IO a
runLinear = coerce


------------------------------------------------------------------------------
-- | Data kind for tracking our linear state as the index to 'Linear'.
data LinearState = LinearState
  { linearNextKey  :: Nat
  , linearOpenKeys :: [Nat]
  }


------------------------------------------------------------------------------
-- | A wrapped 'SIO.Handle' with a phantom parameter for the ST trick.
newtype Handle (s :: Type) key = Handle
  { unsafeGetHandle :: SIO.Handle
  }


------------------------------------------------------------------------------
-- | Open a file and track that you did it in the type system.
openFile
    :: FilePath
    -> IOMode
    -> Linear s ('LinearState next open)
                ('LinearState (next + 1) (next ': open))
                (Handle s next)
openFile = coerce SIO.openFile


------------------------------------------------------------------------------
-- | Close a file and prove it!
closeFile
    :: IsOpen key open ~ 'True
    => Handle s key
    -> Linear s ('LinearState next open)
                ('LinearState next (Close key open))
                ()
closeFile = coerce SIO.hClose


------------------------------------------------------------------------------
-- | Type family to detect if a file handle is already opened (ie. if it exists
-- in the open set.
type family IsOpen
      (key :: k)
      (ts :: [k]) :: Bool where
  IsOpen key '[]         = 'False
  IsOpen key (key ': ts) = 'True
  IsOpen key (_x  ': ts) = IsOpen key ts


------------------------------------------------------------------------------
-- | Type family to remove a file handle from the open set.
type family Close
      (key :: k)
      (ts :: [k]) :: [k] where
  Close key (key ': ts) = ts
  Close key (_x  ': ts) =
    _x ': Close key ts