From acfa1b96bea424e2df06ceebcfb820b3436c395e Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 23 Dec 2021 16:05:55 +0100
Subject: [PATCH] bikeshedding again

---
 src/Quox/Error.idr | 54 ++++++++++++++++++++++++----------------------
 1 file changed, 28 insertions(+), 26 deletions(-)

diff --git a/src/Quox/Error.idr b/src/Quox/Error.idr
index bbe8b0f..2175057 100644
--- a/src/Quox/Error.idr
+++ b/src/Quox/Error.idr
@@ -12,8 +12,8 @@ import Control.Monad.RWS
 %default total
 
 
-||| a representation of a list's length. this is used in the `Ord` instance to
-||| transform the `Ord` constraints into `Eq`s
+||| 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 []
@@ -37,13 +37,12 @@ Uninhabited (OneOf []) where uninhabited x = uninhabited x.elem
 
 export %inline
 inj : ty `Elem` tys => ty -> OneOf tys
-inj value = One %search value
+inj @{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 []      = ()
-All p (x::xs) = (p x, All p xs)
+All p = foldr (,) () . map p
 
 
 private
@@ -51,24 +50,28 @@ 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 z) x) (One Here      y) = False
+eq (One (There _) _) (One Here      _) = False
 
 export %inline
 All Eq types => Eq (OneOf types) where (==) = eq
 
 
-private
-ordsToEqs : Spine types => All Ord types => All Eq types
-ordsToEqs @{NIL}     = ()
-ordsToEqs @{CONS tl} = (%search, ordsToEqs @{tl})
+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 @{ordsToEqs}
+  (==) = eq @{implyAll Ord Eq}
 
 
 private
-cmp : All Ord types => OneOf types -> OneOf types -> Ordering
+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
@@ -79,11 +82,12 @@ export %inline
   compare = cmp
 
 
-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
+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
@@ -122,7 +126,7 @@ 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 = without' {x} xs %search
+(xs `without` x) @{e} = without' xs e
 
 
 private
@@ -135,7 +139,7 @@ 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 _ = get' %search
+get _ @{e} = get' e
 
 
 export %inline
@@ -153,14 +157,12 @@ data Embed : List a -> List a -> Type where
   (::) : x `Elem` ys -> Embed xs ys -> Embed (x::xs) ys
 
 
-private
-embedElem' : Embed xs ys -> x `Elem` xs -> x `Elem` ys
-embedElem' (e :: _)  Here      = e
-embedElem' (_ :: es) (There p) = embedElem' es p
-
 export %inline
 embedElem : Embed xs ys => x `Elem` xs -> x `Elem` ys
-embedElem = embedElem' %search
+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
@@ -205,7 +207,7 @@ implementation
   (Monad m, Embed errs1 errs2) =>
   MonadEmbed (ErrorT errs1 m) (ErrorT errs2 m)
 where
-  embed (MkErrorT act) = MkErrorT $ mapFst {elem $= embedElem} <$> act
+  embed (MkErrorT act) = MkErrorT $ act <&> mapFst {elem $= embedElem}
 
 
 export %inline