diff --git a/example2.hs b/example2.hs
--- a/example2.hs
+++ b/example2.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, GADTs, StandaloneDeriving #-}
+{-# LANGUAGE FlexibleContexts #-}
 
 import GHC.TypeLits
 import Data.Type.Set
@@ -19,3 +20,11 @@
 
 -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
 foobar = foo `union` bar
+
+nonMemberTest :: NonMember (Natural 0) as => Set as -> ()
+nonMemberTest set = ()
+
+-- nonMemberTest meep  is well typed
+meep = asSet $ Ext (S Z) (Ext (S (S Z)) Empty)
+-- nonMemberTest morp is ill typed
+morp = asSet $ Ext (S Z) (Ext (S (S Z)) (Ext Z Empty))
diff --git a/src/Data/Type/Map.hs b/src/Data/Type/Map.hs
--- a/src/Data/Type/Map.hs
+++ b/src/Data/Type/Map.hs
@@ -100,9 +100,13 @@
 instance Updatable v t m n => Updatable v t ((w ':-> y) ': m) ((w ':-> y) ': n) where
   update (Ext w y m) v x = Ext w y (update m v x)
 
-instance Updatable v t '[] '[v ':-> t] where
-  update Empty v x = Ext v x Empty
+-- instance Updatable v t '[] '[v ':-> t] where
+--   update Empty v x = Ext v x Empty
 
+instance Updatable v t s ((v ':-> t) ': s) where
+  update xs v x = Ext v x xs
+
+
 {-| Predicate to check if in normalised map form -}
 type IsMap s = (s ~ Nub (Sort s))
 
@@ -129,8 +133,14 @@
 instance Eq (Map '[]) where
     Empty == Empty = True
 
-instance (KnownSymbol k, Eq (Var k), Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where
-    (Ext k v m) == (Ext k' v' m') = k == k' && v == v' && m == m'
+instance (Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where
+    (Ext Var v m) == (Ext Var v' m') = v == v' && m == m'
+
+instance Ord (Map '[]) where
+    compare Empty Empty = EQ
+
+instance (Ord v, Ord (Map s)) => Ord (Map ((k :-> v) ': s)) where
+    compare (Ext Var v m) (Ext Var v' m') = compare v v' `mappend` compare m m'
 
 {-| Union of two finite maps (normalising) -}
 union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)
diff --git a/src/Data/Type/Set.hs b/src/Data/Type/Set.hs
--- a/src/Data/Type/Set.hs
+++ b/src/Data/Type/Set.hs
@@ -1,13 +1,13 @@
 {-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
              MultiParamTypeClasses, FlexibleInstances, PolyKinds,
              FlexibleContexts, UndecidableInstances, ConstraintKinds,
-             ScopedTypeVariables #-}
+             ScopedTypeVariables, TypeInType #-}
 
 module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
                       Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),
                       Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
                       Delete(..), Proxy(..), remove, Remove, (:\),
-                      Member) where
+                      Member(..), NonMember, MemberP(..)) where
 
 import GHC.TypeLits
 import Data.Type.Bool
@@ -16,7 +16,7 @@
 data Proxy (p :: k) = Proxy
 
 -- Value-level 'Set' representation,  essentially a list
-data Set (n :: [k]) :: * where
+data Set (n :: [k]) where
     {--| Construct an empty set -}
     Empty :: Set '[]
     {--| Extend a set with an element -}
@@ -77,7 +77,7 @@
 {-| Delete elements from a set -}
 type family (m :: [k]) :\ (x :: k) :: [k] where
      '[]       :\ x = '[]
-     (x ': xs) :\ x = xs
+     (x ': xs) :\ x = xs :\ x
      (y ': xs) :\ x = y ': (xs :\ x)
 
 class Remove s t where
@@ -86,8 +86,8 @@
 instance Remove '[] t where
   remove Empty Proxy = Empty
 
-instance {-# OVERLAPS #-} Remove (x ': xs) x where
-  remove (Ext _ xs) Proxy = xs
+instance {-# OVERLAPS #-} Remove xs x => Remove (x ': xs) x where
+  remove (Ext _ xs) x@Proxy = remove xs x
 
 instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
       => Remove (y ': xs) x where
@@ -227,3 +227,10 @@
 
 instance {-# OVERLAPPABLE #-} Member a s => Member a (b ': s) where
   member a (Ext _ xs) = member a xs
+
+type family MemberP a s :: Bool where
+            MemberP a '[]      = False
+            MemberP a (a ': s) = True
+            MemberP a (b ': s) = MemberP a s
+
+type NonMember a s = MemberP a s ~ False
diff --git a/type-level-sets.cabal b/type-level-sets.cabal
--- a/type-level-sets.cabal
+++ b/type-level-sets.cabal
@@ -1,14 +1,14 @@
 name:                   type-level-sets
-version:                0.8.7.0
+version:                0.8.9.0
 synopsis:               Type-level sets and finite maps (with value-level counterparts)
-description:            
+description:
    This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level
    finite maps via 'Map', with value-level counterparts.
    .
-   Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard 
-   and Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (Haskell Symposium, 2014). This version now uses Quicksort to normalise the representation.	
+   Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard
+   and Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (Haskell Symposium, 2014). This version now uses Quicksort to normalise the representation.
    .
-   Here is a brief example for finite maps: 
+   Here is a brief example for finite maps:
    .
    >
    > import Data.Type.Map
@@ -19,26 +19,26 @@
    >     combine x y = x + y
    >
    > foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]
-   > foo = Ext (Var :: (Var "x")) 2 
-   >     $ Ext (Var :: (Var "z")) True 
-   >     $ Ext (Var :: (Var "w")) 5 
-   >     $ Empty 
+   > foo = Ext (Var :: (Var "x")) 2
+   >     $ Ext (Var :: (Var "z")) True
+   >     $ Ext (Var :: (Var "w")) 5
+   >     $ Empty
    >
    > bar :: Map '["y" :-> Int, "w" :-> Int]
    > bar = Ext (Var :: (Var "y")) 3
    >     $ Ext (Var :: (Var "w")) 1
    >     $ Empty
-   >  
+   >
    > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]
    > foobar = foo `union` bar
    .
    The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates).
    The type signatures is commented out as it can be infered. Running the example we get:
    .
-   > >>> foobar	
+   > >>> foobar
    > {w :-> 6, x :-> 2, y :-> 3, z :-> True}
    .
-   Thus, we see that the values for \"w\" are added together. 
+   Thus, we see that the values for \"w\" are added together.
    For sets, here is an example:
    .
    > import GHC.TypeLits
@@ -48,7 +48,7 @@
    > data Natural (a :: Nat) where
    >   Z :: Natural 0
    >   S :: Natural n -> Natural (n + 1)
-   > 
+   >
    > -- foo :: Set '[Natural 0, Natural 1, Natural 3]
    > foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
    >
@@ -63,13 +63,13 @@
 license:                BSD3
 license-file:           LICENSE
 category:               Type System, Data Structures
-copyright:              2013-16 University of Cambridge
+copyright:              2013-18 University of Kent
 author:                 Dominic Orchard
 maintainer:             Dominic Orchard
 stability:              experimental
 build-type:             Simple
 cabal-version:          >= 1.6
-tested-with:            GHC >= 8.0.1
+tested-with:            GHC >= 8.2.2
 
 extra-source-files:     example.hs, example2.hs
 
@@ -84,6 +84,6 @@
 
   exposed-modules:      Data.Type.Set
                         Data.Type.Map
-                        
+
   build-depends:        base < 5,
                         ghc-prim