From ea74c148b70faf27b73f0ce11b2826b436cd605f Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 21 Oct 2023 20:48:28 +0200
Subject: [PATCH] some of this EffExtra stuff doesn't work

---
 lib/Quox/EffExtra.idr      | 28 ++++------------------------
 lib/Quox/Untyped/Erase.idr |  2 +-
 2 files changed, 5 insertions(+), 25 deletions(-)

diff --git a/lib/Quox/EffExtra.idr b/lib/Quox/EffExtra.idr
index 55edfef..6d9d311 100644
--- a/lib/Quox/EffExtra.idr
+++ b/lib/Quox/EffExtra.idr
@@ -69,17 +69,6 @@ subsetTail : Length xs => (0 x : a) -> Subset xs (x :: xs)
 subsetTail _ = subsetWith S
 
 
-export
-catchMaybeAt : (0 lbl : tag) -> (Has (ExceptL lbl e) fs, Length fs) =>
-               (e -> Eff fs a) -> Eff fs a -> Eff fs a
-catchMaybeAt lbl hnd act =
-  catchAt lbl hnd $ lift @{subsetTail $ ExceptL lbl e} act
-
-export %inline
-catchMaybe : (Has (Except e) fs, Length fs) =>
-             (e -> Eff fs a) -> Eff fs a -> Eff fs a
-catchMaybe = catchMaybeAt ()
-
 
 export
 rethrowAtWith : (0 lbl : tag) -> Has (ExceptL lbl e') fs =>
@@ -91,22 +80,13 @@ rethrowWith : Has (Except e') fs => (e -> e') -> Either e a -> Eff fs a
 rethrowWith = rethrowAtWith ()
 
 export
-wrapErr' : Length fs => (e -> e') ->
-           Eff (ExceptL lbl e  :: fs) a ->
-           Eff (ExceptL lbl e' :: fs) a
-wrapErr' f act =
+wrapErr : Length fs => (e -> e') ->
+          Eff (ExceptL lbl e  :: fs) a ->
+          Eff (ExceptL lbl e' :: fs) a
+wrapErr f act =
   catchAt lbl (throwAt lbl . f) @{S Z} $
   lift @{subsetTail _} act
 
-export
-wrapErrAt : (0 lbl : tag) -> (Has (ExceptL lbl e) fs, Length fs) =>
-            (e -> e) -> Eff fs a -> Eff fs a
-wrapErrAt lbl wrap = catchMaybeAt lbl (\ex => throwAt lbl $ wrap ex)
-
-export %inline
-wrapErr : (Has (Except e) fs, Length fs) => (e -> e) -> Eff fs a -> Eff fs a
-wrapErr = wrapErrAt ()
-
 
 export
 handleExcept : Functor m => (forall c. e -> m c) -> ExceptL lbl e a -> m a
diff --git a/lib/Quox/Untyped/Erase.idr b/lib/Quox/Untyped/Erase.idr
index afa5bc3..d14766d 100644
--- a/lib/Quox/Untyped/Erase.idr
+++ b/lib/Quox/Untyped/Erase.idr
@@ -87,7 +87,7 @@ Erase = [Except Error, DefsReader, NameGen]
 
 export
 liftWhnf : Eff Whnf a -> Eff Erase a
-liftWhnf act = lift $ wrapErr' WrapTypeError act
+liftWhnf act = lift $ wrapErr WrapTypeError act
 
 export covering
 computeElimType : ErasureContext d n -> SQty -> Elim d n -> Eff Erase (Term d n)