heartbreaking: Quox.Error doesn't actually work

exe/src/Main.idr

@@ -3,7 +3,6 @@ module Main
 import public Quox.Name
 import public Quox.Syntax
 import public Quox.Equal
-import public Quox.Error
 import public Quox.Pretty
 import public Quox.Typechecker
 

lib/quox-lib.ipkg

@@ -9,7 +9,6 @@ depends = base, contrib, elab-util, sop
 
 sourcedir = "src"
 modules =
-  Quox.Error,
   Quox.NatExtra,
   Quox.OPE,
   Quox.Pretty,

lib/src/Quox/Equal.idr

@@ -2,7 +2,7 @@ module Quox.Equal
 
 import public Quox.Syntax
 import public Quox.Reduce
-import Quox.Error
+import Control.Monad.Either
 
 %default total
 
@@ -22,14 +22,14 @@ private %inline
 ClashE : Mode -> Elim d n -> Elim d n -> Error
 ClashE mode = ClashT mode `on` E
 
-parameters {auto _ : MonadThrow Error m}
+parameters {auto _ : MonadError Error m}
   private %inline
   clashT : Mode -> Term d n -> Term d n -> m a
-  clashT mode = throw .: ClashT mode
+  clashT mode = throwError .: ClashT mode
 
   private %inline
   clashE : Mode -> Elim d n -> Elim d n -> m a
-  clashE mode = throw .: ClashE mode
+  clashE mode = throwError .: ClashE mode
 
   mutual
     private covering
@@ -39,13 +39,13 @@ parameters {auto _ : MonadThrow Error m}
 
     compareTN' mode (TYPE k) (TYPE l) _ _ =
       case mode of
-           Equal => unless (k == l) $ throw $ ClashU Equal k l
+           Equal => unless (k == l) $ throwError $ ClashU Equal k l
-           Sub   => unless (k <= l) $ throw $ ClashU Sub   k l
+           Sub   => unless (k <= l) $ throwError $ ClashU Sub   k l
     compareTN' mode s@(TYPE _) t _ _ = clashT mode s t
 
     compareTN' mode (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
       -- [todo] this should probably always be ==, right..?
-      unless (qty1 == qty2) $ throw $ ClashQ qty1 qty2
+      unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
       compareT0  mode arg2 arg1 -- reversed for contravariant Sub
       compareTS0 mode res1 res2
     compareTN' mode s@(Pi {}) t _ _ = clashT mode s t

lib/src/Quox/Error.idr

