From cdcd926347c54b7ca1c5580a85fb0b43480ae455 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 25 Sep 2021 20:13:13 +0200
Subject: [PATCH] improve error interfaces

---
 src/Quox/Error.idr | 93 +++++++++++++++++++++-------------------------
 1 file changed, 43 insertions(+), 50 deletions(-)

diff --git a/src/Quox/Error.idr b/src/Quox/Error.idr
index 4d2491b..a78cabb 100644
--- a/src/Quox/Error.idr
+++ b/src/Quox/Error.idr
@@ -10,6 +10,8 @@ import Control.Monad.RWS
 %default total
 
 
+||| a proof that an element is in a list. unlike the standard library one, this
+||| is represented as a single number at runtime.
 public export
 data Elem : a -> List a -> Type where
   Here  : x `Elem` (x :: xs)
@@ -22,6 +24,8 @@ Uninhabited (x `Elem` []) where
   uninhabited (There _) impossible
 
 
+||| a representation of a list's length. this is used in the `Ord` instance to
+||| transform the `Ord` constraints into `Eq`s
 public export
 data Spine : List a -> Type where
   NIL  : Spine []
@@ -29,6 +33,8 @@ data Spine : List a -> Type where
 %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
@@ -43,6 +49,7 @@ export %inline
 inj : ty `Elem` tys => ty -> OneOf tys
 inj value = One %search 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 []      = ()
@@ -56,7 +63,7 @@ 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 z) x) (One Here      y) = False
 
-export
+export %inline
 All Eq types => Eq (OneOf types) where (==) = eq
 
 
@@ -65,7 +72,7 @@ ordsToEqs : Spine types => All Ord types => All Eq types
 ordsToEqs @{NIL}     = ()
 ordsToEqs @{CONS tl} = (%search, ordsToEqs @{tl})
 
-private
+private %inline
 [eqOrds] (Spine types, All Ord types) => Eq (OneOf types) where
   (==) = eq @{ordsToEqs}
 
@@ -77,15 +84,16 @@ 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
+export %inline
 (Spine types, All Ord types) => Ord (OneOf types) using eqOrds where
   compare = cmp
 
 
-export
-All Show types => Show (OneOf types) where
-  showPrec d (One Here      value) = showPrec d value
-  showPrec d (One (There p) value) = showPrec d $ One p value
+private shw : All Show types => Prec -> OneOf types -> String
+shw d (One Here      value) = showPrec d value
+shw d (One (There p) value) = shw d $ One p value
+
+export %inline All Show types => Show (OneOf types) where showPrec = shw
 
 
 public export
@@ -173,43 +181,28 @@ MkErrorT act1 <|> MkErrorT act2 = MkErrorT [|act1 `or` act2|] where
 
 
 public export
-interface Monad m => MonadThrow errs m | m where
-  throw : err `Elem` errs => err -> m a
+interface Monad m => MonadThrow err m where
+  throw : err -> m a
 
 public export
-interface
-  (MonadThrow errs1 m1,
-   MonadThrow errs2 m2,
-   err `Elem` errs1) =>
-  MonadCatch err errs1 errs2 m1 m2
-    | err, m1
-where
+interface MonadThrow err m1 => MonadCatch err m1 m2 | err, m1 where
   catch : (act : m1 a) -> (catch : err -> m2 a) -> m2 a
 
 public export
-interface
-  (MonadThrow errs1 m1,
-   MonadThrow errs2 m2,
-   Embed errs1 errs2) =>
-  MonadEmbed errs1 errs2 m1 m2
-    | m1, m2
-where
-  embed : m1 a -> m2 a
+interface (Monad m1, Monad m2) => MonadEmbed m1 m2 where embed : m1 a -> m2 a
 
 
 export %inline
 implementation
