diff --git a/Data/Reflection.hs b/Data/Reflection.hs
--- a/Data/Reflection.hs
+++ b/Data/Reflection.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE Rank2Types, TypeFamilies #-}
 {-# OPTIONS_GHC -fno-cse -fno-full-laziness -fno-float-in -fno-warn-unused-binds #-}
 ----------------------------------------------------------------------------
 -- |
@@ -8,7 +8,7 @@
 --
 -- Maintainer  : Edward Kmett <ekmett@gmail.com>
 -- Stability   : experimental
--- Portability : non-portable (rank-2 types)
+-- Portability : non-portable (rank-2 types, type families)
 --
 -- Based on the Functional Pearl: Implicit Configurations paper by
 -- Oleg Kiselyov and Chung-chieh Shan.
@@ -24,7 +24,6 @@
     -- * Reifying any term at the type level
       Reified(..)
     , reify
-    , reflectT
     -- * Reifying integral values at the type level
     , ReifiedNum(..)
     , reifyIntegral
@@ -43,15 +42,11 @@
 newtype PredTwice s = PredTwice (PredTwice s) deriving (Show)
 
 class ReifiedNum s where
-  reflectNum :: Num a => proxy s -> a
+  reflectNum :: Num a => p 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)
 
@@ -69,13 +64,17 @@
     (j,-1) -> reifyIntegral j (k . predTwice)
     _      -> undefined
 
