add constructor for unification error (6% improvement)

src/Commands.newt

@@ -16,7 +16,6 @@ import Data.SortedMap
 import Lib.Parser
 import Lib.Syntax
 import Lib.Parser.Impl
-import Lib.Error
 
 -- For now we cheat and assume capitalized directories are a module component
 decomposeName : String → String × String
@@ -235,7 +234,7 @@ introActions (Just $ Unsolved fc qn ctx vty User constraints) =
         pure $ map makeEdit cons
   ) $ \ err => do
       putStrLn "Got error in introActions:"
-      putStrLn $ showError "" err
+      putStrLn $ show err
       pure Nil
   where
     introDCon : QName × Int × Tm → List String

src/LSP.newt

@@ -3,6 +3,7 @@ module LSP
 import Prelude
 import Lib.Common
 import Lib.Eval
+import Lib.Error
 import Lib.Types
 import Lib.TopContext
 import Lib.Tokenizer
@@ -15,7 +16,7 @@ import Node
 import Commands
 import Lib.ProcessDecl
 import Lib.Prettier
-import Lib.Error
+
 import Lib.CompileJS
 import Lib.CompileScheme
 
@@ -104,7 +105,7 @@ hoverInfo uri line col = unsafePerformIO $ do
             putStrLn $ "Nothing to see here"
             pure $ js_castBool True
         | Left err => do
-            putStrLn $ showError "" err
+            putStrLn $ show err
             pure $ jsonToJObject JsonNull
     modifyIORef state $ { topContext := top }
     let location = JsonObj $ ("uri", JsonStr fc.file) :: ("range", fcToRange fc) :: Nil
@@ -124,7 +125,7 @@ codeActionInfo uri line col = unsafePerformIO $ do
     pure actions).runM st.topContext
     | Left err => do
       putStrLn "ACTIONS ERROR"
-      putStrLn $ showError "" err
+      putStrLn $ show err
       pure js_null
   modifyIORef state $ { topContext := top }
   pure $ jsonToJObject $ JsonArray $ map actionToJson actions
@@ -161,12 +162,13 @@ codeActionInfo uri line col = unsafePerformIO $ do
         :: ("edit", (single "changes" $ single uri $ JsonArray $ map editToJson edits))
         :: Nil
 
-errorToDiag : Error -> Json
-errorToDiag err =
-  JsonObj
+errorToDiag : Error -> M Json
+errorToDiag err = do
+  msg <- prettyErrorMsg err
+  pure $ JsonObj
     $  ("severity", JsonInt 1)
     :: ("range", fcToRange (getFC err))
-    :: ("message", JsonStr (errorMsg err))
+    :: ("message", JsonStr msg)
     :: ("source", JsonStr "newt") -- what is this key for?
     :: Nil
 -- These shouldn't escape
@@ -242,14 +244,21 @@ checkFile fn = unsafePerformIO $ do
 
         -- pull out errors and infos
         top <- getTop
-        let errors = map (errorToDiag) top.currentMod.modErrors
+        errors <- traverse (errorToDiag) top.currentMod.modErrors
         infos <- getInfos
         pure $ infos ++ errors
         ).runM st.topContext
         | Left err => do
             putStrLn "**** Error without updating top:"
-            putStrLn $ showError "" err
-            pure $ jsonToJObject $ JsonArray $ errorToDiag err :: Nil
+            putStrLn $ show err
+            pure $ jsonToJObject $ JsonArray
+              [ JsonObj $ ("severity", JsonInt 1)
+                        :: ("range", fcToRange (getFC err))
+                        :: ("message", JsonStr (errorMsg err))
+                        :: ("source", JsonStr "newt") -- what is this key for?
+                        :: Nil
+                        ]
+
     -- Cache loaded modules
     modifyIORef state $ { topContext := top }
     pure $ jsonToJObject $ JsonArray json

src/Lib/Derive.newt

@@ -5,7 +5,7 @@ import Lib.Common
 import Lib.Types
 import Lib.Syntax
 import Lib.TopContext
-import Lib.Error
+
 import Lib.Elab -- (lookupDCon)
 import Lib.Prettier
 

src/Lib/Elab.newt

@@ -13,7 +13,6 @@ import Lib.Util
 import Lib.TopContext
 import Lib.Syntax
 import Lib.Types
-import Lib.Error
 
 vprint : Context -> Val -> M String
 vprint ctx v = do
@@ -28,9 +27,6 @@ collectDecl ((FunDef fc nm cl) :: rest@(FunDef _ nm' cl' :: xs)) =
   else (FunDef fc nm cl :: collectDecl rest)
 collectDecl (x :: xs) = x :: collectDecl xs
 
--- TODO Move this, so we don't need to import all of Elab
-rpprint : List String → Tm → String
-rpprint names tm = render 90 $ pprint names tm
 
 showCtx : Context -> M String
 showCtx ctx =
