diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,7 +1,11 @@
 # Mad Props
 
+[Hackage & Docs](http://hackage.haskell.org/package/mad-props)
+
 Mad props is a simple generalized propagator framework. This means it's pretty good at expressing and solving generalized [constraint satisfaction problems](https://en.wikipedia.org/wiki/Constraint_satisfaction_problem).
 
+Note that `mad-props` doesn't use lattice filters for propagation, nor does it yet support dynamic choice of propagator elements (though you can specify choice ordering through the container type you choose). Those things are more a bit more complicated.
+
 There are many other constraint solvers out there, probably most of them are faster than this one, but for those who like the comfort and type-safety of working in Haskell, I've gotcha covered.
 
 With other constraint solvers it can be a bit of a pain to express your problem; you either need to compress your problem down to relations between boolean variables, or try to cram your problem into their particular format. Mad Props uses a Monadic DSL for expressing the variables in your problem and the relationships between them, meaning you can use normal Haskell to express your problem.
@@ -28,7 +32,7 @@
 .9....4..|]
 ```
 
-A Sudoku is a constraint satisfaction problem, the "constraints" are that each of the numbers 1-9 are represented in each row, column and 3x3 grid. `Props` allows us to create `PVars` a.k.a. Propagator Variables. `PVars` represent a piece of information in our problem which is 'unknown' but has some relationship with other variables. To convert Sudoku into a propagator problem we can make a new `PVar` for each cell, the `PVar` will contain either all possible values from 1-9; or ONLY the value which is specified in the puzzle. We use a Set to indicate the possibilities, but you can really use almost any container you like inside a `PVar`.
+Sudoku is a constraint satisfaction problem, the "constraints" are that each of the numbers 1-9 are represented in each row, column and 3x3 grid. 
 
 ```haskell
 txtToBoard :: [String] -> [[S.Set Int]]
@@ -42,9 +46,9 @@
 hardestBoard = txtToBoard hardestProblem
 ```
 
-This function takes our problem and converts it into a nested grid of variables! Each variable 'contains' all the possibilities for that square. Now we need to 'constrain' the problem!
+We've now got our problem as a list of rows of 'cells', each cell is a set containing the possible numbers for that cell.
 
-We can then introduce the constraints of Sudoku as relations between these `PVars`. The cells in each 'quadrant' (i.e. square, row, or column) are each 'related' to one other in the sense that **their values must be disjoint**. No two cells in each quadrant can have the same value. We'll quickly write some shoddy functions to extract the lists of "regions" we need to worry about from our board. Getting the **rows** and **columns** is easy, getting the square **blocks** is a bit more tricky, the implementation here really doesn't matter.
+We need to express the constraint that each 'region' (i.e. row, column and 'block') can only have one of each number in them. We'll write some helper function for collecting the regions of the puzzle:
 
 ```haskell
 rowsOf, colsOf, blocksOf :: [[a]] -> [[a]]
@@ -53,11 +57,13 @@
 blocksOf = chunksOf 9 . concat . concat . fmap transpose . chunksOf 3 . transpose
 ```
 
-Now we can worry about telling the system about our constraints. We'll map over each region relating every variable to every other one. This function assumes we've replaced the `Set a`'s in our board representation with the appropriate `PVar`'s, we'll actually do that soon, but for now you can look the other way.
+Now we can worry about telling the system about our constraints. 
 
+We can now introduce the constraints of Sudoku as relations between cells. The cells in each region are related to one other in the sense that **their values must be disjoint**. No two cells in each quadrant can have the same value. 
+
 ```haskell
 -- | Given a board of 'PVar's, link the appropriate cells with 'disjoint' constraints
-linkBoardCells :: [[PVar (S.Set Int)]] -> Prop ()
+linkBoardCells :: [[PVar S.Set Int]] -> Prop ()
 linkBoardCells xs = do
     let rows = rowsOf xs
     let cols = colsOf xs