-  Monad m =>
-  MonadThrow errs (ErrorT errs m)
+  (Monad m, err `Elem` errs) =>
+  MonadThrow err (ErrorT errs m)
 where
   throw = MkErrorT . pure . Left . inj
 
 export %inline
 implementation
   (Monad m, err `Elem` errs) =>
-  MonadCatch err errs (errs `without` err)
-    (ErrorT errs m)
-    (ErrorT (errs `without` err) m)
+  MonadCatch err (ErrorT errs m) (ErrorT (errs `without` err) m)
 where
   catch (MkErrorT act) handler = MkErrorT $
     act <&> mapFst (get err) >>= \case
@@ -220,7 +213,7 @@ where
 export %inline
 implementation
   (Monad m, Embed errs1 errs2) =>
-  MonadEmbed errs1 errs2 (ErrorT errs1 m) (ErrorT errs2 m)
+  MonadEmbed (ErrorT errs1 m) (ErrorT errs2 m)
 where
   embed (MkErrorT act) = MkErrorT $ mapFst {elem $= embedElem} <$> act
 
@@ -261,46 +254,46 @@ HasIO m => HasIO (ErrorT errs m) where
 
 
 export %inline
-MonadThrow errs m => MonadThrow errs (ReaderT r m) where throw = lift . throw
+MonadThrow err m => MonadThrow err (ReaderT r m) where throw = lift . throw
 
 export %inline
-MonadThrow errs m => MonadThrow errs (WriterT w m) where throw = lift . throw
+MonadThrow err m => MonadThrow err (WriterT w m) where throw = lift . throw
 
 export %inline
-MonadThrow errs m => MonadThrow errs (StateT s m) where throw = lift . throw
+MonadThrow err m => MonadThrow err (StateT s m) where throw = lift . throw
 
 export %inline
-MonadThrow errs m => MonadThrow errs (RWST r w s m) where throw = lift . throw
+MonadThrow err m => MonadThrow err (RWST r w s m) where throw = lift . throw
 
 
 export %inline
 implementation
-  MonadCatch err errs1 errs2 m1 m2 =>
-  MonadCatch err errs1 errs2 (ReaderT r m1) (ReaderT r m2)
+  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 errs1 errs2 m1 m2 =>
-  MonadCatch err errs1 errs2 (WriterT w m1) (WriterT w m2)
+  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 errs1 errs2 m1 m2 =>
-  MonadCatch err errs1 errs2 (StateT s m1) (StateT s m2)
+  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 errs1 errs2 m1 m2 =>
-  MonadCatch err errs1 errs2 (RWST r w s m1) (RWST r w s m2)
+  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
@@ -308,28 +301,28 @@ where
 
 export %inline
 implementation
-  MonadEmbed errs1 errs2 m1 m2 =>
-  MonadEmbed errs1 errs2 (ReaderT r m1) (ReaderT r m2)
+  MonadEmbed m1 m2 =>
+  MonadEmbed (ReaderT r m1) (ReaderT r m2)
 where
   embed (MkReaderT act) = MkReaderT $ embed . act
 
 export %inline
 implementation
-  MonadEmbed errs1 errs2 m1 m2 =>
-  MonadEmbed errs1 errs2 (WriterT w m1) (WriterT w m2)
+  MonadEmbed m1 m2 =>
+  MonadEmbed (WriterT w m1) (WriterT w m2)
 where
   embed (MkWriterT act) = MkWriterT $ embed . act
 
 export %inline
 implementation
-  MonadEmbed errs1 errs2 m1 m2 =>
-  MonadEmbed errs1 errs2 (StateT s m1) (StateT s m2)
+  MonadEmbed m1 m2 =>
+  MonadEmbed (StateT s m1) (StateT s m2)
 where
   embed (ST act) = ST $ embed . act
 
 export %inline
 implementation
-  MonadEmbed errs1 errs2 m1 m2 =>
-  MonadEmbed errs1 errs2 (RWST r w s m1) (RWST r w s m2)
+  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