diff --git a/Data/Reflection.hs b/Data/Reflection.hs
--- a/Data/Reflection.hs
+++ b/Data/Reflection.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE KindSignatures, RankNTypes, ScopedTypeVariables, EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances #-}
+{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, TypeOperators #-}
 
 ----------------------------------------------------------------------------
 -- |
@@ -10,33 +10,34 @@
 -- Stability   : experimental
 -- Portability : non-portable (scoped types, MPTCs, rank-n, FFI, kinds)
 --
--- Implementation of the Functional Pearl: Implicit Configurations paper by
+-- Based on the Functional Pearl: Implicit Configurations paper by
 -- Oleg Kiselyov and Chung-chieh Shan.
 --
 -- <http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf>
 --
--- Packaged and updated to work with the current implementation of scoped type 
--- variables by Edward Kmett.
+-- Modified to work with an applicative phantom type parameter rather than 
+-- explicit scope type variables by Edward Kmett.
 --
 -------------------------------------------------------------------------------
 
 module Data.Reflection 
     ( 
     -- * Reflect Integrals
-      ReflectedNum
+      ReifiesNum
     , reflectNum
     , reifyIntegral
     -- * Reflect Lists of Integrals
-    , ReflectedNums
+    , ReifiesNums
     , reifyIntegrals
     -- * Reflect Storables
-    , ReflectedStorable
+    , ReifiesStorable
     , reflectStorable
     , reifyStorable
     -- * Reflect Anything
-    , Reflects
+    , Reifies
     , reflect
     , reify
+    , Tagged(..)
     ) where
 
 import Foreign.C.Types
@@ -47,101 +48,157 @@
 import Foreign.StablePtr
 import Foreign.Storable
 import System.IO.Unsafe
+import Control.Applicative 
+import Prelude hiding (succ, pred)
 
-data Zero
-data Twice s
-data Succ s
-data Pred s
+class Unused t where unused :: t -> ()
 
-class ReflectedNum s where
-    reflectNum :: Num a => s -> a
+newtype Tagged a b = Tagged { unTagged :: b } deriving (Eq,Ord,Show,Read)
+type Retag f g = forall b. Tagged g b -> Tagged f b
 
-instance ReflectedNum Zero where
-    reflectNum _ = 0
+instance Functor (Tagged a) where 
+    fmap f (Tagged x) = Tagged (f x)
+    {-# INLINE fmap #-}
 
-instance ReflectedNum s => ReflectedNum (Twice s) where
-    reflectNum _ = reflectNum (undefined :: s) * 2
+instance Applicative (Tagged a) where
+    pure = Tagged
+    {-# INLINE pure #-}
+    Tagged f <*> Tagged x = Tagged (f x)
+    {-# INLINE (<*>) #-}
 
-instance ReflectedNum s => ReflectedNum (Succ s) where
-    reflectNum _ = reflectNum (undefined :: s) + 1
+instance Monad (Tagged a) where
+    return = Tagged
+    {-# INLINE return #-}
+    Tagged m >>= k = k m 
+    {-# INLINE (>>=) #-}
+    _ >> n = n
+    {-# INLINE (>>) #-}
 
-instance ReflectedNum s => ReflectedNum (Pred s) where
-    reflectNum _ = reflectNum (undefined :: s) - 1
+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)
+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{} = ()
 
-reifyIntegral :: Integral a => a -> (forall s. ReflectedNum s => s -> w) -> w
-reifyIntegral i k = case quotRem i 2 of
-    (0, 0) -> k (undefined :: Zero)
-    (j, 0) -> reifyIntegral j (\(_ :: s) -> k (undefined :: Twice s))
-    (j, 1) -> reifyIntegral j (\(_ :: s) -> k (undefined :: Succ (Twice s)))
-    (j,-1) -> reifyIntegral j (\(_ :: s) -> k (undefined :: Pred (Twice s)))
-    _      -> undefined
+retag :: Retag f g
+retag = Tagged . unTagged 
+{-# INLINE retag #-}
 
-data Nil
-data Cons s ss
+pop :: Retag (f s) s
+pop = retag
+{-# INLINE pop #-} 
 
-class ReflectedNums ss where
-    reflectNums :: Num a => ss -> [a]
+class ReifiesNum s where
+    reflectNum :: Num a => Tagged s a
 
-instance ReflectedNums Nil where
-    reflectNums _ = []
+instance ReifiesNum Zero where
+    reflectNum = pure 0
 
-instance (ReflectedNum s, ReflectedNums ss) => ReflectedNums (Cons s ss) where
-    reflectNums _ = reflectNum (undefined :: s) : reflectNums (undefined :: ss)
+instance ReifiesNum s => ReifiesNum (Twice s) where
+    reflectNum = (2*) <$> pop reflectNum 
 
-reifyIntegrals :: Integral a => [a] -> (forall ss. ReflectedNums ss => ss -> w) -> w
-reifyIntegrals [] k = k (undefined :: Nil)
-reifyIntegrals (i:ii) k = 
-    reifyIntegral i (\(_ :: s) -> 
-    reifyIntegrals ii (\(_ :: ss) -> 
-    k (undefined :: Cons s ss)))
+instance ReifiesNum s => ReifiesNum (Succ s) where
+    reflectNum = (1+) <$> pop reflectNum
 
-data Store s a 
+instance ReifiesNum s => ReifiesNum (Pred s) where
+    reflectNum = subtract 1 <$> pop reflectNum
 
-class ReflectedStorable s where
-    reflectStorable :: Storable a => s a -> a
+reifyIntegral :: Integral a => a -> (forall s. ReifiesNum s => Tagged s w) -> w
+reifyIntegral i k = case quotRem i 2 of
+    (0, 0) -> zero k 
+    (j, 0) -> reifyIntegral j (twice k)
+    (j, 1) -> reifyIntegral j (twice (succ k))
+    (j,-1) -> reifyIntegral j (twice (pred k))
+    _      -> undefined 
+  where
+    twice :: Retag s (Twice s)
+    twice = retag
+    succ :: Retag s (Succ s)
+    succ = retag
+    pred :: Retag s (Pred s)
+    pred = retag
+    zero :: Tagged Zero a -> a
+    zero = unTagged
 
-instance ReflectedNums s => ReflectedStorable (Store s) where
+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 => Tagged ss [a]
+
+instance ReifiesNums Nil where
+    reflectNums = pure []
+
+instance (ReifiesNum s, ReifiesNums ss) => ReifiesNums (Cons s ss) where
+    reflectNums = (:) <$> car reflectNum <*> cdr reflectNums where
+        car :: Retag (Cons s ss) s
+        car = retag
+        cdr :: Retag (Cons s ss) ss
+        cdr = retag
+
+reifyIntegrals :: Integral a => [a] -> (forall ss. ReifiesNums ss => Tagged ss w) -> w
+reifyIntegrals [] k = nil k where
+    nil :: Tagged Nil a' -> a'
+    nil = unTagged 
+reifyIntegrals (i:ii) k = reifyIntegral i (reifyIntegrals ii (cons k)) where
+    cons :: Tagged (Cons s' ss') a' -> Tagged ss' (Tagged s' a')
+    cons = pure . retag
+    
+newtype Store s a = Store (Store s a)
+instance Unused (Store s a) where unused Store{} = ()
+
+class ReifiesStorable s where
+    reflectStorable :: Storable a => Tagged (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 :: Tagged s' [CChar] -> Tagged (Store s' b) b -> [CChar]
+        bytes (Tagged a) _ = a
     {-# NOINLINE reflectStorable #-}
-    reflectStorable _ = unsafePerformIO . alloca $ \p -> do 
-            pokeArray (castPtr p) bytes
-            peek p 
-        where 
-            bytes = reflectNums (undefined :: s) :: [CChar]
 
-reifyStorable :: Storable a => a -> (forall s. ReflectedStorable s => s a -> w) -> w
-reifyStorable a k = reifyIntegrals (bytes :: [CChar]) (\(_ :: s) -> k (undefined :: Store s a))
+store :: Retag s' (Store s' c)
+store = retag
+
+reifyStorable :: Storable a => a -> (forall s. ReifiesStorable s => Tagged (s a) w) -> w
+reifyStorable a k = reifyIntegrals bytes (store k)
   where
+    bytes :: [CChar]
     bytes = unsafePerformIO $ with a (peekArray (sizeOf a) . castPtr) 
 {-# NOINLINE reifyStorable #-}
 
-class Reflects s a | s -> a where 
-    reflect :: s -> a
+class Reifies s a | s -> a where 
+    reflect :: Tagged s a
 
-data Stable (s :: * -> *) a
+newtype Stable s a = Stable (s (Stable s a))
+instance Unused (Stable s a) where unused Stable{} = ()
 
-{-
-instance ReflectedStorable s => Reflects (Stable s a) a where
-    reflect = unsafePerformIO . fmap const . deRefStablePtr $ reflectStorable (undefined :: s p) 
+instance ReifiesStorable s => Reifies (Stable s a) a where
+    reflect = r where
+        r = unsafePerformIO $ do
+            pure <$> deRefStablePtr p <* freeStablePtr p
 
-reify :: a -> (forall s. Reflects s a => s -> w) -> w
-reify (a :: a) k = unsafePerformIO $ do
-        p <- newStablePtr a
-        reifyStorable p (\(_ :: s (StablePtr a)) -> return (k (undefined :: Stable s a)))
--}
+        p = pointer reflectStorable r
 
-instance ReflectedStorable s => Reflects (Stable s a) a where
-    reflect = unsafePerformIO $ do
-            a <- deRefStablePtr p
-            freeStablePtr p
-            return (const a)
-        where  
-            p = reflectStorable (undefined :: s p)
+        pointer :: Tagged (s' p) p -> Tagged (Stable s' a') a' -> p
+        pointer (Tagged a) _ = a
     {-# NOINLINE reflect #-}
 
-reify :: a -> (forall s. (s `Reflects` a) => s -> w) -> w
-reify (a :: a) k = unsafePerformIO $ do
+reify :: a -> (forall s. Reifies s a => Tagged s w) -> w
+reify a k = unsafePerformIO $ do
         p <- newStablePtr a
-        reifyStorable p (\(_ :: s (StablePtr a)) -> 
-                let k' s = (reflect :: Stable s a -> a) `seq` return (k s) 
-                in k' (undefined :: Stable s a))
+        reifyStorable p (stable (reflect `before` (return <$> k)))
+    where
+        stable :: Retag (s' (StablePtr a')) (Stable s' a')
+        stable = retag
+        before :: Tagged (s' a') a' -> Tagged (s' a') r -> Tagged (s' a') r
+        before = seq
 {-# NOINLINE reify #-}
+
diff --git a/reflection.cabal b/reflection.cabal
--- a/reflection.cabal
+++ b/reflection.cabal
@@ -1,21 +1,22 @@
 name:		    reflection
-version:	    0.1.1
+version:	    0.2.0
 license:	    BSD3
 license-file:   LICENSE
-author:		    Oleg Kiselyov and Chung-chieh Shan
+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
+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 code in "Functional Pearl: Implicit Configurations" by 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.2
 
 library
   build-depends: 
-    base >= 4 && < 4.2
+    base >= 4 && < 5
   exposed-modules:
     Data.Reflection