diff --git a/Data/OpenUnion.hs b/Data/OpenUnion.hs
--- a/Data/OpenUnion.hs
+++ b/Data/OpenUnion.hs
@@ -1,8 +1,6 @@
 -- | Flexible, type-safe open unions.
 module Data.OpenUnion
     ( Union
-    , (:<)
-    , (:\)
     , (@>)
     , liftUnion
     , reUnion
diff --git a/Data/OpenUnion/Internal.hs b/Data/OpenUnion/Internal.hs
--- a/Data/OpenUnion/Internal.hs
+++ b/Data/OpenUnion/Internal.hs
@@ -1,66 +1,131 @@
 -- | Exposed internals for Data.OpenUnion
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE EmptyDataDecls #-}
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE OverlappingInstances #-}
-{-# LANGUAGE IncoherentInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Data.OpenUnion.Internal
     ( Union (..)
-    , (:<)
-    , (:\)
     , (@>)
+    , (@!>)
     , liftUnion
     , reUnion
     , restrict
     , typesExhausted
     ) where
 
+import Control.Exception
 import Data.Dynamic
+import TypeFun.Data.List (SubList, Elem, Delete)
 
 -- | The @Union@ type - the phantom parameter @s@ is a list of types
 -- denoting what this @Union@ might contain.
 -- The value contained is one of those types.
 newtype Union (s :: [*]) = Union Dynamic
 
--- general note: try to keep from re-constructing Unions if an existing one
--- can just be type-coerced.
+instance Show (Union '[]) where
+  show = typesExhausted
 
--- | Remove a type from anywhere in the list.
-type family s :\ a where
-    '[] :\ a = '[]
-    (a ': s) :\ a = s :\ a
-    (a' ': s) :\ a = a' ': (s :\ a)
+instance (Show a, Show (Union (Delete a as)), Typeable a)
+         => Show (Union (a ': as)) where
+  show u = case restrict u of
+    Left sub       -> show sub
+    Right (a :: a) ->
+       let p = Proxy :: Proxy a
+           rep = typeRep p
+       in "Union (" ++ show a ++ " :: " ++ show rep ++ ")"
 
--- | There exists a @s :< s'@ instance if every type in the list @s@
--- can be lifted to @s'@.
-class (:<) (s :: [*]) (s' :: [*])
-instance '[] :< s
-instance (s :< s', Typeable a) => (a ': s) :< (a ': s')
-instance (s :< s', '[a] :< s', Typeable a) => (a ': s) :< s'
+instance Eq (Union '[]) where
+  a == _ = typesExhausted a
 
+instance (Typeable a, Eq (Union (Delete a as)), Eq a)
+         => Eq (Union (a ': as)) where
+  u1 == u2 =
+    let r1 = restrict u1
+        r2 = restrict u2
+    in case (r1, r2) of
+       (Right (a :: a), Right b) -> a == b
+       (Left  a       , Left  b)        -> a == b
+       _                                -> False
+
+instance Ord (Union '[]) where
+  compare a _ = typesExhausted a
+
+instance (Ord a, Typeable a, Ord (Union (Delete a as)))
+         => Ord (Union (a ': as)) where
+  compare u1 u2 =
+    let r1 = restrict u1
+        r2 = restrict u2
+    in case (r1, r2) of
+       (Right (a :: a), Right b) -> compare a b
+       (Left a        , Left b)  -> compare a b
+       (Right _       , Left _)  -> GT
+       (Left  _       , Right _)  -> LT
+
+instance (Exception e) => Exception (Union (e ': '[])) where
+  toException u = case restrict u of
+    Left (sub :: Union '[]) -> typesExhausted sub
+    Right (e  :: e)         -> toException e
+  fromException some = case fromException some of
+    Just (e :: e) -> Just (liftUnion e)
+    Nothing       -> Nothing
+
+instance ( Exception e, Typeable e, Typeable es, Typeable e1
+         , Exception (Union (Delete e (e1 ': es)))
+         , SubList (Delete e (e1 ': es)) (e ': e1 ': es) )
+         => Exception (Union (e ': e1 ': es)) where
+  toException u = case restrict u of
+    Left (sub :: Union (Delete e (e1 ': es))) -> toException sub
+    Right (e  :: e)                   -> toException e
+
+  fromException some = case fromException some of
+    Just (e :: e) -> Just (liftUnion e)
+    Nothing ->
+      let sub :: Maybe (Union (Delete e (e1 ': es)))
+          sub = fromException some
+      in fmap reUnion sub
+
+-- general note: try to keep from re-constructing Unions if an existing one
+-- can just be type-coerced.
+
 -- | `restrict` in right-fixable style.
-(@>) :: Typeable a => (a -> b) -> (Union (s :\ a) -> b) -> Union s -> b
+(@>) :: Typeable a
+     => (a -> b)
+     -> (Union (Delete a s) -> b)
+     -> Union s
+     -> b
 r @> l = either l r . restrict
 infixr 2 @>
 {-# INLINE (@>) #-}
 
-liftUnion :: (Typeable a, '[a] :< s) => a -> Union s
+-- | `restrict` in right-fixable style with existance restriction.
+(@!>) :: (Typeable a, Elem a s)
+      => (a -> b)
+      -> (Union (Delete a s) -> b)
+      -> Union s
+      -> b
+r @!> l = either l r . restrict
+infixr 2 @!>
+{-# INLINE (@!>) #-}
+
+liftUnion :: (Typeable a, Elem a s) => a -> Union s
 liftUnion = Union . toDyn
 {-# INLINE liftUnion #-}
 
 -- | Narrow down a @Union@.
-restrict :: Typeable a => Union s -> Either (Union (s :\ a)) a
+restrict :: Typeable a => Union s -> Either (Union (Delete a s)) a
 restrict (Union d) = maybe (Left $ Union d) Right $ fromDynamic d
 {-# INLINE restrict #-}
 
 -- | Generalize a @Union@.
-reUnion :: (s :< s') => Union s -> Union s'
+reUnion :: (SubList s s') => Union s -> Union s'
 reUnion (Union d) = Union d
 {-# INLINE reUnion #-}
 
diff --git a/example.hs b/example.hs
--- a/example.hs
+++ b/example.hs
@@ -1,7 +1,23 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+
+import Control.Exception
 import Data.OpenUnion
+import Data.Typeable
 
+data Exc1 = Exc1
+            deriving (Eq, Ord, Show, Typeable)
+instance Exception Exc1
+
+data Exc2 = Exc2
+            deriving (Eq, Ord, Show, Typeable)
+instance Exception Exc2
+
+type ExcUnion = Union '[Exc1, Exc2]
+
+showException :: ExcUnion -> IO String
+showException = return . show
+
 type MyUnion = Union '[Char, Int, [()]]
 
 showMyUnion :: MyUnion -> String
@@ -17,3 +33,14 @@
     putStrLn $ showMyUnion $ liftUnion (4 :: Int)
     putStrLn $ showMyUnion $ liftUnion 'a'
     putStrLn $ showMyUnion $ liftUnion [(), ()]
+    let u1 = liftUnion (4  :: Int) :: MyUnion
+        u2 = liftUnion (10 :: Int) :: MyUnion
+        u3 = liftUnion 'a'         :: MyUnion
+    putStrLn $ show u1
+    putStrLn $ show u3
+    putStrLn $ show $ u1 == u1
+    putStrLn $ show $ u1 == u2
+    putStrLn $ show $ u1 == u3
+
+    print =<< catch (throwIO Exc1) showException
+    print =<< catch (throwIO Exc2) showException
diff --git a/open-union.cabal b/open-union.cabal
--- a/open-union.cabal
+++ b/open-union.cabal
@@ -1,11 +1,11 @@
 name:               open-union
-version:            0.1.0.1
+version:            0.2.0.0
 synopsis:           Extensible, type-safe unions.
 category:           Data
 license:            MIT
 license-file:       LICENSE
-author:             Ben Foppa
-homepage:           https://github.com/RobotGymnast/open-union
+author:             Zeke Foppa
+homepage:           https://github.com/bfopa/open-union
 maintainer:         benjamin.foppa@gmail.com
 build-type:         Simple
 cabal-version:      >= 1.9.2
@@ -85,13 +85,15 @@
                   Data.OpenUnion
                   Data.OpenUnion.Internal
 
-    build-depends : base == 4.*
+    build-depends: base == 4.*
+                 , type-fun
 
 executable example
     hs-source-dirs:   .
     main-is: example.hs
-    ghc-options: -Wall -fllvm -O2
+    ghc-options: -Wall -O2
     build-depends : base == 4.*
+                  , type-fun
                   , open-union
 
 source-repository head