-twice :: proxy s -> Proxy (Twice s)
+pop :: p (f s) -> Proxy s
+pop _ = Proxy
+{-# INLINE pop #-}
+
+twice :: p s -> Proxy (Twice s)
 twice _ = Proxy
 
-succTwice :: proxy s -> Proxy (SuccTwice s)
+succTwice :: p s -> Proxy (SuccTwice s)
 succTwice _ = Proxy
 
-predTwice :: proxy s -> Proxy (PredTwice s)
+predTwice :: p s -> Proxy (PredTwice s)
 predTwice _ = Proxy
 
 zero :: (Proxy Zero -> a) -> a
@@ -90,32 +89,29 @@
 intPtrToStablePtr = castPtrToStablePtr . intPtrToPtr
 
 class Reified s where
-  reflect :: p (s a) -> a
+  type Reflected s
+  reflect :: p s -> Reflected s
 
+stable :: p s -> Proxy (Stable s a)
+stable _ = Proxy
+
 unstable :: (p (Stable s a) -> a) -> Proxy s
 unstable _ = Proxy
 
-instance ReifiedNum s => Reified (Stable s) where
+instance ReifiedNum s => Reified (Stable s a) where
+  type Reflected (Stable s a) = a
   reflect = r where
       r = unsafePerformIO $ pure <$> deRefStablePtr p <* freeStablePtr p
       p = intPtrToStablePtr $ reflectNum $ unstable r
   {-# 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 :: Reified s => (Proxy s -> b) -> proxy s -> 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 -> (forall s. (Reified s, Reflected s ~ a) => Proxy s -> w) -> w
 reify a k = unsafePerformIO $ do
     p <- newStablePtr a
     reifyIntegral (stablePtrToIntPtr p) (reflectBefore (fmap return k) . stable)
-  where
-    stable :: p s -> Proxy (Stable s a)
-    stable _ = Proxy
 {-# NOINLINE reify #-}
diff --git a/examples/Constraints.hs b/examples/Constraints.hs
new file mode 100644
--- /dev/null
+++ b/examples/Constraints.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE Rank2Types, TypeFamilies, TypeOperators, ConstraintKinds, PolyKinds, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables #-}
+import Control.Newtype        -- from newtype
+import Data.Constraint        -- from constraints
+import Data.Constraint.Unsafe -- from constraints
+import Data.Monoid            -- from base
+import Data.Proxy             -- from tagged
+import Data.Reflection        -- from reflection
+
+-- | Values in our dynamically constructed monoid over 'a'
+newtype Lift (p :: * -> Constraint) (a :: *) (s :: *) = Lift { lower :: a }
+
+class ReifiableConstraint p where
+  data Def (p :: * -> Constraint) (a :: *)
+  reifiedIns :: (Reified s, Reflected s ~ Def p a) :- p (Lift p a s)
+
+instance Newtype (Lift p a s) a where
+  pack = Lift
+  unpack = lower
+
+-- > ghci> with (Monoid (+) 0) $ mempty <> Lift 2
+-- > 0
+with :: Def p a -> (forall s. (Reified s, Reflected s ~ Def p a) => Lift p a s) -> a
+with d v = reify d $ lower . asProxyOf v
+
+reifyInstance :: Def p a -> (forall s. (Reified s, Reflected s ~ Def p a) => Proxy s -> r) -> r
+reifyInstance = reify
+
+asProxyOf :: f s -> Proxy s -> f s
+asProxyOf a _ = a
+
+-- > using (Monoid (+) 0) $ mappend mempty 12
+using :: forall p a. ReifiableConstraint p => Def p a -> (p a => a) -> a
+using d m = reify d $ \(_ :: Proxy s) -> m \\ trans (unsafeCoerceConstraint :: (p (Lift p a s) :- p a)) reifiedIns
+
+usingT :: forall p f a. ReifiableConstraint p => Def p a -> (p a => f a) -> f a
+usingT d m = reify d $ \(_ :: Proxy s) -> m \\ trans (unsafeCoerceConstraint :: (p (Lift p a s) :- p a)) reifiedIns
+
+instance ReifiableConstraint Monoid where
+  data Def Monoid a = Monoid { mappend_ :: a -> a -> a, mempty_ :: a }
+  reifiedIns = Sub Dict
+
+instance (Reified s, Reflected s ~ Def Monoid a) => Monoid (Lift Monoid a s) where
+  mappend a b        = Lift $ mappend_ (reflect a) (lower a) (lower b)
+  mempty = a where a = Lift $ mempty_ (reflect a)
+
+instance ReifiableConstraint Eq where
+  data Def Eq a = Eq { eq :: a -> a -> Bool }
+  reifiedIns = Sub Dict
+
+instance (Reified s, Reflected s ~ Def Eq a) => Eq (Lift Eq a s) where
+  a == b = eq (reflect a) (lower a) (lower b)
diff --git a/examples/Monoid.hs b/examples/Monoid.hs
--- a/examples/Monoid.hs
+++ b/examples/Monoid.hs
@@ -1,28 +1,22 @@
-{-# LANGUAGE Rank2Types, KindSignatures #-}
-import Data.Reflection
-import Data.Monoid
-import Data.Proxy
+{-# LANGUAGE Rank2Types, TypeFamilies #-}
+import Data.Reflection -- from reflection
+import Data.Monoid     -- from base
+import Data.Proxy      -- from tagged
 
-newtype M (s :: * -> *) a = M { runM :: a }
+-- | Values in our dynamically constructed monoid over 'a'
+newtype M a s = M { runM :: a } deriving (Eq,Ord)
 
+-- | A dictionary describing the contents of a monoid
 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)
-
-reifyMonoid :: (a -> a -> a) -> a -> (forall s. Reified s => Proxy (s (Monoid_ a)) -> r) -> r
-reifyMonoid f z = reify (Monoid_ f z)
+instance (Reified s, Reflected s ~ Monoid_ a) => Monoid (M a s) where
+  mappend a b        = M $ mappend_ (reflect a) (runM a) (runM b)
+  mempty = a where a = M $ mempty_ (reflect a)
 
--- > ghci> withMonoid (+) 0 (mempty `mappend` M 2)
+-- > ghci> withMonoid (+) 0 $ mempty <> 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
+withMonoid :: (a -> a -> a) -> a -> (forall s. (Reified s, Reflected s ~ Monoid_ a) => M a s) -> a
+withMonoid f z v = reify (Monoid_ f z) (runM . asProxyOf v)
+
+asProxyOf :: f s -> Proxy s -> f s
+asProxyOf a _ = a
diff --git a/reflection.cabal b/reflection.cabal
--- a/reflection.cabal
+++ b/reflection.cabal
@@ -1,5 +1,5 @@
 name:           reflection
-version:        0.7
+version:        0.8
 license:        BSD3
 license-file:   LICENSE
 author:         Edward A. Kmett, Oleg Kiselyov and Chung-chieh Shan
@@ -14,25 +14,31 @@
 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@
+  Chung-chieh Shan. However, the API has been modified to use @Rank2Types@ and
+  @TypeFamilies@
   .
   Usage reduces to using two combinators.
   .
-  > reify :: a -> (forall s. Reified s => Proxy (s a) -> w) -> w
-  > reflect :: Reified s => p (s a) -> a
+  > reify :: a -> (forall s. (Reified s, Reflected s ~ a) => Proxy s -> w) -> w
+  > reflect :: Reified s => p s -> Reflected s
   .
-  > ghci> reify 6 (\p -> reflect p + reflect p)
+  > ghci> reify 6 (\p -> reflect p + reflect p) :: Int
   > 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.8/:
   .
+  * Switched to using type families to avoid a problem where the user could cast
+    @Proxy (s a) -> Proxy (s b)@ and get back a values with the wrong type under
+    the API in effect from 0.6. This API yields a much nicer example as well.
+  .
+  * Removed @reflectT@ as it no longer makes sense.
+  .
+  * Added a more advanced example @example/Constraints.hs@ using constraint kinds.
+  .
   /Changes in 0.7/:
   .
   * Uses a much simpler construction where @reify@ now converts a @StablePtr@ to an
@@ -66,14 +72,14 @@
     reduces the need for helper functions and scoped type variables in user
     code.
 
-extra-source-files: examples/Monoid.hs
+extra-source-files: examples/Monoid.hs examples/Constraints.hs
 
 source-repository head
   type: git
   location: git://github.com/ekmett/reflection.git
 
 library
-  other-extensions: Rank2Types
+  other-extensions: Rank2Types, TypeFamilies
   build-depends:
     base >= 4 && < 5,
     tagged >= 0.2.3 && < 0.3