diff --git a/elision.cabal b/elision.cabal
--- a/elision.cabal
+++ b/elision.cabal
@@ -1,5 +1,5 @@
 name:                elision
-version:             0.1.2.0
+version:             0.1.3.0
 synopsis:            Arrows with holes.
 description:         A framework for describing holes in transformations
                      and impure computations purely.
@@ -16,9 +16,13 @@
 library
   hs-source-dirs:      src
   exposed-modules:     Control.Arrow.Elision
+                     , Control.Arrow.Elision.Simple
+                     , Control.Arrow.Elision.Flexible
   default-language:    Haskell2010
   build-depends:       base        >= 4.7   && < 5
+                     , hspec       >= 2.2
                      , profunctors >= 5.1.2
+                     , QuickCheck  >= 2.8
 
 executable example
   hs-source-dirs:      example
diff --git a/src/Control/Arrow/Elision.hs b/src/Control/Arrow/Elision.hs
--- a/src/Control/Arrow/Elision.hs
+++ b/src/Control/Arrow/Elision.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE ExplicitNamespaces, NoImplicitPrelude, RankNTypes, TupleSections,
-             TypeOperators #-}
 {- |
 Module      : Control.Arrow.Elision
 Description : Two functions with a missing "link" to be completed at a later time.
@@ -7,229 +5,7 @@
 License     : BSD2
 Maintainer  : alex@crough.io
 Stability   : Experimental
-Portability : RankNTypes, TupleSection, TypeOperators
 -}