@@ -70,38 +76,45 @@
     disj x xs = S.delete x xs
 ```
 
+This function introduces a few new types, namely `Prop` and `Pvar`. We'll show how `PVar`s are actually created soon, but the gist of this function is that we map over each 'region' and relate every variable to every other one.
 
-Now every pair of `PVars` in each region is linked by the `disj` relation.
+`Prop` is a monad which allows us to create and link `PVar`s together. It keeps track of the constraints on all of our variables and will eventually build a graph that the library uses to solve the problem.
 
-`constrain` accepts two `PVar`s and a function, the function takes a 'choice' from the first variable and uses it to constrain the 'options' from the second. In this case, if the first variable is fixed to a specific value we 'propagate' by removing all matching values from the other variable's pool, you can see the implementation of the `disj` helper above. The information about the 'link' is stored inside the `Prop` monad.
+We call the `constrain` function to state that no cell pairing within a region should have the same number.
 
+`constrain` accepts two `PVar`s and a function, the function takes a 'choice' from the first variable and uses it to constrain the 'options' from the second. In this case, if the first variable is fixed to a specific value we 'propagate' by removing all matching values from the other variable's pool, you can see the implementation of the `disj` helper above. The information about this constraint is stored inside the `Prop` monad.
+
+Set disjunction is symmetric, propagators in general are not, so we'll need to 'constrain' in each direction. Luckily our loop will process each pair twice, so we'll run this once in each direction.
+
 Here's the real signature in case you're curious: 
 
 ```haskell
-constrain :: (Monad m, Typeable g, Typeable (Element f)) 
-          => PVar f -> PVar g -> (Element f -> g -> g) 
+constrain :: Monad m
+          => PVar f a
+          -> PVar g b
+          -> (a -> g b -> g b)
           -> PropT m ()
 ```
 
-Set disjunction is symmetric, propagators in general are not, so we'll need to 'constrain' in each direction. Luckily our loop will process each pair twice, so we'll run this once in each direction.
+We're almost there; we've got a way to constrain a board of `PVar`s, but we need to make the board of `PVar`s somehow!
 
-Now we can link our parts together:
+This is pretty easy; we can make a `PVar` by calling `newPVar` and passing it a container full of possible options the variable could be. We'll convert our `[[S.Set Int]]` into `[[PVar S.Set Int]]` by traversing the structure using `newPVar`.
 
 ```haskell
--- | Given a sudoku board, apply the necessary constraints and return a result board of
--- 'PVar's. We wrap the result in 'Compose' because 'solve' requires a Functor over 'PVar's
-constrainBoard :: [[S.Set Int]]-> Prop (Compose [] [] (PVar (S.Set Int)))
+-- | Given a sudoku board, apply the necessary constraints and return a result board of 'PVar's.
+constrainBoard :: [[S.Set Int]]-> Prop [[PVar S.Set Int]]
 constrainBoard board = do
     vars <- (traverse . traverse) newPVar board
     linkBoardCells vars
-    return (Compose vars)
+    return vars
 ```
 
-We accept a sudoku "board", we replace each `Set Int` with a `PVar (S.Set Int)` using `newPVar` which creates a propagator from a set of possible values. This is a propagator variable which has a `Set` of Ints which the variable could take. We then link all the board's cells together using constraints, and lastly return a `Functor` full of `PVar`s; which will later be replaced with actual values. `Compose` converts a list of lists into a single functor over the nested elements.
+Here's the signature of `newPVar` in case you're curious:
 
 ```haskell
-newPVar :: (Monad m, MonoFoldable f, Typeable f, Typeable (Element f)) 
-        => f -> PropT m (PVar f)
+newPVar :: (Monad m, Foldable f, Typeable f, Typeable a) 
+        => f a 
+        -> PropT m (PVar f a)
 ```
 
 Now that we've got our problem set up we need to execute it!
@@ -111,17 +124,21 @@
 solvePuzzle :: [[S.Set Int]] -> IO ()
 solvePuzzle puz = do
     -- We know it will succeed, but in general you should handle failure safely
-    let Just (Compose results) = solve $ constrainBoard puz
+    let Just results = solve (fmap . fmap) $ constrainBoard puz
     putStrLn $ boardToText results
 ```
 
-We run `solveGraph` to run the propagation solver. It accepts a puzzle, builds and constrains the cells, then calls `solve` which maps over the `Compose`'d board we created in `constrainBoard` and replaces all the `PVar`s with actual results! If all went well we'll have the solution of each cell! Then we'll print it out.
+`solvePuzzle` will print a solution for any valid puzzle you pass it. It accepts a puzzle, builds and constrains the cells, then calls `solve` which will find a valid solution for the constraints we provided if possible. We pass it a 'finalizer' function which accepts a function for resolving any `PVar` to its 'solved' result. In our case we just use `fmap . fmap` to map the resolver over every PVar in the board returned from `constrainBoard`. If all went well we'll have the solution of each cell! Then we'll print it out.
 