@@ -1,325 +0,0 @@
-module Quox.Error
-
-import public Data.List.Elem
-
-import public Control.Monad.Identity
-import Control.Monad.Trans
-import Control.Monad.Reader
-import Control.Monad.Writer
-import Control.Monad.State
-import Control.Monad.RWS
-
-%default total
-
-
-||| a representation of a list's length. this is used in `implyAll` to transform
-||| the constraints one by one
-public export
-data Spine : List a -> Type where
-  NIL  : Spine []
-  CONS : Spine xs -> Spine (x :: xs)
-%builtin Natural Spine
-
-
-||| if `types` is a `List Type`, then `OneOf types` is a value of one of them.
-||| (along with a pointer to which type it is.)
-public export
-record OneOf types where
-  constructor One
-  elem    : type `Elem` types
-  1 value : type
--- this is basically the same as Data.OpenUnion, but using Elem instead of
--- AtIndex is much easier for some stuff here e.g. `get`
-
-export
-Uninhabited (OneOf []) where uninhabited x = uninhabited x.elem
-
-
-export %inline
-one : ty `Elem` types => ty -> OneOf types
-one @{elem} value = One {elem, value}
-
-||| `All p types` computes a constraint for `p a` for each `a` in `types`
-public export
-All : (Type -> Type) -> List Type -> Type
-All p = foldr (,) () . map p
-
-
-private
-eq : All Eq types => OneOf types -> OneOf types -> Bool
-eq (One Here      x) (One Here      y) = x == y
-eq (One (There p) x) (One (There q) y) = eq (One p x) (One q y)
-eq (One Here      _) (One (There _) _) = False
-eq (One (There _) _) (One Here      _) = False
-
-export %inline
-All Eq types => Eq (OneOf types) where (==) = eq
-
-
-export
-implyAll : (0 c, d : Type -> Type) ->
-           (forall a. c a -> d a) => Spine types => All c types => All d types
-implyAll c d @{q} @{spine} @{ps} = go spine ps where
-  go : forall types. Spine types -> All c types -> All d types
-  go NIL       _       = ()
-  go (CONS tl) (p, ps) = (q p, go tl ps)
-
-
-private %inline
-[eqOrds] (Spine types, All Ord types) => Eq (OneOf types) where
-  (==) = eq @{implyAll Ord Eq}
-
-
-private
-cmp : All Ord types => (x, y : OneOf types) -> Ordering
-cmp (One Here      x) (One Here      y) = compare x y
-cmp (One Here      _) (One (There _) _) = LT
-cmp (One (There _) _) (One Here      _) = GT
-cmp (One (There p) x) (One (There q) y) = cmp (One p x) (One q y)
-
-export %inline
-(Spine types, All Ord types) => Ord (OneOf types) using eqOrds where
-  compare = cmp
-
-
-export %inline
-All Show types => Show (OneOf types) where
-  showPrec d = go where
-    go : forall types. All Show types => OneOf types -> String
-    go (One Here      value) = showPrec d value
-    go (One (There p) value) = go $ One p value
-
-
-public export
-record ErrorT (errs : List Type) (m : Type -> Type) (res : Type) where
-  constructor MkErrorT
-  runErrorT : m (Either (OneOf errs) res)
-
-public export
-Error : List Type -> Type -> Type
-Error errs = ErrorT errs Identity
-
-export
-runError : Error errs a -> Either (OneOf errs) a
-runError = runIdentity . runErrorT
-
-
-export %inline
-Functor m => Functor (ErrorT errs m) where
-  map f (MkErrorT act) = MkErrorT $ map (map f) act
-
-export %inline
-Applicative m => Applicative (ErrorT errs m) where
-  pure = MkErrorT . pure . pure
-  MkErrorT mf <*> MkErrorT mx = MkErrorT [|mf <*> mx|]
-
-export %inline
-Monad m => Monad (ErrorT errs m) where
-  MkErrorT act >>= k = MkErrorT $ act >>= either (pure . Left) (runErrorT . k)
-
-
-private
-without' : (xs : List a) -> x `Elem` xs -> List a
-without' (_ :: xs) Here      = xs
-without' (y :: xs) (There p) = y :: without' xs p
-
-infix 9 `without`
-export %inline
-without : (xs : List a) -> (x : a) -> x `Elem` xs => List a
-(xs `without` x) @{e} = without' xs e
-
-
-private
-get' : err `Elem` errs -> OneOf errs -> Either err (OneOf (errs `without` err))
-get' Here      (One Here      x) = Left x
-get' Here      (One (There p) x) = Right (One p x)
-get' (There y) (One Here      x) = Right (One Here x)
-get' (There y) (One (There p) x) = mapSnd {elem $= There} $ get' y (One p x)
-
-export %inline
-get : (0 err : Type) -> err `Elem` errs =>
-      OneOf errs -> Either err (OneOf (errs `without` err))
-get _ @{e} = get' e
-
-
-export %inline
-noErrorsT : Monad m => ErrorT [] m a -> m a
-noErrorsT (MkErrorT act) = act >>= either absurd pure
-
-export %inline
-noErrors : Error [] a -> a
-noErrors = runIdentity . noErrorsT
-
-
-public export
-data Embed : List a -> List a -> Type where
-  Nil  : Embed [] ys
-  (::) : x `Elem` ys -> Embed xs ys -> Embed (x::xs) ys
-
-
-export %inline
-embedElem : Embed xs ys => x `Elem` xs -> x `Elem` ys
-embedElem @{emb} = go emb where
-  go : forall xs. Embed xs ys -> x `Elem` xs -> x `Elem` ys
-  go (e :: _)  Here      = e
-  go (_ :: es) (There p) = go es p
-
-
-export %inline
-(<|>) : Applicative m => ErrorT errs m a -> ErrorT errs m a -> ErrorT errs m a
-MkErrorT act1 <|> MkErrorT act2 = MkErrorT [|act1 `or` act2|] where
-  or : Either l r -> Either l r -> Either l r
-  one `or` two = case one of Left err => two; Right x => pure x
-
-
-public export
-interface Monad m => MonadThrow err m where
-  throw : err -> m a
-
-public export
-interface MonadThrow err m1 => MonadCatch err m1 m2 | err, m1 where
-  catch : (act : m1 a) -> (catch : err -> m2 a) -> m2 a
-
-public export
-interface (Monad m1, Monad m2) => MonadEmbed m1 m2 where embed : m1 a -> m2 a
-
-public export
-MonadThrows : (errs : List Type) -> (m : Type -> Type) -> Type
-MonadThrows []          m = Monad m
-MonadThrows (ty :: tys) m = (MonadThrow ty m, MonadThrows tys m)
-
-
-export %inline
-implementation
-  (Monad m, err `Elem` errs) =>
-  MonadThrow err (ErrorT errs m)
-where
-  throw = MkErrorT . pure . Left . one
-
-export %inline
-implementation
-  (Monad m, err `Elem` errs) =>
-  MonadCatch err (ErrorT errs m) (ErrorT (errs `without` err) m)
-where
-  catch (MkErrorT act) handler = MkErrorT $
-    act <&> mapFst (get err) >>= \case
-      Left (Left  this)  => runErrorT $ handler this
-      Left (Right other) => pure $ Left other
-      Right ok           => pure $ Right ok
-
-export %inline
-implementation
-  (Monad m, Embed errs1 errs2) =>
-  MonadEmbed (ErrorT errs1 m) (ErrorT errs2 m)
-where
-  embed (MkErrorT act) = MkErrorT $ act <&> mapFst {elem $= embedElem}
-
-
-export %inline
-MonadTrans (ErrorT errs) where lift = MkErrorT . map Right
-
-export %inline
-MonadReader r m => MonadReader r (ErrorT errs m) where
-  local f (MkErrorT act) = MkErrorT $ local f act
-  ask = lift ask
-
-export %inline
-MonadWriter w m => MonadWriter w (ErrorT errs m) where
-  tell = MkErrorT . map Right . tell
-
-  pass (MkErrorT act) = MkErrorT $ pass $ do
-    Right (res, f) <- act
-        | Left err => pure (Left err, id)
-    pure (Right res, f)
-
-  listen (MkErrorT act) = MkErrorT $ do
-    (res, x) <- listen act
-    pure $ mapSnd (,x) res
-
-export %inline
-MonadState s m => MonadState s (ErrorT errs m) where
-  get   = lift get
-  put   = lift . put
-  state = lift . state
-
-export %inline
-MonadRWS r w s m => MonadRWS r w s (ErrorT errs m) where
-
-export %inline
-HasIO m => HasIO (ErrorT errs m) where
-  liftIO = MkErrorT . map Right . liftIO
-
-
-export %inline
-MonadThrow err m => MonadThrow err (ReaderT r m) where throw = lift . throw
-
-export %inline
-MonadThrow err m => MonadThrow err (WriterT w m) where throw = lift . throw
-
-export %inline
-MonadThrow err m => MonadThrow err (StateT s m) where throw = lift . throw
-
-export %inline
-MonadThrow err m => MonadThrow err (RWST r w s m) where throw = lift . throw
-
-
-export %inline
-implementation
-  MonadCatch err m1 m2 =>
-  MonadCatch err (ReaderT r m1) (ReaderT r m2)
-where
-  catch (MkReaderT act) handler = MkReaderT $ \r =>
-    act r `catch` runReaderT r . handler
-
-export %inline
-implementation
-  MonadCatch err m1 m2 =>
-  MonadCatch err (WriterT w m1) (WriterT w m2)
-where
-  catch (MkWriterT act) handler = MkWriterT $ \w =>
-    act w `catch` \e => unWriterT (handler e) w
-
-export %inline
-implementation
-  MonadCatch err m1 m2 =>
-  MonadCatch err (StateT s m1) (StateT s m2)
-where
-  catch (ST act) handler = ST $ \s =>
-    act s `catch` \e => runStateT' (handler e) s
-
-export %inline
-implementation
-  MonadCatch err m1 m2 =>
-  MonadCatch err (RWST r w s m1) (RWST r w s m2)
-where
-  catch (MkRWST act) handler = MkRWST $ \r, s, w =>
-    act r s w `catch` \e => unRWST (handler e) r s w
-
-
-export %inline
-implementation
-  MonadEmbed m1 m2 =>
-  MonadEmbed (ReaderT r m1) (ReaderT r m2)
-where
-  embed (MkReaderT act) = MkReaderT $ embed . act
-
-export %inline
-implementation
-  MonadEmbed m1 m2 =>
-  MonadEmbed (WriterT w m1) (WriterT w m2)
-where
-  embed (MkWriterT act) = MkWriterT $ embed . act
-
-export %inline
-implementation
-  MonadEmbed m1 m2 =>
-  MonadEmbed (StateT s m1) (StateT s m2)
-where
-  embed (ST act) = ST $ embed . act
-
-export %inline
-implementation
-  MonadEmbed m1 m2 =>
-  MonadEmbed (RWST r w s m1) (RWST r w s m2)
-where
-  embed (MkRWST act) = MkRWST $ \r, s, w => embed $ act r s w