-module Control.Arrow.Elision
-       ( -- * Types
-         Elision
-       , Elision'
-
-         -- * Constructors
-       , after
-       , basic
-       , before
-       , elide
-       , terminal
-
-         -- * Manipulation
-       , apply
-       , complete
-       , complete'
-       , unelide
-       , unelide'
-
-         -- * Combining Interpreters
-       , Sum
-       , type (//)
-       , (//)
-       , left'
-       , right'
-       , (/>>)
-       , (<</)
-
-       -- * Arrow combinator re-exports
-       , Arrow
-       , ArrowApply
-       , ArrowChoice
-       , (***)
-       , (&&&)
-       , (|||)
-       , (+++)
-       , (<<<)
-       , (<<^)
-       , (^>>)
-       , (>>^)
-       , (^<<)
-       )
-       where
-
-import Control.Applicative (Applicative (..))
-import Control.Arrow       (Arrow (..), ArrowApply (..), ArrowChoice (..),
-                            (<<^), (>>^), (^<<), (^>>))
-import Control.Category    (Category (..), (<<<), (>>>))
-import Control.Monad       (Functor (..), Monad (..), (<=<), (=<<))
-import Data.Either         (Either (..))
-import Data.Function       (const, flip, ($))
-import Data.Profunctor     (Profunctor (..))
-
-infixr 2 //
-infixr 4 />>, <</
-
---------------------------------------------------------------------------------
--- | A lens-esque type that can be used to "skip" part of a function.
---
--- An 'Elision' can be used in the common interpreter pattern, in which case
--- @f@ represents the DSL type, @a@ represents the input of a function and @b@
--- represents the output.
---
--- Use 'complete' or 'unelide' to deconstruct the type.
-newtype Elision f a b =
-  Elision (forall m. Monad m => (forall t. f t -> m t) -> a -> m b)
-
-instance Functor (Elision f a) where
-  fmap = rmap
-
-instance Applicative (Elision f a) where
-  pure x =
-    Elision (const (const (pure x)))
-
-  el0 <*> el1 =
-    Elision $ \cont arg ->
-      let run = complete cont arg
-       in run el0 <*> run el1
-
-instance Monad (Elision f a) where
-  el >>= fn =
-    Elision $ \cont arg ->
-      let run = complete cont arg
-       in run . fn =<< run el
-
-instance Profunctor (Elision f) where
-  dimap l r el =
-    Elision $ \cont ->
-      let fn = unelide el cont
-       in dimap l (fmap r) fn
-
-instance Category (Elision f) where
-  id =
-    Elision (const pure)
-
-  el1 . el0 =
-    Elision (\cont -> unelide el1 cont <=< unelide el0 cont)
-
-instance Arrow (Elision f) where
-  arr fn =
-    Elision (const (pure . fn))
-
-  first el =
-    Elision (\cont ~(x,y) -> fmap (,y) (unelide el cont x))
-
-instance ArrowChoice (Elision f) where
-  left el = Elision $ \cont ->
-    fmap Left . unelide el cont ||| pure . Right
-
-instance ArrowApply (Elision f) where
-  app = Elision (\cont ~(el, arg) -> complete' cont (el `apply` arg))
-
---------------------------------------------------------------------------------
--- | The type of the simplist elision, where @unelide eli f = f@
-type Elision' f a =
-  Elision f (f a) a
-
---------------------------------------------------------------------------------
--- | Deconstruct an Elision, returning its inner type.
-unelide :: Monad m => Elision f a b -> (forall c. f c -> m c) -> a -> m b
-unelide (Elision el) =
-  el
-
---------------------------------------------------------------------------------
--- | Like 'unelide', but applies the unit type to the function immediately.
-unelide' :: Monad m => Elision f () b -> (forall c. f c -> m c) -> m b
-unelide' el fn =
-  unelide el fn ()
-
---------------------------------------------------------------------------------
--- | Construct an interpreter for an elision out of a function an initial
--- argument.
-complete :: Monad m => (forall c. f c -> m c) -> a -> Elision f a b -> m b
-complete fn arg (Elision el) =
-  el fn arg
-
---------------------------------------------------------------------------------
--- | Like 'complete', but the unit type never has to be provided.
-complete' :: Monad m => (forall c. f c -> m c) -> Elision f () b -> m b
-complete' fn =
-  complete fn ()
-
---------------------------------------------------------------------------------
--- | Apply an argument to an arrow and close off the input.
-apply :: Arrow a => a b c -> b -> a () c
-apply arrow arg =
-  arrow <<^ const arg
-
---------------------------------------------------------------------------------
--- | The simplest elision, effectively the identity function.
-basic :: Elision' f a
-basic =
-  Elision (\f x -> f x)
-
---------------------------------------------------------------------------------
--- | Create an elision out of two functions to be completed at a later date.
-elide :: (a -> f c) -> (c -> b) -> Elision f a b
-elide f g =
-  dimap f g basic
-
---------------------------------------------------------------------------------
--- | Create an elision chained to the end of the provided function.
-after :: (a -> f b) -> Elision f a b
-after =
-  flip elide id
-
---------------------------------------------------------------------------------
--- | Create an elision chained to the beginning of the provided function.
-before :: (a -> b) -> Elision f (f a) b
-before =
-  elide id
-
---------------------------------------------------------------------------------
--- | Create an elision with the input fully applied.
-terminal :: f a -> Elision f () a
-terminal x =
-  after (const x)
-
---------------------------------------------------------------------------------
--- | Either @f a@ or @g a@.
-newtype Sum f g a =
-  Sum { runSum :: Either (f a) (g a) }
-
---------------------------------------------------------------------------------
--- | A type synonym for 'Sum' to create harmony with the '//' function.
-type a // b =
-  Sum a b
-
---------------------------------------------------------------------------------
--- | Create a function that can complete an elision of a sum out of two
--- functions that can complete each individual parts.
-(//) :: (forall b. f b -> m b) -> (forall b. g b -> m b) -> Sum f g a -> m a
-f // g =
-  f ||| g <<^ runSum
-
---------------------------------------------------------------------------------
--- | Like 'left', but over the first type argument.
-left' :: Elision f a b -> Elision (f // g) a b
-left' el =
-  Elision (\cont -> unelide el (cont . Sum . Left))
-
---------------------------------------------------------------------------------
--- | Like 'right', but over the first type argument.
-right' :: Elision g a b -> Elision (f // g) a b
-right' e =
-  Elision $ \e' -> unelide e (e' . Sum . Right)
-
---------------------------------------------------------------------------------
--- | Send the output of the left to the input of right, and add their @f@
--- types together.
---
--- This is analogous to a lifted '(>>>)'.
-(/>>) :: Elision f a b -> Elision g b c -> Elision (f // g) a c
-a />> b =
-  left' a >>> right' b
+module Control.Arrow.Elision (module Control.Arrow.Elision.Simple) where
 
---------------------------------------------------------------------------------
--- | Send the output of the right to the input of the left, and add their @f@
--- types together.
---
--- This is analogous to a lifted '(>>>)'.
-(<</) :: Elision f b c -> Elision g a b -> Elision (f // g) a c
-b <</ a =
-  left' b <<< right' a
+import Control.Arrow.Elision.Simple
diff --git a/src/Control/Arrow/Elision/Flexible.hs b/src/Control/Arrow/Elision/Flexible.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Arrow/Elision/Flexible.hs
@@ -0,0 +1,116 @@
+{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances,
+             MultiParamTypeClasses, RankNTypes, TypeFamilies, TypeOperators,
+             UndecidableInstances #-}
+module Control.Arrow.Elision.Flexible
+       ( Nav
+       , Conv(..)
+
+         -- * Flexible Elision completion functions
+       , complete
+       , complete'
+       , unelide
+       , unelide'
+
+         -- * Re-exports from 'Control.Arrow.Elision.Simple'
+       , module Control.Arrow.Elision.Simple
+       ) where
+
+import Control.Arrow.Elision.Simple hiding (complete, complete', unelide,
+                                     unelide')
+
+import qualified Control.Arrow.Elision.Simple as Simple (unelide)
+
+--------------------------------------------------------------------------------
+-- | Determines the transformation requires to take some interpreter @f@ and to
+-- transform it into another interpreter @g@. This is used primarily as the
+-- kind for 'Nav'.
+data Direction
+  = L Direction           -- * In @Nav f (g // h)@, @g@ has a common sub expression.
+  | R Direction           -- * In @Nav f (g // h)@, @h@ has a common sub expression.
+  | X Direction Direction -- * Subexpressions exist for both @f0@ and @f1@ in @g // h@ in @Nav (f0 // f1) (g // h)@
+  | Equiv                 -- * In @Nav f g@, @f ~ g@.
+  | Divergant             -- * There are no common subtypes.
+
+--------------------------------------------------------------------------------
+-- | "Navigate" down a tree of types to find common types which are equivalent.
+-- See 'Direction' for the result.
+type family Nav f g :: Direction where
+    Nav  f        f       = 'Equiv
+    Nav (f // g) (h // i) = 'X (Nav f (h // i)) (Nav g (h // i))
+    Nav  f       (h // i) =  Choose (Converges (Nav f h)) (Nav f h) (Converges (Nav f i)) (Nav f i)
+    Nav  f        g       = 'Divergant
+
+--------------------------------------------------------------------------------
+-- | A constraint that can only be satisfied if a direction terminates in
+-- 'Equiv'.
+class 'True ~ Converges a => Convergant (a :: Direction)
+instance Convergant 'Equiv
+instance Convergant a => Convergant ('L a)
+instance Convergant a => Convergant ('R a)
+instance (Convergant a, Convergant b) => Convergant ('X a b)
+
+--------------------------------------------------------------------------------
+-- A type level function which determines if @a@ terminates in 'Equiv'.
+--
+-- Because 'True ~ Converges a' can be cumbersome to type, this module also
+-- provides an equivalent typeclass, 'Convergant', which can be used as a
+-- constraint on a function.
+type family Converges a where
+    Converges  'Equiv     = 'True
+    Converges  'Divergant = 'False
+    Converges ('L k)      =  Converges k
+    Converges ('R k)      =  Converges k
+    Converges ('X k1 k2)  =  And (Converges k1) (Converges k2)
+
+type family And a b where
+    And 'True 'True = 'True
+    And  a      b   = 'False
+
+--------------------------------------------------------------------------------
+-- Pass in whether or not the function converges along with the type, and
+-- return either @a@ or @b@ if they converge, favoring @a@.
+type family Choose (exA :: Bool) (a :: Direction) (exB :: Bool) (b :: Direction) where
+    Choose 'True  a exB    b = 'L a
+    Choose 'False a 'True  b = 'R b
+    Choose 'False a 'False b = 'Divergant
+
+--------------------------------------------------------------------------------
+-- | In @Conv k f g@, the interpreter for @f@ is completely covered by the
+-- interpreter for @g@, so @g@ can be substituted for @f@ with 'conv'.
+class (k ~ Nav f g, Convergant k) => Conv k f g where
+    conv :: (g a -> m a) -> f a -> m a
+
+instance Conv 'Equiv f f where
+    conv = id
+
+instance ('L k ~ Nav f (g // h), Conv k f g) => Conv ('L k) f (g // h) where
+    conv f = conv (f . Sum . Left)
+
+instance ('R k ~ Nav f (g // h), Conv k f h) => Conv ('R k) f (g // h) where
+    conv f = conv (f . Sum . Right)
+
+instance ( 'X k0 k1 ~ Nav (e // f) (g // h)
+         , Conv k0 e (g // h)
+         , Conv k1 f (g // h)
+         ) => Conv ('X k0 k1) (e // f) (g // h) where
+    conv f = conv f ||| conv f ^<< runSum
+
+--------------------------------------------------------------------------------
+-- | A flexible version of 'Control.Arrow.Elision.Simple.unelide'
+unelide :: (Monad m, Conv k f g) => Elision f a b -> (forall c. g c -> m c) -> a -> m b
+unelide el fn = Simple.unelide el (conv fn)
+
+--------------------------------------------------------------------------------
+-- | A flexible version of 'Control.Arrow.Elision.Simple.unelide''
+unelide' :: (Monad m, Conv k f g) => Elision f () b -> (forall c. g c -> m c) -> m b
+unelide' el fn = unelide el fn ()
+
+--------------------------------------------------------------------------------
+-- | A flexible version of 'Control.Arrow.Elision.Simple.complete'
+complete :: (Monad m, Conv k f g) => (forall c. g c -> m c) -> a -> Elision f a b -> m b
+complete fn x el = unelide el fn x
+
+--------------------------------------------------------------------------------
+-- | A flexible version of 'Control.Arrow.Elision.Simple.complete''
+complete' :: (Monad m, Conv k f g) => (forall c. g c -> m c) -> Elision f () b -> m b
+complete' fn el = unelide' el fn
diff --git a/src/Control/Arrow/Elision/Simple.hs b/src/Control/Arrow/Elision/Simple.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Arrow/Elision/Simple.hs
@@ -0,0 +1,225 @@
+{-# LANGUAGE ExplicitNamespaces, NoImplicitPrelude, RankNTypes, TupleSections,
+             TypeOperators #-}
+module Control.Arrow.Elision.Simple
+       ( -- * Types
+         Elision
+       , Elision'
+
+         -- * Constructors
+       , basic
+       , elide
+       , elideLeft
+       , elideRight
+       , terminal
+
+         -- * Manipulation
+       , apply
+       , complete
+       , complete'
+       , unelide
+       , unelide'
+
+         -- * Combining Interpreters
+       , Sum(..)
+       , type (//)
+       , (//)
+       , left'
+       , right'
+       , (/>>)
+       , (<</)
+
+       -- * Arrow combinator re-exports
+       , Arrow
+       , ArrowApply
+       , ArrowChoice
+       , (***)
+       , (&&&)
+       , (|||)
+       , (+++)
+       , (<<<)
+       , (<<^)
+       , (^>>)
+       , (>>^)
+       , (^<<)
+       , arr
+       ) where
+
+
+import Control.Applicative (Applicative (..))
+import Control.Arrow       (Arrow (..), ArrowApply (..), ArrowChoice (..),
+                            (<<^), (>>^), (^<<), (^>>))
+import Control.Category    (Category (..), (<<<), (>>>))
+import Control.Monad       (Functor (..), Monad (..), (<=<), (=<<))
+import Data.Either         (Either (..))
+import Data.Function       (const, flip, ($))
+import Data.Profunctor     (Profunctor (..))
+
+infixr 2 //
+infixr 4 />>, <</
+
+--------------------------------------------------------------------------------
+-- | A lens-esque type that can be used to "skip" part of a function.
+--
+-- An 'Elision' can be used in the common interpreter pattern, in which case
+-- @f@ represents the DSL type, @a@ represents the input of a function and @b@
+-- represents the output.
+--
+-- Use 'complete' or 'unelide' to deconstruct the type.
+newtype Elision f a b =
+  Elision (forall m. Monad m => (forall t. f t -> m t) -> a -> m b)
+
+instance Functor (Elision f a) where
+  fmap = rmap
+
+instance Applicative (Elision f a) where
+  pure x =
+    Elision (const (const (pure x)))
+
+  el0 <*> el1 =
+    Elision $ \cont arg ->
+        complete cont arg el0 <*> complete cont arg el1
+
+instance Monad (Elision f a) where
+  el >>= fn =
+    Elision $ \cont arg ->
+        complete cont arg . fn =<< complete cont arg el
+
+instance Profunctor (Elision f) where
+  dimap l r el =
+    Elision $ \cont ->
+      let fn = unelide el cont
+       in dimap l (fmap r) fn
+
+instance Category (Elision f) where
+  id =
+    Elision (const pure)
+
+  el1 . el0 =
+    Elision (\cont -> unelide el1 cont <=< unelide el0 cont)
+
+instance Arrow (Elision f) where
+  arr fn =
+    Elision (const (pure . fn))
+
+  first el =
+    Elision (\cont ~(x,y) -> fmap (,y) (unelide el cont x))
+
+instance ArrowChoice (Elision f) where
+  left el = Elision $ \cont ->
+    fmap Left . unelide el cont ||| pure . Right
+
+instance ArrowApply (Elision f) where
+  app = Elision (\cont ~(el, arg) -> complete' cont (el `apply` arg))
+
+--------------------------------------------------------------------------------
+-- | The type of the simplist elision, where @unelide eli f = f@
+type Elision' f a =
+  Elision f (f a) a
+
+--------------------------------------------------------------------------------
+-- | Deconstruct an Elision, returning its inner type.
+unelide :: Monad m => Elision f a b -> (forall c. f c -> m c) -> a -> m b
+unelide (Elision el) =
+  el
+
+--------------------------------------------------------------------------------
+-- | Like 'unelide', but applies the unit type to the function immediately.
+unelide' :: Monad m => Elision f () b -> (forall c. f c -> m c) -> m b
+unelide' el fn =
+  unelide el fn ()
+
+--------------------------------------------------------------------------------
+-- | Construct an interpreter for an elision out of a function an initial
+-- argument.
+complete :: Monad m => (forall c. f c -> m c) -> a -> Elision f a b -> m b
+complete fn arg (Elision el) =
+  el fn arg
+
+--------------------------------------------------------------------------------
+-- | Like 'complete', but the unit type never has to be provided.
+complete' :: Monad m => (forall c. f c -> m c) -> Elision f () b -> m b
+complete' fn =
+  complete fn ()
+
+--------------------------------------------------------------------------------
+-- | Apply an argument to an arrow and close off the input.
+apply :: Arrow a => a b c -> b -> a () c
+apply arrow arg =
+  arrow <<^ const arg
+
+--------------------------------------------------------------------------------
+-- | The simplest elision, effectively the identity function.
+basic :: Elision' f a
+basic =
+  Elision (\f x -> f x)
+
+--------------------------------------------------------------------------------
+-- | Create an elision out of two functions to be completed at a later date.
+elide :: (a -> f c) -> (c -> b) -> Elision f a b
+elide f g =
+  dimap f g basic
+
+--------------------------------------------------------------------------------
+-- | Create an elision chained to the end of the provided function.
+elideLeft :: (a -> f b) -> Elision f a b
+elideLeft =
+  flip elide id
+
+--------------------------------------------------------------------------------
+-- | Create an elision chained to the beginning of the provided function.
+elideRight :: (a -> b) -> Elision f (f a) b
+elideRight =
+  elide id
+
+--------------------------------------------------------------------------------
+-- | Create an elision with the input fully applied.
+terminal :: f a -> Elision f () a
+terminal x =
+  elideLeft (const x)
+
+--------------------------------------------------------------------------------
+-- | Either @f a@ or @g a@.
+newtype Sum f g a =
+  Sum { runSum :: Either (f a) (g a) }
+
+--------------------------------------------------------------------------------
+-- | A type synonym for 'Sum' to create harmony with the '//' function.
+type a // b =
+  Sum a b
+
+--------------------------------------------------------------------------------
+-- | Create a function that can complete an elision of a sum out of two
+-- functions that can complete each individual parts.
+(//) :: (forall b. f b -> m b) -> (forall b. g b -> m b) -> Sum f g a -> m a
+f // g =
+  f ||| g <<^ runSum
+
+--------------------------------------------------------------------------------
+-- | Like 'left', but over the first type argument.
+left' :: Elision f a b -> Elision (f // g) a b
+left' el =
+  Elision (\cont -> unelide el (cont . Sum . Left))
+
+--------------------------------------------------------------------------------
+-- | Like 'right', but over the first type argument.
+right' :: Elision g a b -> Elision (f // g) a b
+right' e =
+  Elision $ \e' -> unelide e (e' . Sum . Right)
+
+--------------------------------------------------------------------------------
+-- | Send the output of the left to the input of right, and add their @f@
+-- types together.
+--
+-- This is analogous to a lifted '(>>>)'.
+(/>>) :: Elision f a b -> Elision g b c -> Elision (f // g) a c
+a />> b =
+  left' a >>> right' b
+
+--------------------------------------------------------------------------------
+-- | Send the output of the right to the input of the left, and add their @f@
+-- types together.
+--
+-- This is analogous to a lifted '(>>>)'.
+(<</) :: Elision f b c -> Elision g a b -> Elision (f // g) a c
+b <</ a =
+  left' b <<< right' a