-Here are some types first, then we'll try it out:
+Unfortunately `solve` has a bit of a complicated signature, there are simpler versions, but unfortunately they're not possible until GHC supports proper ImpredicativeTypes.
 
 ```haskell
-solve :: (Functor f, Typeable (Element g)) 
-      => Prop (f (PVar g)) -> Maybe (f (Element g))
+solve :: forall a r.
+        -- A finalizer which accepts a PVar 'resolver' as an argument
+        -- alongside the result of the Prop setup, and returns some result
+        ((forall f x. PVar f x -> x) -> a -> r)
+      -> Prop a
+      -> (Maybe r)
 ```
 
 We can plug in our hardest sudoku and after a second or two we'll print out the answer!
@@ -159,7 +176,7 @@
 type Coord = (Int, Int)
 
 -- | Given a number of queens, constrain them to not overlap
-constrainQueens :: Int -> Prop [PVar (S.Set Coord)]
+constrainQueens :: Int -> Prop [PVar S.Set Coord]
 constrainQueens n = do
     -- All possible grid locations
     let locations = S.fromList [(x, y) | x <- [0..n - 1], y <- [0..n - 1]]
@@ -204,7 +221,7 @@
 -- | Solve and print an N-Queens puzzle
 nQueens :: Int -> IO ()
 nQueens n = do
-    let Just results = solve (constrainQueens n)
+    let Just results = solve fmap (constrainQueens n)
     putStrLn $ showSolution n results
 
 -- | Solve and print all possible solutions of an N-Queens puzzle
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -6,5 +6,4 @@
 main :: IO ()
 main = do
     S.solveEasyPuzzle
--- main = NQ.solve 12
--- main = hardLogic
+    NQ.solve 8
diff --git a/mad-props.cabal b/mad-props.cabal
--- a/mad-props.cabal
+++ b/mad-props.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 33df843ae197b9debc55c9ed25dfb25eb1a01e4deb1623975fa0cb69e25705be
+-- hash: 663fc348378bb0879419e139117b3cb738781875d627cbe8259dded81e0fd92b
 
 name:           mad-props
-version:        0.1.0.0
+version:        0.2.0.0
 synopsis:       Monadic DSL for building constraint solvers using basic propagators.
 description:    Please see the README on GitHub at <https://github.com/ChrisPenner/mad-props#readme>
 category:       Propagators
@@ -42,14 +42,13 @@
       Paths_mad_props
   hs-source-dirs:
       src
-  ghc-options: -Wall -fno-warn-name-shadowing -O2
+  ghc-options: -Wall -fno-warn-name-shadowing -fwarn-redundant-constraints -O2
   build-depends:
       MonadRandom
     , base >=4.7 && <5
     , containers
     , lens
     , logict
-    , mono-traversable
     , mtl
     , psqueues
     , random
@@ -64,7 +63,7 @@
       Paths_mad_props
   hs-source-dirs:
       app
-  ghc-options: -Wall -fno-warn-name-shadowing -O2 -threaded -rtsopts -with-rtsopts=-N
+  ghc-options: -Wall -fno-warn-name-shadowing -fwarn-redundant-constraints -O2 -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       MonadRandom
     , base >=4.7 && <5
@@ -72,7 +71,6 @@
     , lens
     , logict
     , mad-props
-    , mono-traversable
     , mtl
     , psqueues
     , random
diff --git a/src/Examples/NQueens.hs b/src/Examples/NQueens.hs
--- a/src/Examples/NQueens.hs
+++ b/src/Examples/NQueens.hs
@@ -19,7 +19,7 @@
 type Coord = (Int, Int)
 
 -- | Given a number of queens, constrain them to not overlap
-constrainQueens :: Int -> Prop [PVar (S.Set Coord)]
+constrainQueens :: Int -> Prop [PVar S.Set Coord]
 constrainQueens n = do
     -- All possible grid locations
     let locations = S.fromList [(x, y) | x <- [0..n - 1], y <- [0..n - 1]]
@@ -64,13 +64,12 @@
 -- | Solve and print an N-Queens puzzle
 nQueens :: Int -> IO ()
 nQueens n = do