@@ -144,7 +140,7 @@ findMatches ctx ty ((name, type) :: xs) = do
       setMetaContext mc
       (_::_ name) <$> findMatches ctx ty xs)
     (\ err => do
-      debug $ \ _ => "No match \{show ty} \{rpprint Nil type} \{showError "" err}"
+      debug $ \ _ => "No match \{show ty} \{rpprint Nil type} \{show err}"
       setMetaContext mc
       findMatches ctx ty xs)
 
@@ -166,7 +162,7 @@ contextMatches ctx ty = go (zip ctx.env ctx.types)
           tm <- quote ctx.lvl tm
           (_::_ (tm, vty)) <$> go xs)
         (\ err => do
-          debug $ \ _ => "No match \{show ty} \{rpprint (names ctx) type} \{showError "" err}"
+          debug $ \ _ => "No match \{show ty} \{rpprint (names ctx) type} \{show err}"
           setMetaContext mc
           go xs)
 
@@ -394,7 +390,7 @@ solve env m sp t = do
   -- Will this get is into trouble?
   Right ren <- tryError $ invert l sp
     | Left err => do
-        debug $ \ _ => "postpone constraint \{showError "" err}"
+        debug $ \ _ => "postpone constraint \{show err}"
         addConstraint env m sp t
   -- force unlet
   hack <- quote l t
