5 files changed, 28 insertions, 49 deletions
diff --git a/src/Inky/Data/Assoc.idr b/src/Inky/Data/Assoc.idr
index a009515..0818ba3 100644
--- a/src/Inky/Data/Assoc.idr
+++ b/src/Inky/Data/Assoc.idr
@@ -15,6 +15,18 @@ Functor Assoc where
 
 namespace Irrelevant
   public export
+  record Assoc0 (0 a : Type) (n : String) where
+    constructor (:-)
+    0 name : String
+    {auto 0 prf : n = name}
+    value : a
+
+  public export
+  map : (a -> b) -> Assoc0 a n -> Assoc0 b n
+  map f (n :- x) = n :- f x
+
+namespace Contexts
+  public export
   record Assoc0 (0 p : a -> Type) (x : Assoc a) where
     constructor (:-)
     0 name : String
diff --git a/src/Inky/Data/Context.idr b/src/Inky/Data/Context.idr
index 0d3df99..4c5f6cf 100644
--- a/src/Inky/Data/Context.idr
+++ b/src/Inky/Data/Context.idr
@@ -24,13 +24,11 @@ mapNames f (ctx :< nx) = cong (:< nx.name) $ mapNames f ctx
 -- Construction ----------------------------------------------------------------
 
 public export
-fromAll : (ctx : Context a) -> All (const b) ctx.names -> Context b
-fromAll [<] [<] = [<]
-fromAll (ctx :< (n :- _)) (sx :< x) = fromAll ctx sx :< (n :- x)
+fromAll : {sx : SnocList String} -> All (Assoc0 a) sx -> Context a
+fromAll [<] = [<]
+fromAll {sx = sx :< n} (ctx :< (_ :- x)) = fromAll ctx :< (n :- x)
 
 export
-fromAllNames :
-  (ctx : Context a) -> (sx : All (const b) ctx.names) ->
-  (fromAll ctx sx).names = ctx.names
-fromAllNames [<] [<] = Refl
-fromAllNames (ctx :< (n :- _)) (sx :< x) = cong (:< n) $ fromAllNames ctx sx
+fromAllNames : {sx : SnocList String} -> (ctx : All (Assoc0 a) sx) -> (fromAll ctx).names = sx
+fromAllNames [<] = Refl
+fromAllNames {sx = sx :< n} (ctx :< (k :- x)) = cong (:< n) $ fromAllNames ctx
diff --git a/src/Inky/Data/Irrelevant.idr b/src/Inky/Data/Irrelevant.idr
deleted file mode 100644
index ca72470..0000000
--- a/src/Inky/Data/Irrelevant.idr
+++ /dev/null
@@ -1,19 +0,0 @@
-module Inky.Data.Irrelevant
-
-public export
-record Irrelevant (a : Type) where
-  constructor Forget
-  0 value : a
-
-public export
-Functor Irrelevant where
-  map f x = Forget (f x.value)
-
-public export
-Applicative Irrelevant where
-  pure x = Forget x
-  f <*> x = Forget (f.value x.value)
-
-public export
-Monad Irrelevant where
-  join x = Forget (x.value.value)
diff --git a/src/Inky/Data/Row.idr b/src/Inky/Data/Row.idr
index 05e1fd0..42f18da 100644
--- a/src/Inky/Data/Row.idr
+++ b/src/Inky/Data/Row.idr
@@ -5,7 +5,6 @@ import public Inky.Data.Context
 import public Inky.Data.SnocList.Quantifiers
 
 import Inky.Data.SnocList.Elem
-import Inky.Data.Irrelevant
 import Inky.Decidable
 
 public export
@@ -77,8 +76,8 @@ snocCong :
 snocCong eq1 eq2 = rowCong $ cong2 (\x, y => x.context :< y) eq1 eq2
 
 public export
-fromAll : (row : Row a) -> All (const b) row.names -> Row b
-fromAll row sx = MkRow (fromAll row.context sx) (rewrite fromAllNames row.context sx in row.fresh)
+fromAll : {sx : SnocList String} -> (ctx : All (Assoc0 b) sx) -> (0 fresh : AllFresh sx) -> Row b
+fromAll ctx fresh = MkRow (fromAll ctx) (rewrite fromAllNames ctx in fresh)
 
 -- Interfaces ------------------------------------------------------------------
 
@@ -114,16 +113,14 @@ export
 isFresh :
   (names : SnocList String) ->
   (name : String) ->
-  Dec' (Irrelevant $ name `FreshIn` names)
-isFresh names name =
-  map irrelevant (\contra, prfs => anyNegAll contra $ relevant names prfs.value) $
-  all (\x => (decSo $ x /= name).forget) names
+  LazyEither (name `FreshIn` names) (Any (\x => So (x == name)) names)
+isFresh names name = all (\x => not (so $ x == name)) names
 
 export
 extend : Row a -> Assoc a -> Maybe (Row a)
-extend row x with (isFresh row.names x.name)
-  _ | True `Because` Forget prf = Just (row :< x)
-  _ | False `Because` _ = Nothing
+extend row x = case (isFresh row.names x.name) of
+  True `Because` prf => Just ((:<) row x @{prf})
+  False `Because` _ => Nothing
 
 -- Search ----------------------------------------------------------------------
 
diff --git a/src/Inky/Data/SnocList/Quantifiers.idr b/src/Inky/Data/SnocList/Quantifiers.idr
index ac6287b..886c4e4 100644
--- a/src/Inky/Data/SnocList/Quantifiers.idr
+++ b/src/Inky/Data/SnocList/Quantifiers.idr
@@ -3,7 +3,6 @@ module Inky.Data.SnocList.Quantifiers
 import public Data.SnocList.Quantifiers
 
 import Data.List.Quantifiers
-import Inky.Data.Irrelevant
 import Inky.Data.SnocList
 import Inky.Data.SnocList.Elem
 import Inky.Decidable
@@ -26,23 +25,15 @@ HSnocList : SnocList Type -> Type
 HSnocList = All id
 
 public export
-all : ((x : a) -> Dec' (p x)) -> (sx : SnocList a) -> LazyEither (All p sx) (Any (Not . p) sx)
+all :
+  ((x : a) -> LazyEither (p x) (q x)) ->
+  (sx : SnocList a) -> LazyEither (All p sx) (Any q sx)
 all f [<] = True `Because` [<]
 all f (sx :< x) =
   map (\prfs => snd prfs :< fst prfs) (either Here There) $
   both (f x) (all f sx)
 
 public export
-irrelevant : {0 sx : SnocList a} -> All (Irrelevant . p) sx -> Irrelevant (All p sx)
-irrelevant [<] = Forget [<]
-irrelevant (prfs :< px) = [| irrelevant prfs :< px |]
-
-public export
-relevant : (sx : SnocList a) -> (0 prfs : All p sx) -> All (Irrelevant . p) sx
-relevant [<] _ = [<]
-relevant (sx :< x) prfs = relevant sx (tail prfs) :< Forget (head prfs)
-
-public export
 tabulate : LengthOf sx -> (forall x. Elem x sx -> p x) -> All p sx
 tabulate Z f = [<]
 tabulate (S len) f = tabulate len (f . There) :< f Here