lib/src/Quox/Lexer.idr

@@ -1,12 +1,12 @@
 module Quox.Lexer
 
-import Quox.Error
 import public Quox.Token
 
 import Data.String
 import Data.String.Extra
 import public Text.Lexer
 import public Text.Lexer.Tokenizer
+import Control.Monad.Either
 import Generics.Derive
 
 %default total
@@ -117,10 +117,10 @@ tokens = choice [
 
 
 export
-lex : MonadThrow Error m => String -> m (List (WithBounds Token))
+lex : MonadError Error m => String -> m (List (WithBounds Token))
 lex str =
   let (res, (reason, line, col, str)) = lex tokens str in
   case reason of
        EndInput => pure $ mapMaybe sequence res
        _        => let char = assert_total strIndex str 0 in
-                   throw $ Err {reason, line, col, char}
+                   throwError $ Err {reason, line, col, char}

lib/src/Quox/Typechecker.idr

@@ -2,34 +2,36 @@ module Quox.Typechecker
 
 import public Quox.Syntax
 import public Quox.Typing
-import Quox.Error
+import Control.Monad.Either
 
+%hide Equal.Error
 %default total
 
 
 private covering %inline
-expectTYPE : MonadThrow Typing.Error m => Term d n -> m Universe
+expectTYPE : MonadError Error m => Term d n -> m Universe
 expectTYPE s =
   case (whnfT s).fst of
        TYPE l => pure l
-       _      => throw $ ExpectedTYPE s
+       _      => throwError $ ExpectedTYPE s
 
 private covering %inline
-expectPi : MonadThrow Typing.Error m => Term d n ->
+expectPi : MonadError Error m => Term d n ->
            m (Qty, Term d n, ScopeTerm d n)
 expectPi ty =
   case (whnfT ty).fst of
        Pi qty _ arg res => pure (qty, arg, res)
-       _                => throw $ ExpectedPi ty
+       _                => throwError $ ExpectedPi ty
 
 private %inline
-expectEqualQ : MonadThrow Equal.Error m =>
+expectEqualQ : MonadError Error m =>
                (expect, actual : Qty) -> m ()
-expectEqualQ pi rh = unless (pi == rh) $ throw $ ClashQ pi rh
+expectEqualQ pi rh =
+  unless (pi == rh) $ throwError $ EqualError $ ClashQ pi rh
 
 
 private %inline
-popQ : MonadThrow Equal.Error m => Qty -> QOutput (S n) -> m (QOutput n)
+popQ : MonadError Error m => Qty -> QOutput (S n) -> m (QOutput n)
 popQ pi (qctx :< rh) = expectEqualQ pi rh $> qctx
 
 
@@ -71,14 +73,14 @@ mutual
   -- computer but pushing is less work for the me
 
   export covering %inline
-  check : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
+  check : MonadError Error m => {d, n : Nat} ->
           (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
           (subj : Term d n) -> (ty : Term d n) ->
           m (CheckResult n)
   check ctx sg subj ty = check' ctx sg (pushSubstsT subj) ty
 
   export covering %inline
-  infer : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
+  infer : MonadError Error m => {d, n : Nat} ->
           (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
           (subj : Elim d n) ->
           m (InferResult d n)
@@ -86,7 +88,7 @@ mutual
 
 
   export covering
-  check' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
+  check' : MonadError Error m => {d, n : Nat} ->
            (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
            (subj : NotCloTerm d n) -> (ty : Term d n) ->
            m (CheckResult n)
@@ -94,7 +96,7 @@ mutual
   check' ctx sg (Element (TYPE l) _) ty = do
     l' <- expectTYPE ty
     expectEqualQ zero sg
-    unless (l < l') $ throw $ BadUniverse l l'
+    unless (l < l') $ throwError $ BadUniverse l l'
     pure zero
 
   -- [todo] factor this stuff out
@@ -117,11 +119,11 @@ mutual
   check' ctx sg (Element (E e) _) ty = do
     infres <- infer ctx sg e
     ignore $ check ctx zero ty (TYPE UAny)
-    infres.type `subT` ty
+    either (throwError . EqualError) pure $ infres.type `subT` ty
     pure infres.qout
 
   export covering
-  infer' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
+  infer' : MonadError Error m => {d, n : Nat} ->
            (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
            (subj : NotCloElim d n) ->
            m (InferResult d n)
@@ -131,7 +133,7 @@ mutual
          Just g => do
            expectEqualQ (globalSubjQty g) sg
            pure $ InfRes {type = g.type, qout = zero}
-         Nothing => throw $ NotInScope x
+         Nothing => throwError $ NotInScope x
 
   infer' ctx sg (Element (B i) _) =
     pure $ lookupBound sg i ctx

lib/src/Quox/Typing.idr

@@ -101,7 +101,9 @@ record InferResult d n where
 
 public export
 data Error
-= NotInScope Name
+= NotInScope   Name
 | ExpectedTYPE (Term d n)
 | ExpectedPi   (Term d n)
-| BadUniverse Universe Universe
+| BadUniverse  Universe Universe
+| EqualError   (Equal.Error)
+%hide Equal.Error

tests/src/TAP.idr

@@ -1,8 +1,7 @@
 module TAP
 -- [todo] extract this and Quox.Error to their own packages
 
-import public Quox.Error
+import public Control.Monad.Either
-
 import Data.String
 import Data.List.Elem
 import Data.SnocList
@@ -40,11 +39,6 @@ toLines xs = "---" :: concatMap toLines1 xs <+> ["..."]
 
 public export interface ToInfo e where toInfo : e -> Info
 
-export
-All ToInfo es => ToInfo (OneOf es) where
-  toInfo (One Here      value) = toInfo value
-  toInfo (One (There x) value) = toInfo (One x value)
-
 export %inline ToInfo () where toInfo () = []
 
 export %inline Show a => ToInfo (List (String, a)) where toInfo = map (map show)
@@ -67,16 +61,16 @@ lazyToIO : Lazy a -> IO a
 lazyToIO val = primIO $ \w => MkIORes (force val) w
 
 export
-testIO : (All ToInfo es, ToInfo a) => String -> ErrorT es IO a -> Test
+testIO : (ToInfo e, ToInfo a) => String -> EitherT e IO a -> Test
 testIO label act = One $ MakeTest label $ do
-  case !(runErrorT act) of
+  case !(runEitherT act) of
        Right val => success val
        Left  err => failure err
 
 export %inline
-test : (All ToInfo es, ToInfo a) => String -> Lazy (Error es a) -> Test
+test : (ToInfo e, ToInfo a) => String -> Lazy (Either e a) -> Test
 test label val =
-  testIO label $ MkErrorT $ lazyToIO $ runError val
+  testIO label $ MkEitherT $ lazyToIO val
 
 export %inline
 todoWith : String -> String -> Test
@@ -100,10 +94,11 @@ skip : Test -> Test
 skip test = skipWith test ""
 
 export
-testThrows : Show a => String -> Lazy (Error es a) -> Test
+testThrows : (ToInfo e, Show a) =>
-testThrows label act = One $ MakeTest label $ do
+             String -> (e -> Bool) -> Lazy (Either e a) -> Test
-  case runError !(lazyToIO act) of
+testThrows label p act = One $ MakeTest label $ do
-       Left  err => success ()
+  case !(lazyToIO act) of
+       Left  err => if p err then success () else failure err
        Right val => failure [("success", val)]
 
 infix 0 :-

tests/src/Tests.idr

@@ -9,7 +9,7 @@ import System
 
 allTests = [
   Lexer.tests,
-  skip Equal.tests
+  Equal.tests
 ]
 
 main = do

tests/src/Tests/Equal.idr

@@ -22,13 +22,13 @@ ToInfo Equal.Error where
      ("right", prettyStr True rh)]
 
 
-M = Error [Equal.Error]
+M = Either Equal.Error
 
 testEq : String -> Lazy (M ()) -> Test
 testEq = test
 
 testNeq : String -> Lazy (M ()) -> Test
-testNeq = testThrows
+testNeq label = testThrows label $ const True
 
 
 subT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()

tests/src/Tests/Lexer.idr

@@ -4,31 +4,39 @@ import Quox.Lexer
 import TAP
 
 
+RealError = Quox.Lexer.Error
+%hide Quox.Lexer.Error
+
 export
-ToInfo Error where
+ToInfo RealError where
   toInfo (Err reason line col char) =
     [("reason", show reason),
      ("line",   show line),
      ("col",    show col),
      ("char",   show char)]
 
-data ExtraError
+data Error
-= WrongAnswer (List Token) (List Token)
+= LexerError RealError
+| WrongAnswer (List Token) (List Token)
 | TestFailed  (List Token)
 
-ToInfo ExtraError where
+ToInfo Error where
+  toInfo (LexerError err) = toInfo err
   toInfo (WrongAnswer exp got) =
     [("expected", show exp), ("received", show got)]
   toInfo (TestFailed got) =
     [("failed", show got)]
 
 
+lex' : String -> Either Error (List Token)
+lex' = bimap LexerError (map val) . lex
+
 parameters (label : String) (input : String)
-  acceptsSuchThat' : (List Token -> Maybe ExtraError) -> Test
+  acceptsSuchThat' : (List Token -> Maybe Error) -> Test
-  acceptsSuchThat' p = test {es = [Lexer.Error, ExtraError]} label $ do
+  acceptsSuchThat' p = test label $ delay $ do
-    res <- map val <$> lex input
+    res <- bimap LexerError (map val) $ lex input
     case p res of
-         Just err => throw err
+         Just err => throwError err
          Nothing  => pure ()
 
   acceptsSuchThat : (List Token -> Bool) -> Test
@@ -43,8 +51,8 @@ parameters (label : String) (input : String)
   accepts = acceptsSuchThat $ const True
 
   rejects : Test
-  rejects = testThrows {es = [Lexer.Error]} label $ delay $
+  rejects = testThrows label (\case LexerError _ => True; _ => False) $ delay $
-    map val <$> lex input
+            bimap LexerError (map val) $ lex {m = Either RealError} input
 
 parameters (input : String) {default False esc : Bool}
   show' : String -> String