diff --git a/Data/Reflection.hs b/Data/Reflection.hs
--- a/Data/Reflection.hs
+++ b/Data/Reflection.hs
@@ -1,190 +1,30 @@
-{-# LANGUAGE Rank2Types, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances #-}
+{-# LANGUAGE Rank2Types #-}
 {-# OPTIONS_GHC -fno-cse -fno-full-laziness -fno-float-in #-}
-
 ----------------------------------------------------------------------------
 -- |
 -- Module     : Data.Reflection
--- Copyright  : 2009-2011 Edward Kmett, 2004 Oleg Kiselyov and Chung-chieh Shan
+-- Copyright  : 2009-2012 Edward Kmett, 2004 Oleg Kiselyov and Chung-chieh Shan
 -- License    : BSD3
 --
 -- Maintainer  : Edward Kmett <ekmett@gmail.com>
 -- Stability   : experimental
--- Portability : non-portable (MPTCs, fundeps, rank-2 types, flexible instances)
+-- Portability : non-portable (rank-2 types)
 --
 -- Based on the Functional Pearl: Implicit Configurations paper by
 -- Oleg Kiselyov and Chung-chieh Shan.
 --
 -- <http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf>
 --
--- Modified to minimize extensions and work with Data.Proxy rather than 
+-- Modified to minimize extensions and work with Data.Proxy rather than
 -- explicit scoped type variables and undefined values by Edward Kmett.
---
 -------------------------------------------------------------------------------
 
 module Data.Reflection
     (
-    -- * Reflect Integrals
-      ReifiesNum(..)
-    , reifyIntegral
-    -- * Reflect Lists of Integrals
-    , ReifiesNums(..)
-    , reifyIntegrals
-    -- * Reflect Storables
-    , ReifiesStorable(..)
-    , reifyStorable
-    -- * Reflect Anything
-    , Reifies(..)
+    -- * Reifying any term at the type level
+      Reified
+    , reflect, reflectT
     , reify
     ) where
 
-import Foreign.C.Types
-import Foreign.Marshal.Alloc
-import Foreign.Marshal.Array
-import Foreign.Marshal.Utils
-import Foreign.Ptr
-import Foreign.StablePtr
-import Foreign.Storable
-import System.IO.Unsafe
-import Control.Applicative 
-import Prelude hiding (succ, pred)
-import Data.Proxy
-
-
-newtype Zero = Zero Zero deriving (Show)
-newtype Twice s = Twice (Twice s) deriving (Show)
-newtype Succ s = Succ (Succ s) deriving (Show)
-newtype Pred s = Pred (Pred s) deriving (Show)
-
--- silence compiler warnings about unused constructors
-class Unused t where 
-  unused :: t -> ()
-instance Unused Zero where 
-  unused Zero{} = ()
-instance Unused (Twice s) where 
-  unused Twice{} = ()
-instance Unused (Succ s) where 
-  unused Succ{} = ()
-instance Unused (Pred s) where 
-  unused Pred{} = ()
-
-
-class ReifiesNum s where
-  reflectNum :: Num a => proxy s -> a
-
-instance ReifiesNum Zero where
-  reflectNum = pure 0
-
-pop :: proxy (f s) -> Proxy s
-pop _ = Proxy
-{-# INLINE pop #-} 
-
-instance ReifiesNum s => ReifiesNum (Twice s) where
-  reflectNum p = 2 * reflectNum (pop p)
-
-instance ReifiesNum s => ReifiesNum (Succ s) where
-  reflectNum p = 1 + reflectNum (pop p)
-
-instance ReifiesNum s => ReifiesNum (Pred s) where
-  reflectNum p = reflectNum (pop p) - 1
-
-reifyIntegral :: Integral a => a -> (forall s. ReifiesNum s => Proxy s -> w) -> w
-reifyIntegral i k = case quotRem i 2 of
-    (0, 0) -> zero k 
-    (j, 0) -> reifyIntegral j (k . twice)
-    (j, 1) -> reifyIntegral j (k . succ . twice)
-    (j,-1) -> reifyIntegral j (k . pred . twice)
-    _      -> undefined 
-
-twice :: proxy s -> Proxy (Twice s)
-twice _ = Proxy
-
-succ :: proxy s -> Proxy (Succ s)
-succ _ = Proxy 
-
-pred :: proxy s -> Proxy (Pred s)
-pred _ = Proxy
-
-zero :: (Proxy Zero -> a) -> a
-zero k = k Proxy
-
-newtype Nil = Nil Nil
-newtype Cons s ss = Cons (Cons s ss)
-instance Unused Nil where unused Nil{} = ()
-instance Unused (Cons s ss) where unused Cons{} = ()
-
-class ReifiesNums ss where
-  reflectNums :: Num a => proxy ss -> [a]
-
-instance ReifiesNums Nil where
-  reflectNums = pure []
-
-instance (ReifiesNum s, ReifiesNums ss) => ReifiesNums (Cons s ss) where
-  reflectNums p = reflectNum (car p) : reflectNums (cdr p) where
-    car :: proxy (Cons s ss) -> Proxy s
-    car _ = Proxy
-    cdr :: proxy (Cons s ss) -> Proxy ss
-    cdr _ = Proxy
-
-reifyIntegrals :: Integral a => [a] -> (forall ss. ReifiesNums ss => Proxy ss -> w) -> w
-reifyIntegrals [] k = nil k where
-    nil :: (Proxy Nil -> a') -> a'
-    nil f = f Proxy
-reifyIntegrals (i:ii) k = reifyIntegral i (reifyIntegrals ii (cons k)) where
-    cons :: (Proxy (Cons s' ss') -> a') -> proxy ss' -> proxy s' -> a'
-    cons f _ _ = f Proxy
-    
-newtype Store s a = Store (Store s a)
-instance Unused (Store s a) where unused Store{} = ()
-
-class ReifiesStorable s where
-    reflectStorable :: Storable a => proxy (s a) -> a
-
-instance ReifiesNums s => ReifiesStorable (Store s) where
-    reflectStorable = r where 
-        r = unsafePerformIO $ alloca $ \p -> do 
-            pokeArray (castPtr p) (bytes reflectNums r)
-            pure <$> peek p 
-        bytes :: (Proxy s' -> [CChar]) -> (proxy (Store s' b) -> b) -> [CChar]
-        bytes k _ = k Proxy
-    {-# NOINLINE reflectStorable #-}
-
-store :: proxy s' -> Proxy (Store s' c)
-store _ = Proxy
-
-reifyStorable :: Storable a => a -> (forall s. ReifiesStorable s => Proxy (s a) -> w) -> w
-reifyStorable a k = reifyIntegrals bytes (k . store)
-  where
-    bytes :: [CChar]
-    bytes = unsafePerformIO $ with a (peekArray (sizeOf a) . castPtr) 
-{-# NOINLINE reifyStorable #-}
-
-class Reifies s a | s -> a where 
-    reflect :: proxy s -> a
-
-newtype Stable s a = Stable (s (Stable s a))
-instance Unused (Stable s a) where 
-    unused Stable{} = ()
-
-instance ReifiesStorable s => Reifies (Stable s a) a where
-    reflect = r where
-        r = unsafePerformIO $ 
-                 pure <$> deRefStablePtr p <* freeStablePtr p
-        p = pointer reflectStorable r
-
-        pointer :: (Proxy (s' p) -> p) -> (proxy (Stable s' a') -> a') -> p
-        pointer f _ = f Proxy
-    {-# NOINLINE reflect #-}
-
--- This had to be moved to the top level, due to an apparent bug in the ghc inliner introduced in ghc 7.0.x
-reflectBefore :: Reifies s a => (Proxy s -> b) -> proxy s -> b
-reflectBefore f = let b = f Proxy in b `seq` const b
-{-# NOINLINE reflectBefore #-}
-
-reify :: a -> (forall s. Reifies s a => Proxy s -> w) -> w
-reify a k = unsafePerformIO $ do
-        p <- newStablePtr a
-        reifyStorable p (reflectBefore (return <$> k) . stable)
-    where
-        stable :: proxy (s' (StablePtr a')) -> Proxy (Stable s' a')
-        stable _ = Proxy
-{-# NOINLINE reify #-}
+import Data.Reflection.Internal
diff --git a/Data/Reflection/Internal.hs b/Data/Reflection/Internal.hs
new file mode 100644
--- /dev/null
+++ b/Data/Reflection/Internal.hs
@@ -0,0 +1,192 @@
+{-# LANGUAGE Rank2Types #-}
+{-# OPTIONS_GHC -fno-cse -fno-full-laziness -fno-float-in #-}
+----------------------------------------------------------------------------
+-- |
+-- Module     : Data.Reflection.Internal
+-- Copyright  : 2009-2012 Edward Kmett, 2004 Oleg Kiselyov and Chung-chieh Shan
+-- License    : BSD3
+--
+-- Maintainer  : Edward Kmett <ekmett@gmail.com>
+-- Stability   : experimental
+-- Portability : non-portable (rank-2 types)
+--
+-- Based on the Functional Pearl: Implicit Configurations paper by
+-- Oleg Kiselyov and Chung-chieh Shan.
+--
+-- <http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf>
+--
+-- Modified to minimize extensions and work with Data.Proxy rather than
+-- explicit scoped type variables and undefined values by Edward Kmett.
+-------------------------------------------------------------------------------
+
+module Data.Reflection.Internal
+    (
+    -- * Reifying any term at the type level
+      Reified(..)
+    , reify
+    , reflectT
+    -- * Special cases
+    -- ** Reifying integral values as types
+    , ReifiedNum(..)
+    , reifyIntegral
+    -- ** Reifying lists of integrals values as types
+    , ReifiedNums(..)
+    , reifyIntegrals
+    -- ** Reifying storables values as types
+    , ReifiedStorable(..)
+    , reifyStorable
+    ) where
+
+import Foreign.C.Types
+import Foreign.Marshal.Alloc
+import Foreign.Marshal.Array
+import Foreign.Marshal.Utils
+import Foreign.Ptr
+import Foreign.StablePtr
+import Foreign.Storable
+import System.IO.Unsafe
+import Control.Applicative
+import Prelude hiding (succ, pred)
+import Data.Proxy
+
+newtype Zero = Zero Zero deriving (Show)
+newtype Twice s = Twice (Twice s) deriving (Show)
+newtype Succ s = Succ (Succ s) deriving (Show)
+newtype Pred s = Pred (Pred s) deriving (Show)
+
+-- silence compiler warnings about unused constructors
+class Unused t where
+  unused :: t -> ()
+instance Unused Zero where
+  unused Zero{} = ()
+instance Unused (Twice s) where
+  unused Twice{} = ()
+instance Unused (Succ s) where
+  unused Succ{} = ()
+instance Unused (Pred s) where
+  unused Pred{} = ()
+
+class ReifiedNum s where
+  reflectNum :: Num a => proxy s -> a
+
+instance ReifiedNum Zero where
+  reflectNum = pure 0
+
+pop :: proxy (f s) -> Proxy s
+pop _ = Proxy
+{-# INLINE pop #-}
+
+instance ReifiedNum s => ReifiedNum (Twice s) where
+  reflectNum p = 2 * reflectNum (pop p)
+
+instance ReifiedNum s => ReifiedNum (Succ s) where
+  reflectNum p = 1 + reflectNum (pop p)
+
+instance ReifiedNum s => ReifiedNum (Pred s) where
+  reflectNum p = reflectNum (pop p) - 1
+
+reifyIntegral :: Integral a => a -> (forall s. ReifiedNum s => Proxy s -> w) -> w
+reifyIntegral i k = case quotRem i 2 of
+    (0, 0) -> zero k
+    (j, 0) -> reifyIntegral j (k . twice)
+    (j, 1) -> reifyIntegral j (k . succ . twice)
+    (j,-1) -> reifyIntegral j (k . pred . twice)
+    _      -> undefined
+
+twice :: proxy s -> Proxy (Twice s)
+twice _ = Proxy
+
+succ :: proxy s -> Proxy (Succ s)
+succ _ = Proxy
+
+pred :: proxy s -> Proxy (Pred s)
+pred _ = Proxy
+
+zero :: (Proxy Zero -> a) -> a
+zero k = k Proxy
+
+newtype Nil = Nil Nil
+newtype Cons s ss = Cons (Cons s ss)
+instance Unused Nil where unused Nil{} = ()
+instance Unused (Cons s ss) where unused Cons{} = ()
+
+class ReifiedNums ss where
+  reflectNums :: Num a => proxy ss -> [a]
+
+instance ReifiedNums Nil where
+  reflectNums = pure []
+
+instance (ReifiedNum s, ReifiedNums ss) => ReifiedNums (Cons s ss) where
+  reflectNums p = reflectNum (car p) : reflectNums (cdr p) where
+    car :: proxy (Cons s ss) -> Proxy s
+    car _ = Proxy
+    cdr :: proxy (Cons s ss) -> Proxy ss
+    cdr _ = Proxy
+
+reifyIntegrals :: Integral a => [a] -> (forall ss. ReifiedNums ss => Proxy ss -> w) -> w
+reifyIntegrals [] k = nil k where
+    nil :: (Proxy Nil -> a') -> a'
+    nil f = f Proxy
+reifyIntegrals (i:ii) k = reifyIntegral i (reifyIntegrals ii (cons k)) where
+    cons :: (Proxy (Cons s' ss') -> a') -> proxy ss' -> proxy s' -> a'
+    cons f _ _ = f Proxy
+
+newtype Store s a = Store (Store s a)
+instance Unused (Store s a) where unused Store{} = ()
+
+class ReifiedStorable s where
+    reflectStorable :: Storable a => proxy (s a) -> a
+
+instance ReifiedNums s => ReifiedStorable (Store s) where
+    reflectStorable = r where
+        r = unsafePerformIO $ alloca $ \p -> do
+            pokeArray (castPtr p) (bytes reflectNums r)
+            pure <$> peek p
+        bytes :: (Proxy s' -> [CChar]) -> (proxy (Store s' b) -> b) -> [CChar]
+        bytes k _ = k Proxy
+    {-# NOINLINE reflectStorable #-}
+
+store :: proxy s' -> Proxy (Store s' c)
+store _ = Proxy
+
+reifyStorable :: Storable a => a -> (forall s. ReifiedStorable s => Proxy (s a) -> w) -> w
+reifyStorable a k = reifyIntegrals bytes (k . store)
+  where
+    bytes :: [CChar]
+    bytes = unsafePerformIO $ with a (peekArray (sizeOf a) . castPtr)
+{-# NOINLINE reifyStorable #-}
+
+class Reified s where
+    reflect :: proxy (s a) -> a
+
+newtype Stable s a = Stable (s (Stable s a))
+instance Unused (Stable s a) where
+    unused Stable{} = ()
+
+instance ReifiedStorable s => Reified (Stable s) where
+    reflect = r where
+        r = unsafePerformIO $ pure <$> deRefStablePtr p <* freeStablePtr p
+        p = pointer reflectStorable r
+
+        pointer :: (Proxy (s' p) -> p) -> (proxy (Stable s' a') -> a') -> p
+        pointer f _ = f Proxy
+    {-# NOINLINE reflect #-}
+
+reflectT :: Reified s => t s a -> a
+reflectT p = reflect (t p) where
+  t :: p x y -> Proxy (x y)
+  t _ = Proxy
+
+-- This had to be moved to the top level, due to an apparent bug in the ghc inliner introduced in ghc 7.0.x
+reflectBefore :: Reified s => (Proxy (s a) -> b) -> proxy (s a) -> b
+reflectBefore f = let b = f Proxy in b `seq` const b
+{-# NOINLINE reflectBefore #-}
+
+reify :: a -> (forall s. Reified s => Proxy (s a) -> w) -> w
+reify a k = unsafePerformIO $ do
+        p <- newStablePtr a
+        reifyStorable p (reflectBefore (return <$> k) . stable)
+    where
+        stable :: proxy (s' (StablePtr a')) -> Proxy (Stable s' a')
+        stable _ = Proxy
+{-# NOINLINE reify #-}
diff --git a/examples/Monoid.hs b/examples/Monoid.hs
new file mode 100644
--- /dev/null
+++ b/examples/Monoid.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE Rank2Types, KindSignatures #-}
+import Data.Reflection
+import Data.Monoid
+import Data.Proxy
+
+newtype M (s :: * -> *) a = M { runM :: a }
+
+data Monoid_ a = Monoid_ { mappend_ :: a -> a -> a, mempty_ :: a }
+
+instance Reified s => Monoid (M s a) where
+  mappend a b = M $ mappend_ (reflectM a) (runM a) (runM b)
+  mempty = r where r = M $ mempty_ $ reflectM r
+
+monoidProxy :: M s a -> Proxy (s (Monoid_ a))
+monoidProxy _ = Proxy
+
+reflectM :: Reified s => M s a -> Monoid_ a
+reflectM m = reflect (monoidProxy m) where
+
+reifyMonoid :: (a -> a -> a) -> a -> (forall s. Reified s => Proxy (s (Monoid_ a)) -> r) -> r
+reifyMonoid f z = reify (Monoid_ f z)
+
+-- > ghci> withMonoid (+) 0 (mempty `mappend` M 2)
+-- > 2
+withMonoid :: (a -> a -> a) -> a -> (forall s. Reified s => M s a) -> a
+withMonoid f z v = reifyMonoid f z (\p -> runM (v `asProxyOf` p)) where
+  asProxyOf :: M s x -> Proxy (s (Monoid_ x)) -> M s x
+  asProxyOf a _ = a
diff --git a/reflection.cabal b/reflection.cabal
--- a/reflection.cabal
+++ b/reflection.cabal
@@ -1,32 +1,72 @@
-name:		reflection
-version:	0.5.0.1
-license:	BSD3
+name:           reflection
+version:        0.6
+license:        BSD3
 license-file:   LICENSE
-author:		Edward A. Kmett, Oleg Kiselyov and Chung-chieh Shan
-maintainer:	Edward A. Kmett <ekmett@gmail.com>
-stability:	experimental
-homepage:	http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf
-category:	Data, Reflection, Dependent Types
-synopsis:	Functional Pearl: Implicit Configurations
+author:         Edward A. Kmett, Oleg Kiselyov and Chung-chieh Shan
+maintainer:     Edward A. Kmett <ekmett@gmail.com>
+stability:      experimental
+homepage:       http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf
+category:       Data, Reflection, Dependent Types
+synopsis:       Functional Pearl: Implicit Configurations
 copyright:      2009 Edward A. Kmett, 2004 Oleg Kiselyov and Chung-chieh Shan
-description:    Implementation of the ideas presented in the paper "Functional Pearl: Implicit Configurations" by Oleg Kiselyov and Chung-chieh Shan.
-                Modified to avoid the use of scoped type variables, and to use a phantom type wrapper rather than dummy arguments.
 build-type:     Simple
-cabal-version:  >=1.6
+cabal-version:  >= 1.6
+description:
+  This package provides an implementation of the ideas presented in the paper
+  "Functional Pearl: Implicit Configurations" by Oleg Kiselyov and
+  Chung-chieh Shan. However, the API has been modified to use only
+  one extension: @Rank2Types@
+  .
+  Usage reduces to using two combinators.
+  .
+  > reify :: a -> (forall s. Reified s => Proxy (s a) -> w) -> w
+  > reflect :: Reified s => p (s a) -> a
+  .
+  > ghci> reify 6 (\p -> reflect p + reflect p)
+  > 12
+  .
+  The argument passed along by reify is just a @data Proxy t = Proxy@, so all of the
+  information needed to reconstruct your value has been moved to the type level.
+  This enables it to be used when constructing instances (See @examples/Monoid.hs@).
+  An additional combinator, that may be more useful when building instances is also
+  supplied.
+  .
+  > reflectT :: Reified s => p s a -> a
+  .
+  /Changes in 0.6/:
+  .
+  * Removed the dependency on multiparameter type classes, functional
+    dependencies, and flexible instances, by making @Reifies@ a single
+    parameter type class in the same fashion as @ReifiesStorable@.
+  .
+  * Moved the building blocks to @Data.Reflection.Internal@ to reduce API clutter.
+  .
+  * Added @reflectT@
+  .
+  /Changes in 0.5/:
+  .
+  * Generalized the type signatures in reflect to allow you to pass any type
+    with kind @* -> *@ wrapped around the desired type as the phantom type
+    argument rather than just a @Proxy@.
+  .
+  /Changes in 0.4/:
+  .
+  * Converted from `Data.Tagged` to using `Data.Proxy` for reflection. This
+    reduces the need for helper functions and scoped type variables in user
+    code.
 
+extra-source-files: examples/Monoid.hs
+
 source-repository head
   type: git
   location: git://github.com/ekmett/reflection.git
 
 library
-  other-extensions:
-    Rank2Types
-    MultiParamTypeClasses
-    FunctionalDependencies
-    FlexibleInstances
-  build-depends: 
+  other-extensions: Rank2Types
+  build-depends:
     base >= 4 && < 5,
     tagged >= 0.2.3 && < 0.3
   exposed-modules:
     Data.Reflection
+    Data.Reflection.Internal
   ghc-options: -Wall