-    let Just results = solve (constrainQueens n)
+    let Just results = solve fmap (constrainQueens n)
     putStrLn $ showSolution n results
 
 -- | Solve and print all possible solutions of an N-Queens puzzle
 -- This will include duplicates.
 nQueensAll :: Int -> IO ()
 nQueensAll n = do
-    let results = solveAll (constrainQueens n)
+    let results = solveAll fmap (constrainQueens n)
     traverse_ (putStrLn . showSolution n) results
-
diff --git a/src/Examples/Sudoku.hs b/src/Examples/Sudoku.hs
--- a/src/Examples/Sudoku.hs
+++ b/src/Examples/Sudoku.hs
@@ -17,7 +17,6 @@
 import Text.RawString.QQ (r)
 import qualified Data.Set as S
 import Data.List
-import Data.Functor.Compose
 
 -- | Convert a textual board into a board containing sets of cells of possible numbers
 txtToBoard :: [String] -> [[S.Set Int]]
@@ -77,7 +76,7 @@
 
 
 -- | Given a board of 'PVar's, link the appropriate cells with 'disjoint' constraints
-linkBoardCells :: [[PVar (S.Set Int)]] -> Prop ()
+linkBoardCells :: [[PVar S.Set Int]] -> Prop ()
 linkBoardCells xs = do
     let rows = rowsOf xs
     let cols = colsOf xs
@@ -91,17 +90,17 @@
 
 -- | Given a sudoku board, apply the necessary constraints and return a result board of
 -- 'PVar's. We wrap the result in 'Compose' because 'solve' requires a Functor over 'PVar's
-constrainBoard :: [[S.Set Int]]-> Prop (Compose [] [] (PVar (S.Set Int)))
+constrainBoard :: [[S.Set Int]]-> Prop [[PVar S.Set Int]]
 constrainBoard board = do
     vars <- (traverse . traverse) newPVar board
     linkBoardCells vars
-    return (Compose vars)
+    return vars
 
 -- Solve a given sudoku board and print it to screen
 solvePuzzle :: [[S.Set Int]] -> IO ()
 solvePuzzle puz = do
     -- We know it will succeed, but in general you should handle failure safely
-    let Just (Compose results) = solve $ constrainBoard puz
+    let Just results = solve (fmap . fmap) $ constrainBoard puz
     putStrLn $ boardToText results
 
 solveEasyPuzzle :: IO ()
diff --git a/src/Props/Internal/Backtracking.hs b/src/Props/Internal/Backtracking.hs
--- a/src/Props/Internal/Backtracking.hs
+++ b/src/Props/Internal/Backtracking.hs
@@ -30,12 +30,12 @@
 instance MT.HasMinTracker BState where
   minTracker = bsMinTracker
 
