diff --git a/bench/EnumVect.hs b/bench/EnumVect.hs
new file mode 100644
--- /dev/null
+++ b/bench/EnumVect.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE RebindableSyntax, GADTs, TypeFamilies, ScopedTypeVariables #-}
+
+module EnumVect where
+
+import Data.Vector.Unboxed hiding (foldl')
+import Data.Foldable (foldl')
+import Data.Ix
+import Control.Monad.Constrained hiding (replicate, zipWith)
+import Prob
+import qualified Prelude
+
+data EnumVect a where
+  EnumVect :: (Ix a, Bounded a) => Vector Double -> EnumVect a
+
+runEnumVect :: EnumVect a -> Vector Double
+runEnumVect (EnumVect xs) = xs
+{-# INLINE runEnumVect #-}
+
+instance Functor EnumVect where
+    type Suitable EnumVect a = (Ix a, Bounded a)
+    fmap (f :: a -> b) (EnumVect xs :: EnumVect a) =
+        EnumVect $
+        accum
+            (+)
+            (replicate (rangeSize (minBound :: b,maxBound)) 0)
+            [ (index (minBound,maxBound) (f x), xs ! index (minBound,maxBound) x)
+            | x <- range (minBound, maxBound) ]
+    {-# INLINE fmap #-}
+
+
+instance Applicative EnumVect where
+    type Unconstrained EnumVect = Dist
+    reflect (EnumVect xs) =
+        Dist (Prelude.zip (range (minBound, maxBound)) (toList xs))
+    reify (Dist (xs :: [(a, Double)])) =
+        EnumVect $
+        accum
+            (+)
+            (replicate (rangeSize (minBound :: a, maxBound)) 0)
+            [ (index (minBound, maxBound) x, p)
+            | (x,p) <- xs ]
+    {-# INLINE reflect #-}
+    {-# INLINE reify #-}
+
+instance Monad EnumVect where
+    EnumVect xs >>= (f :: a -> EnumVect b) =
+        EnumVect $
+        foldl'
+            g
+            (replicate (rangeSize (minBound :: b, maxBound)) 0)
+            (range (minBound, maxBound))
+      where
+        g acc e =
+            let fac = xs ! index (minBound, maxBound) e
+            in zipWith
+                   (\accm n ->
+                         accm + fac * n)
+                   acc
+                   (runEnumVect (f e))
+        {-# INLINE g #-}
+    {-# INLINE (>>=) #-}
+
+probOfV :: a -> EnumVect a -> Double
+probOfV x (EnumVect xs) = xs ! index (minBound,maxBound) x
+{-# INLINE probOfV #-}
+
+uniformV
+    :: (Ix a, Bounded a)
+    => [a] -> EnumVect a
+uniformV (xs :: [a]) =
+    EnumVect $
+    accum
+        (+)
+        (replicate (rangeSize (minBound :: a,maxBound)) 0)
+        [ (index (minBound,maxBound) x, sz)
+        | x <- xs ]
+        where sz = 1 / fromIntegral (Prelude.length xs)
+{-# INLINE uniformV #-}
+
+upToV :: (Integral a, Bounded a, Ix a) => a -> EnumVect a
+upToV (n :: a) =
+    EnumVect $
+    accum
+        (+)
+        (replicate (rangeSize (minBound :: a,maxBound)) 0)
+        [ (index (minBound,maxBound) x, 1 / fromIntegral n)
+        | x <- [1 .. n] ]
+{-# INLINE upToV #-}
diff --git a/bench/MuchAdo.hs b/bench/MuchAdo.hs
new file mode 100644
--- /dev/null
+++ b/bench/MuchAdo.hs
@@ -0,0 +1,129 @@
+{-# LANGUAGE ApplicativeDo    #-}
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+
+module MuchAdo where
+
+import           Control.Monad.Constrained.Ap
+import           Data.Set
+import           Prob
+import           EnumVect
+import           Numeric.Sized.WordOfSize
+
+sumThriceAdoFinal :: [Int] -> Int
+sumThriceAdoFinal xs = size . retractAp @ Final $ do
+  a <- fromList' xs
+  b <- fromList' xs
+  c <- upTo' (a + b)
+  d <- fromList' xs
+  e <- fromList' xs
+  pure (c + e + d)
+  where
+    upTo' = liftAp . fromDistinctAscList . enumFromTo 1
+    fromList' = liftAp . fromList
+
+sumThriceAdoInitial :: [Int] -> Int
+sumThriceAdoInitial xs = size . retractAp @ Initial $ do
+  a <- fromList' xs
+  b <- fromList' xs
+  c <- upTo' (a + b)
+  d <- fromList' xs
+  e <- fromList' xs
+  pure (c + e + d)
+  where
+    upTo' = liftAp . fromDistinctAscList . enumFromTo 1
+    fromList' = liftAp . fromList
+
+sumThriceAdoConstrained :: [Int] -> Int
+sumThriceAdoConstrained xs = size . retractAp @ ConstrainedWrapper $ do
+  a <- fromList' xs
+  b <- fromList' xs
+  c <- upTo' (a + b)
+  d <- fromList' xs
+  e <- fromList' xs
+  pure (c + e + d)
+  where
+    upTo' = liftAp . fromDistinctAscList . enumFromTo 1
+    fromList' = liftAp . fromList
+
+sumThriceAdoCodensity :: [Int] -> Int
+sumThriceAdoCodensity xs = size . retractAp @ Codensity $ do
+  a <- fromList' xs
+  b <- fromList' xs
+  c <- upTo' (a + b)
+  d <- fromList' xs
+  e <- fromList' xs
+  pure (c + e + d)
+  where
+    upTo' = liftAp . fromDistinctAscList . enumFromTo 1
+    fromList' = liftAp . fromList
+
+diceAdoFinal :: Int -> [Int] -> Double
+diceAdoFinal n die' = probOf n . retractAp @ Final $ do
+  a <- die
+  b <- die
+  c <- upTo' (a + b)
+  d <- die
+  e <- die
+  pure (c + e + d)
+  where
+    die = liftAp (uniform die')
+    upTo' = liftAp . upTo
+
+diceAdoInitial :: Int -> [Int] -> Double
+diceAdoInitial n die' = probOf n . retractAp @ Initial $ do
+  a <- die
+  b <- die
+  c <- upTo' (a + b)
+  d <- die
+  e <- die
+  pure (c + e + d)
+  where
+    die = liftAp (uniform die')
+    upTo' = liftAp . upTo
+
+diceAdoConstrained :: Int -> [Int] -> Double
+diceAdoConstrained n die' = probOf n . retractAp @ ConstrainedWrapper $ do
+  a <- die
+  b <- die
+  c <- upTo' (a + b)
+  d <- die
+  e <- die
+  pure (c + e + d)
+  where
+    die = liftAp (uniform die')
+    upTo' = liftAp . upTo
+
+diceAdoCodensity :: Int -> [Int] -> Double
+diceAdoCodensity n die' = probOf n . retractAp @ Codensity $ do
+  a <- die
+  b <- die
+  c <- upTo' (a + b)
+  d <- die
+  e <- die
+  pure (c + e + d)
+  where
+    die = liftAp (uniform die')
+    upTo' = liftAp . upTo
+
+diceVectAdoInitial :: WordOfSize 3 -> [WordOfSize 3] -> Double
+diceVectAdoInitial n die' = probOfV n . retractAp @ Initial $ do
+  a <- die
+  b <- upTo' a
+  c <- die
+  d <- upTo' c
+  pure (b + d)
+  where
+    die = liftAp (uniformV die')
+    upTo' = liftAp . upToV
+
+diceVectAdoCodensity :: WordOfSize 3 -> [WordOfSize 3] -> Double
+diceVectAdoCodensity n die' = probOfV n . retractAp @ Codensity $ do
+  a <- die
+  b <- upTo' a
+  c <- die
+  pure (b + c)
+  where
+    die = liftAp (uniformV die')
+    upTo' = liftAp . upToV
diff --git a/bench/NoAdo.hs b/bench/NoAdo.hs
new file mode 100644
--- /dev/null
+++ b/bench/NoAdo.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE DataKinds        #-}
+
+module NoAdo where
+
+import           Control.Monad.Constrained
+import           Data.Set
+import           EnumVect
+import           Prob
+import           Numeric.Sized.WordOfSize
+
+sumThriceNoAdo :: [Int] -> Int
+sumThriceNoAdo xs = size $ do
+  a <- fromList' xs
+  b <- fromList' xs
+  c <- upTo' (a + b)
+  d <- fromList' xs
+  e <- fromList' xs
+  pure (c + e + d)
+  where
+    upTo' n = fromList [1..n]
+    fromList' = fromList
+
+diceNoAdo :: Int -> [Int] -> Double
+diceNoAdo n die' = probOf n $ do
+  a <- die
+  b <- die
+  c <- upTo' (a + b)
+  d <- die
+  e <- die
+  pure (c + e + d)
+  where
+    die = uniform die'
+    upTo' = upTo
+
+diceVectNoAdo :: WordOfSize 3 -> [WordOfSize 3] -> Double
+diceVectNoAdo n die' = probOfV n $ do
+  a <- die
+  b <- upTo' a
+  c <- die
+  d <- upTo' c
+  pure (b + d)
+  where
+    die = uniformV die'
+    upTo' = upToV
diff --git a/bench/Prob.hs b/bench/Prob.hs
new file mode 100644
--- /dev/null
+++ b/bench/Prob.hs
@@ -0,0 +1,125 @@
+{-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE RebindableSyntax           #-}
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE Strict                     #-}
+
+module Prob where
+
+import           Control.Monad.Constrained
+
+import qualified Prelude
+
+import           Data.Map.Strict           (Map)
+import qualified Data.Map.Strict           as Map
+
+newtype Prob a
+  = Prob
+  { runProb :: Map a Double
+  } deriving (Show, Eq, Ord)
+
+newtype Dist a
+  = Dist
+  { runDist :: [(a,Double)]
+  } deriving (Prelude.Functor, Monoid)
+
+instance Prelude.Applicative Dist where
+  pure x = Dist [(x , 1)]
+  {-# INLINE pure #-}
+  Dist fs <*> Dist xs
+    = Dist
+    [ (f x, fp * xp)
+    | (f , fp) <- fs
+    , (x , xp) <- xs ]
+  {-# INLINE (<*>) #-}
+
+instance Prelude.Monad Dist where
+  Dist xs >>= f
+    = Dist
+    [ (y, xp * yp)
+    | (x , xp) <- xs
+    , (y , yp) <- runDist (f x) ]
+  {-# INLINE (>>=) #-}
+
+instance Functor Prob where
+    type Suitable Prob a = Ord a
+    fmap f (Prob xs) = Prob (Map.mapKeysWith (+) f xs)
+    {-# INLINE fmap #-}
+
+
+instance Applicative Prob where
+    type Unconstrained Prob = Dist
+    reflect = Dist . Map.toList . runProb
+    {-# INLINE reflect #-}
+    reify = Prob . Map.fromListWith (+) . runDist
+    {-# INLINE reify #-}
+    _ *> x = x
+    {-# INLINE (*>) #-}
+    x <* _ = x
+    {-# INLINE (<*) #-}
+
+scaled :: Prob a -> Double -> Prob a
+scaled (Prob xs) n = Prob (Map.map (n*) xs)
+{-# INLINE scaled #-}
+
+instance Monad Prob where
+    Prob xs >>= f =
+        Map.foldlWithKey'
+            (\a x p ->
+                  combScale p a (f x))
+            mempty
+            xs
+    {-# INLINE (>>=) #-}
+
+instance (Ord a) =>
+         Monoid (Prob a) where
+    mempty = Prob Map.empty
+    {-# INLINE mempty #-}
+    mappend (Prob xs) (Prob ys) = Prob (Map.unionWith (+) xs ys)
+    {-# INLINE mappend #-}
+
+combScale
+    :: (Ord a)
+    => Double -> Prob a -> Prob a -> Prob a
+combScale p (Prob xs) (Prob ys) =
+    Prob
+        (Map.mergeWithKey
+             (\_ x y ->
+                   Just $ x + p * y)
+             id
+             (Map.map (p *))
+             xs
+             ys)
+{-# INLINE combScale #-}
+
+instance Foldable Prob where
+    foldMap f (Prob xs) =
+        Map.foldMapWithKey
+            (\k _ ->
+                  f k)
+            xs
+    {-# INLINE foldMap #-}
+
+uniform
+    :: (Ord a)
+    => [a] -> Prob a
+uniform xs =
+    (Prob . Map.fromListWith (+) . map (flip (,) (1 / fromIntegral l))) xs
+  where
+    l = length xs
+{-# INLINE uniform #-}
+
+upTo :: (Integral a) => a -> Prob a
+upTo n = uniform [1..n]
+{-# INLINE upTo #-}
+
+eighths :: Prob Integer
+eighths = uniform [1..8]
+{-# INLINE eighths #-}
+
+probOf
+    :: (Ord a)
+    => a -> Prob a -> Double
+probOf x (Prob xs) = Map.findWithDefault 0 x xs
+{-# INLINE probOf #-}
diff --git a/bench/bench.hs b/bench/bench.hs
new file mode 100644
--- /dev/null
+++ b/bench/bench.hs
@@ -0,0 +1,43 @@
+module Main (main) where
+
+import MuchAdo
+import NoAdo
+
+import Criterion.Main
+
+import Control.DeepSeq
+
+import GHC.TypeLits
+
+import Numeric.Sized.WordOfSize
+
+instance KnownNat n => NFData (WordOfSize n)
+
+main :: IO ()
+main =
+    defaultMain
+        [ env (pure ([1 .. 6], 8)) $
+          \ ~(xs,n) ->
+               bgroup
+                   "probabilistic inference map"
+                   [ bench "Applicative rewriting, Final encoding"       $ whnf (diceAdoFinal       n) xs
+                   , bench "Applicative rewriting, Initial encoding"     $ whnf (diceAdoInitial     n) xs
+                   , bench "Applicative rewriting, Constrained encoding" $ whnf (diceAdoConstrained n) xs
+                   , bench "Applicative rewriting, Codensity encoding"   $ whnf (diceAdoCodensity   n) xs
+                   , bench "No rewriting"                                $ whnf (diceNoAdo          n) xs]
+        , env (pure [1 .. 5]) $
+          \xs ->
+               bgroup
+                   "set"
+                   [ bench "Applicative rewriting, Final encoding"       $ whnf sumThriceAdoFinal       xs
+                   , bench "Applicative rewriting, Initial encoding"     $ whnf sumThriceAdoInitial     xs
+                   , bench "Applicative rewriting, Constrained encoding" $ whnf sumThriceAdoConstrained xs
+                   , bench "Applicative rewriting, Codensity encoding"   $ whnf sumThriceAdoCodensity   xs
+                   , bench "No rewriting"                                $ whnf sumThriceNoAdo          xs]
+        , env (pure ([1 .. 5], 30)) $
+          \ ~(xs,n) ->
+               bgroup
+                   "probabilistic inference vect"
+                   [ bench "Applicative rewriting, Initial encoding"  $ whnf (diceVectAdoInitial   n) xs
+                   , bench "Applicative rewriting Codensity encoding" $ whnf (diceVectAdoCodensity n) xs
+                   , bench "No rewriting"                             $ whnf (diceVectNoAdo        n) xs]]
diff --git a/constrained-monads.cabal b/constrained-monads.cabal
--- a/constrained-monads.cabal
+++ b/constrained-monads.cabal
@@ -1,5 +1,5 @@
 name:                constrained-monads
-version:             0.4.0.0
+version:             0.5.0.0
 synopsis:            Typeclasses and instances for monads with constraints. 
 description:         A library for monads with constraints over the types they contain. This allows set, etc to conform to the monad class. It is structured as a prelude replacement: everything that doesn't conflict with the new definitions of 'Functor', 'Monad', etc is reexported.
                      
@@ -25,9 +25,12 @@
                      , Control.Monad.Constrained.Cont
                      , Control.Monad.Constrained.IntSet
                      , Control.Monad.Constrained.Ap
+  other-modules:       Control.Monad.Constrained.Internal.Unconstrained
   build-depends:       base >= 4.9 && < 5
                      , containers >= 0.5
                      , transformers >= 0.5
+                     , free >= 0.12
+                     , deepseq >= 1.4
   default-language:    Haskell2010
   ghc-options:         -Wall
 
@@ -47,6 +50,27 @@
                        -Wall
   default-language:    Haskell2010
 
+benchmark bench
+  default-language:    Haskell2010
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      bench
+  main-is:             bench.hs
+  other-modules:       MuchAdo
+                     , NoAdo
+                     , Prob
+                     , EnumVect
+  ghc-options:         -O2 -rtsopts -threaded
+
+  build-depends:       base >= 4.8
+                     , constrained-monads >= 0.4.1
+                     , criterion >= 0.6
+                     , containers >= 0.5
+                     , smallcheck >= 1.1.1
+                     , QuickCheck >= 2.8
+                     , vector >= 0.11
+                     , transformers >= 0.5
+                     , nat-sized-numbers >= 0.2
+                     , deepseq >= 1.4
 
 
 source-repository head
diff --git a/src/Control/Monad/Constrained.hs b/src/Control/Monad/Constrained.hs
--- a/src/Control/Monad/Constrained.hs
+++ b/src/Control/Monad/Constrained.hs
@@ -1,14 +1,16 @@
-{-# LANGUAGE ConstraintKinds      #-}
-{-# LANGUAGE BangPatterns         #-}
-{-# LANGUAGE DataKinds            #-}
-{-# LANGUAGE GADTs                #-}
-{-# LANGUAGE LambdaCase           #-}
-{-# LANGUAGE RebindableSyntax     #-}
-{-# LANGUAGE TypeFamilies         #-}
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE ScopedTypeVariables  #-}
-{-# LANGUAGE RankNTypes           #-}
+{-# LANGUAGE ConstraintKinds        #-}
+{-# LANGUAGE BangPatterns           #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE LambdaCase             #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE RebindableSyntax       #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
 
 -- | A module for constrained monads. This module is intended to be imported
 -- with the @-XRebindableSyntax@ extension turned on: everything from the
@@ -25,11 +27,8 @@
   ,Traversable(..)
   ,MonadFail(..)
   ,
-   -- * Horrible type-level stuff
-  Ap(..)
-  ,lowerP
-  ,lowerM
-  ,liftAp
+   -- * Unconstrained applicative stuff
+   ap
   ,
    -- * Useful functions
    guard
@@ -75,8 +74,9 @@
 import           Data.Sequence                    (Seq)
 import           Data.Set                         (Set)
 import qualified Data.Set                         as Set
-import           Data.Tree                        (Tree(..))
+import           Data.Tree                        (Tree (..))
 
+import           Control.Monad.ST                 (ST)
 import           Control.Monad.Trans.Cont         (ContT)
 import           Control.Monad.Trans.Except       (ExceptT (..), runExceptT)
 import           Control.Monad.Trans.Identity     (IdentityT (..))
@@ -84,32 +84,20 @@
 import           Control.Monad.Trans.Reader       (ReaderT (..), mapReaderT)
 import           Control.Monad.Trans.State        (StateT (..))
 import qualified Control.Monad.Trans.State.Strict as Strict (StateT (..))
+import           Data.Functor.Compose             (Compose (..))
+import           Data.Functor.Const               (Const)
+import           Data.Functor.Product             (Product (..))
+import           Data.Functor.Sum                 (Sum (..))
 
-import           Control.Arrow (first)
+import           Control.Arrow                    (first)
+import           Control.Monad.Trans.State.Strict (runState, state)
 import           Data.Tuple
-import           Control.Monad.Trans.State.Strict (state, runState)
 
---------------------------------------------------------------------------------
--- Type-level shenanigans
---------------------------------------------------------------------------------
-
--- | A free applicative. Applicative operations are defined in terms of
--- /interpretations/ of this.
-data Ap f a where
-  Pure :: a -> Ap f a
-  Ap :: Ap f (a -> b) -> f a -> Ap f b
-
-instance Prelude.Functor (Ap f) where
-  fmap f (Pure a) = Pure (f a)
-  fmap f (Ap x y) = Ap ((f .) Prelude.<$> x) y
-
-instance Prelude.Applicative (Ap f) where
-  pure = Pure
-  Pure f <*> y = Prelude.fmap f y
-  Ap x y <*> z = Ap (flip Prelude.<$> x Prelude.<*> z) y
+import           Control.Applicative.Free         (Ap (Ap, Pure))
+import qualified Control.Applicative.Free         as Initial
 
-liftAp :: f a -> Ap f a
-liftAp = Ap (Pure id)
+import Control.Monad.Constrained.Internal.Unconstrained
+-- import qualified Control.Applicative.Free.Final   as Final
 
 --------------------------------------------------------------------------------
 -- Standard classes
@@ -129,23 +117,28 @@
 -- 'Prelude.Functor'. The way to make a standard 'Prelude.Functor' conform
 -- is by indicating that it has no constraints. For instance, for @[]@:
 --
--- @instance 'Functor' [] where
---  type 'Suitable' [] a = ()
---  fmap = map
---  (<$) = (Prelude.<$)@
+-- @
+-- instance 'Functor' [] where
+--   fmap = map
+--   (<$) = (Prelude.<$)
+-- @
 --
 -- Monomorphic types can also conform, using GADT aliases. For instance,
 -- if you create an alias for 'Data.IntSet.IntSet' of kind @* -> *@:
 --
--- @data IntSet a where
---  IntSet :: IntSet.'Data.IntSet.IntSet' -> IntSet 'Int'@
+-- @
+-- data IntSet a where
+--   IntSet :: IntSet.'Data.IntSet.IntSet' -> IntSet 'Int'
+-- @
 --
 -- It can be made to conform to 'Functor' like so:
 --
--- @instance 'Functor' IntSet where
---  type 'Suitable' IntSet a = a ~ 'Int'
---  'fmap' f (IntSet xs) = IntSet (IntSet.'Data.IntSet.map' f xs)
---  x '<$' xs = if 'null' xs then 'empty' else 'pure' x@
+-- @
+-- instance 'Functor' IntSet where
+--   type 'Suitable' IntSet a = a ~ 'Int'
+--   'fmap' f (IntSet xs) = IntSet (IntSet.'Data.IntSet.map' f xs)
+--   x '<$' xs = if 'null' xs then 'empty' else 'pure' x
+-- @
 --
 -- It can also be made conform to 'Foldable', etc. This type is provided in
 -- "Control.Monad.Constrained.IntSet".
@@ -159,15 +152,16 @@
     --    'fmap' = Set.'Set.map'
     --    x '<$' xs = if Set.'Set.null' xs then Set.'Set.empty' else Set.'Set.singleton' x@
     type Suitable f a :: Constraint
+    type Suitable f a = ()
 
     -- | Maps a function over a functor
     fmap
-        :: Suitable f b
+        :: (Suitable f b)
         => (a -> b) -> f a -> f b
 
     -- | Replace all values in the input with a default value.
     infixl 4 <$
-    (<$) :: Suitable f a => a -> f b -> f a
+    (<$) :: (Suitable f a) => a -> f b -> f a
     (<$) = fmap . const
     {-# INLINE (<$) #-}
 
@@ -177,8 +171,10 @@
 -- provided in the Prelude. This is to facilitate the lifting of functions
 -- to arbitrary numbers of arguments.
 --
--- A minimal complete definition must include implementations of 'lower'
--- functions satisfying the following laws:
+-- A minimal complete definition must include implementations of 'reflect' and
+-- 'reify' which convert to and from a law-abiding applicative, such that they
+-- form an isomorphism. Alternatively, you can conform to the standard prelude
+-- classes, and satisfy the following laws:
 --
 -- [/identity/]
 --
@@ -214,26 +210,30 @@
 --   * @('<*>') = 'ap'@
 --
 -- (which implies that 'pure' and '<*>' satisfy the applicative functor laws).
-class Functor f =>
+class (Prelude.Applicative (Unconstrained f), Functor f) =>
       Applicative f  where
-    {-# MINIMAL lower #-}
 
+    type Unconstrained f :: * -> *
+    type Unconstrained f = f
+
+    {-# MINIMAL reflect , reify #-}
+    reflect :: f a -> Unconstrained f a
+    reify
+        :: Suitable f a
+        => Unconstrained f a -> f a
     -- | Lift a value.
     pure
         :: Suitable f a
         => a -> f a
-    pure x = lower (Pure x)
+    pure = reify . Prelude.pure
     {-# INLINE pure #-}
-
     infixl 4 <*>
-
     -- | Sequential application.
     (<*>)
         :: Suitable f b
         => f (a -> b) -> f a -> f b
-    (<*>) = liftA2 ($)
+    (<*>) fs xs = reify (reflect fs Prelude.<*> reflect xs)
     {-# INLINE (<*>) #-}
-
     infixl 4 *>
     -- | Sequence actions, discarding the value of the first argument.
     (*>)
@@ -241,7 +241,6 @@
         => f a -> f b -> f b
     (*>) = liftA2 (const id)
     {-# INLINE (*>) #-}
-
     infixl 4 <*
     -- | Sequence actions, discarding the value of the second argument.
     (<*)
@@ -249,100 +248,35 @@
         => f a -> f b -> f a
     (<*) = liftA2 const
     {-# INLINE (<*) #-}
-    -- | The shenanigans introduced by this function are to account for the fact
-    -- that you can't (I don't think) write an arbitrary lift function on
-    -- non-monadic applicatives that have constrained types. For instance, if
-    -- the only present functions are:
-    --
-    -- @'pure'  :: 'Suitable' f a => a -> f b
-    --'fmap'  :: 'Suitable' f b => (a -> b) -> f a -> f b
-    --('<*>') :: 'Suitable' f b => f (a -> b) -> f a -> f b@
-    --
-    -- I can't see a way to define:
-    --
-    -- @'liftA2' :: 'Suitable' f c => (a -> b -> c) -> f a -> f b -> f c@
-    --
-    -- Of course, if:
-    --
-    -- @('>>=') :: 'Suitable' f b => f a -> (a -> f b) -> f b@
-    --
-    -- is available, 'liftA2' could be defined as:
-    --
-    -- @'liftA2' f xs ys = do
-    --    x <- xs
-    --    y <- ys
-    --    'pure' (f x y)@
-    --
-    -- But now we can't define the 'lower' functions for things which are
-    -- 'Applicative' but not 'Monad' (square matrices,
-    -- 'Control.Applicative.ZipList's, etc). Also, some types have a more
-    -- efficient @('<*>')@ than @('>>=')@ (see, for instance, the
-    -- <https://simonmar.github.io/posts/2015-10-20-Fun-With-Haxl-1.html Haxl>
-    -- monad).
-    --
-    -- The one missing piece is @-XApplicativeDo@: I can't figure out a way
-    -- to get do-notation to desugar to using the 'lower' functions, rather
-    -- than @('<*>')@.
-    --
-    -- From some preliminary performance testing, it seems that this approach
-    -- has /no/ performance overhead.
-    --
-    -- Utility definitions of this function are provided: if your 'Applicative'
-    -- is a @Prelude.'Prelude.Applicative'@, 'lower' can be defined in terms of
-    -- @('<*>')@. 'lowerP' does exactly this.
-    --
-    -- Alternatively, if your applicative is a 'Monad', 'lower' can be defined
-    -- in terms of @('>>=')@, which is what 'lowerM' does.
-    lower
-        :: Suitable f a
-        => Ap f a -> f a
-
     liftA2
-        :: Suitable f c
+        :: (Suitable f c)
         => (a -> b -> c) -> f a -> f b -> f c
-    liftA2 f xs ys =
-        lower (Ap (Ap (Pure f) xs) ys)
-
+    liftA2 f xs ys = reify (Control.Applicative.liftA2 f (reflect xs) (reflect ys))
+    {-# INLINE liftA2 #-}
     liftA3
-        :: Suitable f d
+        :: (Suitable f d)
         => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
     liftA3 f xs ys zs =
-        lower (Ap (Ap (Ap (Pure f) xs) ys) zs)
-
-    {-# INLINE liftA2 #-}
+        reify (Control.Applicative.liftA3 f (reflect xs) (reflect ys) (reflect zs))
     {-# INLINE liftA3 #-}
 
 infixl 4 <**>
 -- | A variant of '<*>' with the arguments reversed.
 (<**>) :: (Applicative f, Suitable f b) => f a -> f (a -> b) -> f b
 (<**>) = liftA2 (flip ($))
-
--- | A definition of 'lower' that uses monadic operations.
-lowerM :: (Monad f, Suitable f a) => Ap f a -> f a
-lowerM = go pure where
-  go :: (Suitable f b, Monad f) => (a -> f b) -> Ap f a -> f b
-  go f (Pure x) = f x
-  go f (Ap xs x) = go (\c -> x >>= f . c) xs
-
--- | A definition of 'lower' which uses the "Prelude"'s @('Prelude.<*>')@.
-lowerP :: Prelude.Applicative f => Ap f a -> f a
-lowerP (Pure x) = Prelude.pure x
-lowerP (Ap (Pure f) xs) = Prelude.fmap f xs
-lowerP (Ap ys xs) = lowerP ys Prelude.<*> xs
-{-# INLINABLE lowerP #-}
-
-{-# INLINE liftA2P #-}
-{-# INLINE liftA3P #-}
--- | Definitions for the various lifts using only "Prelude" functions.
-liftA2P
-    :: (Prelude.Applicative f)
-    => (a -> b -> c) -> f a -> f b -> f c
-liftA2P f x y = f Prelude.<$> x Prelude.<*> y
+{-# INLINE (<**>) #-}
 
-liftA3P
-    :: Prelude.Applicative f
-    => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
-liftA3P f xs ys zs = f Prelude.<$> xs Prelude.<*> ys Prelude.<*> zs
+-- | A definition of 'reify' that uses monadic operations. This is actually
+-- the instance of applicative for codensity in disguise.
+ap
+    :: (Monad f, Suitable f a)
+    => (a -> f a) -> Initial.Ap f a -> f a
+ap = flip runAp
+  where
+    runAp :: (Suitable f b, Monad f) => Ap f a -> (a -> f b) -> f b
+    runAp (Pure x) = \c -> c x
+    runAp (Ap xs fs) = \c -> xs >>= \x -> runAp fs (\g -> (c . g) x)
+{-# INLINE ap #-}
 
 {- | The 'Monad' class defines the basic operations over a /monad/,
 a concept from a branch of mathematics known as /category theory/.
@@ -509,7 +443,7 @@
     -- from left to right, and collect the results. For a version that ignores
     -- the results see 'traverse_'.
     traverse
-        :: (Suitable t b, Applicative f, Suitable f (t b))
+        :: (Suitable t b, Applicative f, Suitable f (t b), Suitable f b)
         => (a -> f b) -> t a -> f (t b)
 
 
@@ -558,11 +492,13 @@
 --
 (<$>) :: (Functor f, Suitable f b) => (a -> b) -> f a -> f b
 (<$>) = fmap
+{-# INLINE (<$>) #-}
 
 infixr 1 =<<, <=<
 -- | A flipped version of '>>='
 (=<<) :: (Monad f, Suitable f b) => (a -> f b) -> f a -> f b
 (=<<) = flip (>>=)
+{-# INLINE (=<<) #-}
 
 -- | Right-to-left Kleisli composition of monads. @('>=>')@, with the arguments flipped.
 --
@@ -572,11 +508,13 @@
 -- > (<=<) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c
 (<=<) :: (Monad f, Suitable f c) => (b -> f c) -> (a -> f b) -> a -> f c
 (f <=< g) x = f =<< g x
+{-# INLINE (<=<) #-}
 
 infixl 1 >=>
 
 -- | Left-to-right Kleisli composition of monads.
 (>=>) :: (Monad f, Suitable f c) => (a -> f b) -> (b -> f c) -> a -> f c
+{-# INLINE (>=>) #-}
 (f >=> g) x = f x >>= g
 
 -- | @'forever' act@ repeats the action infinitely.
@@ -586,7 +524,9 @@
 
 -- | Monadic fold over the elements of a structure,
 -- associating to the left, i.e. from left to right.
-foldM :: (Foldable t, Monad m, Suitable m b) => (b -> a -> m b) -> b -> t a -> m b
+foldM
+    :: (Foldable t, Monad m, Suitable m b)
+    => (b -> a -> m b) -> b -> t a -> m b
 foldM f z0 xs = foldr f' pure xs z0
   where f' x k z = f z x >>= k
 
@@ -598,49 +538,67 @@
 -- 2
 -- 3
 -- 4
-for_ :: (Foldable t, Applicative f, Suitable f ()) => t a -> (a -> f b) -> f ()
+for_
+    :: (Foldable t, Applicative f, Suitable f ())
+    => t a -> (a -> f b) -> f ()
 {-# INLINE for_ #-}
 for_ = flip traverse_
 
 -- | Map each element of a structure to an action, evaluate these
 -- actions from left to right, and ignore the results. For a version
 -- that doesn't ignore the results see 'traverse'.
-traverse_ :: (Applicative f, Foldable t, Suitable f ()) => (a -> f b) -> t a -> f ()
-traverse_ f = foldr (\e a -> f e *> a) (pure ())
+traverse_
+    :: (Applicative f, Foldable t, Suitable f ())
+    => (a -> f b) -> t a -> f ()
+traverse_ f =
+    foldr (\e a -> f e *> a) (pure ())
+{-# INLINE traverse_ #-}
 
 -- | Evaluate each action in the structure from left to right, and
 -- ignore the results. For a version that doesn't ignore the results
 -- see 'Data.Traversable.sequenceA'.
 sequenceA_ :: (Foldable t, Applicative f, Suitable f ()) => t (f a) -> f ()
 sequenceA_ = foldr (*>) (pure ())
+{-# INLINE sequenceA_ #-}
 
 -- | @'guard' b@ is @'pure' ()@ if @b@ is 'True',
 -- and 'empty' if @b@ is 'False'.
 guard :: (Alternative f, Suitable f ()) => Bool -> f ()
 guard True = pure ()
 guard False = empty
+{-# INLINE guard #-}
 
 -- | @'ensure' b x@ is @x@ if @b@ is 'True',
 -- and 'empty' if @b@ is 'False'.
 ensure :: (Alternative f, Suitable f a) => Bool -> f a -> f a
 ensure True x = x
 ensure False _ = empty
+{-# INLINE ensure #-}
 
 -- | Evaluate each action in the structure from left to right, and
 -- and collect the results. For a version that ignores the results
 -- see 'sequenceA_'.
 sequenceA
-    :: (Applicative f, Suitable t a, Suitable f (t a), Traversable t)
+    :: (Applicative f
+       ,Suitable t a
+       ,Suitable f (t a)
+       ,Traversable t
+       ,Suitable f a)
     => t (f a) -> f (t a)
 sequenceA = traverse id
+{-# INLINE sequenceA #-}
 
 -- |The 'mapAccumL' function behaves like a combination of 'fmap'
 -- and 'foldl'; it applies a function to each element of a structure,
 -- passing an accumulating parameter from left to right, and returning
 -- a final value of this accumulator together with the new structure.
-mapAccumL :: (Traversable t, Suitable t c) => (a -> b -> (a, c)) -> a -> t b -> (a, t c)
-mapAccumL f s t = swap $ runState (traverse (state . (swap .: flip f)) t) s where
-  (.:) = (.).(.)
+mapAccumL
+    :: (Traversable t, Suitable t c)
+    => (a -> b -> (a, c)) -> a -> t b -> (a, t c)
+mapAccumL f s t = swap $ runState (traverse (state . (swap .: flip f)) t) s
+  where
+    (.:) = (.) . (.)
+{-# INLINE mapAccumL #-}
 
 -- | @'replicateM' n act@ performs the action @n@ times,
 -- gathering the results.
@@ -696,10 +654,12 @@
 -- 2
 void :: (Functor f, Suitable f ()) => f a -> f ()
 void = (<$) ()
+{-# INLINE void #-}
 
 -- | Collapse one monadic layer.
 join :: (Monad f, Suitable f a) => f (f a) -> f a
 join x = x >>= id
+{-# INLINE join #-}
 
 --------------------------------------------------------------------------------
 -- syntax
@@ -707,8 +667,9 @@
 
 -- | Function to which the @if ... then ... else@ syntax desugars to
 ifThenElse :: Bool -> a -> a -> a
-ifThenElse True t _ = t
+ifThenElse True  t _ = t
 ifThenElse False _ f = f
+{-# INLINE ifThenElse #-}
 
 infixl 1 >>
 -- | Sequence two actions, discarding the result of the first. Alias for
@@ -717,12 +678,14 @@
     :: (Applicative f, Suitable f b)
     => f a -> f b -> f b
 (>>) = (*>)
+{-# INLINE (>>) #-}
 
 -- | Alias for 'pure'.
 return
     :: (Applicative f, Suitable f a)
     => a -> f a
 return = pure
+{-# INLINE return #-}
 
 --------------------------------------------------------------------------------
 -- instances
@@ -732,97 +695,158 @@
     type Suitable [] a = ()
     fmap = map
     (<$) = (Prelude.<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
+
 instance Applicative [] where
-    lower = lowerP
+    type Unconstrained [] = []
+    reify = id
+    reflect = id
     (<*>) = (Prelude.<*>)
     (*>) = (Prelude.*>)
     (<*) = (Prelude.<*)
     pure = Prelude.pure
-    liftA2 = liftA2P
-    liftA3 = liftA3P
+    liftA2 = Control.Applicative.liftA2
+    liftA3 = Control.Applicative.liftA3
+    {-# INLINE reify #-}
+    {-# INLINE reflect #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+    {-# INLINE pure #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE liftA3 #-}
 
 instance Alternative [] where
-  empty = []
-  (<|>) = (++)
+    empty = []
+    (<|>) = (++)
+    {-# INLINE empty #-}
+    {-# INLINE (<|>) #-}
 
 instance Monad [] where
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
 
 instance MonadFail [] where
     fail _ = []
+    {-# INLINE fail #-}
 
 instance Traversable [] where
     traverse f = foldr (liftA2 (:) . f) (pure [])
+    {-# INLINE traverse #-}
 
 instance Functor Maybe where
     type Suitable Maybe a = ()
     fmap = Prelude.fmap
     (<$) = (Prelude.<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
 instance Applicative Maybe where
-    lower = lowerP
+    reify = id
+    {-# INLINE reify #-}
+    reflect = id
+    {-# INLINE reflect #-}
     (<*>) = (Prelude.<*>)
+    {-# INLINE (<*>) #-}
     (*>) = (Prelude.*>)
+    {-# INLINE (*>) #-}
     (<*) = (Prelude.<*)
+    {-# INLINE (<*) #-}
     pure = Prelude.pure
-    liftA2 = liftA2P
-    liftA3 = liftA3P
+    {-# INLINE pure #-}
+    liftA2 = Control.Applicative.liftA2
+    {-# INLINE liftA2 #-}
+    liftA3 = Control.Applicative.liftA3
+    {-# INLINE liftA3 #-}
 
 instance Alternative Maybe where
     empty = Control.Applicative.empty
     (<|>) = (Control.Applicative.<|>)
+    {-# INLINE empty #-}
+    {-# INLINE (<|>) #-}
 
 instance Monad Maybe where
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
 
 instance MonadFail Maybe where
     fail _ = Nothing
+    {-# INLINE fail #-}
 
 instance Traversable Maybe where
     traverse _ Nothing = pure Nothing
     traverse f (Just x) = fmap Just (f x)
+    {-# INLINE traverse #-}
 
 instance Functor IO where
     type Suitable IO a = ()
     fmap = Prelude.fmap
     (<$) = (Prelude.<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
 instance Applicative IO where
-    lower = lowerP
+    reify = id
+    reflect = id
     (<*>) = (Prelude.<*>)
     (*>) = (Prelude.*>)
     (<*) = (Prelude.<*)
     pure = Prelude.pure
-    liftA2 = liftA2P
-    liftA3 = liftA3P
+    liftA2 = Control.Applicative.liftA2
+    liftA3 = Control.Applicative.liftA3
+    {-# INLINE reify #-}
+    {-# INLINE reflect #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+    {-# INLINE pure #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE liftA3 #-}
 
 instance Alternative IO where
     empty = Control.Applicative.empty
     (<|>) = (Control.Applicative.<|>)
+    {-# INLINE empty #-}
+    {-# INLINE (<|>) #-}
 
 instance Monad IO where
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
 
 instance MonadFail IO where
     fail = Prelude.fail
+    {-# INLINE fail #-}
 
 instance Functor Identity where
     type Suitable Identity a = ()
     fmap = Prelude.fmap
     (<$) = (Prelude.<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
 instance Applicative Identity where
-    lower = lowerP
+    reify = id
+    reflect = id
     (<*>) = (Prelude.<*>)
     (*>) = (Prelude.*>)
     (<*) = (Prelude.<*)
     pure = Prelude.pure
-    liftA2 = liftA2P
-    liftA3 = liftA3P
+    liftA2 = Control.Applicative.liftA2
+    liftA3 = Control.Applicative.liftA3
+    {-# INLINE reify #-}
+    {-# INLINE reflect #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+    {-# INLINE pure #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE liftA3 #-}
 
 instance Monad Identity where
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
 
 instance Traversable Identity where
     traverse f (Identity x) = fmap Identity (f x)
@@ -831,210 +855,346 @@
     type Suitable (Either e) a = ()
     fmap = Prelude.fmap
     (<$) = (Prelude.<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
 instance Applicative (Either a) where
-    lower = lowerP
+    reify = id
+    reflect = id
     (<*>) = (Prelude.<*>)
     (*>) = (Prelude.*>)
     (<*) = (Prelude.<*)
     pure = Prelude.pure
-    liftA2 = liftA2P
-    liftA3 = liftA3P
+    liftA2 = Control.Applicative.liftA2
+    liftA3 = Control.Applicative.liftA3
+    {-# INLINE reify #-}
+    {-# INLINE reflect #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+    {-# INLINE pure #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE liftA3 #-}
 
 instance Monad (Either a) where
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
 
 instance IsString a =>
          MonadFail (Either a) where
     fail = Left . fromString
+    {-# INLINE fail #-}
 
 instance Traversable (Either a) where
     traverse f = either (pure . Left) (fmap Right . f)
+    {-# INLINE traverse #-}
 
 instance Functor Set where
     type Suitable Set a = Ord a
     fmap = Set.map
+    {-# INLINE fmap #-}
     x <$ xs = if null xs then Set.empty else Set.singleton x
+    {-# INLINE (<$) #-}
 
+
 instance Applicative Set where
+    type Unconstrained Set = StrictLeftFold
     pure = Set.singleton
-    fs <*> xs = foldMap (`Set.map` xs) fs
+    {-# INLINE pure #-}
     xs *> ys = if null xs then Set.empty else ys
+    {-# INLINE (*>) #-}
     xs <* ys = if null ys then Set.empty else xs
-    lower = lowerM
+    {-# INLINE (<*) #-}
+    reify (StrictLeftFold xs) = xs (flip Set.insert) Set.empty
+    {-# INLINE reify #-}
+    reflect xs = StrictLeftFold (\f b -> Set.foldl' f b xs)
+    {-# INLINE reflect #-}
 
 instance Monad Set where
     (>>=) = flip foldMap
+    {-# INLINE (>>=) #-}
 
 instance MonadFail Set where
     fail _ = Set.empty
+    {-# INLINE fail #-}
 
 instance Alternative Set where
     empty = Set.empty
     (<|>) = Set.union
+    {-# INLINE empty #-}
+    {-# INLINE (<|>) #-}
 
 instance Functor (Map a) where
     type Suitable (Map a) b = ()
     fmap = Prelude.fmap
     (<$) = (Prelude.<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
 instance Functor ((,) a) where
     type Suitable ((,) a) b = ()
     fmap = Prelude.fmap
     (<$) = (Prelude.<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
 instance Monoid a => Applicative ((,) a) where
-    lower = lowerP
+    reify = id
+    reflect = id
     (<*>) = (Prelude.<*>)
     (*>) = (Prelude.*>)
     (<*) = (Prelude.<*)
     pure = Prelude.pure
-    liftA2 = liftA2P
-    liftA3 = liftA3P
+    liftA2 = Control.Applicative.liftA2
+    liftA3 = Control.Applicative.liftA3
+    {-# INLINE reify #-}
+    {-# INLINE reflect #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+    {-# INLINE pure #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE liftA3 #-}
 
 instance Monoid a => Monad ((,) a) where
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
 
 instance Traversable ((,) a) where
     traverse f (x,y) = fmap ((,) x) (f y)
+    {-# INLINE traverse #-}
 
 instance Functor IntMap where
     type Suitable IntMap a = ()
     fmap = Prelude.fmap
     (<$) = (Prelude.<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
 instance Functor Seq where
     type Suitable Seq a = ()
     fmap = Prelude.fmap
     (<$) = (Prelude.<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
 instance Applicative Seq where
-    lower = lowerP
+    reify = id
+    reflect = id
     (<*>) = (Prelude.<*>)
     (*>) = (Prelude.*>)
     (<*) = (Prelude.<*)
     pure = Prelude.pure
-    liftA2 = liftA2P
-    liftA3 = liftA3P
+    liftA2 = Control.Applicative.liftA2
+    liftA3 = Control.Applicative.liftA3
+    {-# INLINE reify #-}
+    {-# INLINE reflect #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+    {-# INLINE pure #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE liftA3 #-}
 
 instance Alternative Seq where
     empty = Control.Applicative.empty
     (<|>) = (Control.Applicative.<|>)
+    {-# INLINE empty #-}
+    {-# INLINE (<|>) #-}
 
 instance Monad Seq where
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
 
 instance MonadFail Seq where
     fail _ = empty
+    {-# INLINE fail #-}
 
 instance Functor Tree where
     type Suitable Tree a = ()
     fmap = Prelude.fmap
     (<$) = (Prelude.<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
 instance Applicative Tree where
-    lower = lowerP
+    reify = id
+    reflect = id
     (<*>) = (Prelude.<*>)
     (*>) = (Prelude.*>)
     (<*) = (Prelude.<*)
     pure = Prelude.pure
-    liftA2 = liftA2P
-    liftA3 = liftA3P
+    liftA2 = Control.Applicative.liftA2
+    liftA3 = Control.Applicative.liftA3
+    {-# INLINE reify #-}
+    {-# INLINE reflect #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+    {-# INLINE pure #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE liftA3 #-}
 
 instance Monad Tree where
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
 
+instance Traversable Tree where
+    traverse f (Node x ts) =
+        let g = (reflect . f)
+        in reify
+               (Node Prelude.<$> g x Prelude.<*>
+                Prelude.traverse (Prelude.traverse g) ts)
+    {-# INLINE traverse #-}
+
 instance Functor ((->) a) where
     type Suitable ((->) a) b = ()
     fmap = Prelude.fmap
     (<$) = (Prelude.<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
 instance Applicative ((->) a) where
-    lower = lowerP
+    reify = id
+    reflect = id
     (<*>) = (Prelude.<*>)
     (*>) = (Prelude.*>)
     (<*) = (Prelude.<*)
     pure = Prelude.pure
-    liftA2 = liftA2P
-    liftA3 = liftA3P
+    liftA2 = Control.Applicative.liftA2
+    liftA3 = Control.Applicative.liftA3
+    {-# INLINE reify #-}
+    {-# INLINE reflect #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+    {-# INLINE pure #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE liftA3 #-}
 
 instance Monad ((->) a) where
-  (>>=) = (Prelude.>>=)
+    (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
 
 instance Functor (ContT r m) where
     type Suitable (ContT r m) a = ()
     fmap = Prelude.fmap
     (<$) = (Prelude.<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
 instance Applicative (ContT r m) where
-    lower = lowerP
+    reify = id
+    reflect = id
     (<*>) = (Prelude.<*>)
     (*>) = (Prelude.*>)
     (<*) = (Prelude.<*)
     pure = Prelude.pure
-    liftA2 = liftA2P
-    liftA3 = liftA3P
+    liftA2 = Control.Applicative.liftA2
+    liftA3 = Control.Applicative.liftA3
+    {-# INLINE reify #-}
+    {-# INLINE reflect #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+    {-# INLINE pure #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE liftA3 #-}
 
 instance Monad (ContT r m) where
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
 
 instance Functor Control.Applicative.ZipList where
     type Suitable Control.Applicative.ZipList a = ()
     fmap = Prelude.fmap
     (<$) = (Prelude.<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
 instance Applicative Control.Applicative.ZipList where
-    lower = lowerP
+    reify = id
+    reflect = id
     (<*>) = (Prelude.<*>)
     (*>) = (Prelude.*>)
     (<*) = (Prelude.<*)
     pure = Prelude.pure
-    liftA2 = liftA2P
-    liftA3 = liftA3P
+    liftA2 = Control.Applicative.liftA2
+    liftA3 = Control.Applicative.liftA3
+    {-# INLINE reify #-}
+    {-# INLINE reflect #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+    {-# INLINE pure #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE liftA3 #-}
 
-instance Functor m => Functor (Strict.StateT s m) where
+instance Functor m =>
+         Functor (Strict.StateT s m) where
     type Suitable (Strict.StateT s m) a = Suitable m (a, s)
-    fmap f m = Strict.StateT $ \ s ->
-        (\ (!a, !s') -> (f a, s')) <$> Strict.runStateT m s
+    fmap f m =
+        Strict.StateT $
+        \s ->
+             (\(!a,!s') ->
+                   (f a, s')) <$>
+             Strict.runStateT m s
     {-# INLINE fmap #-}
-    x <$ xs = Strict.StateT ((fmap.first) (const x) . Strict.runStateT xs)
+    x <$ xs = Strict.StateT ((fmap . first) (const x) . Strict.runStateT xs)
+    {-# INLINE (<$) #-}
 
-instance Monad m =>
+instance (Monad m, Prelude.Monad (Unconstrained m)) =>
          Applicative (Strict.StateT s m) where
+    type Unconstrained (Strict.StateT s m)
+        = Strict.StateT s (Unconstrained m)
+
+    reflect (Strict.StateT xs) = Strict.StateT (reflect . xs)
+    {-# INLINE reflect #-}
     pure a =
         Strict.StateT $
-        \(!s) ->
+        \ !s ->
              pure (a, s)
     {-# INLINE pure #-}
     Strict.StateT mf <*> Strict.StateT mx =
         Strict.StateT $
-        \s -> do
-            (f,s') <- mf s
-            (x,s'') <- mx s'
+        \ !s -> do
+            (f,!s') <- mf s
+            (x,!s'') <- mx s'
             pure (f x, s'')
+    {-# INLINE (<*>) #-}
     Strict.StateT xs *> Strict.StateT ys =
         Strict.StateT $
-        \(!s) -> do
-            (_,s') <- xs s
+        \ !s -> do
+            (_,!s') <- xs s
             ys s'
+    {-# INLINE (*>) #-}
     Strict.StateT xs <* Strict.StateT ys =
         Strict.StateT $
-        \(!s) -> do
-            (x,s') <- xs s
-            (_,s'') <- ys s'
-            pure (x,s'')
-    lower = lowerM
+        \ !s -> do
+            (x,!s') <- xs s
+            (_,!s'') <- ys s'
+            pure (x, s'')
+    {-# INLINE (<*) #-}
+    reify (Strict.StateT xs) = Strict.StateT (reify . xs)
+    {-# INLINE reify #-}
 
-instance (Monad m, Alternative m) => Alternative (Strict.StateT s m) where
+instance (Monad m, Alternative m, Prelude.Monad (Unconstrained m)) =>
+         Alternative (Strict.StateT s m) where
     empty = Strict.StateT (const empty)
     {-# INLINE empty #-}
-    Strict.StateT m <|> Strict.StateT n = Strict.StateT $ \ s -> m s <|> n s
+    Strict.StateT m <|> Strict.StateT n =
+        Strict.StateT $
+        \ !s ->
+             m s <|> n s
     {-# INLINE (<|>) #-}
 
-instance (Monad m) => Monad (Strict.StateT s m) where
-    m >>= k = Strict.StateT $ \ s -> do
-        (a, s') <- Strict.runStateT m s
-        Strict.runStateT (k a) s'
+instance (Monad m, Prelude.Monad (Unconstrained m)) =>
+         Monad (Strict.StateT s m) where
+    m >>= k =
+        Strict.StateT $
+        \ !s -> do
+            (a, !s') <- Strict.runStateT m s
+            Strict.runStateT (k a) s'
     {-# INLINE (>>=) #-}
 
 instance Functor m => Functor (StateT s m) where
@@ -1044,8 +1204,12 @@
     {-# INLINE fmap #-}
     x <$ StateT xs = StateT ((fmap.first) (const x) . xs)
 
-instance (Monad m) =>
+
+instance (Monad m, Prelude.Monad (Unconstrained m)) =>
          Applicative (StateT s m) where
+    type Unconstrained (StateT s m) = StateT s (Unconstrained m)
+    reflect (StateT xs) = StateT (reflect . xs)
+    {-# INLINE reflect #-}
     pure a =
         StateT $
         \s ->
@@ -1068,15 +1232,19 @@
             ~(x,s') <- xs s
             ~(_,s'') <- ys s'
             pure (x,s'')
-    lower = lowerM
+    reify (StateT xs) = StateT (reify . xs)
 
-instance (Monad m, Alternative m) => Alternative (StateT s m) where
+instance (Monad m, Alternative m, Prelude.Monad (Unconstrained m)) =>
+         Alternative (StateT s m) where
     empty = StateT (const empty)
     {-# INLINE empty #-}
-    StateT m <|> StateT n = StateT $ \ s -> m s <|> n s
+    StateT m <|> StateT n =
+        StateT $
+        \s ->
+             m s <|> n s
     {-# INLINE (<|>) #-}
 
-instance (Monad m) => Monad (StateT s m) where
+instance (Monad m, Prelude.Monad (Unconstrained m)) => Monad (StateT s m) where
     m >>= k  = StateT $ \ s -> do
         ~(a, s') <- runStateT m s
         runStateT (k a) s'
@@ -1087,18 +1255,24 @@
     fmap f = mapReaderT (fmap f)
     {-# INLINE fmap #-}
     x <$ ReaderT xs = ReaderT (\r -> x <$ xs r)
+    {-# INLINE (<$) #-}
 
+
 instance (Applicative m) => Applicative (ReaderT r m) where
+    type Unconstrained (ReaderT r m)
+        = ReaderT r (Unconstrained m)
     pure = liftReaderT . pure
+    reflect (ReaderT f) = ReaderT (reflect . f)
+    {-# INLINE reflect #-}
     {-# INLINE pure #-}
     f <*> v = ReaderT $ \ r -> runReaderT f r <*> runReaderT v r
     {-# INLINE (<*>) #-}
-    lower ys = ReaderT $ \r -> lower (tr r ys) where
-      tr :: r -> Ap (ReaderT r m) xs -> Ap m xs
-      tr _ (Pure x) = Pure x
-      tr r (Ap xs x) = Ap (tr r xs) (runReaderT x r)
+    reify ys = ReaderT (reify . runReaderT ys)
+    {-# INLINE reify #-}
     ReaderT xs *> ReaderT ys = ReaderT (\c -> xs c *> ys c)
     ReaderT xs <* ReaderT ys = ReaderT (\c -> xs c <* ys c)
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
 
 instance (Alternative m) => Alternative (ReaderT r m) where
     empty   = liftReaderT empty
@@ -1109,6 +1283,7 @@
 instance MonadFail m =>
          MonadFail (ReaderT r m) where
     fail = ReaderT . const . fail
+    {-# INLINE fail #-}
 
 instance (Monad m) => Monad (ReaderT r m) where
     m >>= k  = ReaderT $ \ r -> do
@@ -1124,52 +1299,86 @@
          Functor (MaybeT m) where
     type Suitable (MaybeT m) a = (Suitable m (Maybe a), Suitable m a)
     fmap f (MaybeT xs) = MaybeT ((fmap . fmap) f xs)
+    {-# INLINE fmap #-}
     x <$ MaybeT xs = MaybeT (fmap (x <$) xs)
+    {-# INLINE (<$) #-}
 
-instance Monad m =>
+
+instance (Prelude.Monad (Unconstrained m), Monad m) =>
          Applicative (MaybeT m) where
+    type Unconstrained (MaybeT m) = MaybeT (Unconstrained m)
+    reflect (MaybeT x) = MaybeT (reflect x)
+    {-# INLINE reflect #-}
     pure x = MaybeT (pure (Just x))
+    {-# INLINE pure #-}
     MaybeT fs <*> MaybeT xs = MaybeT (liftA2 (<*>) fs xs)
-    lower = lowerM
+    reify (MaybeT x) = MaybeT (reify x)
+    {-# INLINE reify #-}
     MaybeT xs *> MaybeT ys = MaybeT (liftA2 (*>) xs ys)
     MaybeT xs <* MaybeT ys = MaybeT (liftA2 (<*) xs ys)
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
 
-instance Monad m =>
+instance (Monad m, Prelude.Monad (Unconstrained m)) =>
          Monad (MaybeT m) where
     MaybeT x >>= f = MaybeT (x >>= maybe (pure Nothing) (runMaybeT . f))
+    {-# INLINE (>>=) #-}
 
-instance Monad m =>
+instance (Monad m, Prelude.Monad (Unconstrained m)) =>
          MonadFail (MaybeT m) where
     fail _ = empty
+    {-# INLINE fail #-}
 
-instance Monad m =>
+instance (Monad m, Prelude.Monad (Unconstrained m)) =>
          Alternative (MaybeT m) where
     empty = MaybeT (pure Nothing)
+    {-# INLINE empty #-}
     MaybeT x <|> MaybeT y = MaybeT (x >>= maybe y (pure . Just))
+    {-# INLINE (<|>) #-}
 
 instance Functor m =>
          Functor (ExceptT e m) where
     type Suitable (ExceptT e m) a = Suitable m (Either e a)
     fmap f (ExceptT xs) = ExceptT ((fmap . fmap) f xs)
+    {-# INLINE fmap #-}
     x <$ ExceptT xs = ExceptT (fmap (x <$) xs)
+    {-# INLINE (<$) #-}
 
-instance Monad m =>
+
+instance (Monad m, Prelude.Monad (Unconstrained m)) =>
          Applicative (ExceptT e m) where
+    type Unconstrained (ExceptT e m) = ExceptT e (Unconstrained m)
+    reflect (ExceptT x) = ExceptT (reflect x)
+    {-# INLINE reflect #-}
     pure x = ExceptT (pure (Right x))
+    {-# INLINE pure #-}
     ExceptT fs <*> ExceptT xs = ExceptT (liftA2 (<*>) fs xs)
-    lower = lowerM
+    reify (ExceptT xs) = ExceptT (reify xs)
+    {-# INLINE reify #-}
     ExceptT xs *> ExceptT ys = ExceptT (xs *> ys)
     ExceptT xs <* ExceptT ys = ExceptT (xs <* ys)
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
 
-instance (Monad m, IsString e) => MonadFail (ExceptT e m) where
+instance (Monad m, IsString e, Prelude.Monad (Unconstrained m)) =>
+         MonadFail (ExceptT e m) where
     fail = ExceptT . pure . Left . fromString
+    {-# INLINE fail #-}
 
-instance Monad m => Monad (ExceptT e m) where
-  ExceptT xs >>= f = ExceptT (xs >>= either (pure . Left) (runExceptT . f))
+instance (Monad m, Prelude.Monad (Unconstrained m)) =>
+         Monad (ExceptT e m) where
+    ExceptT xs >>= f = ExceptT (xs >>= either (pure . Left) (runExceptT . f))
+    {-# INLINE (>>=) #-}
 
-instance (Monad m, Monoid e) => Alternative (ExceptT e m) where
-  empty = ExceptT (pure (Left mempty))
-  ExceptT xs <|> ExceptT ys = ExceptT (xs >>= either (const ys) (pure . Right))
+instance (Monad m, Monoid e, Prelude.Monad (Unconstrained m)) =>
+         Alternative (ExceptT e m) where
+    empty = ExceptT (pure (Left mempty))
+    {-# INLINE empty #-}
+    ExceptT xs <|> ExceptT ys =
+        ExceptT (xs >>= either (const ys) (pure . Right))
+    {-# INLINE (<|>) #-}
 
 instance Functor m =>
          Functor (IdentityT m) where
@@ -1180,25 +1389,151 @@
     (<$) =
         (coerce :: (a -> f b -> f a) -> a -> IdentityT f b -> IdentityT f a)
             (<$)
+    {-# INLINE fmap #-}
+    {-# INLINE (<$) #-}
 
 instance Applicative m =>
          Applicative (IdentityT m) where
+    type Unconstrained (IdentityT m) = IdentityT (Unconstrained m)
+    reflect (IdentityT x) = IdentityT (reflect x)
+    {-# INLINE reflect #-}
     pure = (coerce :: (a -> f a) -> a -> IdentityT f a) pure
+    {-# INLINE pure #-}
     (<*>) =
         (coerce :: (f (a -> b) -> f a -> f b) -> IdentityT f (a -> b) -> IdentityT f a -> IdentityT f b)
             (<*>)
-    lower =
-        (coerce :: (Ap f xs -> f b) -> (Ap (IdentityT f) xs -> IdentityT f b))
-            lower
+    reify =
+        (coerce :: (Unconstrained f b -> f b) -> (IdentityT (Unconstrained f) b -> IdentityT f b))
+            reify
+    {-# INLINE reify #-}
     IdentityT xs *> IdentityT ys = IdentityT (xs *> ys)
     IdentityT xs <* IdentityT ys = IdentityT (xs <* ys)
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
 
 instance Monad m =>
          Monad (IdentityT m) where
     (>>=) =
         (coerce :: (f a -> (a -> f b) -> f b) -> IdentityT f a -> (a -> IdentityT f b) -> IdentityT f b)
             (>>=)
+    {-# INLINE (>>=) #-}
 
 instance MonadFail m =>
          MonadFail (IdentityT m) where
     fail = IdentityT . fail
+    {-# INLINE fail #-}
+
+instance Functor (ST s) where
+    type Suitable (ST s) a = ()
+    fmap = Prelude.fmap
+    {-# INLINE fmap #-}
+    (<$) = (Prelude.<$)
+    {-# INLINE (<$) #-}
+
+instance Applicative (ST s) where
+    reify = id
+    reflect = id
+    (<*>) = (Prelude.<*>)
+    (*>) = (Prelude.*>)
+    (<*) = (Prelude.<*)
+    pure = Prelude.pure
+    liftA2 = Control.Applicative.liftA2
+    liftA3 = Control.Applicative.liftA3
+    {-# INLINE reify #-}
+    {-# INLINE reflect #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+    {-# INLINE pure #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE liftA3 #-}
+
+instance Monad (ST s) where
+    (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
+
+instance Functor (Const a) where
+    type Suitable (Const a) b = ()
+    fmap = Prelude.fmap
+    {-# INLINE fmap #-}
+    (<$) = (Prelude.<$)
+    {-# INLINE (<$) #-}
+
+instance Monoid a => Applicative (Const a) where
+    reify = id
+    reflect = id
+    (<*>) = (Prelude.<*>)
+    (*>) = (Prelude.*>)
+    (<*) = (Prelude.<*)
+    pure = Prelude.pure
+    liftA2 = Control.Applicative.liftA2
+    liftA3 = Control.Applicative.liftA3
+    {-# INLINE reify #-}
+    {-# INLINE reflect #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+    {-# INLINE pure #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE liftA3 #-}
+
+instance (Functor f, Functor g) =>
+         Functor (Compose f g) where
+    type Suitable (Compose f g) a = (Suitable g a, Suitable f (g a))
+    fmap f (Compose xs) = Compose ((fmap . fmap) f xs)
+    {-# INLINE fmap #-}
+
+
+instance (Applicative f, Applicative g) =>
+         Applicative (Compose f g) where
+  type Unconstrained (Compose f g) =
+       Compose (Unconstrained f) (Unconstrained g)
+  reify (Compose xs) = Compose (reify (Prelude.fmap reify xs))
+  {-# INLINE reify #-}
+  reflect (Compose xs) = Compose (Prelude.fmap reflect (reflect xs))
+  {-# INLINE reflect #-}
+
+instance (Alternative f, Applicative g) => Alternative (Compose f g) where
+    empty = Compose empty
+    {-# INLINE empty #-}
+    Compose x <|> Compose y = Compose (x <|> y)
+    {-# INLINE (<|>) #-}
+
+instance (Functor f, Functor g) => Functor (Product f g) where
+    type Suitable (Product f g) a = (Suitable f a, Suitable g a)
+    fmap f (Pair x y) = Pair (fmap f x) (fmap f y)
+    {-# INLINE fmap #-}
+
+
+instance (Applicative f, Applicative g) =>
+         Applicative (Product f g) where
+    type Unconstrained (Product f g) =
+        Product (Unconstrained f) (Unconstrained g)
+    pure x = Pair (pure x) (pure x)
+    {-# INLINE pure #-}
+    Pair f g <*> Pair x y = Pair (f <*> x) (g <*> y)
+    {-# INLINE (<*>) #-}
+    reify (Pair xs ys) = Pair (reify xs) (reify ys)
+    {-# INLINE reify #-}
+    reflect (Pair xs ys) = Pair (reflect xs) (reflect ys)
+    {-# INLINE reflect #-}
+
+instance (Alternative f, Alternative g) => Alternative (Product f g) where
+    empty = Pair empty empty
+    {-# INLINE empty #-}
+    Pair x1 y1 <|> Pair x2 y2 = Pair (x1 <|> x2) (y1 <|> y2)
+    {-# INLINE (<|>) #-}
+
+instance (Monad f, Monad g) => Monad (Product f g) where
+    Pair m n >>= f = Pair (m >>= fstP . f) (n >>= sndP . f)
+      where
+        fstP (Pair a _) = a
+        sndP (Pair _ b) = b
+    {-# INLINE (>>=) #-}
+
+instance (Functor f, Functor g) => Functor (Sum f g) where
+    type Suitable (Sum f g) a = (Suitable f a, Suitable g a)
+    fmap f (InL x) = InL (fmap f x)
+    fmap f (InR y) = InR (fmap f y)
+    {-# INLINE fmap #-}
diff --git a/src/Control/Monad/Constrained/Ap.hs b/src/Control/Monad/Constrained/Ap.hs
--- a/src/Control/Monad/Constrained/Ap.hs
+++ b/src/Control/Monad/Constrained/Ap.hs
@@ -1,37 +1,50 @@
-{-# LANGUAGE ConstraintKinds  #-}
-{-# LANGUAGE RankNTypes       #-}
-{-# LANGUAGE RebindableSyntax #-}
-{-# LANGUAGE TypeFamilies     #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DeriveFunctor         #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE RebindableSyntax      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE UndecidableInstances  #-}
 
 -- | This module allows the use of the Applicative Do extension with
 -- constrained monads.
 module Control.Monad.Constrained.Ap
   (Monad(..)
   ,MonadFail(..)
+  ,Codensity(..)
+  ,ConstrainedWrapper(..)
   ,return
   ,ifThenElse
-  ,(>>))
+  ,(>>)
+  ,Initial
+  ,Final
+  ,FreeApplicative(..)
+  ,module RestPrelude)
   where
 
-import           Control.Monad.Constrained        (Ap (..), liftAp, lower)
 import qualified Control.Monad.Constrained        as Constrained
 
 import           GHC.Exts
 
 import qualified Control.Monad
-import           Prelude                          hiding (Monad (..))
+import           Prelude                          as RestPrelude hiding
+                                                                  (Monad (..))
 import qualified Prelude
 
 import           Control.Monad.Trans.Cont         (ContT)
-import           Control.Monad.Trans.Except       (ExceptT(..))
+import           Control.Monad.Trans.Except       (ExceptT (..))
 import           Control.Monad.Trans.Identity     (IdentityT (..))
-import           Control.Monad.Trans.Maybe        (MaybeT(..))
+import           Control.Monad.Trans.Maybe        (MaybeT (..))
 import           Control.Monad.Trans.Reader       (ReaderT (..))
 import           Control.Monad.Trans.State        (StateT)
 import qualified Control.Monad.Trans.State.Strict as Strict (StateT)
 import           Data.Functor.Identity            (Identity)
 import           Data.Sequence                    (Seq)
 
+import qualified Control.Applicative.Free         as Initial
+import qualified Control.Applicative.Free.Final   as Final
+
 -- | This class is for types which have no constraints on their applicative
 -- operations, but /do/ have constraints on the monadic operations.
 --
@@ -76,30 +89,117 @@
   -- | Called when a pattern match fails in do-notation.
   fail :: Suitable f a => String -> f a
 
-instance Constrained.Monad f =>
-         Monad (Ap f) where
-    type Suitable (Ap f) a = Constrained.Suitable f a
-    (>>=) ap f = liftAp (lower ap Constrained.>>= (lower . f))
-    join = liftAp . go id . fmap lower
+instance (Constrained.Monad f) =>
+         Monad (Initial f) where
+    type Suitable (Initial f) a = Constrained.Suitable f a
+    (>>=) ap f = Initial.liftAp (retractAp ap Constrained.>>= (retractAp . f))
+    {-# INLINE (>>=) #-}
+    join = Initial.liftAp . go retractAp
       where
         go
             :: forall a f b.
                (Constrained.Suitable f b, Constrained.Monad f)
-            => (a -> f b) -> Ap f a -> f b
-        go c (Pure x) = c x
-        go f (Ap xs x) =
-            go
-                (\c ->
-                      x Constrained.>>= (f . c))
-                xs
+            => (a -> f b) -> Initial f a -> f b
+        go c (Initial.Pure x) = c x
+        go f (Initial.Ap x xs) = x Constrained.>>= \y -> go (\c -> (f . c) y) xs
+    {-# INLINE join #-}
+
+type Initial = Initial.Ap
+type Final = Final.Ap
+
+instance (Constrained.Monad f) =>
+         Monad (Final f) where
+    type Suitable (Final f) a = (Constrained.Suitable f a, Constrained.Suitable f (f a))
+    (>>=) ap f = Final.liftAp (retractAp ap Constrained.>>= retractAp . f)
+    {-# INLINE (>>=) #-}
+    join = Final.liftAp . Constrained.join . retractAp . fmap retractAp
+    {-# INLINE join #-}
+
+newtype Codensity f a = Codensity
+    { runCodensity :: forall b. Constrained.Suitable f b =>
+                                (a -> f b) -> f b
+    } deriving Functor
+
+instance Applicative (Codensity f) where
+  pure x = Codensity (\k -> k x)
+  {-# INLINE pure #-}
+  Codensity f <*> Codensity g = Codensity (\bfr -> f (\ab -> g (bfr . ab)))
+  {-# INLINE (<*>) #-}
+
+instance (Constrained.Monad f) => Monad (Codensity f) where
+  type Suitable (Codensity f) a = Constrained.Suitable f a
+  m >>= k = liftAp (retractAp m Constrained.>>= (retractAp . k))
+  {-# INLINE (>>=) #-}
+  join (Codensity xs) = Codensity (Constrained.=<< xs retractAp)
+  {-# INLINE join #-}
+
+class FreeApplicative ap f where
+  liftAp :: f a -> ap f a
+  retractAp :: (Constrained.Suitable f a) => ap f a -> f a
+
+newtype ConstrainedWrapper f a
+  = ConstrainedWrapper
+  { unwrapConstrained :: Constrained.Unconstrained f a }
+
+instance Constrained.Applicative f => FreeApplicative ConstrainedWrapper f where
+  liftAp = ConstrainedWrapper . Constrained.reflect
+  {-# INLINE liftAp #-}
+  retractAp (ConstrainedWrapper xs) = Constrained.reify xs
+  {-# INLINE retractAp #-}
+
+instance Constrained.Applicative f =>
+         Functor (ConstrainedWrapper f) where
+    fmap f (ConstrainedWrapper xs) = ConstrainedWrapper (fmap f xs)
+    {-# INLINE fmap #-}
+
+instance Constrained.Applicative f =>
+         Applicative (ConstrainedWrapper f) where
+    pure = ConstrainedWrapper . pure
+    ConstrainedWrapper fs <*> ConstrainedWrapper xs =
+        ConstrainedWrapper (fs <*> xs)
+    {-# INLINE pure #-}
+    {-# INLINE (<*>) #-}
+
+instance Constrained.Monad f =>
+         Monad (ConstrainedWrapper f) where
+    type Suitable (ConstrainedWrapper f) a
+        = (Constrained.Suitable f a, Constrained.Suitable f (f a))
+    ConstrainedWrapper xs >>= f =
+        liftAp (Constrained.reify xs Constrained.>>= (retractAp . f))
+    {-# INLINE (>>=) #-}
+    join =
+        liftAp .
+        Constrained.join . retractAp . fmap retractAp
+    {-# INLINE join #-}
+
+instance Constrained.Applicative f => FreeApplicative Final f where
+  liftAp = Final.liftAp
+  {-# INLINE liftAp #-}
+  retractAp = Constrained.reify . Final.runAp Constrained.reflect
+  {-# INLINE retractAp #-}
+
+instance Constrained.Applicative f => FreeApplicative Initial f where
+  liftAp = Initial.liftAp
+  {-# INLINE liftAp #-}
+  retractAp = Constrained.reify . Initial.runAp Constrained.reflect
+  {-# INLINE retractAp #-}
+
+instance Constrained.Monad f => FreeApplicative Codensity f where
+  liftAp xs = Codensity (xs Constrained.>>=)
+  {-# INLINE liftAp #-}
+  retractAp (Codensity fs) = fs Constrained.pure
+  {-# INLINE retractAp #-}
+
 -- | An alias for 'pure'
 return :: Applicative f => a -> f a
 return = pure
+{-# INLINE return #-}
 
 -- | Function to which the @if ... then ... else@ syntax desugars to
 ifThenElse :: Bool -> a -> a -> a
-ifThenElse True t _ = t
+ifThenElse True t _  = t
 ifThenElse False _ f = f
+{-# INLINE ifThenElse #-}
 
 infixl 1 >>
 -- | Sequence two actions, discarding the result of the first. Alias for
@@ -108,30 +208,40 @@
     :: Applicative f
     => f a -> f b -> f b
 (>>) = (*>)
+{-# INLINE (>>) #-}
 
 instance Monad [] where
     type Suitable [] a = ()
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
     join = Control.Monad.join
+    {-# INLINE join #-}
 
 instance MonadFail [] where
     fail _ = []
+    {-# INLINE fail #-}
 
 instance Monad Maybe where
     type Suitable Maybe a = ()
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
     join = Control.Monad.join
+    {-# INLINE join #-}
 
 instance MonadFail Maybe where
     fail _ = Nothing
+    {-# INLINE fail #-}
 
 instance Monad IO where
     type Suitable IO a = ()
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
     join = Control.Monad.join
+    {-# INLINE join #-}
 
 instance MonadFail IO where
     fail = Prelude.fail
+    {-# INLINE fail #-}
 
 instance Monad Identity where
     type Suitable Identity a = ()
@@ -141,47 +251,63 @@
 instance Monad (Either e) where
     type Suitable (Either e) a = ()
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
     join = Control.Monad.join
+    {-# INLINE join #-}
 
 instance IsString a =>
          MonadFail (Either a) where
     fail = Left . fromString
+    {-# INLINE fail #-}
 
 instance Monoid m =>
          Monad ((,) m) where
     type Suitable ((,) m) a = ()
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
     join = Control.Monad.join
+    {-# INLINE join #-}
 
 instance Monad Seq where
     type Suitable Seq a = ()
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
     join = Control.Monad.join
+    {-# INLINE join #-}
 
 instance MonadFail Seq where
     fail _ = Constrained.empty
+    {-# INLINE fail #-}
 
 instance Monad ((->) b) where
     type Suitable ((->) b) a = ()
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
     join = Control.Monad.join
+    {-# INLINE join #-}
 
 instance Monad (ContT r m) where
     type Suitable (ContT r m) a = ()
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
     join = Control.Monad.join
+    {-# INLINE join #-}
 
 instance Prelude.Monad m =>
          Monad (Strict.StateT s m) where
     type Suitable (Strict.StateT s m) a = ()
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
     join = Control.Monad.join
+    {-# INLINE join #-}
 
 instance Prelude.Monad m =>
          Monad (StateT s m) where
     type Suitable (StateT s m) a = ()
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
     join = Control.Monad.join
+    {-# INLINE join #-}
 
 instance Monad m =>
          Monad (ReaderT s m) where
@@ -201,34 +327,46 @@
 instance MonadFail m =>
          MonadFail (ReaderT r m) where
     fail = ReaderT . const . fail
+    {-# INLINE fail #-}
 
 instance Prelude.Monad m =>
          Monad (MaybeT m) where
     type Suitable (MaybeT m) a = ()
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
     join = Control.Monad.join
+    {-# INLINE join #-}
 
 instance Prelude.Monad m =>
          MonadFail (MaybeT m) where
     fail _ = Control.Monad.mzero
+    {-# INLINE fail #-}
 
 instance Prelude.Monad m =>
          Monad (ExceptT e m) where
     type Suitable (ExceptT e m) a = ()
     (>>=) = (Prelude.>>=)
+    {-# INLINE (>>=) #-}
     join = Control.Monad.join
+    {-# INLINE join #-}
 
 instance (Prelude.Monad m, IsString e) => MonadFail (ExceptT e m) where
     fail = ExceptT . pure . Left . fromString
+    {-# INLINE fail #-}
 
 instance Monad m =>
          Monad (IdentityT m) where
     type Suitable (IdentityT m) a = Suitable m a
     (>>=) =
-        (coerce :: (f a -> (a -> f b) -> f b) -> IdentityT f a -> (a -> IdentityT f b) -> IdentityT f b)
+        (coerce
+           :: (f a -> (a -> f b) -> f b)
+           -> IdentityT f a -> (a -> IdentityT f b) -> IdentityT f b)
             (>>=)
+    {-# INLINE (>>=) #-}
     join (IdentityT x) = IdentityT (join (fmap runIdentityT x))
+    {-# INLINE join #-}
 
 instance MonadFail m =>
          MonadFail (IdentityT m) where
     fail = IdentityT . fail
+    {-# INLINE fail #-}
diff --git a/src/Control/Monad/Constrained/Cont.hs b/src/Control/Monad/Constrained/Cont.hs
--- a/src/Control/Monad/Constrained/Cont.hs
+++ b/src/Control/Monad/Constrained/Cont.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE RebindableSyntax     #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 -- | This module is a duplication of the Control.Monad.Cont module, from the\
 -- mtl.
@@ -12,18 +14,20 @@
   ,mapCont
   ,withCont)where
 
-import Control.Monad.Constrained
+import           Control.Monad.Constrained
 
-import qualified Control.Monad.Trans.Cont as Cont
-import           Control.Monad.Trans.Cont hiding (callCC)
+import           Control.Monad.Trans.Cont         hiding (callCC)
+import qualified Control.Monad.Trans.Cont         as Cont
 
+import qualified Control.Monad.Trans.Except       as Except
+import qualified Control.Monad.Trans.Identity     as Identity
+import qualified Control.Monad.Trans.Maybe        as Maybe
 import qualified Control.Monad.Trans.Reader       as Reader
 import qualified Control.Monad.Trans.State.Lazy   as State.Lazy
 import qualified Control.Monad.Trans.State.Strict as State.Strict
-import qualified Control.Monad.Trans.Identity     as Identity
-import qualified Control.Monad.Trans.Maybe        as Maybe
-import qualified Control.Monad.Trans.Except       as Except
 
+import qualified Prelude
+
 -- | A class for monads which can embed continuations.
 class Monad m => MonadCont m where
     {- | @callCC@ (call-with-current-continuation)
@@ -49,20 +53,24 @@
 instance MonadCont (ContT r m) where
     callCC = Cont.callCC
 
-instance MonadCont m => MonadCont (Maybe.MaybeT m) where
+instance (MonadCont m, Prelude.Monad (Unconstrained m)) =>
+         MonadCont (Maybe.MaybeT m) where
     callCC = Maybe.liftCallCC callCC
 
 instance MonadCont m => MonadCont (Reader.ReaderT r m) where
     callCC = Reader.liftCallCC callCC
 
-instance MonadCont m => MonadCont (State.Lazy.StateT s m) where
+instance (MonadCont m, Prelude.Monad (Unconstrained m)) =>
+         MonadCont (State.Lazy.StateT s m) where
     callCC = State.Lazy.liftCallCC callCC
 
-instance MonadCont m => MonadCont (State.Strict.StateT s m) where
+instance (MonadCont m, Prelude.Monad (Unconstrained m)) =>
+         MonadCont (State.Strict.StateT s m) where
     callCC = State.Strict.liftCallCC callCC
 
 instance MonadCont m => MonadCont (Identity.IdentityT m) where
     callCC = Identity.liftCallCC callCC
 
-instance MonadCont m => MonadCont (Except.ExceptT e m) where
+instance (MonadCont m, Prelude.Monad (Unconstrained m)) =>
+         MonadCont (Except.ExceptT e m) where
     callCC = Except.liftCallCC callCC
diff --git a/src/Control/Monad/Constrained/Error.hs b/src/Control/Monad/Constrained/Error.hs
--- a/src/Control/Monad/Constrained/Error.hs
+++ b/src/Control/Monad/Constrained/Error.hs
@@ -26,6 +26,8 @@
 import qualified Control.Monad.Trans.State.Lazy   as State.Lazy
 import qualified Control.Monad.Trans.State.Strict as State.Strict
 
+import qualified Prelude
+
 -- | A class for monads which can error out.
 class Monad m =>
       MonadError e m  | m -> e where
@@ -49,7 +51,7 @@
     catchError (Left x) f = f x
     catchError r _ = r
 
-instance Monad m => MonadError e (ExceptT e m) where
+instance (Monad m, Prelude.Monad (Unconstrained m)) => MonadError e (ExceptT e m) where
     type SuitableError (ExceptT e m) a = Suitable m (Either e a)
     throwError = ExceptT . pure . Left
     catchError = catchE
@@ -72,7 +74,7 @@
     throwError = lift . throwError
     catchError = Identity.liftCatch catchError
 
-instance MonadError e m =>
+instance (MonadError e m, Prelude.Monad (Unconstrained m)) =>
          MonadError e (Maybe.MaybeT m) where
     type SuitableError (Maybe.MaybeT m) a
         = (SuitableError m a
@@ -87,14 +89,16 @@
     throwError = lift . throwError
     catchError = Reader.liftCatch catchError
 
-instance MonadError e m => MonadError e (State.Lazy.StateT s m) where
+instance (MonadError e m, Prelude.Monad (Unconstrained m)) =>
+         MonadError e (State.Lazy.StateT s m) where
     type SuitableError (State.Lazy.StateT s m) a
-        = (Suitable m (a,s), SuitableError m (a,s), SuitableError m a)
+        = (Suitable m (a, s), SuitableError m (a, s), SuitableError m a)
     throwError = lift . throwError
     catchError = State.Lazy.liftCatch catchError
 
-instance MonadError e m => MonadError e (State.Strict.StateT s m) where
+instance (MonadError e m, Prelude.Monad (Unconstrained m)) =>
+         MonadError e (State.Strict.StateT s m) where
     type SuitableError (State.Strict.StateT s m) a
-        = (Suitable m (a,s), SuitableError m (a,s), SuitableError m a)
+        = (Suitable m (a, s), SuitableError m (a, s), SuitableError m a)
     throwError = lift . throwError
     catchError = State.Strict.liftCatch catchError
diff --git a/src/Control/Monad/Constrained/IO.hs b/src/Control/Monad/Constrained/IO.hs
--- a/src/Control/Monad/Constrained/IO.hs
+++ b/src/Control/Monad/Constrained/IO.hs
@@ -20,6 +20,8 @@
 
 import           GHC.Exts
 
+import qualified Prelude
+
 -- | A class for monads which can have IO actions lifted into them.
 class Monad m =>
       MonadIO m  where
@@ -35,7 +37,7 @@
     type SuitableIO (IdentityT m) a = SuitableIO m a
     liftIO = lift . liftIO
 
-instance MonadIO m =>
+instance (MonadIO m, Prelude.Monad (Unconstrained m)) =>
          MonadIO (MaybeT m) where
     type SuitableIO (MaybeT m) a = (Suitable m (Maybe a), SuitableIO m a)
     liftIO = lift . liftIO
@@ -50,12 +52,12 @@
     type SuitableIO (ReaderT r m) a = SuitableIO m a
     liftIO = lift . liftIO
 
-instance MonadIO m =>
+instance (MonadIO m, Prelude.Monad (Unconstrained m)) =>
          MonadIO (StateT s m) where
     type SuitableIO (StateT s m) a = (SuitableIO m a, Suitable m (a, s))
     liftIO = lift . liftIO
 
-instance MonadIO m =>
+instance (MonadIO m, Prelude.Monad (Unconstrained m)) =>
          MonadIO (Lazy.StateT s m) where
     type SuitableIO (Lazy.StateT s m) a = (SuitableIO m a, Suitable m (a, s))
     liftIO = lift . liftIO
diff --git a/src/Control/Monad/Constrained/IntSet.hs b/src/Control/Monad/Constrained/IntSet.hs
--- a/src/Control/Monad/Constrained/IntSet.hs
+++ b/src/Control/Monad/Constrained/IntSet.hs
@@ -1,95 +1,157 @@
-{-# LANGUAGE GADTs             #-}
-{-# LANGUAGE RebindableSyntax  #-}
-{-# LANGUAGE TypeFamilies      #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE GADTs              #-}
+{-# LANGUAGE RebindableSyntax   #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies       #-}
 
 -- | This module creates an 'IntSet' type with a phantom type variable, allowing
 -- it to conform to 'Functor', 'Foldable', etc. Other than that, it's a
 -- duplication of the "Data.IntSet" module.
 module Control.Monad.Constrained.IntSet
-  (IntSet
+  ( -- * IntSet type
+    IntSet
+    -- * Operators
   ,(\\)
+    -- * Query
   ,lookupLT
   ,lookupLE
   ,lookupGT
   ,lookupGE
+  ,isSubsetOf
+  ,isProperSubsetOf
+   -- * Construction
   ,insert
   ,delete
+   -- * Combine
   ,difference
   ,intersection
+   -- * Filter
   ,filter
   ,partition
   ,split
+  ,splitMember
+  ,splitRoot
+  -- * Min/Max
   ,maxView
-  ,minView)
+  ,minView
+  ,deleteMin
+  ,deleteMax
+  -- * Ordered List
+  ,toAscList
+  ,toDescList
+  ,fromAscList
+  ,fromDistinctAscList)
   where
 
-import           Control.Monad.Constrained hiding (filter)
+import           Control.Monad.Constrained                        hiding
+                                                                   (filter)
 
-import qualified Data.IntSet               as IntSet
+import qualified Data.IntSet                                      as IntSet
 
-import           Data.Foldable             (Foldable (..))
+import           Data.Foldable                                    (Foldable (..))
 import           Data.Functor.Classes
 import           Data.Semigroup
 
-import           Control.Arrow             (first)
+import           Control.Arrow                                    (first)
 import           GHC.Exts
 
+import           Control.Monad.Constrained.Internal.Unconstrained
+
+import           Data.Data                                        (Data)
+import           Data.Typeable                                    (Typeable)
+
+import           Control.DeepSeq                                  (NFData (..))
+
 -- | This type is a wrapper around 'Data.IntSet.IntSet', with a phantom type
 -- variable which must always be 'Int'. This allows it to conform to 'Functor',
 -- 'Foldable', 'Applicative', 'Monad', etc.
 data IntSet a where
-        IntSet :: IntSet.IntSet -> IntSet Int
+        IntSet :: !IntSet.IntSet -> IntSet Int
 
+deriving instance Typeable (IntSet a)
+deriving instance a ~ Int => Data (IntSet a)
+
+instance NFData (IntSet a) where
+    rnf (IntSet xs) = rnf xs
+
 instance Foldable IntSet where
     foldr f b (IntSet xs) = IntSet.foldr f b xs
+    {-# INLINE foldr #-}
     foldl f b (IntSet xs) = IntSet.foldl f b xs
+    {-# INLINE foldl #-}
     foldr' f b (IntSet xs) = IntSet.foldr' f b xs
+    {-# INLINE foldr' #-}
     foldl' f b (IntSet xs) = IntSet.foldl' f b xs
+    {-# INLINE foldl' #-}
     null (IntSet xs) = IntSet.null xs
+    {-# INLINE null #-}
     length (IntSet xs) = IntSet.size xs
+    {-# INLINE length #-}
     minimum (IntSet xs) = IntSet.findMin xs
+    {-# INLINE minimum #-}
     maximum (IntSet xs) = IntSet.findMax xs
+    {-# INLINE maximum #-}
     elem x (IntSet xs) = IntSet.member x xs
+    {-# INLINE elem #-}
 
 instance Functor IntSet where
     type Suitable IntSet a = a ~ Int
     fmap f (IntSet xs) = IntSet (IntSet.map f xs)
+    {-# INLINE fmap #-}
     x <$ IntSet xs =
         IntSet
             (if IntSet.null xs
                  then IntSet.empty
                  else IntSet.singleton x)
+    {-# INLINE (<$) #-}
 
 instance Semigroup (IntSet a) where
     IntSet xs <> IntSet ys = IntSet (IntSet.union xs ys)
+    {-# INLINE (<>) #-}
 
 instance a ~ Int => Monoid (IntSet a) where
     mempty = IntSet IntSet.empty
+    {-# INLINE mempty #-}
     mappend = (<>)
+    {-# INLINE mappend #-}
 
 instance Applicative IntSet where
+    type Unconstrained IntSet = StrictLeftFold
     pure x = IntSet (IntSet.singleton x)
+    {-# INLINE pure #-}
     xs *> ys =
         if null xs
             then mempty
             else ys
+    {-# INLINE (*>) #-}
     xs <* ys =
         if null ys
             then mempty
             else xs
-    lower = lowerM
+    {-# INLINE (<*) #-}
+    reify (StrictLeftFold xs) = IntSet (xs (flip IntSet.insert) IntSet.empty)
+    {-# INLINE reify #-}
+    reflect (IntSet xs) = StrictLeftFold (\f b -> IntSet.foldl' f b xs)
+    {-# INLINE reflect #-}
 
+
 instance Alternative IntSet where
     empty = mempty
+    {-# INLINE empty #-}
     (<|>) = mappend
+    {-# INLINE (<|>) #-}
 
 instance Monad IntSet where
     (>>=) = flip foldMap
+    {-# INLINE (>>=) #-}
 
-instance a ~ Int => IsList (IntSet a) where
-  type Item (IntSet a) = a
-  fromList = IntSet . IntSet.fromList
-  toList = foldr (:) []
+instance a ~ Int =>
+         IsList (IntSet a) where
+    type Item (IntSet a) = a
+    fromList = IntSet . IntSet.fromList
+    {-# INLINE fromList #-}
+    toList = foldr (:) []
+    {-# INLINE toList #-}
 
 infixl 9 \\
 -- | /O(n+m)/. See 'difference'.
@@ -102,6 +164,7 @@
 -- > lookupLT 5 (fromList [3, 5]) == Just 3
 lookupLT :: a -> IntSet a -> Maybe a
 lookupLT x (IntSet xs) = IntSet.lookupLT x xs
+{-# INLINE lookupLT #-}
 
 -- | /O(log n)/. Find smallest element greater than the given one.
 --
@@ -109,6 +172,7 @@
 -- > lookupGT 5 (fromList [3, 5]) == Nothing
 lookupGT :: a -> IntSet a -> Maybe a
 lookupGT x (IntSet xs) = IntSet.lookupGT x xs
+{-# INLINE lookupGT #-}
 
 -- | /O(log n)/. Find largest element smaller or equal to the given one.
 --
@@ -117,6 +181,7 @@
 -- > lookupLE 5 (fromList [3, 5]) == Just 5
 lookupLE :: a -> IntSet a -> Maybe a
 lookupLE x (IntSet xs) = IntSet.lookupLE x xs
+{-# INLINE lookupLE #-}
 
 -- | /O(log n)/. Find smallest element greater or equal to the given one.
 --
@@ -125,34 +190,41 @@
 -- > lookupGE 6 (fromList [3, 5]) == Nothing
 lookupGE :: a -> IntSet a -> Maybe a
 lookupGE x (IntSet xs) = IntSet.lookupGE x xs
+{-# INLINE lookupGE #-}
 
 -- | /O(min(n,W))/. Add a value to the set. There is no left- or right bias for
 -- IntSets.
 insert :: a -> IntSet a -> IntSet a
 insert x (IntSet xs) = IntSet (IntSet.insert x xs)
+{-# INLINE insert #-}
 
 -- | /O(min(n,W))/. Delete a value in the set. Returns the
 -- original set when the value was not present.
 delete :: a -> IntSet a -> IntSet a
 delete x (IntSet xs) = IntSet (IntSet.delete x xs)
+{-# INLINE delete #-}
 
 -- | /O(n+m)/. Difference between two sets.
 difference :: IntSet a -> IntSet a -> IntSet a
 difference (IntSet xs) (IntSet ys) = IntSet (IntSet.difference xs ys)
+{-# INLINE difference #-}
 
 -- | /O(n+m)/. The intersection of two sets.
 intersection :: IntSet a -> IntSet a -> IntSet a
 intersection (IntSet xs) (IntSet ys) = IntSet (IntSet.intersection xs ys)
+{-# INLINE intersection #-}
 
 -- | /O(n)/. Filter all elements that satisfy some predicate.
 filter :: (a -> Bool) -> IntSet a -> IntSet a
 filter p (IntSet xs) = IntSet (IntSet.filter p xs)
+{-# INLINE filter #-}
 
 -- | /O(n)/. partition the set according to some predicate.
 partition :: (a -> Bool) -> IntSet a -> (IntSet a, IntSet a)
 partition p (IntSet xs) =
     let (ys,zs) = IntSet.partition p xs
     in (IntSet ys, IntSet zs)
+{-# INLINE partition #-}
 
 -- | /O(min(n,W))/. The expression (@'split' x set@) is a pair @(set1,set2)@
 -- where @set1@ comprises the elements of @set@ less than @x@ and @set2@
@@ -163,38 +235,90 @@
 split x (IntSet xs) =
     let (ys,zs) = IntSet.split x xs
     in (IntSet ys, IntSet zs)
+{-# INLINE split #-}
 
 -- | /O(min(n,W))/. Retrieves the maximal key of the set, and the set
 -- stripped of that element, or 'Nothing' if passed an empty set.
 maxView :: IntSet a -> Maybe (a, IntSet a)
 maxView (IntSet xs) = (fmap.fmap) IntSet (IntSet.maxView xs)
+{-# INLINE maxView #-}
 
 -- | /O(min(n,W))/. Retrieves the minimal key of the set, and the set
 -- stripped of that element, or 'Nothing' if passed an empty set.
 minView :: IntSet a -> Maybe (a, IntSet a)
 minView (IntSet xs) = (fmap.fmap) IntSet (IntSet.minView xs)
+{-# INLINE minView #-}
 
 instance Show1 IntSet where
     liftShowsPrec _ _ d (IntSet xs) = showsPrec d xs
+    {-# INLINE liftShowsPrec #-}
 
 instance Show a =>
          Show (IntSet a) where
     showsPrec = showsPrec1
+    {-# INLINE showsPrec #-}
 
 instance a ~ Int =>
          Read (IntSet a) where
     readsPrec n = (fmap . first) IntSet . readsPrec n
+    {-# INLINE readsPrec #-}
 
 instance Eq1 IntSet where
     liftEq _ (IntSet xs) (IntSet ys) = xs == ys
+    {-# INLINE liftEq #-}
 
 instance Eq a =>
          Eq (IntSet a) where
     (==) = eq1
+    {-# INLINE (==) #-}
 
 instance Ord1 IntSet where
     liftCompare _ (IntSet xs) (IntSet ys) = compare xs ys
+    {-# INLINE liftCompare #-}
 
 instance Ord a =>
          Ord (IntSet a) where
     compare = compare1
+    {-# INLINE compare #-}
+
+isSubsetOf :: IntSet a -> IntSet a -> Bool
+isSubsetOf (IntSet xs) (IntSet ys) = IntSet.isSubsetOf xs ys
+{-# INLINE isSubsetOf #-}
+
+isProperSubsetOf :: IntSet a -> IntSet a -> Bool
+isProperSubsetOf (IntSet xs) (IntSet ys) = IntSet.isProperSubsetOf xs ys
+{-# INLINE isProperSubsetOf #-}
+
+splitMember :: a -> IntSet a -> (IntSet a, Bool, IntSet a)
+splitMember x (IntSet xs) =
+    let (ys,m,zs) = IntSet.splitMember x xs
+    in (IntSet ys, m, IntSet zs)
+{-# INLINE splitMember #-}
+
+splitRoot :: IntSet a -> [IntSet a]
+splitRoot (IntSet xs) = fmap IntSet (IntSet.splitRoot xs)
+{-# INLINE splitRoot #-}
+
+deleteMin :: IntSet a -> IntSet a
+deleteMin (IntSet xs) = IntSet (IntSet.deleteMin xs)
+{-# INLINE deleteMin #-}
+
+deleteMax :: IntSet a -> IntSet a
+deleteMax (IntSet xs) = IntSet (IntSet.deleteMax xs)
+{-# INLINE deleteMax #-}
+
+toAscList :: IntSet a -> [a]
+toAscList (IntSet xs) = IntSet.toAscList xs
+{-# INLINE toAscList #-}
+
+toDescList :: IntSet a -> [a]
+toDescList (IntSet xs) = IntSet.toAscList xs
+{-# INLINE toDescList #-}
+
+fromAscList :: [Int] -> IntSet Int
+fromAscList  = IntSet . IntSet.fromAscList
+{-# INLINE fromAscList #-}
+
+fromDistinctAscList :: [Int] -> IntSet Int
+fromDistinctAscList = IntSet . IntSet.fromDistinctAscList
+{-# INLINE fromDistinctAscList #-}
diff --git a/src/Control/Monad/Constrained/Internal/Unconstrained.hs b/src/Control/Monad/Constrained/Internal/Unconstrained.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Constrained/Internal/Unconstrained.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE RankNTypes   #-}
+{-# LANGUAGE BangPatterns #-}
+
+module Control.Monad.Constrained.Internal.Unconstrained where
+
+newtype StrictLeftFold a
+  = StrictLeftFold (forall b. (b -> a -> b) -> b -> b)
+
+instance Functor StrictLeftFold where
+    fmap f (StrictLeftFold xs) = StrictLeftFold (\c -> xs (\ !a -> c a . f))
+    {-# INLINE fmap #-}
+
+instance Applicative StrictLeftFold where
+    pure x =
+        StrictLeftFold (\c b -> c b x)
+    {-# INLINE pure #-}
+    StrictLeftFold fs <*> StrictLeftFold xs =
+      StrictLeftFold (\c -> fs (\ !fb f -> xs (\ !xb -> c xb . f) fb))
+    {-# INLINE (<*>) #-}
diff --git a/src/Control/Monad/Constrained/Reader.hs b/src/Control/Monad/Constrained/Reader.hs
--- a/src/Control/Monad/Constrained/Reader.hs
+++ b/src/Control/Monad/Constrained/Reader.hs
@@ -27,6 +27,8 @@
 import qualified Control.Monad.Trans.Maybe        as Maybe
 import qualified Control.Monad.Trans.Except       as Except
 
+import qualified Prelude
+
 -- | A class for reader monads.
 class Monad m =>
       MonadReader r m  | m -> r where
@@ -83,11 +85,10 @@
         r <- ask'
         local' f (Cont.runContT m (local' (const r) . c))
 
-instance MonadReader r m => MonadReader r (Except.ExceptT e m) where
+instance (MonadReader r m, Prelude.Monad (Unconstrained m)) =>
+         MonadReader r (Except.ExceptT e m) where
     type ReaderSuitable (Except.ExceptT e m) a
-        = (ReaderSuitable m a
-          ,Suitable m (Either e a)
-          ,ReaderSuitable m (Either e a))
+        = (ReaderSuitable m a, Suitable m (Either e a), ReaderSuitable m (Either e a))
     ask = lift ask
     local = Except.mapExceptT . local
     reader = lift . reader
@@ -98,7 +99,7 @@
     local = Identity.mapIdentityT . local
     reader = lift . reader
 
-instance MonadReader r m =>
+instance (MonadReader r m, Prelude.Monad (Unconstrained m)) =>
          MonadReader r (Maybe.MaybeT m) where
     type ReaderSuitable (Maybe.MaybeT m) a
         = (ReaderSuitable m a
@@ -108,7 +109,7 @@
     local = Maybe.mapMaybeT . local
     reader = lift . reader
 
-instance MonadReader r m =>
+instance (MonadReader r m, Prelude.Monad (Unconstrained m)) =>
          MonadReader r (State.Lazy.StateT s m) where
     type ReaderSuitable (State.Lazy.StateT s m) a
         = (ReaderSuitable m a
@@ -118,7 +119,7 @@
     local = State.Lazy.mapStateT . local
     reader = lift . reader
 
-instance MonadReader r m =>
+instance (MonadReader r m, Prelude.Monad (Unconstrained m)) =>
          MonadReader r (State.Strict.StateT s m) where
     type ReaderSuitable (State.Strict.StateT s m) a
         = (ReaderSuitable m a
diff --git a/src/Control/Monad/Constrained/State.hs b/src/Control/Monad/Constrained/State.hs
--- a/src/Control/Monad/Constrained/State.hs
+++ b/src/Control/Monad/Constrained/State.hs
@@ -31,6 +31,8 @@
 import qualified Control.Monad.Trans.Reader       as Reader
 import qualified Control.Monad.Trans.Except       as Except
 
+import qualified Prelude
+
 -- | A class for monads with state.
 class Monad m =>
       MonadState s m  | m -> s where
@@ -79,19 +81,21 @@
               let s' = f s
               in s' `seq` ((), s'))
 
-instance Monad m => MonadState s (StateT s m) where
-  type StateSuitable (StateT s m) a = Suitable m (a, s)
-  state f = StateT (pure . f)
+instance (Monad m, Prelude.Monad (Unconstrained m)) =>
+         MonadState s (StateT s m) where
+    type StateSuitable (StateT s m) a = Suitable m (a, s)
+    state f = StateT (pure . f)
 
-instance Monad m => MonadState s (State.Lazy.StateT s m) where
-  type StateSuitable (State.Lazy.StateT s m) a = Suitable m (a, s)
-  state f = State.Lazy.StateT (pure . f)
+instance (Monad m, Prelude.Monad (Unconstrained m)) =>
+         MonadState s (State.Lazy.StateT s m) where
+    type StateSuitable (State.Lazy.StateT s m) a = Suitable m (a, s)
+    state f = State.Lazy.StateT (pure . f)
 
 instance (MonadState s m, Suitable m r) => MonadState s (Cont.ContT r m) where
     type StateSuitable (Cont.ContT r m) a = StateSuitable m a
     state = lift . state
 
-instance MonadState s m =>
+instance (MonadState s m, Prelude.Monad (Unconstrained m)) =>
          MonadState s (Maybe.MaybeT m) where
     type StateSuitable (Maybe.MaybeT m) a
         = (Suitable m (Maybe a), StateSuitable m a)
@@ -107,7 +111,7 @@
     type StateSuitable (Reader.ReaderT r m) a = StateSuitable m a
     state = lift . state
 
-instance MonadState s m =>
+instance (MonadState s m, Prelude.Monad (Unconstrained m)) =>
          MonadState s (Except.ExceptT e m) where
     type StateSuitable (Except.ExceptT e m) a
         = (Suitable m (Either e a), StateSuitable m a)
diff --git a/src/Control/Monad/Constrained/Writer.hs b/src/Control/Monad/Constrained/Writer.hs
--- a/src/Control/Monad/Constrained/Writer.hs
+++ b/src/Control/Monad/Constrained/Writer.hs
@@ -45,6 +45,11 @@
 import           Data.Functor.Identity
 import           Data.Functor.Classes
 
+import qualified Prelude
+
+import           Control.Applicative.Free hiding (liftAp)
+import qualified Control.Applicative.Free as Free
+
 -- | A class for monads with logging ability.
 class (Monoid w, Monad m) => MonadWriter w m | m -> w where
     type WriterSuitable m a :: Constraint
@@ -61,7 +66,7 @@
     -- easier to manage.
     passC   :: WriterSuitable m a => (a -> w -> w) -> m a -> m a
 
-instance MonadWriter w m =>
+instance (MonadWriter w m, Prelude.Monad (Unconstrained m)) =>
          MonadWriter w (Except.ExceptT e m) where
     type WriterSuitable (Except.ExceptT e m) a
         = (WriterSuitable m a
@@ -87,7 +92,7 @@
     => m (a, w -> w) -> m a
 pass = fmap fst . passC snd
 
-instance MonadWriter w m =>
+instance (MonadWriter w m, Prelude.Monad (Unconstrained m)) =>
          MonadWriter w (State.Lazy.StateT s m) where
     type WriterSuitable (State.Lazy.StateT s m) a
         = (WriterSuitable m a
@@ -103,7 +108,7 @@
              State.Lazy.runStateT m)
     passC c m = State.Lazy.StateT (passC (c . fst) . State.Lazy.runStateT m)
 
-instance MonadWriter w m =>
+instance (MonadWriter w m, Prelude.Monad (Unconstrained m)) =>
          MonadWriter w (State.Strict.StateT s m) where
     type WriterSuitable (State.Strict.StateT s m) a
         = (WriterSuitable m a
@@ -127,11 +132,10 @@
     listenC f = Identity.mapIdentityT (listenC f)
     passC f = Identity.mapIdentityT (passC f)
 
-instance MonadWriter w m => MonadWriter w (Maybe.MaybeT m) where
+instance (MonadWriter w m, Prelude.Monad (Unconstrained m)) =>
+         MonadWriter w (Maybe.MaybeT m) where
     type WriterSuitable (Maybe.MaybeT m) a
-        = (WriterSuitable m a
-          ,WriterSuitable m (Maybe a)
-          ,Suitable m (Maybe a))
+        = (WriterSuitable m a, WriterSuitable m (Maybe a), Suitable m (Maybe a))
     writer = lift . writer
     tell = lift . tell
     listenC f = (Maybe.mapMaybeT . listenC . flip) (fmap . flip f)
@@ -160,16 +164,20 @@
   fmap f (WriterT_ x) = WriterT_ (fmap f x)
   x <$ WriterT_ xs = WriterT_ (x <$ xs)
 
-instance Monad m =>
+
+instance (Monad m, Prelude.Monad (Unconstrained m)) =>
          Applicative (WriterT s m) where
+    type Unconstrained (WriterT s m) = Ap (WriterT s m)
     pure x = WriterT_ (pure x)
     WriterT_ fs <*> WriterT_ xs = WriterT_ (fs <*> xs)
     WriterT_ xs *> WriterT_ ys = WriterT_ (xs *> ys)
     WriterT_ xs <* WriterT_ ys = WriterT_ (xs <* ys)
-    lower = lowerM
+    reify = ap (WriterT_ . pure)
+    reflect = Free.liftAp
 
-instance Monad m => Monad (WriterT s m) where
-  WriterT_ xs >>= f = WriterT_ (xs >>= (unWriterT . f))
+instance (Monad m, Prelude.Monad (Unconstrained m)) =>
+         Monad (WriterT s m) where
+    WriterT_ xs >>= f = WriterT_ (xs >>= (unWriterT . f))
 
 -- first_  :: (Functor f, Suitable f (b, c)) => (a -> f b) -> (a, c) -> f (b, c)
 -- first_  f (x,y) = fmap (flip (,) y) (f x)
@@ -216,7 +224,7 @@
 
 {-# INLINE runWriter #-}
 
-instance (Monoid s, Monad m) =>
+instance (Monoid s, Monad m, Prelude.Monad (Unconstrained m)) =>
          MonadWriter s (WriterT s m) where
     type WriterSuitable (WriterT s m) a = Suitable m (a, s)
     tell s = WriterT (pure ((), s))
@@ -242,21 +250,21 @@
   type SuitableLift (WriterT w) m a = Suitable m (a, w)
   lift xs = WriterT_ . State.Strict.StateT $ (\s -> fmap (flip (,) s) xs)
 
-instance MonadState s m =>
+instance (MonadState s m, Prelude.Monad (Unconstrained m)) =>
          MonadState s (WriterT w m) where
     type StateSuitable (WriterT w m) a = (StateSuitable m a, Suitable m (a, w))
     get = lift get
     put = lift . put
     state = lift . state
 
-instance MonadError e m =>
+instance (MonadError e m, Prelude.Monad (Unconstrained m)) =>
          MonadError e (WriterT w m) where
     type SuitableError (WriterT w m) a = SuitableError m (a, w)
     throwError e = WriterT_ . State.Strict.StateT $ const (throwError e)
     catchError (WriterT_ xs) f =
         WriterT_ (State.Strict.liftCatch catchError xs (unWriterT . f))
 
-instance MonadReader r m =>
+instance (MonadReader r m, Prelude.Monad (Unconstrained m)) =>
          MonadReader r (WriterT w m) where
     type ReaderSuitable (WriterT w m) a
         = (ReaderSuitable m a
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -28,12 +28,12 @@
 import           Data.Functor.Identity
 
 instance Functor Gen where
-  type Suitable Gen a = ()
   fmap = Prelude.fmap
   (<$) = (Prelude.<$)
 
 instance Applicative Gen where
-  lower = lowerP
+  reify = id
+  reflect = id
 
 instance Monad Gen where
   (>>=) = (Prelude.>>=)
@@ -50,6 +50,7 @@
     :: (Functor f, Prelude.Functor f, Suitable f a, Eq (f a), Show (f a))
     => f b -> a -> Property
 replaceIsSame xs x = label "replace is same" $ (x <$ xs) === (x Prelude.<$ xs)
+
 
 pureIsSame
     :: (Applicative f