Replace monad stack with hard-coded monad

src/Lib/Elab.idr

@@ -1,9 +1,5 @@
 module Lib.Elab
 
-import Control.Monad.Error.Either
-import Control.Monad.Error.Interface
-import Control.Monad.State
-import Control.Monad.Identity
 import Lib.Parser.Impl
 import Lib.Prettier
 import Data.List
@@ -169,7 +165,7 @@ rename meta ren lvl v = go ren lvl v
             go ren lvl !(vappSpine val sp)
           _ => do
             debug "rename: \{show ix} is unsolved"
-            catchError {e=Error} (goSpine ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err))
+            catchError (goSpine ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err))
     go ren lvl (VLam fc n icit rig t) = pure (Lam fc n icit rig !(go (lvl :: ren) (S lvl) !(t $$ VVar fc lvl [<])))
     go ren lvl (VPi fc n icit rig ty tm) = pure (Pi fc n icit rig !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar emptyFC lvl [<])))
     go ren lvl (VU fc) = pure (U fc)
@@ -215,7 +211,7 @@ solve env m sp t = do
   -- force unlet
   hack <- quote l t
   t <- eval env CBN hack
-  catchError {e=Error} (do
+  catchError (do
     tm <- rename m ren l t
 
     let tm = lams (length sp) (reverse ctx_.boundNames) tm
@@ -288,7 +284,7 @@ unify env mode t u = do
     unifyRef t'@(VRef fc k def sp)  u'@(VRef fc' k' def' sp') =
       -- unifySpine is a problem for cmp (S x) (S y) =?= cmp x y
         do
-        -- catchError {e = Error} (unifySpine env mode (k == k') sp sp') $ \ err => do
+        -- catchError(unifySpine env mode (k == k') sp sp') $ \ err => do
             Nothing <- tryEval env t'
               | Just v => do
               debug "tryEval \{show t'} to \{show v}"
@@ -577,7 +573,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
   -- We get unification constraints from matching the data constructors
   -- codomain with the scrutinee type
   debug "unify dcon cod with scrut\n  \{show ty'}\n  \{show scty}"
-  Just res <- catchError {e = Error} (Just <$> unify ctx'.env Pattern ty' scty)
+  Just res <- catchError(Just <$> unify ctx'.env Pattern ty' scty)
               (\err => do
                   debug "SKIP \{dcName} because unify error \{errorMsg err}"
                   pure Nothing)
@@ -621,7 +617,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
         pure $ Just $ CaseCons dcName (map getName vars) tm
 
     _ => do
-        Right res <- tryError {e = Error} (unify ctx'.env Pattern ty' scty)
+        Right res <- tryError (unify ctx'.env Pattern ty' scty)
           | Left err => do
             debug "SKIP \{dcName} because unify error \{errorMsg err}"
             pure Nothing

src/Lib/Eval.idr

@@ -5,7 +5,6 @@ import Lib.Parser.Impl
 import Lib.Prettier
 import Lib.Types
 import Lib.TopContext
-import Control.Monad.Error.Interface
 
 import Data.IORef
 import Data.Fin
@@ -74,7 +73,7 @@ tryEval : Env -> Val -> M (Maybe Val)
 tryEval env (VRef fc k _ sp) =
   case lookup k !(get) of
       Just (MkEntry _ name ty (Fn tm)) =>
-        catchError {e=Error} (
+        catchError (
             do
             debug "app \{name} to \{show sp}"
             vtm <- eval [] CBN tm

src/Lib/ProcessDecl.idr

@@ -36,7 +36,7 @@ findMatches ctx ty ((MkEntry _ name type def) :: xs) = do
   -- FIXME we're restoring state, but the INFO logs have already been emitted
   -- Also redo this whole thing to run during elab, recheck constraints, etc.
   mc <- readIORef top.metas
-  catchError {e=Error} (do
+  catchError(do
       -- TODO sort out the FC here
       let fc = getFC ty
       debug "TRY \{name} : \{pprint [] type} for \{show ty}"
@@ -64,7 +64,7 @@ contextMatches ctx ty = go (zip ctx.env (toList ctx.types))
       let True = isCandidate ty type | False => go xs
       top <- get
       mc <- readIORef top.metas
-      catchError {e=Error} (do
+      catchError(do
           debug "TRY context \{nm} : \{pprint (names ctx) type} for \{show ty}"
           unifyCatch (getFC ty) ctx ty vty
           mc' <- readIORef top.metas

src/Lib/Types.idr

@@ -4,10 +4,6 @@ module Lib.Types
 import public Lib.Common
 import public Lib.Prettier
 
-import public Control.Monad.Error.Either
-import public Control.Monad.Error.Interface
-import public Control.Monad.State
-
 import Data.Fin
 import Data.IORef
 import Data.List
@@ -494,9 +490,79 @@ export
 names : Context -> List String
 names ctx = toList $ map fst ctx.types
 
+-- public export
+-- M : Type -> Type
+-- M = (StateT TopContext (EitherT Error IO))
+
 public export
-M : Type -> Type
+record M a where
-M = (StateT TopContext (EitherT Error IO))
+  constructor MkM
+  runM : TopContext -> IO (Either Error (TopContext, a))
+
+export
+Functor M where
+  map f (MkM run) = MkM $ \tc => do
+    result <- run tc
+    case result of
+      Left err => pure $ Left err
+      Right (tc', a) => pure $ Right (tc', f a)
+
+export
+Applicative M where
+  pure x = MkM $ \tc => pure $ Right (tc, x)
+  (MkM f) <*> (MkM x) = MkM $ \tc => do
+    resultF <- f tc
+    case resultF of
+      Left err => pure $ Left err
+      Right (tc', f') => do
+        resultX <- x tc'
+        case resultX of
+          Left err => pure $ Left err
+          Right (tc'', x') => pure $ Right (tc'', f' x')
+
+export
+Monad M where
+  (MkM x) >>= f = MkM $ \tc => do
+    resultX <- x tc
+    case resultX of
+      Left err => pure $ Left err
+      Right (tc', a) => runM (f a) tc'
+
+export
+HasIO M where
+  liftIO io = MkM $ \tc => do
+    result <- io
+    pure $ Right (tc, result)
+
+export
+throwError : Error -> M a
+throwError err = MkM $ \_ => pure $ Left err
+
+export
+catchError : M a -> (Error -> M a) -> M a
+catchError (MkM ma) handler = MkM $ \tc => do
+  result <- ma tc
+  case result of
+    Left err => runM (handler err) tc
+    Right (tc', a) => pure $ Right (tc', a)
+
+export
+tryError : M a -> M (Either Error a)
+tryError ma = catchError (map Right ma) (pure . Left)
+
+export
+get : M TopContext
+get = MkM $ \ tc => pure $ Right (tc, tc)
+
+export
+put : TopContext -> M ()
+put tc = MkM $ \_ => pure $ Right (tc, ())
+
+export
+modify : (TopContext -> TopContext) -> M ()
+modify f = do
+  tc <- get
+  put (f tc)
 
 ||| Force argument and print if verbose is true
 export

src/Main.idr

@@ -1,9 +1,5 @@
 module Main
 
--- import Control.App
-import Control.Monad.Error.Either
-import Control.Monad.Error.Interface
-import Control.Monad.State
 import Data.List
 import Data.List1
 import Data.String
@@ -151,7 +147,7 @@ processModule importFC base stk qn@(QN ns nm) = do
     -- tryParseDecl :
     tryProcessDecl : List String -> Decl -> M ()
     tryProcessDecl ns decl = do
-      Left err <- tryError {e=Error} $ processDecl ns decl | _ => pure ()
+      Left err <- tryError $ processDecl ns decl | _ => pure ()
       addError err
 
 processFile : String -> M ()
@@ -235,7 +231,7 @@ main : IO ()
 main = do
   -- we'll need to reset for each file, etc.
   ctx <- empty
-  Right _  <- runEitherT $ runStateT ctx $ main'
+  Right _  <- runM main' ctx
     | Left err => do
         putStrLn "ERROR at \{show $ getFC err}: \{errorMsg err}"
         exitFailure

test/src/Main.idr

@@ -1,7 +1,5 @@
 module Main
 
-import Control.Monad.Error.Either
-import Control.Monad.Error.Interface
 import Lib.Types
 import Lib.ProcessDecl
 import Lib.TopContext