-rselect :: (Foldable f, Functor f) => f a -> Backtrack a
+rselect :: (Foldable f) => f a -> Backtrack a
 rselect (toList -> fa) = (shuffleM fa) >>= select
 {-# INLINE rselect #-}
 
-select :: (Foldable f, Functor f) => f a -> Backtrack a
-select fa = asum (pure <$> fa)
+select :: (Foldable f) => f a -> Backtrack a
+select (toList -> fa) = asum (pure <$> fa)
 {-# INLINE select #-}
 
 runBacktrack :: MT.MinTracker -> Graph -> Backtrack a -> Maybe (a, Graph)
diff --git a/src/Props/Internal/Graph.hs b/src/Props/Internal/Graph.hs
--- a/src/Props/Internal/Graph.hs
+++ b/src/Props/Internal/Graph.hs
@@ -43,7 +43,6 @@
 import Data.Maybe
 import Data.Typeable
 import Data.Typeable.Lens
-import Data.MonoTraversable
 
 type DFilter = Dynamic
 type DChoice = Dynamic
@@ -51,22 +50,22 @@
 newtype Vertex = Vertex Int
   deriving (Show, Eq, Ord)
 
-data SuperPos f where
-    Observed :: MonoFoldable f => Element f -> SuperPos f
-    Unknown :: MonoFoldable f => f -> SuperPos f
+data SuperPos f a where
+    Observed :: Foldable f => a -> SuperPos f a
+    Unknown :: Foldable f => f a -> SuperPos f a
 
-instance Show (SuperPos f) where
+instance Show (SuperPos f a) where
   show (Observed _) = "Observed"
   show (Unknown _) = "Unknown"
 
-_Unknown :: (Show f, Show (Element f), MonoFoldable f) => Prism' (SuperPos f) f
+_Unknown :: Foldable f => Prism' (SuperPos f a) (f a)
 _Unknown = prism' embed match
   where
     embed = Unknown
     match (Unknown f) = Just f
     match _ = Nothing
 
-_Observed :: (Show (Element f), MonoFoldable f) => Prism' (SuperPos f) (Element f)
+_Observed :: Foldable f => Prism' (SuperPos f a) a
 _Observed = prism' embed match
   where
     embed = Observed
@@ -74,11 +73,11 @@
     match _ = Nothing
 
 data Quantum =
-    forall f. (Show (SuperPos f), Typeable f, Typeable (Element f), MonoFoldable f) => Quantum
-        { options   :: SuperPos f
+    forall f a. (Show (SuperPos f a), Typeable f, Typeable a, Foldable f) => Quantum
+        { options   :: SuperPos f a
         }
 
-superPos :: (Typeable f, Typeable (Element f), MonoFoldable f) => Traversal' Quantum (SuperPos f)
+superPos :: (Typeable f, Typeable a) => Traversal' Quantum (SuperPos f a)
 superPos f (Quantum o) = Quantum <$> (o & _cast %%~ f)
 
 instance Show Quantum where
@@ -126,5 +125,5 @@
 {-# INLINE edgesFrom #-}
 
 entropyOfQ :: Quantum -> (Maybe Int)
-entropyOfQ (Quantum (Unknown xs)) = Just $ olength xs
+entropyOfQ (Quantum (Unknown xs)) = Just $ length xs
 entropyOfQ _ = Nothing
diff --git a/src/Props/Internal/Links.hs b/src/Props/Internal/Links.hs
--- a/src/Props/Internal/Links.hs
+++ b/src/Props/Internal/Links.hs
@@ -7,14 +7,13 @@
 
 import qualified Data.Set as S
 import Props.Internal.PropT
-import Data.Typeable
 
 {-|
 Apply the constraint that two variables may NOT be set to the same value. This constraint is bidirectional.
 
 E.g. you might apply this constraint to two cells in the same row of sudoku grid to assert they don't contain the same value.
 -}
-disjoint :: forall a m. (Monad m, Typeable a, Ord a) => PVar (S.Set a) -> PVar (S.Set a) -> PropT m ()
+disjoint :: forall a m. (Monad m, Ord a) => PVar S.Set a -> PVar S.Set a -> PropT m ()
 disjoint a b = do
     constrain a b disj
     constrain b a disj
@@ -25,7 +24,7 @@
 {-|
 Apply the constraint that two variables MUST be set to the same value. This constraint is bidirectional.
 -}
-equal :: forall a m. (Monad m, Typeable a, Ord a) => PVar (S.Set a) -> PVar (S.Set a) -> PropT m ()
+equal :: forall a m. (Monad m, Ord a) => PVar S.Set a -> PVar S.Set a -> PropT m ()
 equal a b = do
     constrain a b eq
     constrain b a eq
@@ -39,8 +38,8 @@
 
 E.g. if @a@ must always be greater than @b@, you could require:
 
-> require (>) a b 
+> require (>) a b
 -}
-require :: (Monad m, Typeable a, Ord a, Typeable b) => (a -> b -> Bool) -> PVar (S.Set a) -> PVar (S.Set b) -> PropT m ()
+require :: Monad m => (a -> b -> Bool) -> PVar S.Set a -> PVar S.Set b -> PropT m ()
 require f a b = do
     constrain a b (S.filter . f)
diff --git a/src/Props/Internal/PropT.hs b/src/Props/Internal/PropT.hs
--- a/src/Props/Internal/PropT.hs
+++ b/src/Props/Internal/PropT.hs
@@ -4,6 +4,9 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeApplications #-}
 
 module Props.Internal.PropT
     ( Prop
@@ -22,7 +25,6 @@
 import Control.Lens
 import Data.Typeable
 import Data.Dynamic
-import Data.MonoTraversable
 import Data.Maybe
 
 -- | Pure version of 'PropT'
@@ -38,22 +40,29 @@
     deriving newtype (Functor, Applicative, Monad, MonadIO, MonadTrans)
 
 {-|
-A propagator variable where the possible values are contained in the MonoFoldable type @f@.
+A propagator variable where the possible values @a@ are contained in the container @f@.
 -}
-data PVar f = PVar Vertex
-  deriving (Eq -- ^ Nominal equality, Ignores contents
-    , Ord -- ^ Nominal ordering, Ignores contents.
-    , Show
-           )
+data PVar (f :: * -> *) a where
+  PVar :: (Typeable a, Typeable f) => Vertex -> PVar f a
 
+-- | Nominal equality, Ignores contents
+instance Eq (PVar f a) where
+  (PVar v) == (PVar t) = v == t
+
+instance Ord (PVar f a) where
+  PVar v <= PVar t = v <= t
+
+instance Show (PVar f a) where
+  show (PVar _) = unwords ["PVar", show (typeRep (Proxy @f)), show (typeRep (Proxy @a))]
+
 {-|
 Used to create a new propagator variable within the setup for your problem.
 
-@f@ is any MonoFoldable container which contains each of the possible states which the variable could take. In practice this most standard containers make a good candidate, it's easy to define a your own instance if needed.
+@f@ is any Foldable container which contains each of the possible states which the variable could take.
 
-E.g. For a sudoku solver you would use 'newPVar' to create a variable for each cell, passing a @Set Int@ or @IntSet@ containing the numbers @[1..9]@.
+E.g. For a sudoku solver you would use 'newPVar' to create a variable for each cell, passing a @Set Int@ containing the numbers @[1..9]@.
 -}
-newPVar :: (Monad m, MonoFoldable f, Typeable f, Typeable (Element f)) => f -> PropT m (PVar f)
+newPVar :: (Monad m, Foldable f, Typeable f, Typeable a) => f a -> PropT m (PVar f a)
 newPVar xs = PropT $ do
     v <- vertexCount <+= 1
     vertices . at v ?= (Quantum (Unknown xs), mempty)
@@ -62,19 +71,24 @@
 {-|
 'constrain' the relationship between two 'PVar's. Note that this is a ONE WAY relationship; e.g. @constrain a b f@ will propagate constraints from @a@ to @b@ but not vice versa.
 
-Given @PVar f@ and @PVar g@ as arguments, provide a function which will filter/alter the options in @g@ according to the choice.
+Given @PVar f a@ and @PVar g b@ as arguments, provide a function which will filter/alter the options in @g@ according to the choice.
 
-For a sudoku puzzle @f@ and @g@ each represent cells on the board. If @f ~ Set Int@ and @g ~ Set Int@, then you might pass a constraint filter:
+For a sudoku puzzle you'd have two @Pvar Set Int@'s, each representing a cell on the board.
+You can constrain @b@ to be a different value than @a@ with the following call:
 
 > constrain a b $ \elementA setB -> S.delete elementA setB)
 
 Take a look at some linking functions which are already provided: 'disjoint', 'equal', 'require'
 -}
-constrain :: (Monad m, Typeable g, Typeable (Element f)) => PVar f -> PVar g -> (Element f -> g -> g) -> PropT m ()
+constrain :: Monad m
+          => PVar f a
+          -> PVar g b
+          -> (a -> g b -> g b)
+          -> PropT m ()
 constrain (PVar from') (PVar to') f = PropT $ do
     edgeBetween from' to' ?= toDyn f
 
-readPVar :: (Typeable (Element f)) => Graph -> PVar f -> Element f
+readPVar :: Graph -> PVar f a -> a
 readPVar g (PVar v) =
     fromMaybe (error "readPVar called on unsolved graph")
     $ (g ^? valueAt v . folding unpackQuantum)
@@ -83,36 +97,63 @@
 unpackQuantum (Quantum (Observed xs)) = cast xs
 unpackQuantum (Quantum _) = Nothing
 
-buildGraph :: (Monad m) => PropT m a -> m (a, Graph)
+buildGraph :: PropT m a -> m (a, Graph)
 buildGraph = flip runStateT emptyGraph . runGraphM
 
 {-|
-Given an action which initializes and constrains a problem and returns some container of 'PVar's, 'solveT' will attempt to find a solution which passes all valid constraints.
+Provide an initialization action which constrains the problem, and a finalizer, and 'solveT' will return a result if one exists.
+
+The finalizer is an annoyance caused by the fact that GHC does not yet support Impredicative Types.
+
+For example, if you wrote a solution to the nQueens problem, you might run it like so:
+
+> -- Set up the problem for 'n' queens and return their PVar's as a list.
+> initNQueens :: Int -> Prop [PVar S.Set Coord]
+> initNQueens = ...
+>
+> solution :: [Coord]
+> solution = solve (initNQueens 8) (\readPVar vars -> fmap readPVar vars)
+which converts 'PVar's into a result.Given an action which initializes and constrains a problem 'solveT' will  and returns some container of 'PVar's, 'solveT' will attempt to find a solution which passes all valid constraints.
 -}
-solveT :: (Monad m, Functor f, Typeable (Element g)) => PropT m (f (PVar g)) -> m (Maybe (f (Element g)))
-solveT m = do
+solveT :: forall m a r.
+       Monad m
+       => ((forall f x. PVar f x -> x) -> a -> r)
+       -> PropT m a
+       -> m (Maybe r)
+solveT f m = do
     (a, g) <- buildGraph m
     case P.solve g of
         Nothing -> return Nothing
-        Just solved -> return . Just $ readPVar solved <$> a
+        Just solved -> return . Just $ f (readPVar solved) a
 
+
 {-|
 Like 'solveT', but finds ALL possible solutions. There will likely be duplicates.
 -}
-solveAllT :: (Monad m, Functor f, Typeable (Element g)) => PropT m (f (PVar g)) -> m ([f (Element g)])
-solveAllT m = do
-    (fa, g) <- buildGraph m
+solveAllT :: forall m a r.
+          Monad m
+          => ((forall f x. PVar f x -> x) -> a -> r)
+          -> PropT m a
+          -> m [r]
+solveAllT f m = do
+    (a, g) <- buildGraph m
     let gs = P.solveAll g
-    return $ gs <&> \g' -> (readPVar g') <$> fa
+    return $ gs <&> \g' -> f (readPVar g') a
 
 {-|
 Pure version of 'solveT'
 -}
-solve :: (Functor f, Typeable (Element g)) => Prop (f (PVar g)) -> Maybe (f (Element g))
-solve = runIdentity . solveT
+solve :: forall a r.
+        ((forall f x. PVar f x -> x) -> a -> r)
+      -> Prop a
+      -> (Maybe r)
+solve f = runIdentity . solveT f
 
 {-|
 Pure version of 'solveAllT'
 -}
-solveAll :: (Functor f, Typeable (Element g)) => Prop (f (PVar g)) -> [f (Element g)]
-solveAll = runIdentity . solveAllT
+solveAll :: forall a r.
+            ((forall f x. PVar f x -> x) -> a -> r)
+          -> Prop a
+          -> [r]
+solveAll f = runIdentity . solveAllT f
diff --git a/src/Props/Internal/Props.hs b/src/Props/Internal/Props.hs
--- a/src/Props/Internal/Props.hs
+++ b/src/Props/Internal/Props.hs
@@ -15,7 +15,6 @@
 import Props.Internal.Graph
 import qualified Props.Internal.MinTracker as MT
 import Data.Dynamic
-import Data.MonoTraversable
 import Data.Foldable
 import Control.Monad.State
 
@@ -41,10 +40,9 @@
 
 choicesOfQ' :: Quantum -> Vertex -> Backtrack ()
 choicesOfQ' (Quantum (Observed{})) _ = error "Can't collapse an already collapsed node!"
-choicesOfQ' (Quantum (Unknown xs :: SuperPos f)) n = do
-    let options = otoList xs
-    choice <- select options
-    graph . valueAt n . superPos .= (Observed choice :: SuperPos f)
+choicesOfQ' (Quantum (Unknown xs :: SuperPos f a)) n = do
+    choice <- select xs
+    graph . valueAt n . superPos .= (Observed choice :: SuperPos f a)
     propagate (n, toDyn choice)
 {-# INLINE choicesOfQ' #-}
 
@@ -73,8 +71,8 @@
     return ()
   where
     alterQ :: Quantum -> (Maybe Int, Quantum)
-    alterQ (Quantum (Unknown xs :: SuperPos f)) = do
-        let filteredDown = (forceDyn $ dynApp (dynApp dfilter v) (toDyn xs) :: f)
-         in (Just $ olength filteredDown, Quantum (Unknown filteredDown))
+    alterQ (Quantum (Unknown xs :: SuperPos f a)) = do
+        let filteredDown = (forceDyn $ dynApp (dynApp dfilter v) (toDyn xs) :: f a)
+         in (Just $ length filteredDown, Quantum (Unknown filteredDown))
     alterQ q = (Nothing, q)
 {-# INLINE propagateSingle #-}