@@ -588,10 +584,7 @@ unifyCatch fc ctx ty' ty = do
     res <- catchError (unify ctx.env UNormal ty' ty) $ \err => do
       let names = map fst ctx.types
       debug $ \ _ => "fail \{show ty'} \{show ty}"
-      a <- quote ctx.lvl ty'
-      b <- quote ctx.lvl ty
-      let msg = "unification failure: \{errorMsg err}\n  failed to unify \{rpprint names a}\n             with \{rpprint names b}\n  "
-      throwError (E fc msg)
+      throwError $ UnificationError fc names ty' ty err
     case res of
       MkResult Nil => pure MkUnit
       cs => do

src/Lib/Error.newt

@@ -1,30 +1,26 @@
 module Lib.Error
 
 import Prelude
+import Lib.Types
+import Lib.Eval
 import Lib.Common
 
--- I'll want to get Context / Val in some of these
--- and a pretty printer in the monad
-data Error
-  = E FC String
-  | ENotInScope FC String
-  | Postpone FC QName String
+prettyErrorMsg : Error -> M String
+prettyErrorMsg (E x str) = pure str
+prettyErrorMsg (ENotInScope x nm) = pure "\{nm} not in scope"
+prettyErrorMsg (Postpone x k str) = pure str
+prettyErrorMsg (UnificationError fc names a b err) = do
+  let lvl = length' names
+  a <- quote lvl a
+  b <- quote lvl b
+  pure "unification failure: \{errorMsg err}\n  failed to unify \{rpprint names a}\n             with \{rpprint names b}\n  "
 
-
-instance HasFC Error where
-  getFC (E x str) = x
-  getFC (ENotInScope x _) = x
-  getFC (Postpone x k str) = x
-
-errorMsg : Error -> String
-errorMsg (E x str) = str
-errorMsg (ENotInScope x nm) = "\{nm} not in scope"
-errorMsg (Postpone x k str) = str
-
-showError : (src : String) -> Error -> String
-showError src err =
+-- Use prettyError when possible
+showError : (src : String) -> Error -> M String
+showError src err = do
     let fc = getFC err
-  in "ERROR at \{show $ getFC err}: \{errorMsg err}\n" ++ go fc 0 (lines src)
+    msg <- prettyErrorMsg err
+    pure $ "ERROR at \{show fc}: \{msg}\n" ++ go fc 0 (lines src)
   where
     go : FC → Int → List String → String
     go fc l Nil = ""
@@ -35,3 +31,4 @@ showError src err =
       else if fcLine fc - 3 < l then "  " ++ x ++ "\n" ++ go fc (l + 1) xs
       else go fc (l + 1) xs
 
+

src/Lib/Eval.newt

@@ -9,7 +9,7 @@ import Lib.TopContext
 import Data.IORef
 import Data.SnocList
 import Data.SortedMap
-import Lib.Error
+
 
 eval : Env -> Tm -> M Val
 
@@ -329,7 +329,7 @@ zonkApp top l env t sp = do
     x <- zonk top l env t'
     pure x)
     (\err => do
-      debug $ \_ => "result err \{showError "" err}"
+      debug $ \_ => "result err \{show err}"
       pure $ appSpine t' sp)
   where
     -- lookup name and return Def if flagged inline

src/Lib/Parser/Impl.newt

@@ -7,7 +7,7 @@ import Data.String
 import Data.Int
 import Data.List1
 import Data.SortedMap
-import Lib.Error
+import Lib.Types
 
 TokenList : U
 TokenList = List BTok

src/Lib/ProcessDecl.newt

@@ -6,7 +6,7 @@ import Data.String
 
 import Lib.Common
 import Lib.Elab
-import Lib.Error
+
 import Lib.Parser
 import Lib.Syntax
 import Data.SortedMap

src/Lib/ProcessModule.newt

@@ -146,7 +146,7 @@ processModule importFC repo stk modns = do
 
   top <- getTop
   -- print errors (for batch processing case)
-  for_ (reverse top.currentMod.modErrors) $ \ err => putStrLn $ showError src err
+  for_ (reverse top.currentMod.modErrors) $ showError src >=> putStrLn
 
   -- update modules with result, leave the rest of context in case this is top file
   top <- getTop

src/Lib/Tokenizer.newt

@@ -12,7 +12,7 @@ import Lib.Token
 import Lib.Common
 import Data.String
 import Data.SnocList
-import Lib.Error
+import Lib.Types
 
 standalone : List Char
 standalone = unpack "()\\{}[],.@;"

src/Lib/TopContext.newt

@@ -6,7 +6,7 @@ import Data.String
 import Prelude
 import Lib.Common
 import Lib.Types
-import Lib.Error
+
 
 -- TODO move the def in here (along with M) or merge this into types
 -- The Monad can be its own file if we pull all of the monad update functions there.

src/Lib/Types.newt

@@ -3,7 +3,6 @@ module Lib.Types
 import Prelude
 import Lib.Common
 import Lib.Prettier
-import Lib.Error
 
 import Data.IORef
 import Data.SnocList
@@ -235,6 +234,33 @@ data MetaKind = Normal | User | AutoSolve | ErrorHole
 derive Show MetaKind
 derive Eq MetaKind
 
+rpprint : List String → Tm → String
+rpprint names tm = render 90 $ pprint names tm
+
+-- In types so we can have Val / Tm / Context
+data Error
+  = E FC String
+  | ENotInScope FC String
+  | Postpone FC QName String
+  | UnificationError FC (List String) Val Val Error
+
+instance HasFC Error where
+  getFC (E x str) = x
+  getFC (UnificationError fc _ _ _ _) = fc
+  getFC (ENotInScope x _) = x
+  getFC (Postpone x k str) = x
+
+-- Non-pretty version, there is an in-monad prettyErrorMsg in Lib.Error
+errorMsg : Error -> String
+errorMsg (E x str) = str
+errorMsg (ENotInScope x nm) = "\{nm} not in scope"
+errorMsg (Postpone x k str) = str
+errorMsg (UnificationError fc names a b err) =
+  "unification failure: \{errorMsg err}\n  failed to unify \{show a}\n             with \{show b}\n  "
+
+instance Show Error where
+  show err = "ERROR at \{show $ getFC err}: \{errorMsg err}\n"
+
 -- constrain meta applied to val to be a val
 
 data MConstraint = MkMc FC Env (SnocList Val) Val
@@ -536,4 +562,3 @@ profile desc work = do
   end <- getTime
   putStrLn "PROF \{desc} \{show $ end - start} ms"
   pure res
-

src/Main.newt

@@ -8,6 +8,7 @@ import Lib.CompileJS
 import Lib.CompileScheme
 import Lib.Parser
 import Lib.Elab
+import Lib.Error
 import Lib.Util
 import Lib.Parser.Impl
 import Lib.Prettier
@@ -20,7 +21,6 @@ import Lib.Syntax
 import Lib.ReplParser
 import Node
 import Revision
-import Lib.Error
 
 dirFileSource : String → FileSource
 dirFileSource base = MkFileSource base $ \fc fn => do
@@ -177,10 +177,10 @@ runCommand DumpTop = do
 runString : String → M Unit
 runString line = do
   let (Right toks) = tokenise "<stdin>" line
-    | Left err => putStrLn (showError line err)
+    | Left err => showError line err >>= putStrLn
   let (Right cmd) = parse "<stdin>" parseCommand toks
-    | Left err => putStrLn (showError line err)
-  catchError (runCommand cmd) (\ err => putStrLn $ showError line err)
+    | Left err => showError line err >>= putStrLn
+  catchError (runCommand cmd) (showError line >=> putStrLn)
 
 runRepl : M Unit
 runRepl = do

src/Prelude.newt

@@ -102,7 +102,7 @@ class Monad (m : U → U) where
   bind : ∀ a b. m a → (a → m b) → m b
   pure : ∀ a. a → m a
 
-infixl 1 _>>=_ _>>_
+infixl 1 _>>=_ _>>_ _>=>_
 _>>=_ : ∀ m a b. {{Monad m}} → (m a) → (a → m b) → m b
 ma >>= amb = bind ma amb
 
@@ -112,6 +112,9 @@ ma >> mb = bind ma (\ _ => mb)
 join : ∀ m a. {{Monad m}} → m (m a) → m a
 join mma = mma >>= id
 
+_>=>_ : ∀ m a b c. {{Monad m}} → (a → m b) → (b → m c) → a → m c
+(mab >=> mac) a = mab a >>= mac
+
 -- Equality
 
 infixl 1 _≡_