diff --git a/CHANGES b/CHANGES
new file mode 100644
--- /dev/null
+++ b/CHANGES
@@ -0,0 +1,25 @@
+Changelog for singletons project
+================================
+
+0.8.2
+-----
+
+Added this changelog
+
+Update to work with latest version of GHC (7.6.1). (There was a change to
+Template Haskell).
+
+Moved library into Data.Singletons.
+
+0.8.1
+-----
+
+Update to work with latest version of GHC. (There was a change to
+Template Haskell).
+
+Updated dependencies in cabal to include the newer version of TH.
+
+0.8
+---
+
+Initial public release
diff --git a/Data/Singletons.hs b/Data/Singletons.hs
new file mode 100644
--- /dev/null
+++ b/Data/Singletons.hs
@@ -0,0 +1,151 @@
+{- Data/Singletons.hs
+
+(c) Richard Eisenberg 2012
+eir@cis.upenn.edu
+
+This is the public interface file to the singletons library. Please
+see the accompanying README file for more information. Haddock is
+not currently compatible with the features used here, so the documentation
+is all in the README file and /Dependently typed programming with singletons/,
+available at <http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf>
+-}
+
+{-# LANGUAGE TypeFamilies, GADTs, KindSignatures, TemplateHaskell,
+             DataKinds, PolyKinds, TypeOperators, MultiParamTypeClasses,
+             FlexibleContexts, RankNTypes, UndecidableInstances,
+             FlexibleInstances, ScopedTypeVariables
+ #-}
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+
+module Data.Singletons (
+  Any,
+  Demote, Sing(..), SingI(sing), SingE(fromSing), SingRep, (:==), (:==:),
+  SingInstance(..), SingKind(singInstance),
+  sTrue, sFalse, SBool, sNothing, sJust, SMaybe, sLeft, sRight, SEither,
+  sTuple0, sTuple2, sTuple3, sTuple4, sTuple5, sTuple6, sTuple7,
+  STuple0, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7,
+  Not, sNot, (:&&), (%:&&), (:||), (%:||), (:&&:), (:||:), (:/=), (:/=:),
+  SEq((%==%), (%/=%), (%:==), (%:/=)),
+  If, sIf, 
+  sNil, sCons, SList, (:++), (%:++), Head, Tail,
+  cases, bugInGHC,
+  genSingletons, singletons, genPromotions, promote,
+  ) where
+
+import Prelude hiding ((++))
+import Data.Singletons.Singletons
+import Data.Singletons.Promote
+import Language.Haskell.TH
+import GHC.Exts
+import Data.Singletons.Util
+
+-- Declarations of singleton structures
+data family Sing (a :: k)
+class SingI (a :: k) where
+  sing :: Sing a
+class SingE (a :: k) where
+  type Demote a :: *
+  fromSing :: Sing a -> Demote (Any :: k)
+
+-- SingRep is a synonym for (SingI, SingE)
+class (SingI a, SingE a) => SingRep a
+instance (SingI a, SingE a) => SingRep a
+
+type family (a :: k) :==: (b :: k) :: Bool
+type a :== b = a :==: b -- :== and :==: are synonyms
+
+data SingInstance (a :: k) where
+  SingInstance :: SingRep a => SingInstance a
+class (b ~ Any) => SingKind (b :: k) where
+  singInstance :: forall (a :: k). Sing a -> SingInstance a
+
+-- provide a few useful singletons...
+$(genSingletons [''Bool, ''Maybe, ''Either, ''[]])
+$(genSingletons [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)])
+
+-- ... with some functions over Booleans
+$(singletons [d|
+  not :: Bool -> Bool
+  not False = True
+  not True  = False
+
+  (&&) :: Bool -> Bool -> Bool
+  False && a = False
+  True  && a = a
+
+  (||) :: Bool -> Bool -> Bool
+  False || a = a
+  True  || a = True
+  |])
+
+-- symmetric syntax synonyms
+type a :&&: b = a :&& b
+type a :||: b = a :|| b
+
+type a :/=: b = Not (a :==: b)
+type a :/= b = a :/=: b
+
+-- the singleton analogue of @Eq@
+class (t ~ Any) => SEq (t :: k) where
+  (%==%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :==: b)
+  (%:==) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :==: b)
+  (%:==) = (%==%)
+  (%:/=) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/=: b)
+  a %:/= b = sNot (a %==% b)
+  (%/=%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/=: b)
+  (%/=%) = (%:/=)
+
+-- type-level conditional
+type family If (a :: Bool) (b :: k) (c :: k) :: k
+type instance If 'True b c = b
+type instance If 'False b c = c
+
+-- singleton conditional
+sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
+sIf STrue b c = b
+sIf SFalse b c = c
+
+type instance '[] :==: '[] = True
+type instance '[] :==: (h ': t) = False
+type instance (h ': t) :==: '[] = False
+type instance (h ': t) :==: (h' ': t') = (h :==: h') :&&: (t :==: t')
+
+instance SEq (Any :: k) => SEq (Any :: [k]) where
+  SNil %==% SNil = STrue
+  SNil %==% (SCons _ _) = SFalse
+  (SCons _ _) %==% SNil = SFalse
+  (SCons a b) %==% (SCons a' b') = (a %==% a') %:&& (b %==% b')
+
+type family Head (a :: [k]) :: k
+type instance Head (h ': t) = h
+
+type family Tail (a :: [k]) :: [k]
+type instance Tail (h ': t) = t
+
+$(singletons [d|
+  (++) :: [a] -> [a] -> [a]
+  [] ++ a = a
+  (h:t) ++ a = h:(t ++ a)
+  |])
+
+-- allows for automatic checking of all constructors in a GADT for instance
+-- inference
+cases :: Name -> Q Exp -> Q Exp -> Q Exp
+cases tyName expq bodyq = do
+  info <- reifyWithWarning tyName
+  case info of
+    TyConI (DataD _ _ _ ctors _) -> buildCases ctors
+    TyConI (NewtypeD _ _ _ ctor _) -> buildCases [ctor]
+    _ -> fail $ "Using <<cases>> with something other than a type constructor: "
+                ++ (show tyName)
+  where buildCases :: [Con] -> Q Exp
+        buildCases ctors =
+          caseE expq (map ((flip (flip match (normalB bodyq)) []) . conToPat) ctors)
+
+        conToPat :: Con -> Q Pat
+        conToPat = ctor1Case
+          (\name tys -> conP name (replicate (length tys) wildP))
+
+-- useful when suppressing GHC's warnings about incomplete pattern matches
+bugInGHC :: forall a. a
+bugInGHC = error "Bug encountered in GHC -- this should never happen"
diff --git a/Data/Singletons/CustomStar.hs b/Data/Singletons/CustomStar.hs
new file mode 100644
--- /dev/null
+++ b/Data/Singletons/CustomStar.hs
@@ -0,0 +1,91 @@
+{- Data/Singletons/CustomStar.hs
+
+(c) Richard Eisenbeg 2012
+eir@cis.upenn.edu
+
+This file implements singletonStar, which generates a datatype Rep and associated
+singleton from a list of types. The promoted version of Rep is kind * and the
+Haskell types themselves. This is still very experimental, so expect unusual
+results!
+-} 
+
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+
+module Data.Singletons.CustomStar where
+
+import Language.Haskell.TH
+import Data.Singletons.Util
+import Data.Singletons.Promote
+import Data.Singletons.Singletons
+import Control.Monad
+
+-- Produce a representation and singleton for the collection of types given
+singletonStar :: [Name] -> Q [Dec]
+singletonStar names = do
+  kinds <- mapM getKind names
+  ctors <- zipWithM (mkCtor True) names kinds
+  let repDecl = DataD [] repName [] ctors
+                      [mkName "Eq", mkName "Show", mkName "Read"]
+  fakeCtors <- zipWithM (mkCtor False) names kinds
+  eqTypeInstances <- mapM mkEqTypeInstance [ (c1, c2) | c1 <- fakeCtors,
+                                                        c2 <- fakeCtors ]
+  singletonDecls <- singDataD True [] repName [] fakeCtors
+                              [mkName "Eq", mkName "Show", mkName "Read"]
+  return $ repDecl :
+           eqTypeInstances ++
+           singletonDecls
+  where -- get the kinds of the arguments to the tycon with the given name
+        getKind :: Name -> Q [Kind]
+        getKind name = do
+          info <- reifyWithWarning name
+          case info of
+            TyConI (DataD (_:_) _ _ _ _) ->
+               fail "Cannot make a representation of a constrainted data type"
+            TyConI (DataD [] _ tvbs _ _) ->
+               return $ map extractTvbKind tvbs
+            TyConI (NewtypeD (_:_) _ _ _ _) ->
+               fail "Cannot make a representation of a constrainted newtype"
+            TyConI (NewtypeD [] _ tvbs _ _) ->
+               return $ map extractTvbKind tvbs
+            TyConI (TySynD _ tvbs _) ->
+               return $ map extractTvbKind tvbs
+            PrimTyConI _ n _ ->
+               return $ replicate n StarT
+            _ -> fail $ "Invalid thing for representation: " ++ (show name)
+        
+        -- first parameter is whether this is a real ctor (with a fresh name)
+        -- or a fake ctor (when the name is actually a Haskell type)
+        mkCtor :: Bool -> Name -> [Kind] -> Q Con
+        mkCtor real name args = do
+          (types, vars) <- evalForPair $ mapM kindToType args
+          let ctor = NormalC ((if real then reinterpret else id) name)
+                             (map (\ty -> (NotStrict, ty)) types)
+          if length vars > 0
+            then return $ ForallC (map PlainTV vars) [] ctor
+            else return ctor
+
+        -- demote a kind back to a type, accumulating any unbound parameters
+        kindToType :: Kind -> QWithAux [Name] Type
+        kindToType (ForallT _ _ _) = fail "Explicit forall encountered in kind"
+        kindToType (AppT k1 k2) = do
+          t1 <- kindToType k1
+          t2 <- kindToType k2
+          return $ AppT t1 t2
+        kindToType (SigT _ _) = fail "Sort signature encountered in kind"
+        kindToType (VarT n) = do
+          addElement n
+          return $ VarT n
+        kindToType (ConT n) = return $ ConT n
+        kindToType (PromotedT _) = fail "Promoted type used as a kind"
+        kindToType (TupleT n) = return $ TupleT n
+        kindToType (UnboxedTupleT _) = fail "Unboxed tuple kind encountered"
+        kindToType ArrowT = return ArrowT
+        kindToType ListT = return ListT
+        kindToType (PromotedTupleT _) = fail "Promoted tuple kind encountered"
+        kindToType PromotedNilT = fail "Promoted nil kind encountered"
+        kindToType PromotedConsT = fail "Promoted cons kind encountered"
+        kindToType StarT = return $ ConT repName
+        kindToType ConstraintT =
+          fail $ "Cannot make a representation of a type that has " ++
+                 "an argument of kind Constraint"
+        kindToType (LitT _) = fail "Literal encountered at the kind level"
diff --git a/Data/Singletons/Promote.hs b/Data/Singletons/Promote.hs
new file mode 100644
--- /dev/null
+++ b/Data/Singletons/Promote.hs
@@ -0,0 +1,548 @@
+{- Data/Singletons/Promote.hs
+
+(c) Richard Eisenberg 2012
+eir@cis.upenn.edu
+
+This file contains functions to promote term-level constructs to the
+type level. It is an internal module to the singletons package.
+-}
+
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+
+module Data.Singletons.Promote where
+
+import Language.Haskell.TH
+import Data.Singletons.Util
+import Prelude hiding (exp)
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+import Control.Monad
+import Data.Maybe
+import Control.Monad.Writer
+import Data.List
+
+anyTypeName, falseName, trueName, andName, tyEqName, repName, ifName,
+  headName, tailName :: Name
+anyTypeName = mkName "Any"
+falseName = mkName "False"
+trueName = mkName "True"
+andName = mkName "&&"
+tyEqName = mkName ":==:"
+repName = mkName "Rep"
+ifName = mkName "If"
+headName = mkName "Head"
+tailName = mkName "Tail"
+
+falseTy :: Type
+falseTy = promoteDataCon falseName
+
+trueTy :: Type
+trueTy = promoteDataCon trueName
+
+andTy :: Type
+andTy = promoteVal andName
+
+ifTyFam :: Type
+ifTyFam = ConT ifName
+
+headTyFam :: Type
+headTyFam = ConT headName
+
+tailTyFam :: Type
+tailTyFam = ConT tailName
+
+genPromotions :: [Name] -> Q [Dec]
+genPromotions names = do
+  checkForRep names
+  infos <- mapM reifyWithWarning names
+  decls <- mapM promoteInfo infos
+  return $ concat decls
+
+promoteInfo :: Info -> Q [Dec]
+promoteInfo (ClassI dec instances) =
+  fail "Promotion of class info not supported"
+promoteInfo (ClassOpI name ty className fixity) =
+  fail "Promotion of class members info not supported"
+promoteInfo (TyConI dec) = evalWithoutAux $ promoteDec Map.empty dec
+promoteInfo (FamilyI dec instances) =
+  fail "Promotion of type family info not yet supported" -- KindFams
+promoteInfo (PrimTyConI name numArgs unlifted) =
+  fail "Promotion of primitive type constructors not supported"
+promoteInfo (DataConI name ty tyname fixity) =
+  fail $ "Promotion of individual constructors not supported; " ++
+         "promote the type instead"
+promoteInfo (VarI name ty mdec fixity) =
+  fail "Promotion of value info not supported"
+promoteInfo (TyVarI name ty) =
+  fail "Promotion of type variable info not supported"
+
+promoteDataCon :: Name -> Type
+promoteDataCon name =
+  if isTupleName name
+    then PromotedTupleT (tupleDegree $ nameBase name)
+    else PromotedT name
+
+promoteValName :: Name -> Name
+promoteValName n
+  | nameBase n == "undefined" = anyTypeName
+  | otherwise                 = upcase n
+
+promoteVal :: Name -> Type
+promoteVal = ConT . promoteValName
+
+promoteType :: Type -> Q Kind
+promoteType (ForallT tvbs [] ty) = promoteType ty -- ForallKinds
+promoteType (ForallT _ (_:_) _) = fail "Cannot promote type with constrained variables"
+promoteType (VarT name) = return $ VarT name
+promoteType (ConT name) = return $ if (nameBase name) == "TypeRep" ||
+                                      (nameBase name) == (nameBase repName)
+                                     then StarT else ConT name
+promoteType (TupleT n) = return $ TupleT n
+promoteType (UnboxedTupleT n) = fail "Promotion of unboxed tuples not supported"
+promoteType ArrowT = return ArrowT
+promoteType ListT = return ListT
+promoteType (AppT (AppT ArrowT (ForallT (_:_) _ _)) _) =
+  fail "Cannot promote types of rank above 1."
+promoteType (AppT ty1 ty2) = do
+  k1 <- promoteType ty1
+  k2 <- promoteType ty2
+  return $ AppT k1 k2
+promoteType (SigT ty _) = fail "Cannot promote type of kind other than *"
+promoteType (LitT _) = fail "Cannot promote a type-level literal"
+promoteType (PromotedT _) = fail "Cannot promote a promoted data constructor"
+promoteType (PromotedTupleT _) = fail "Cannot promote tuples that are already promoted"
+promoteType PromotedNilT = fail "Cannot promote a nil that is already promoted"
+promoteType PromotedConsT = fail "Cannot promote a cons that is already promoted"
+promoteType StarT = fail "* used as a type"
+promoteType ConstraintT = fail "Constraint used as a type"
+
+-- a table to keep track of variable->type mappings
+type TypeTable = Map.Map Name Type
+
+-- Promote each declaration in a splice
+promote :: Q [Dec] -> Q [Dec]
+promote qdec = do
+  decls <- qdec
+  (promDecls, _) <- promoteDecs decls
+  return $ decls ++ promDecls
+
+checkForRep :: [Name] -> Q ()
+checkForRep names =
+  when (any ((== nameBase repName) . nameBase) names)
+    (fail $ "A data type named <<Rep>> is a special case.\n" ++
+            "Promoting it will not work as expected.\n" ++
+            "Please choose another name for your data type.")
+
+checkForRepInDecls :: [Dec] -> Q ()
+checkForRepInDecls decls =
+  checkForRep (map extractNameFromDec decls)
+  where extractNameFromDec :: Dec -> Name
+        extractNameFromDec (DataD _ name _ _ _) = name
+        extractNameFromDec (NewtypeD _ name _ _ _) = name
+        extractNameFromDec (TySynD name _ _) = name
+        extractNameFromDec (FamilyD _ name _ _) = name
+        extractNameFromDec _ = mkName "NotRep"
+
+-- Promote a list of declarations; returns the promoted declarations
+-- and a list of names of declarations without accompanying type signatures.
+-- (This list is needed by singletons to strike such definitions.)
+
+-- Promoting declarations proceeds in two stages:
+-- 1) Promote everything except type signatures
+-- 2) Promote type signatures. This must be done in a second pass because
+--    a function type signature gets promoted to a type family declaration.
+--    Although function signatures do not differentiate between uniform parameters
+--    and non-uniform parameters, type family declarations do. We need
+--    to process a function's definition to get the count of non-uniform
+--    parameters before producing the type family declaration.
+--    At this point, any function written without a type signature is rejected
+--    and removed.
+promoteDecs :: [Dec] -> Q ([Dec], [Name])
+promoteDecs decls = do
+  checkForRepInDecls decls
+  let vartbl = Map.empty
+  (newDecls, numArgsTable) <- evalForPair $ mapM (promoteDec vartbl) decls
+  (declss, namess) <- mapAndUnzipM (promoteDec' numArgsTable) decls
+  let moreNewDecls = concat declss
+      names = concat namess
+      noTypeSigs = Set.toList $ Set.difference (Map.keysSet $
+                                                  Map.filter (>= 0) numArgsTable)
+                                               (Set.fromList names)
+      noTypeSigsPro = map promoteValName noTypeSigs
+      newDecls' = foldl (\decls name ->
+                          filter (not . (containsName name)) decls)
+                        (concat newDecls) (noTypeSigs ++ noTypeSigsPro)
+  mapM_ (\n -> reportWarning $ "No type binding for " ++ (show (nameBase n)) ++
+                               "; removing all declarations including it")
+        noTypeSigs
+  return (newDecls' ++ moreNewDecls, noTypeSigs)
+
+-- produce the type instance for (:==:) for the given pair of constructors
+mkEqTypeInstance :: (Con, Con) -> Q Dec
+mkEqTypeInstance (c1, c2) =
+  if c1 == c2
+  then do
+    let (name, numArgs) = extractNameArgs c1
+    lnames <- replicateM numArgs (newName "a")
+    rnames <- replicateM numArgs (newName "b")
+    let lvars = map VarT lnames
+        rvars = map VarT rnames
+    return $ TySynInstD
+      tyEqName
+      [foldType (PromotedT name) lvars,
+       foldType (PromotedT name) rvars]
+      (tyAll (zipWith (\l r -> foldType (ConT tyEqName) [l, r])
+                      lvars rvars))
+  else do
+    let (lname, lNumArgs) = extractNameArgs c1
+        (rname, rNumArgs) = extractNameArgs c2
+    lnames <- replicateM lNumArgs (newName "a")
+    rnames <- replicateM rNumArgs (newName "b")
+    return $ TySynInstD
+      tyEqName
+      [foldType (PromotedT lname) (map VarT lnames),
+       foldType (PromotedT rname) (map VarT rnames)]
+      falseTy
+  where tyAll :: [Type] -> Type -- "all" at the type level
+        tyAll [] = trueTy
+        tyAll [one] = one
+        tyAll (h:t) = foldType andTy [h, (tyAll t)]
+
+-- keeps track of the number of non-uniform parameters to promoted values
+type NumArgsTable = Map.Map Name Int
+type NumArgsQ = QWithAux NumArgsTable
+
+-- used when a type is declared as a type synonym, not a type family
+-- no need to declare "type family ..." for these
+typeSynonymFlag :: Int
+typeSynonymFlag = -1
+
+promoteDec :: TypeTable -> Dec -> NumArgsQ [Dec]
+promoteDec vars (FunD name clauses) = do
+  let proName = promoteValName name
+      vars' = Map.insert name (promoteVal name) vars
+      numArgs = getNumPats (head clauses) -- count the parameters
+      -- Haskell requires all clauses to have the same number of parameters
+  instDecls <- lift $ mapM (promoteClause vars' proName) clauses
+  addBinding name numArgs -- remember the number of parameters
+  return $ concat instDecls
+  where getNumPats :: Clause -> Int
+        getNumPats (Clause pats _ _) = length pats
+promoteDec vars (ValD pat body decs) = do
+  -- see also the comment for promoteTopLevelPat
+  when (length decs > 0)
+    (fail $ "Promotion of global variable with <<where>> clause " ++
+                "not yet supported")
+  (rhs, decls) <- lift $ evalForPair $ promoteBody vars body
+  (lhss, decls') <- lift $ evalForPair $ promoteTopLevelPat pat
+  if any (flip containsName rhs) (map lhsName lhss)
+    then do -- definition is recursive. use type families & require ty sigs
+      mapM (flip addBinding 0) (map lhsRawName lhss)
+      return $ (map (\(LHS _ nm hole) -> TySynInstD nm [] (hole rhs)) lhss) ++
+               decls ++ decls'
+    else do -- definition is not recursive; just use "type" decls
+      mapM (flip addBinding typeSynonymFlag) (map lhsRawName lhss)
+      return $ (map (\(LHS _ nm hole) -> TySynD nm [] (hole rhs)) lhss) ++
+               decls ++ decls'
+promoteDec vars (DataD cxt name tvbs ctors derivings) = 
+  promoteDataD vars cxt name tvbs ctors derivings
+promoteDec vars (NewtypeD cxt name tvbs ctor derivings) =
+  promoteDataD vars cxt name tvbs [ctor] derivings
+promoteDec vars (TySynD name tvbs ty) =
+  fail "Promotion of type synonym declaration not yet supported"
+promoteDec vars (ClassD cxt name tvbs fundeps decs) =
+  fail "Promotion of class declaration not yet supported"
+promoteDec vars (InstanceD cxt ty decs) =
+  fail "Promotion of instance declaration not yet supported"
+promoteDec vars (SigD name ty) = return [] -- handle in promoteDec'
+promoteDec vars (ForeignD fgn) =
+  fail "Promotion of foreign function declaration not yet supported"
+promoteDec vars (InfixD fixity name)
+  | isUpcase name = return [] -- automatic: promoting a type or data ctor
+  | otherwise     = return [InfixD fixity (promoteValName name)] -- value
+promoteDec vars (PragmaD prag) =
+  fail "Promotion of pragmas not yet supported"
+promoteDec vars (FamilyD flavour name tvbs mkind) =
+  fail "Promotion of type and data families not yet supported"
+promoteDec vars (DataInstD cxt name tys ctors derivings) =
+  fail "Promotion of data instances not yet supported"
+promoteDec vars (NewtypeInstD cxt name tys ctors derivings) =
+  fail "Promotion of newtype instances not yet supported"
+promoteDec vars (TySynInstD name tys ty) =
+  fail "Promotion of type synonym instances not yet supported)"
+
+-- only need to check if the datatype derives Eq. The rest is automatic.
+promoteDataD :: TypeTable -> Cxt -> Name -> [TyVarBndr] -> [Con] ->
+                [Name] -> NumArgsQ [Dec]
+promoteDataD vars cxt name tvbs ctors derivings =
+  if any (\n -> (nameBase n) == "Eq") derivings
+    then do
+      let pairs = [ (c1, c2) | c1 <- ctors, c2 <- ctors ]
+      lift $ mapM mkEqTypeInstance pairs
+    else return [] -- the actual promotion is automatic
+
+-- second pass through declarations to deal with type signatures
+-- returns the new declarations and the list of names that have been
+-- processed
+promoteDec' :: NumArgsTable -> Dec -> Q ([Dec], [Name])
+promoteDec' nat (SigD name ty) = case Map.lookup name nat of
+  Nothing -> fail $ "Type declaration is missing its binding: " ++ (show name)
+  Just numArgs -> 
+    -- if there are no args, then use a type synonym, not a type family
+    -- in the type synonym case, we ignore the type signature
+    if numArgs == typeSynonymFlag then return $ ([], [name]) else do 
+      k <- promoteType ty
+      let ks = unravel k
+          (argKs, resultKs) = splitAt numArgs ks -- divide by uniformity
+      resultK <- ravel resultKs -- rebuild the arrow kind
+      tyvarNames <- mapM newName (replicate (length argKs) "a")
+      return ([FamilyD TypeFam
+                       (promoteValName name)
+                       (zipWith KindedTV tyvarNames argKs)
+                       (Just resultK)], [name])
+    where unravel :: Kind -> [Kind] -- get argument kinds from an arrow kind
+          unravel (AppT (AppT ArrowT k1) k2) =
+            let ks = unravel k2 in k1 : ks
+          unravel k = [k]
+          
+          ravel :: [Kind] -> Q Kind
+          ravel [] = fail "Internal error: raveling nil"
+          ravel [k] = return k
+          ravel (h:t) = do
+            k <- ravel t
+            return $ (AppT (AppT ArrowT h) k)
+promoteDec' _ _ = return ([], [])
+
+promoteClause :: TypeTable -> Name -> Clause -> Q [Dec]
+promoteClause vars name (Clause pats body []) = do
+  -- promoting the patterns creates variable bindings. These are passed
+  -- to the function promoted the RHS
+  (types, vartbl) <- evalForPair $ mapM promotePat pats
+  let vars' = Map.union vars vartbl
+  (ty, decls) <- evalForPair $ promoteBody vars' body
+  return $ decls ++ [TySynInstD name types ty]
+promoteClause _ _ (Clause _ _ (_:_)) =
+  fail "A <<where>> clause in a function definition is not yet supported"
+
+-- the LHS of a top-level expression is a name and "type with hole"
+-- the hole is filled in by the RHS
+data TopLevelLHS = LHS { lhsRawName :: Name -- the unpromoted name
+                       , lhsName :: Name
+                       , lhsHole :: Type -> Type
+                       }
+
+-- Treatment of top-level patterns is different from other patterns
+-- because type families have type patterns as their LHS. However,
+-- it is not possible to use type patterns at the top level, so we
+-- have to use other techniques.
+promoteTopLevelPat :: Pat -> QWithDecs [TopLevelLHS]
+promoteTopLevelPat (LitP _) = fail "Cannot declare a global literal."
+promoteTopLevelPat (VarP name) = return [LHS name (promoteValName name) id]
+promoteTopLevelPat (TupP pats) = case length pats of
+  0 -> return [] -- unit as LHS of pattern... ignore
+  1 -> fail "1-tuple encountered during top-level pattern promotion"
+  n -> promoteTopLevelPat (ConP (tupleDataName n) pats)
+promoteTopLevelPat (UnboxedTupP _) =
+  fail "Promotion of unboxed tuples not supported"
+
+-- to promote a constructor pattern, we need to create extraction type
+-- families to pull out the individual arguments of the constructor
+promoteTopLevelPat (ConP name pats) = do
+  ctorInfo <- lift $ reifyWithWarning name
+  (ctorType, argTypes) <- lift $ extractTypes ctorInfo
+  when (length argTypes /= length pats) $
+    fail $ "Inconsistent data constructor pattern: " ++ (show name) ++ " " ++
+           (show pats)
+  kind <- lift $ promoteType ctorType
+  argKinds <- lift $ mapM promoteType argTypes
+  extractorNamesRaw <- lift $ replicateM (length pats) (newName "Extract")
+
+  -- TH doesn't allow "newName"s to work at the top-level, so we have to
+  -- do this trick to ensure the Extract functions are unique
+  let extractorNames = map (mkName . show) extractorNamesRaw
+  varName <- lift $ newName "a"
+  zipWithM (\nm arg -> addElement $ FamilyD TypeFam
+                                            nm
+                                            [KindedTV varName kind]
+                                            (Just arg))
+           extractorNames argKinds
+  componentNames <- lift $ replicateM (length pats) (newName "a")
+  zipWithM (\extractorName componentName ->
+    addElement $ TySynInstD extractorName
+                            [foldType (promoteDataCon name)
+                                      (map VarT componentNames)]
+                            (VarT componentName))
+    extractorNames componentNames
+
+  -- now we have the extractor families. Use the appropriate families
+  -- in the "holes"
+  promotedPats <- mapM promoteTopLevelPat pats
+  return $ concat $
+    zipWith (\lhslist extractor ->
+               map (\(LHS raw nm hole) -> LHS raw nm
+                                              (hole . (AppT (ConT extractor))))
+                   lhslist)
+            promotedPats extractorNames
+  where extractTypes :: Info -> Q (Type, [Type])
+        extractTypes (DataConI datacon _dataconTy tyname _fixity) = do
+          tyinfo <- reifyWithWarning tyname
+          extractTypesHelper datacon tyinfo
+        extractTypes _ = fail "Internal error: unexpected Info in extractTypes"
+ 
+        extractTypesHelper :: Name -> Info -> Q (Type, [Type])
+        extractTypesHelper datacon
+                           (TyConI (DataD _cxt tyname tvbs cons _derivs)) =
+          let mcon = find ((== datacon) . fst . extractNameArgs) cons in
+          case mcon of
+            Nothing -> fail $ "Internal error reifying " ++ (show datacon)
+            Just con -> return (foldType (ConT tyname)
+                                         (map (VarT . extractTvbName) tvbs),
+                                extractConArgs con)
+        extractTypesHelper datacon
+                           (TyConI (NewtypeD cxt tyname tvbs con derivs)) =
+          extractTypesHelper datacon (TyConI (DataD cxt tyname tvbs [con] derivs))
+        extractTypesHelper datacon _ =
+          fail $ "Cannot promote data constructor " ++ (show datacon)
+
+        extractConArgs :: Con -> [Type]
+        extractConArgs = ctor1Case (\_ tys -> tys)
+promoteTopLevelPat (InfixP l name r) = promoteTopLevelPat (ConP name [l, r])
+promoteTopLevelPat (UInfixP _ _ _) =
+  fail "Unresolved infix constructors not supported"
+promoteTopLevelPat (ParensP _) = 
+  fail "Unresolved infix constructors not supported"
+promoteTopLevelPat (TildeP pat) = do
+  lift $ reportWarning "Lazy pattern converted into regular pattern in promotion"
+  promoteTopLevelPat pat
+promoteTopLevelPat (BangP pat) = do
+  lift $ reportWarning "Strict pattern converted into regular pattern in promotion"
+  promoteTopLevelPat pat
+promoteTopLevelPat (AsP name pat) =
+  fail "Promotion of aliased patterns at top level not yet supported"
+promoteTopLevelPat WildP = return []
+promoteTopLevelPat (RecP _ _) =
+  fail "Promotion of record patterns at top level not yet supported"
+
+-- must do a similar trick as what is in the ConP case, but this is easier
+-- because Lib defined Head and Tail
+promoteTopLevelPat (ListP pats) = do
+  promotedPats <- mapM promoteTopLevelPat pats
+  return $ concat $ snd $
+    mapAccumL (\extractFn lhss ->
+                 ((AppT tailTyFam) . extractFn,
+                  map (\(LHS raw nm hole) ->
+                         LHS raw nm (hole . (AppT headTyFam) . extractFn)) lhss))
+              id promotedPats
+promoteTopLevelPat (SigP pat _) = do
+  lift $ reportWarning $ "Promotion of explicit type annotation in pattern " ++
+                         "not yet supported."
+  promoteTopLevelPat pat
+promoteTopLevelPat (ViewP _ _) =
+  fail "Promotion of view patterns not yet supported"
+
+type TypesQ = QWithAux TypeTable
+
+-- promotes a term pattern into a type pattern, accumulating variable
+-- binding in the auxiliary TypeTable
+promotePat :: Pat -> TypesQ Type
+promotePat (LitP lit) = fail $ "Promoting literals not supported: " ++ (show lit)
+promotePat (VarP name) = do
+  tyVar <- lift $ newName (nameBase name)
+  addBinding name (VarT tyVar)
+  return $ VarT tyVar
+promotePat (TupP pats) = do
+  types <- mapM promotePat pats
+  let baseTup = PromotedTupleT (length types)
+      tup = foldType baseTup types
+  return tup
+promotePat (UnboxedTupP _) = fail "Unboxed tuples not supported"
+promotePat (ConP name pats) = do
+  types <- mapM promotePat pats
+  let tyCon = foldType (promoteDataCon name) types
+  return tyCon
+promotePat (InfixP pat1 name pat2) = promotePat (ConP name [pat1, pat2])
+promotePat (UInfixP _ _ _) = fail "Unresolved infix constructions not supported"
+promotePat (ParensP _) = fail "Unresolved infix constructions not supported"
+promotePat (TildeP pat) = do
+  lift $ reportWarning "Lazy pattern converted into regular pattern in promotion"
+  promotePat pat
+promotePat (BangP pat) = do
+  lift $ reportWarning "Strict pattern converted into regular pattern in promotion"
+  promotePat pat
+promotePat (AsP name pat) = do
+  ty <- promotePat pat
+  addBinding name ty
+  return ty
+promotePat WildP = do
+  name <- lift $ newName "z"
+  return $ VarT name
+promotePat (RecP _ _) = fail "Promotion of record patterns not yet supported"
+promotePat (ListP pats) = do
+  types <- mapM promotePat pats
+  return $ foldr (\h t -> AppT (AppT PromotedConsT h) t) PromotedNilT types
+promotePat (SigP pat _) = do
+  lift $ reportWarning $ "Promotion of explicit type annotation in pattern " ++
+                         "not yet supported"
+  promotePat pat
+promotePat (ViewP _ _) = fail "View patterns not yet supported"
+
+-- promoting a body may produce auxiliary declarations. Accumulate these.
+type QWithDecs = QWithAux [Dec]
+
+promoteBody :: TypeTable -> Body -> QWithDecs Type
+promoteBody vars (NormalB exp) = promoteExp vars exp
+promoteBody vars (GuardedB _) =
+  fail "Promoting guards in patterns not yet supported"
+
+promoteExp :: TypeTable -> Exp -> QWithDecs Type
+promoteExp vars (VarE name) = case Map.lookup name vars of
+  Just ty -> return ty
+  Nothing -> return $ promoteVal name
+promoteExp vars (ConE name) = return $ promoteDataCon name
+promoteExp vars (LitE lit) = fail "Promotion of literal expressions not supported"
+promoteExp vars (AppE exp1 exp2) = do
+  ty1 <- promoteExp vars exp1
+  ty2 <- promoteExp vars exp2
+  return $ AppT ty1 ty2
+promoteExp vars (InfixE mexp1 exp mexp2) =
+  case (mexp1, mexp2) of
+    (Nothing, Nothing) -> promoteExp vars exp
+    (Just exp1, Nothing) -> promoteExp vars (AppE exp exp1)
+    (Nothing, Just exp2) ->
+      fail "Promotion of right-only sections not yet supported"
+    (Just exp1, Just exp2) -> promoteExp vars (AppE (AppE exp exp1) exp2)
+promoteExp vars (UInfixE _ _ _) =
+  fail "Promotion of unresolved infix operators not supported"
+promoteExp vars (ParensE _) = fail "Promotion of unresolved parens not supported"
+promoteExp vars (LamE pats exp) =
+  fail "Promotion of lambda expressions not yet supported"
+promoteExp vars (LamCaseE alts) =
+  fail "Promotion of lambda-case expressions not yet supported"
+promoteExp vars (TupE exps) = do
+  tys <- mapM (promoteExp vars) exps
+  let tuple = PromotedTupleT (length tys)
+      tup = foldType tuple tys
+  return tup
+promoteExp vars (UnboxedTupE _) = fail "Promotion of unboxed tuples not supported"
+promoteExp vars (CondE bexp texp fexp) = do
+  tys <- mapM (promoteExp vars) [bexp, texp, fexp]
+  return $ foldType ifTyFam tys
+promoteExp vars (MultiIfE alts) =
+  fail "Promotion of multi-way if not yet supported"
+promoteExp vars (LetE decs exp) =
+  fail "Promotion of let statements not yet supported"
+promoteExp vars (CaseE exp matches) =
+  fail "Promotion of case statements not yet supported"
+promoteExp vars (DoE stmts) = fail "Promotion of do statements not supported"
+promoteExp vars (CompE stmts) =
+  fail "Promotion of list comprehensions not yet supported"
+promoteExp vars (ArithSeqE _) = fail "Promotion of ranges not supported"
+promoteExp vars (ListE exps) = do
+  tys <- mapM (promoteExp vars) exps
+  return $ foldr (\ty lst -> AppT (AppT PromotedConsT ty) lst) PromotedNilT tys
+promoteExp vars (SigE exp ty) =
+  fail "Promotion of explicit type annotations not yet supported"
+promoteExp vars (RecConE name fields) =
+  fail "Promotion of record construction not yet supported"
+promoteExp vars (RecUpdE exp fields) =
+  fail "Promotion of record updates not yet supported"
diff --git a/Data/Singletons/Singletons.hs b/Data/Singletons/Singletons.hs
new file mode 100644
--- /dev/null
+++ b/Data/Singletons/Singletons.hs
@@ -0,0 +1,597 @@
+{- Data/Singletons/Singletons.hs
+
+(c) Richard Eisenberg 2012
+eir@cis.upenn.edu
+
+This file contains functions to refine constructs to work with singleton
+types. It is an internal module to the singletons package.
+-}
+
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+
+module Data.Singletons.Singletons where
+
+import Language.Haskell.TH
+import Data.Singletons.Util
+import Data.Singletons.Promote
+import qualified Data.Map as Map
+import Control.Monad
+import Control.Monad.Writer
+import Data.List
+
+-- map to track bound variables
+type ExpTable = Map.Map Name Exp
+
+-- translating a type gives a type with a hole in it,
+-- represented here as a function
+type TypeFn = Type -> Type
+
+-- a list of argument types extracted from a type application
+type TypeContext = [Type]
+
+singFamilyName, isSingletonName, forgettableName, comboClassName, witnessName,
+  demoteName, singKindClassName, singInstanceMethName, singInstanceName,
+  sEqClassName, sEqMethName, sconsName, snilName, smartSconsName,
+  smartSnilName, sIfName, undefinedName :: Name
+singFamilyName = mkName "Sing"
+isSingletonName = mkName "SingI"
+forgettableName = mkName "SingE"
+comboClassName = mkName "SingRep"
+witnessName = mkName "sing"
+forgetName = mkName "fromSing"
+demoteName = mkName "Demote"
+singKindClassName = mkName "SingKind"
+singInstanceMethName = mkName "singInstance"
+singInstanceName = mkName "SingInstance"
+sEqClassName = mkName "SEq"
+sEqMethName = mkName "%==%"
+sconsName = mkName "SCons"
+snilName = mkName "SNil"
+smartSconsName = mkName "sCons"
+smartSnilName = mkName "sNil"
+sIfName = mkName "sIf"
+undefinedName = mkName "undefined"
+
+mkTupleName :: Int -> Name
+mkTupleName n = mkName $ "STuple" ++ (show n)
+
+singFamily :: Type
+singFamily = ConT singFamilyName
+
+singKindConstraint :: Kind -> Pred
+singKindConstraint k = ClassP singKindClassName [SigT anyType k]
+
+singInstanceMeth :: Exp
+singInstanceMeth = VarE singInstanceMethName
+
+singInstanceTyCon :: Type
+singInstanceTyCon = ConT singInstanceName
+
+singInstanceDataCon :: Exp
+singInstanceDataCon = ConE singInstanceName
+
+singInstancePat :: Pat
+singInstancePat = ConP singInstanceName []
+
+demote :: Type
+demote = ConT demoteName
+
+anyType :: Type
+anyType = ConT anyTypeName
+
+singDataConName :: Name -> Name
+singDataConName nm = case nameBase nm of
+  "[]" -> snilName
+  ":"  -> sconsName
+  tuple | isTupleString tuple -> mkTupleName (tupleDegree tuple)
+  _ -> prefixUCName "S" ":%" nm
+
+singTyConName :: Name -> Name
+singTyConName name | nameBase name == "[]" = mkName "SList"
+                   | isTupleName name = mkTupleName (tupleDegree $ nameBase name)
+                   | otherwise        = prefixUCName "S" ":%" name
+
+singDataCon :: Name -> Exp
+singDataCon = ConE . singDataConName
+
+smartConName :: Name -> Name
+smartConName = locase . singDataConName
+
+smartCon :: Name -> Exp
+smartCon = VarE . smartConName
+
+singValName :: Name -> Name
+singValName n
+  | nameBase n == "undefined" = undefinedName
+  | otherwise                 = (prefixLCName "s" "%") $ upcase n
+
+singVal :: Name -> Exp
+singVal = VarE . singValName
+
+-- generate singleton definitions from an ADT
+genSingletons :: [Name] -> Q [Dec]
+genSingletons names = do
+  checkForRep names
+  infos <- mapM reifyWithWarning names
+  decls <- mapM singInfo infos
+  return $ concat decls
+
+singInfo :: Info -> Q [Dec]
+singInfo (ClassI dec instances) =
+  fail "Singling of class info not supported"
+singInfo (ClassOpI name ty className fixity) =
+  fail "Singling of class members info not supported"
+singInfo (TyConI dec) = singDec dec
+singInfo (FamilyI dec instances) =
+  fail "Singling of type family info not yet supported" -- KindFams
+singInfo (PrimTyConI name numArgs unlifted) =
+  fail "Singling of primitive type constructors not supported"
+singInfo (DataConI name ty tyname fixity) =
+  fail $ "Singling of individual constructors not supported; " ++
+         "single the type instead"
+singInfo (VarI name ty mdec fixity) =
+  fail "Singling of value info not supported"
+singInfo (TyVarI name ty) =
+  fail "Singling of type variable info not supported"
+
+-- refine a constructor. the first parameter is the type variable that
+-- the singleton GADT is parameterized by
+-- runs in the QWithDecs monad because auxiliary declarations are produced
+singCtor :: Type -> Con -> QWithDecs Con 
+singCtor a = ctorCases
+  (\name types -> do
+    let sName = singDataConName name
+        sCon = singDataCon name
+        pCon = promoteDataCon name
+    indexNames <- lift $ replicateM (length types) (newName "n")
+    let indices = map VarT indexNames
+    kinds <- lift $ mapM promoteType types
+    args <- lift $ buildArgTypes types indices
+    let tvbs = zipWith KindedTV indexNames kinds
+        bareKindVars = filter isVarK kinds
+
+    -- SingI instance
+    addElement $ InstanceD ((map singKindConstraint bareKindVars) ++
+                            (map (ClassP comboClassName . return) indices))
+                           (AppT (ConT isSingletonName)
+                                 (foldType pCon (zipWith SigT indices kinds)))
+                           [ValD (VarP witnessName)
+                                 (NormalB $ foldExp sCon (replicate (length types)
+                                                           (VarE witnessName)))
+                                 []]
+
+    -- smart constructor type signature
+    smartConType <- lift $ conTypesToFunType indexNames args kinds
+                                      (AppT singFamily (foldType pCon indices))
+    addElement $ SigD (smartConName name) smartConType
+     
+    -- smart constructor
+    let vars = map VarE indexNames
+        smartConBody = mkSingInstances vars (foldExp (singDataCon name) vars)
+    addElement $ FunD (smartConName name)
+                      [Clause (map VarP indexNames)
+                        (NormalB smartConBody)
+                        []]
+
+    return $ ForallC tvbs
+                     ((EqualP a (foldType (promoteDataCon name) indices)) :
+                       (map (ClassP comboClassName . return) indices) ++
+                       (map singKindConstraint bareKindVars))
+                     (NormalC sName $ map (\ty -> (NotStrict,ty)) args))
+  (\tvbs cxt ctor -> case cxt of
+    _:_ -> fail "Singling of constrained constructors not yet supported"
+    [] -> singCtor a ctor)
+  where buildArgTypes :: [Type] -> [Type] -> Q [Type]
+        buildArgTypes types indices = do
+          typeFns <- mapM (singType False) types
+          return $ zipWith id typeFns indices
+
+        conTypesToFunType :: [Name] -> [Type] -> [Kind] -> Type -> Q Type
+        conTypesToFunType [] [] [] ret = return ret
+        conTypesToFunType (nm : nmtail) (ty : tytail) (k : ktail) ret = do
+          rhs <- conTypesToFunType nmtail tytail ktail ret    
+          let innerty = AppT (AppT ArrowT ty) rhs
+          return $ ForallT [KindedTV nm k]
+                           (if isVarK k then [singKindConstraint k] else [])
+                           innerty
+        conTypesToFunType _ _ _ _ =
+          fail "Internal error in conTypesToFunType"
+
+        mkSingInstances :: [Exp] -> Exp -> Exp
+        mkSingInstances [] exp = exp
+        mkSingInstances (var:tail) exp =
+          CaseE (AppE singInstanceMeth var)
+                [Match singInstancePat (NormalB $ mkSingInstances tail exp) []]
+
+-- refine the declarations given
+singletons :: Q [Dec] -> Q [Dec]
+singletons qdec = do
+  decls <- qdec
+  singDecs decls
+
+singDecs :: [Dec] -> Q [Dec]
+singDecs decls = do
+  (promDecls, badNames) <- promoteDecs decls
+  -- need to remove the bad names returned from promoteDecs
+  newDecls <- mapM singDec
+                   (filter (\dec ->
+                     not $ or (map (\f -> f dec)
+                              (map containsName badNames))) decls)
+  return $ decls ++ promDecls ++ (concat newDecls)
+
+singDec :: Dec -> Q [Dec]
+singDec (FunD name clauses) = do
+  let sName = singValName name
+      vars = Map.singleton name (VarE sName)
+  liftM return $ funD sName (map (singClause vars) clauses)
+singDec (ValD _ (GuardedB _) _) =
+  fail "Singling of definitions of values with a pattern guard not yet supported"
+singDec (ValD _ _ (_:_)) =
+  fail "Singling of definitions of values with a <<where>> clause not yet supported"
+singDec (ValD pat (NormalB exp) []) = do
+  (sPat, vartbl) <- evalForPair $ singPat TopLevel pat
+  sExp <- singExp vartbl exp
+  return [ValD sPat (NormalB sExp) []]
+singDec (DataD (_:_) _ _ _ _) =
+  fail "Singling of constrained datatypes not supported"
+singDec (DataD cxt name tvbs ctors derivings) =
+  singDataD False cxt name tvbs ctors derivings
+singDec (NewtypeD cxt name tvbs ctor derivings) =
+  singDataD False cxt name tvbs [ctor] derivings
+singDec (TySynD name tvbs ty) =
+  fail "Singling of type synonyms not yet supported"
+singDec (ClassD cxt name tvbs fundeps decs) =
+  fail "Singling of class declaration not yet supported"
+singDec (InstanceD cxt ty decs) =
+  fail "Singling of class instance not yet supported"
+singDec (SigD name ty) = do
+  tyTrans <- singType True ty
+  return [SigD (singValName name) (tyTrans (promoteVal name))]
+singDec (ForeignD fgn) =
+  let name = extractName fgn in do
+    reportWarning $ "Singling of foreign functions not supported -- " ++
+                    (show name) ++ " ignored"
+    return []
+  where extractName :: Foreign -> Name
+        extractName (ImportF _ _ _ n _) = n
+        extractName (ExportF _ _ n _) = n
+singDec (InfixD fixity name)
+  | isUpcase name = return [InfixD fixity (singDataConName name)]
+  | otherwise     = return [InfixD fixity (singValName name)]
+singDec (PragmaD prag) = do
+    reportWarning "Singling of pragmas not supported"
+    return []
+singDec (FamilyD flavour name tvbs mkind) =
+  fail "Singling of type and data families not yet supported"
+singDec (DataInstD cxt name tys ctors derivings) = 
+  fail "Singling of data instances not yet supported"
+singDec (NewtypeInstD cxt name tys ctor derivings) =
+  fail "Singling of newtype instances not yet supported"
+singDec (TySynInstD name tys ty) =
+  fail "Singling of type family instances not yet supported"
+
+-- the first parameter is True when we're refining the special case "Rep"
+-- and false otherwise. We wish to consider the promotion of "Rep" to be *
+-- not a promoted data constructor.
+singDataD :: Bool -> Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> Q [Dec]
+singDataD rep cxt name tvbs ctors derivings = do
+  aName <- newName "a"
+  let a = VarT aName
+  let tvbNames = map extractTvbName tvbs
+  k <- promoteType (foldType (ConT name) (map VarT tvbNames))
+  (ctors', ctorInstDecls) <- evalForPair $ mapM (singCtor a) ctors
+  
+  -- instance for SingKind
+  let singKindInst =
+        InstanceD []
+                  (AppT (ConT singKindClassName)
+                        (SigT anyType k))
+                  [FunD singInstanceMethName
+                        (map mkSingInstanceClause ctors')]
+  
+  -- SEq instance
+  let ctorPairs = [ (c1, c2) | c1 <- ctors', c2 <- ctors' ]
+  sEqMethClauses <- mapM mkEqMethClause ctorPairs
+  let sEqInst =
+        InstanceD (map (\k -> ClassP sEqClassName [SigT anyType k])
+                       (getBareKinds ctors'))
+                  (AppT (ConT sEqClassName)
+                        (SigT anyType k))
+                  [FunD sEqMethName sEqMethClauses]
+  
+  -- e.g. type SNat (a :: Nat) = Sing a
+  let kindedSynInst =
+        TySynD (singTyConName name)
+               [KindedTV aName k]
+               (AppT singFamily a)
+
+  -- SingE instance
+  forgetClauses <- mapM mkForgetClause ctors
+  let singEInst =
+        InstanceD []
+                  (AppT (ConT forgettableName) (SigT a k))
+                  [TySynInstD demoteName [a]
+                     (foldType (ConT name)
+                        (map (\kv -> AppT demote (SigT anyType (VarT kv)))
+                             tvbNames)),
+                   FunD forgetName
+                        forgetClauses]
+
+  return $ (if (any (\n -> (nameBase n) == "Eq") derivings)
+            then (sEqInst :)
+            else id) $
+             (DataInstD [] singFamilyName [SigT a k] ctors' []) :
+             singEInst :
+             kindedSynInst :
+             singKindInst :
+             ctorInstDecls
+  where mkSingInstanceClause :: Con -> Clause
+        mkSingInstanceClause = ctor1Case
+          (\nm tys ->
+            Clause [ConP nm (replicate (length tys) WildP)]
+                   (NormalB singInstanceDataCon) [])
+
+        mkEqMethClause :: (Con, Con) -> Q Clause
+        mkEqMethClause (c1, c2) =
+          if c1 == c2
+          then do
+            let (name, numArgs) = extractNameArgs c1
+            lnames <- replicateM numArgs (newName "a")
+            rnames <- replicateM numArgs (newName "b")
+            let lpats = map VarP lnames
+                rpats = map VarP rnames
+                lvars = map VarE lnames
+                rvars = map VarE rnames
+            return $ Clause
+              [ConP name lpats, ConP name rpats]
+              (NormalB $
+                allExp (zipWith (\l r -> foldExp (VarE sEqMethName) [l, r])
+                                lvars rvars))
+              []
+          else do
+            let (lname, lNumArgs) = extractNameArgs c1
+                (rname, rNumArgs) = extractNameArgs c2
+            return $ Clause
+              [ConP lname (replicate lNumArgs WildP),
+               ConP rname (replicate rNumArgs WildP)]
+              (NormalB (singDataCon falseName))
+              []
+
+        mkForgetClause :: Con -> Q Clause
+        mkForgetClause c = do
+          let (name, numArgs) = extractNameArgs c
+          varNames <- replicateM numArgs (newName "a")
+          return $ Clause [ConP (singDataConName name) (map VarP varNames)]
+                          (NormalB $ foldExp
+                             (ConE $ (if rep then reinterpret else id) name)
+                             (map (AppE (VarE forgetName) . VarE) varNames))
+                          []
+
+        getBareKinds :: [Con] -> [Kind]
+        getBareKinds = foldl (\res -> ctorCases
+          (\_ _ -> res) -- must be a constant constructor
+          (\tvbs _ _ -> union res (filter isVarK $ map extractTvbKind tvbs)))
+          []
+
+        allExp :: [Exp] -> Exp
+        allExp [] = singDataCon trueName
+        allExp [one] = one
+        allExp (h:t) = AppE (AppE (singVal andName) h) (allExp t)
+
+singKind :: Kind -> Q (Kind -> Kind)
+singKind (ForallT _ _ _) =
+  fail "Singling of explicitly quantified kinds not yet supported"
+singKind (VarT _) = fail "Singling of kind variables not yet supported"
+singKind (ConT _) = fail "Singling of named kinds not yet supported"
+singKind (TupleT _) = fail "Singling of tuple kinds not yet supported"
+singKind (UnboxedTupleT _) = fail "Unboxed tuple used as kind"
+singKind ArrowT = fail "Singling of unsaturated arrow kinds not yet supported"
+singKind ListT = fail "Singling of list kinds not yet supported"
+singKind (AppT (AppT ArrowT k1) k2) = do
+  k1fn <- singKind k1
+  k2fn <- singKind k2
+  k <- newName "k"
+  return $ \f -> AppT (AppT ArrowT (k1fn (VarT k))) (k2fn (AppT f (VarT k)))
+singKind (AppT _ _) = fail "Singling of kind applications not yet supported"
+singKind (SigT _ _) =
+  fail "Singling of explicitly annotated kinds not yet supported"
+singKind (LitT _) = fail "Type literal used as kind"
+singKind (PromotedT _) = fail "Promoted data constructor used as kind"
+singKind (PromotedTupleT _) = fail "Promoted tuple used as kind"
+singKind PromotedNilT = fail "Promoted nil used as kind"
+singKind PromotedConsT = fail "Promoted cons used as kind"
+singKind StarT = return $ \k -> AppT (AppT ArrowT k) StarT
+singKind ConstraintT = fail "Singling of constraint kinds not yet supported"
+
+-- the first parameter is whether or not this type occurs in a positive position
+singType :: Bool -> Type -> Q TypeFn
+singType = singTypeRec []
+
+-- the first parameter is the list of types the current type is applied to
+-- the second parameter is whether or not this type occurs in a positive position
+singTypeRec :: TypeContext -> Bool -> Type -> Q TypeFn
+singTypeRec ctx pos (ForallT tvbs (_:_) ty) =
+  fail "Singling of constrained functions not yet supported"
+singTypeRec (_:_) pos (ForallT _ _ _) =
+  fail "I thought this was impossible in Haskell. Email me at eir@cis.upenn.edu with your code if you see this message."
+singTypeRec [] pos (ForallT _ [] ty) = -- Sing makes handling foralls automatic
+  singTypeRec [] pos ty
+singTypeRec (_:_) pos (VarT _) =
+  fail "Singling of type variables of arrow kinds not yet supported"
+singTypeRec [] pos (VarT name) = 
+  return $ \ty -> AppT singFamily ty
+singTypeRec ctx pos (ConT name) = -- we don't need to process the context with Sing
+  return $ \ty -> AppT singFamily ty
+singTypeRec ctx pos (TupleT n) = -- just like ConT
+  return $ \ty -> AppT singFamily ty
+singTypeRec ctx pos (UnboxedTupleT n) =
+  fail "Singling of unboxed tuple types not yet supported"
+singTypeRec ctx pos ArrowT = case ctx of
+  [ty1, ty2] -> do
+    t <- newName "t"
+    sty1 <- singTypeRec [] (not pos) ty1
+    sty2 <- singTypeRec [] pos ty2
+    k1 <- promoteType ty1
+    -- need a SingKind constraint on all kind variables that appear
+    -- outside of any kind constructor in a negative position (to the
+    -- left of an odd number of arrows)
+    let polykinds = extractPolyKinds (not pos) k1
+    return (\f -> ForallT [KindedTV t k1]
+                          (map (\k -> ClassP singKindClassName [SigT anyType k]) polykinds)
+                          (AppT (AppT ArrowT (sty1 (VarT t)))
+                                (sty2 (AppT f (VarT t)))))
+    where extractPolyKinds :: Bool -> Kind -> [Kind]
+          extractPolyKinds pos (AppT (AppT ArrowT k1) k2) =
+            (extractPolyKinds (not pos) k1) ++ (extractPolyKinds pos k2)
+          extractPolyKinds False (VarT k) = [VarT k]
+          extractPolyKinds _ _ = []
+  _ -> fail "Internal error in Sing: converting ArrowT with improper context"
+singTypeRec ctx pos ListT =
+  return $ \ty -> AppT singFamily ty
+singTypeRec ctx pos (AppT ty1 ty2) =
+  singTypeRec (ty2 : ctx) pos ty1 -- recur with the ty2 in the applied context
+singTypeRec ctx pos (SigT ty knd) =
+  fail "Singling of types with explicit kinds not yet supported"
+singTypeRec ctx pos (LitT _) = fail "Singling of type-level literals not yet supported"
+singTypeRec ctx pos (PromotedT _) =
+  fail "Singling of promoted data constructors not yet supported"
+singTypeRec ctx pos (PromotedTupleT _) =
+  fail "Singling of type-level tuples not yet supported"
+singTypeRec ctx pos PromotedNilT = fail "Singling of promoted nil not yet supported"
+singTypeRec ctx pos PromotedConsT = fail "Singling of type-level cons not yet supported"
+singTypeRec ctx pos StarT = fail "* used as type"
+singTypeRec ctx pos ConstraintT = fail "Constraint used as type"
+
+singClause :: ExpTable -> Clause -> Q Clause
+singClause vars (Clause pats (NormalB exp) []) = do
+  (sPats, vartbl) <- evalForPair $ mapM (singPat Parameter) pats
+  let vars' = Map.union vartbl vars
+  sBody <- normalB $ singExp vars' exp
+  return $ Clause sPats sBody []
+singClause _ (Clause _ (GuardedB _) _) =
+  fail "Singling of guarded patterns not yet supported"
+singClause _ (Clause _ _ (_:_)) =
+  fail "Singling of <<where>> declarations not yet supported"
+
+type ExpsQ = QWithAux ExpTable
+
+-- we need to know where a pattern is to anticipate when
+-- GHC's brain might explode
+data PatternContext = LetBinding
+                    | CaseStatement
+                    | TopLevel
+                    | Parameter
+                    | Statement
+                    deriving Eq
+
+checkIfBrainWillExplode :: PatternContext -> ExpsQ ()
+checkIfBrainWillExplode CaseStatement = return ()
+checkIfBrainWillExplode Statement = return ()
+checkIfBrainWillExplode Parameter = return ()
+checkIfBrainWillExplode _ =
+  fail $ "Can't use a singleton pattern outside of a case-statement or\n" ++
+         "do expression: GHC's brain will explode if you try. (Do try it!)"
+
+-- convert a pattern, building up the lexical scope as we go
+singPat :: PatternContext -> Pat -> ExpsQ Pat
+singPat patCxt (LitP lit) =
+  fail "Singling of literal patterns not yet supported"
+singPat patCxt (VarP name) =
+  let newName = if patCxt == TopLevel then singValName name else name in do
+    addBinding name (VarE newName)
+    return $ VarP newName
+singPat patCxt (TupP pats) =
+  singPat patCxt (ConP (tupleDataName (length pats)) pats)
+singPat patCxt (UnboxedTupP pats) =
+  fail "Singling of unboxed tuples not supported"
+singPat patCxt (ConP name pats) = do
+  checkIfBrainWillExplode patCxt
+  pats' <- mapM (singPat patCxt) pats
+  return $ ConP (singDataConName name) pats'
+singPat patCxt (InfixP pat1 name pat2) = singPat patCxt (ConP name [pat1, pat2])
+singPat patCxt (UInfixP _ _ _) =
+  fail "Singling of unresolved infix patterns not supported"
+singPat patCxt (ParensP _) =
+  fail "Singling of unresolved paren patterns not supported"
+singPat patCxt (TildeP pat) = do
+  pat' <- singPat patCxt pat
+  return $ TildeP pat'
+singPat patCxt (BangP pat) = do
+  pat' <- singPat patCxt pat
+  return $ BangP pat'
+singPat patCxt (AsP name pat) = do
+  let newName = if patCxt == TopLevel then singValName name else name in do
+    pat' <- singPat patCxt pat
+    addBinding name (VarE newName)
+    return $ AsP name pat'
+singPat patCxt WildP = return WildP
+singPat patCxt (RecP name fields) =
+  fail "Singling of record patterns not yet supported"
+singPat patCxt (ListP pats) = do
+  checkIfBrainWillExplode patCxt
+  sPats <- mapM (singPat patCxt) pats
+  return $ foldr (\elt lst -> ConP sconsName [elt, lst]) (ConP snilName []) sPats
+singPat patCxt (SigP pat ty) =
+  fail "Singling of annotated patterns not yet supported"
+singPat patCxt (ViewP exp pat) =
+  fail "Singling of view patterns not yet supported"
+
+singExp :: ExpTable -> Exp -> Q Exp
+singExp vars (VarE name) = case Map.lookup name vars of
+  Just exp -> return exp
+  Nothing -> return (singVal name)
+singExp vars (ConE name) = return $ smartCon name
+singExp vars (LitE lit) =
+  fail "Singling of literal expressions not yet supported"
+singExp vars (AppE exp1 exp2) = do
+  exp1' <- singExp vars exp1
+  exp2' <- singExp vars exp2
+  return $ AppE exp1' exp2'
+singExp vars (InfixE mexp1 exp mexp2) =
+  case (mexp1, mexp2) of
+    (Nothing, Nothing) -> singExp vars exp
+    (Just exp1, Nothing) -> singExp vars (AppE exp exp1)
+    (Nothing, Just exp2) ->
+      fail "Singling of right-only sections not yet supported"
+    (Just exp1, Just exp2) -> singExp vars (AppE (AppE exp exp1) exp2)
+singExp vars (UInfixE _ _ _) =
+  fail "Singling of unresolved infix expressions not supported"
+singExp vars (ParensE _) =
+  fail "Singling of unresolved paren expressions not supported"
+singExp vars (LamE pats exp) = do
+  (pats', vartbl) <- evalForPair $ mapM (singPat Parameter) pats
+  let vars' = Map.union vartbl vars -- order matters; union is left-biased
+  singExp vars' exp
+singExp vars (LamCaseE matches) = 
+  fail "Singling of case expressions not yet supported"
+singExp vars (TupE exps) = do
+  sExps <- mapM (singExp vars) exps
+  sTuple <- singExp vars (ConE (tupleDataName (length exps)))
+  return $ foldExp sTuple sExps
+singExp vars (UnboxedTupE exps) =
+  fail "Singling of unboxed tuple not supported"
+singExp vars (CondE bexp texp fexp) = do
+  exps <- mapM (singExp vars) [bexp, texp, fexp]
+  return $ foldExp (VarE sIfName) exps
+singExp vars (MultiIfE alts) =
+  fail "Singling of multi-way if statements not yet supported"
+singExp vars (LetE decs exp) =
+  fail "Singling of let expressions not yet supported"
+singExp vars (CaseE exp matches) =
+  fail "Singling of case expressions not yet supported"
+singExp vars (DoE stmts) =
+  fail "Singling of do expressions not yet supported"
+singExp vars (CompE stmts) =
+  fail "Singling of list comprehensions not yet supported"
+singExp vars (ArithSeqE range) =
+  fail "Singling of ranges not yet supported"
+singExp vars (ListE exps) = do
+  sExps <- mapM (singExp vars) exps
+  return $ foldr (\x -> (AppE (AppE (VarE smartSconsName) x)))
+                 (VarE smartSnilName) sExps
+singExp vars (SigE exp ty) =
+  fail "Singling of annotated expressions not yet supported"
+singExp vars (RecConE name fields) =
+  fail "Singling of record construction not yet supported"
+singExp vars (RecUpdE exp fields) =
+  fail "Singling of record updates not yet supported"
diff --git a/Data/Singletons/TypeRepStar.hs b/Data/Singletons/TypeRepStar.hs
new file mode 100644
--- /dev/null
+++ b/Data/Singletons/TypeRepStar.hs
@@ -0,0 +1,31 @@
+{- Data/Singletons/TypeRepStar.hs
+
+(c) Richard Eisenberg 2012
+eir@cis.upenn.edu
+
+This file contains the definitions for considering TypeRep to be the demotion
+of *. This is still highly experimental, so expect unusual results!
+
+-}
+
+{-# LANGUAGE RankNTypes, TypeFamilies, KindSignatures, FlexibleInstances,
+             GADTs, UndecidableInstances, ScopedTypeVariables #-}
+
+module Data.Singletons.TypeRepStar where
+
+import Data.Singletons
+import Data.Typeable
+
+data instance Sing (a :: *) where
+  STypeRep :: Typeable a => Sing a
+
+sTypeRep :: forall (a :: *). Typeable a => Sing a
+sTypeRep = STypeRep
+
+instance Typeable a => SingI (a :: *) where
+  sing = STypeRep
+instance SingE (a :: *) where
+  type Demote a = TypeRep
+  fromSing STypeRep = typeOf (undefined :: a)
+instance SingKind (Any :: *) where
+  singInstance STypeRep = SingInstance
diff --git a/Data/Singletons/Util.hs b/Data/Singletons/Util.hs
new file mode 100644
--- /dev/null
+++ b/Data/Singletons/Util.hs
@@ -0,0 +1,165 @@
+{- Data/Singletons/Util.hs
+
+(c) Richard Eisenberg 2012
+eir@cis.upenn.edu
+
+This file contains helper functions internal to the singletons package.
+Users of the package should not need to consult this file.
+-}
+
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+
+module Data.Singletons.Util where
+
+import Language.Haskell.TH
+import Language.Haskell.TH.Syntax
+import Data.Char
+import Data.Maybe
+import Data.Data
+import Data.List
+import Control.Monad
+import Control.Monad.Writer
+import qualified Data.Map as Map
+import Data.Generics
+
+-- reify a declaration, warning the user about splices if the reify fails
+reifyWithWarning :: Name -> Q Info
+reifyWithWarning name = recover
+  (fail $ "Looking up " ++ (show name) ++ " in the list of available " ++
+        "declarations failed.\nThis lookup fails if the declaration " ++
+        "referenced was made in same Template\nHaskell splice as the use " ++
+        "of the declaration. If this is the case, put\nthe reference to " ++
+        "the declaration in a new splice.")
+  (reify name)
+
+-- check if a string is the name of a tuple
+isTupleString :: String -> Bool
+isTupleString s =
+  (length s > 1) &&
+  (head s == '(') &&
+  (last s == ')') &&
+  ((length (takeWhile (== ',') (tail s))) == ((length s) - 2))
+
+-- check if a name is a tuple name
+isTupleName :: Name -> Bool
+isTupleName = isTupleString . nameBase
+
+-- extract the degree of a tuple
+tupleDegree :: String -> Int
+tupleDegree "()" = 0
+tupleDegree s = length s - 1
+
+-- reduce the four cases of a 'Con' to just two: monomorphic and polymorphic
+-- and convert 'StrictType' to 'Type'
+ctorCases :: (Name -> [Type] -> a) -> ([TyVarBndr] -> Cxt -> Con -> a) -> Con -> a
+ctorCases genFun forallFun ctor = case ctor of
+  NormalC name stypes -> genFun name (map snd stypes)
+  RecC name vstypes -> genFun name (map (\(_,_,ty) -> ty) vstypes)
+  InfixC (_,ty1) name (_,ty2) -> genFun name [ty1, ty2]
+  ForallC [] [] ctor' -> ctorCases genFun forallFun ctor'
+  ForallC tvbs cx ctor' -> forallFun tvbs cx ctor' 
+
+-- reduce the four cases of a 'Con' to just 1: a polymorphic Con is treated
+-- as a monomorphic one
+ctor1Case :: (Name -> [Type] -> a) -> Con -> a
+ctor1Case mono = ctorCases mono (\_ _ ctor -> ctor1Case mono ctor)
+
+-- extract the name and number of arguments to a constructor
+extractNameArgs :: Con -> (Name, Int)
+extractNameArgs = ctor1Case (\name tys -> (name, length tys))
+
+-- reinterpret a name. This is useful when a Name has an associated
+-- namespace that we wish to forget
+reinterpret :: Name -> Name
+reinterpret = mkName . nameBase
+
+-- is an identifier uppercase?
+isUpcase :: Name -> Bool
+isUpcase n = let first = head (nameBase n) in isUpper first || first == ':'
+
+-- make an identifier uppercase
+upcase :: Name -> Name
+upcase n =
+  let str = nameBase n 
+      first = head str in
+    if isLetter first
+     then mkName ((toUpper first) : tail str)
+     else mkName (':' : str)
+
+-- make an identifier lowercase
+locase :: Name -> Name
+locase n =
+  let str = nameBase n
+      first = head str in
+    if isLetter first
+     then mkName ((toLower first) : tail str)
+     else mkName (tail str) -- remove the ":"
+
+-- put an uppercase prefix on a name. Takes two prefixes: one for identifiers
+-- and one for symbols
+prefixUCName :: String -> String -> Name -> Name
+prefixUCName pre tyPre n = case (nameBase n) of
+    (':' : rest) -> mkName (tyPre ++ rest)
+    alpha -> mkName (pre ++ alpha)
+
+-- put a lowercase prefix on a name. Takes two prefixes: one for identifiers
+-- and one for symbols
+prefixLCName :: String -> String -> Name -> Name
+prefixLCName pre tyPre n =
+  let str = nameBase n
+      first = head str in
+    if isLetter first
+     then mkName (pre ++ str)
+     else mkName (tyPre ++ str)
+
+-- extract the name from a TyVarBndr
+extractTvbName :: TyVarBndr -> Name
+extractTvbName (PlainTV n) = n
+extractTvbName (KindedTV n _) = n
+
+-- extract the kind from a TyVarBndr. Returns '*' by default.
+extractTvbKind :: TyVarBndr -> Kind
+extractTvbKind (PlainTV _) = StarT -- FIXME: This seems wrong.
+extractTvbKind (KindedTV _ k) = k
+
+-- apply a type to a list of types
+foldType :: Type -> [Type] -> Type
+foldType = foldl AppT
+
+-- apply an expression to a list of expressions
+foldExp :: Exp -> [Exp] -> Exp
+foldExp = foldl AppE
+
+-- is a kind a variable?
+isVarK :: Kind -> Bool
+isVarK (VarT _) = True
+isVarK _ = False
+
+-- a monad transformer for writing a monoid alongside returning a Q
+type QWithAux m = WriterT m Q
+
+-- run a computation with an auxiliary monoid, discarding the monoid result
+evalWithoutAux :: QWithAux m a -> Q a
+evalWithoutAux = liftM fst . runWriterT
+
+-- run a computation with an auxiliary monoid, returning only the monoid result
+evalForAux :: QWithAux m a -> Q m
+evalForAux = execWriterT
+
+-- run a computation with an auxiliary monoid, return both the result
+-- of the computation and the monoid result
+evalForPair :: QWithAux m a -> Q (a, m)
+evalForPair = runWriterT
+
+-- in a computation with an auxiliary map, add a binding to the map
+addBinding :: Ord k => k -> v -> QWithAux (Map.Map k v) ()
+addBinding k v = tell (Map.singleton k v)
+
+-- in a computation with an auxiliar list, add an element to the list
+addElement :: elt -> QWithAux [elt] ()
+addElement elt = tell [elt]
+
+-- does a TH structure contain a name?
+containsName :: Data a => Name -> a -> Bool
+containsName n = everything (||) (mkQ False (== n))
+
diff --git a/README b/README
--- a/README
+++ b/README
@@ -3,7 +3,7 @@
 
 This is the README file for the singletons library. This file contains all the
 documentation for the definitions and functions in the library. As of the time
-of this writing (June 2, 2012), haddock has not quite caught up with GHC in
+of this writing (September 12, 2012), haddock has not quite caught up with GHC in
 handling kind-polymorphic code, and the HEAD version of haddock cannot process
 Template Haskell. Thus, the documentation is in here. In the future, it will
 be generated by haddock.
@@ -25,7 +25,7 @@
 Compatibility
 -------------
 
-The singletons library requires GHC version 7.5.20120529 or greater.
+The singletons library requires GHC version 7.6.1 or greater.
 Any code that uses the singleton generation primitives will also need
 to enable a long list of GHC extensions. This list includes, but
 is not necessarily limited to, the following:
@@ -52,7 +52,7 @@
 These functions should all be used within top-level Template Haskell splices.
 See #supported-features# for a list of what Haskell constructs are supported.
 
-These functions are all defined in Singletons.Lib.
+These functions are all defined in Data.Singletons.
 
 
 genPromotion :: [Name] -> Q [Dec]
@@ -316,12 +316,14 @@
 ----------------------------
 Supported Haskell constructs
 ----------------------------
+#supported-features#
 
 The following constructs are fully supported:
 
 * variables
 * tuples
 * constructors
+* if statements
 * infix expressions
 * !, ~, and _ patterns
 * aliased patterns (except at top-level)
@@ -353,7 +355,17 @@
 
 See the paper cited above for reasons why these are problematic.
 
+As described briefly in the paper, the singletons generation mechanism does not
+currently work for higher-order datatypes (though higher-order functions are
+just peachy). So, if you have a declaration such as
 
+> data Foo = Bar (Bool -> Maybe Bool)
+
+, its singleton will not work correctly. It turns out that getting this to work
+requires fairly thorough changes to the whole singleton generation scheme.
+Please shout (to eir@cis.upenn.edu) if you have a compelling use case for this
+and I can take a look at it. No promises, though.
+
 -------------
 Support for *
 -------------
@@ -364,7 +376,7 @@
 updated for this to really work out. In the meantime, users who wish to
 experiment with this feature have two options:
 
-1) The module Singletons.TypeRepStar has all the definitions possible for
+1) The module Data.Singletons.TypeRepStar has all the definitions possible for
 making * the promoted version of TypeRep, as TypeRep is currently implemented.
 The singleton associated with TypeRep has one constructor:
 
@@ -397,7 +409,7 @@
 >   SBool :: Sing Bool
 >   SMaybe :: SingRep a => Sing a -> Sing (Maybe a)
 
-The expected part is that @Nat@, @Bool@, and @Maybe@ above are the real @Nat@,
+The unexpected part is that @Nat@, @Bool@, and @Maybe@ above are the real @Nat@,
 @Bool@, and @Maybe@, not just promoted data constructors.
 
 
diff --git a/Singletons/CustomStar.hs b/Singletons/CustomStar.hs
deleted file mode 100644
--- a/Singletons/CustomStar.hs
+++ /dev/null
@@ -1,91 +0,0 @@
-{- Singletons/CustomStar.hs
-
-(c) Richard Eisenbeg 2012
-eir@cis.upenn.edu
-
-This file implements singletonStar, which generates a datatype Rep and associated
-singleton from a list of types. The promoted version of Rep is kind * and the
-Haskell types themselves. This is still very experimental, so expect unusual
-results!
--} 
-
-{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
-
-module Singletons.CustomStar where
-
-import Language.Haskell.TH
-import Singletons.Util
-import Singletons.Promote
-import Singletons.Singletons
-import Control.Monad
-
--- Produce a representation and singleton for the collection of types given
-singletonStar :: [Name] -> Q [Dec]
-singletonStar names = do
-  kinds <- mapM getKind names
-  ctors <- zipWithM (mkCtor True) names kinds
-  let repDecl = DataD [] repName [] ctors
-                      [mkName "Eq", mkName "Show", mkName "Read"]
-  fakeCtors <- zipWithM (mkCtor False) names kinds
-  eqTypeInstances <- mapM mkEqTypeInstance [ (c1, c2) | c1 <- fakeCtors,
-                                                        c2 <- fakeCtors ]
-  singletonDecls <- singDataD True [] repName [] fakeCtors
-                              [mkName "Eq", mkName "Show", mkName "Read"]
-  return $ repDecl :
-           eqTypeInstances ++
-           singletonDecls
-  where -- get the kinds of the arguments to the tycon with the given name
-        getKind :: Name -> Q [Kind]
-        getKind name = do
-          info <- reifyWithWarning name
-          case info of
-            TyConI (DataD (_:_) _ _ _ _) ->
-               fail "Cannot make a representation of a constrainted data type"
-            TyConI (DataD [] _ tvbs _ _) ->
-               return $ map extractTvbKind tvbs
-            TyConI (NewtypeD (_:_) _ _ _ _) ->
-               fail "Cannot make a representation of a constrainted newtype"
-            TyConI (NewtypeD [] _ tvbs _ _) ->
-               return $ map extractTvbKind tvbs
-            TyConI (TySynD _ tvbs _) ->
-               return $ map extractTvbKind tvbs
-            PrimTyConI _ n _ ->
-               return $ replicate n StarT
-            _ -> fail $ "Invalid thing for representation: " ++ (show name)
-        
-        -- first parameter is whether this is a real ctor (with a fresh name)
-        -- or a fake ctor (when the name is actually a Haskell type)
-        mkCtor :: Bool -> Name -> [Kind] -> Q Con
-        mkCtor real name args = do
-          (types, vars) <- evalForPair $ mapM kindToType args
-          let ctor = NormalC ((if real then reinterpret else id) name)
-                             (map (\ty -> (NotStrict, ty)) types)
-          if length vars > 0
-            then return $ ForallC (map PlainTV vars) [] ctor
-            else return ctor
-
-        -- demote a kind back to a type, accumulating any unbound parameters
-        kindToType :: Kind -> QWithAux [Name] Type
-        kindToType (ForallT _ _ _) = fail "Explicit forall encountered in kind"
-        kindToType (AppT k1 k2) = do
-          t1 <- kindToType k1
-          t2 <- kindToType k2
-          return $ AppT t1 t2
-        kindToType (SigT _ _) = fail "Sort signature encountered in kind"
-        kindToType (VarT n) = do
-          addElement n
-          return $ VarT n
-        kindToType (ConT n) = return $ ConT n
-        kindToType (PromotedT _) = fail "Promoted type used as a kind"
-        kindToType (TupleT n) = return $ TupleT n
-        kindToType (UnboxedTupleT _) = fail "Unboxed tuple kind encountered"
-        kindToType ArrowT = return ArrowT
-        kindToType ListT = return ListT
-        kindToType (PromotedTupleT _) = fail "Promoted tuple kind encountered"
-        kindToType PromotedNilT = fail "Promoted nil kind encountered"
-        kindToType PromotedConsT = fail "Promoted cons kind encountered"
-        kindToType StarT = return $ ConT repName
-        kindToType ConstraintT =
-          fail $ "Cannot make a representation of a type that has " ++
-                 "an argument of kind Constraint"
-        kindToType (LitT _) = fail "Literal encountered at the kind level"
diff --git a/Singletons/Lib.hs b/Singletons/Lib.hs
deleted file mode 100644
--- a/Singletons/Lib.hs
+++ /dev/null
@@ -1,159 +0,0 @@
-{- Singletons/Lib.hs
-
-(c) Richard Eisenberg 2012
-eir@cis.upenn.edu
-
-This is the public interface file to the singletons library. Please
-see the accompanying README file for more information. Haddock is
-not currently compatible with the features used here, so the documentation
-is all in the README file and /Dependently typed programming with singletons/,
-available at <http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf>
--}
-
-{-# LANGUAGE TypeFamilies, GADTs, KindSignatures, TemplateHaskell,
-             DataKinds, PolyKinds, TypeOperators, MultiParamTypeClasses,
-             FlexibleContexts, RankNTypes, UndecidableInstances,
-             FlexibleInstances, ScopedTypeVariables
- #-}
-{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
-
-module Singletons.Lib (
-  Any,
-  Demote, Sing(..), SingI, sing, SingE, fromSing, SingRep, (:==), (:==:),
-  SingInstance(..), SingKind, singInstance,
-  sTrue, sFalse, SBool, sNothing, sJust, SMaybe, sLeft, sRight, SEither,
-  sTuple0, sTuple2, sTuple3, sTuple4, sTuple5, sTuple6, sTuple7,
-  STuple0, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7,
-  Not, sNot, (:&&), (%:&&), (:||), (%:||), (:&&:), (:||:), (:/=), (:/=:),
-  SEq, (%==%), (%/=%), (%:==), (%:/=),
-  If, sIf, 
-  sNil, sCons, SList, (:++), (%:++), Head, Tail,
-  cases, bugInGHC,
-  genSingletons, singletons, genPromotions, promote,
-  ) where
-
-import Prelude hiding ((++))
-import Singletons.Singletons
-import Singletons.Promote
-import Language.Haskell.TH
-import GHC.Exts
-import Singletons.Util
-
--- Declarations of singleton structures
-data family Sing (a :: k)
-class SingI (a :: k) where
-  sing :: Sing a
-class SingE (a :: k) where
-  type Demote a :: *
-  fromSing :: Sing a -> Demote (Any :: k)
-
--- SingRep is a synonym for (SingI, SingE)
-class (SingI a, SingE a) => SingRep a
-instance (SingI a, SingE a) => SingRep a
-
-type family (a :: k) :==: (b :: k) :: Bool
-type a :== b = a :==: b -- :== and :==: are synonyms
-
-data SingInstance (a :: k) where
-  SingInstance :: SingRep a => SingInstance a
-class (b ~ Any) => SingKind (b :: k) where
-  singInstance :: forall (a :: k). Sing a -> SingInstance a
-
--- provide a few useful singletons...
-$(genSingletons [''Bool, ''Maybe, ''Either, ''[]])
-$(genSingletons [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)])
-
--- ... with some functions over Booleans
-$(singletons [d|
-  not :: Bool -> Bool
-  not False = True
-  not True  = False
-
-  (&&) :: Bool -> Bool -> Bool
-  False && a = False
-  True  && a = a
-
-  (||) :: Bool -> Bool -> Bool
-  False || a = a
-  True  || a = True
-  |])
-
--- symmetric syntax synonyms
-type a :&&: b = a :&& b
-type a :||: b = a :|| b
-
-type a :/=: b = Not (a :==: b)
-type a :/= b = a :/=: b
-
--- the singleton analogue of @Eq@
-class (t ~ Any) => SEq (t :: k) where
-  (%==%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :==: b)
-  (%:==) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :==: b)
-  (%:==) = (%==%)
-  (%:/=) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/=: b)
-  a %:/= b = sNot (a %==% b)
-  (%/=%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/=: b)
-  (%/=%) = (%:/=)
-
--- type-level conditional
-type family If (a :: Bool) (b :: k) (c :: k) :: k
-type instance If 'True b c = b
-type instance If 'False b c = c
-
--- singleton conditional
-sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
-sIf STrue b c = b
-sIf SFalse b c = c
-
-type instance '[] :==: '[] = True
-type instance '[] :==: (h ': t) = False
-type instance (h ': t) :==: '[] = False
-type instance (h ': t) :==: (h' ': t') = (h :==: h') :&&: (t :==: t')
-
-instance SEq (Any :: k) => SEq (Any :: [k]) where
-  SNil %==% SNil = STrue
-  SNil %==% (SCons _ _) = SFalse
-  (SCons _ _) %==% SNil = SFalse
-  (SCons a b) %==% (SCons a' b') = (a %==% a') %:&& (b %==% b')
-
-type family Head (a :: [k]) :: k
-type instance Head (h ': t) = h
-
-type family Tail (a :: [k]) :: [k]
-type instance Tail (h ': t) = t
-
--- must handle (++) by hand because of bug in module interface system
--- when kind-polymorphic code is produced by Template Haskell
-(++) :: [a] -> [a] -> [a]
-[] ++ a = a
-(h:t) ++ a = h:(t ++ a)
-
-type family (a :: [k]) :++ (b :: [k]) :: [k]
-type instance '[] :++ a = a
-type instance (h ': t) :++ a = (h ': (t :++ a))
-
-(%:++) :: Sing a -> Sing b -> Sing (a :++ b)
-SNil %:++ a = a
-(SCons h t) %:++ a = sCons h (t %:++ a)
-
--- allows for automatic checking of all constructors in a GADT for instance
--- inference
-cases :: Name -> Q Exp -> Q Exp -> Q Exp
-cases tyName expq bodyq = do
-  info <- reifyWithWarning tyName
-  case info of
-    TyConI (DataD _ _ _ ctors _) -> buildCases ctors
-    TyConI (NewtypeD _ _ _ ctor _) -> buildCases [ctor]
-    _ -> fail $ "Using <<cases>> with something other than a type constructor: "
-                ++ (show tyName)
-  where buildCases :: [Con] -> Q Exp
-        buildCases ctors =
-          caseE expq (map ((flip (flip match (normalB bodyq)) []) . conToPat) ctors)
-
-        conToPat :: Con -> Q Pat
-        conToPat = ctor1Case
-          (\name tys -> conP name (replicate (length tys) wildP))
-
--- useful when suppressing GHC's warnings about incomplete pattern matches
-bugInGHC :: forall a. a
-bugInGHC = error "Bug encountered in GHC -- this should never happen"
diff --git a/Singletons/Promote.hs b/Singletons/Promote.hs
deleted file mode 100644
--- a/Singletons/Promote.hs
+++ /dev/null
@@ -1,548 +0,0 @@
-{- Singletons/Promote.hs
-
-(c) Richard Eisenberg 2012
-eir@cis.upenn.edu
-
-This file contains functions to promote term-level constructs to the
-type level. It is an internal module to the singletons package.
--}
-
-{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
-
-module Singletons.Promote where
-
-import Language.Haskell.TH
-import Singletons.Util
-import Prelude hiding (exp)
-import qualified Data.Map as Map
-import qualified Data.Set as Set
-import Control.Monad
-import Data.Maybe
-import Control.Monad.Writer
-import Data.List
-
-anyTypeName, falseName, trueName, andName, tyEqName, repName, ifName,
-  headName, tailName :: Name
-anyTypeName = mkName "Any"
-falseName = mkName "False"
-trueName = mkName "True"
-andName = mkName "&&"
-tyEqName = mkName ":==:"
-repName = mkName "Rep"
-ifName = mkName "If"
-headName = mkName "Head"
-tailName = mkName "Tail"
-
-falseTy :: Type
-falseTy = promoteDataCon falseName
-
-trueTy :: Type
-trueTy = promoteDataCon trueName
-
-andTy :: Type
-andTy = promoteVal andName
-
-ifTyFam :: Type
-ifTyFam = ConT ifName
-
-headTyFam :: Type
-headTyFam = ConT headName
-
-tailTyFam :: Type
-tailTyFam = ConT tailName
-
-genPromotions :: [Name] -> Q [Dec]
-genPromotions names = do
-  checkForRep names
-  infos <- mapM reifyWithWarning names
-  decls <- mapM promoteInfo infos
-  return $ concat decls
-
-promoteInfo :: Info -> Q [Dec]
-promoteInfo (ClassI dec instances) =
-  fail "Promotion of class info not supported"
-promoteInfo (ClassOpI name ty className fixity) =
-  fail "Promotion of class members info not supported"
-promoteInfo (TyConI dec) = evalWithoutAux $ promoteDec Map.empty dec
-promoteInfo (FamilyI dec instances) =
-  fail "Promotion of type family info not yet supported" -- KindFams
-promoteInfo (PrimTyConI name numArgs unlifted) =
-  fail "Promotion of primitive type constructors not supported"
-promoteInfo (DataConI name ty tyname fixity) =
-  fail $ "Promotion of individual constructors not supported; " ++
-         "promote the type instead"
-promoteInfo (VarI name ty mdec fixity) =
-  fail "Promotion of value info not supported"
-promoteInfo (TyVarI name ty) =
-  fail "Promotion of type variable info not supported"
-
-promoteDataCon :: Name -> Type
-promoteDataCon name =
-  if isTupleName name
-    then PromotedTupleT (tupleDegree $ nameBase name)
-    else PromotedT name
-
-promoteValName :: Name -> Name
-promoteValName n
-  | nameBase n == "undefined" = anyTypeName
-  | otherwise                 = upcase n
-
-promoteVal :: Name -> Type
-promoteVal = ConT . promoteValName
-
-promoteType :: Type -> Q Kind
-promoteType (ForallT tvbs [] ty) = promoteType ty -- ForallKinds
-promoteType (ForallT _ (_:_) _) = fail "Cannot promote type with constrained variables"
-promoteType (VarT name) = return $ VarT name
-promoteType (ConT name) = return $ if (nameBase name) == "TypeRep" ||
-                                      (nameBase name) == (nameBase repName)
-                                     then StarT else ConT name
-promoteType (TupleT n) = return $ TupleT n
-promoteType (UnboxedTupleT n) = fail "Promotion of unboxed tuples not supported"
-promoteType ArrowT = return ArrowT
-promoteType ListT = return ListT
-promoteType (AppT (AppT ArrowT (ForallT (_:_) _ _)) _) =
-  fail "Cannot promote types of rank above 1."
-promoteType (AppT ty1 ty2) = do
-  k1 <- promoteType ty1
-  k2 <- promoteType ty2
-  return $ AppT k1 k2
-promoteType (SigT ty _) = fail "Cannot promote type of kind other than *"
-promoteType (LitT _) = fail "Cannot promote a type-level literal"
-promoteType (PromotedT _) = fail "Cannot promote a promoted data constructor"
-promoteType (PromotedTupleT _) = fail "Cannot promote tuples that are already promoted"
-promoteType PromotedNilT = fail "Cannot promote a nil that is already promoted"
-promoteType PromotedConsT = fail "Cannot promote a cons that is already promoted"
-promoteType StarT = fail "* used as a type"
-promoteType ConstraintT = fail "Constraint used as a type"
-
--- a table to keep track of variable->type mappings
-type TypeTable = Map.Map Name Type
-
--- Promote each declaration in a splice
-promote :: Q [Dec] -> Q [Dec]
-promote qdec = do
-  decls <- qdec
-  (promDecls, _) <- promoteDecs decls
-  return $ decls ++ promDecls
-
-checkForRep :: [Name] -> Q ()
-checkForRep names =
-  when (any ((== nameBase repName) . nameBase) names)
-    (fail $ "A data type named <<Rep>> is a special case.\n" ++
-            "Promoting it will not work as expected.\n" ++
-            "Please choose another name for your data type.")
-
-checkForRepInDecls :: [Dec] -> Q ()
-checkForRepInDecls decls =
-  checkForRep (map extractNameFromDec decls)
-  where extractNameFromDec :: Dec -> Name
-        extractNameFromDec (DataD _ name _ _ _) = name
-        extractNameFromDec (NewtypeD _ name _ _ _) = name
-        extractNameFromDec (TySynD name _ _) = name
-        extractNameFromDec (FamilyD _ name _ _) = name
-        extractNameFromDec _ = mkName "NotRep"
-
--- Promote a list of declarations; returns the promoted declarations
--- and a list of names of declarations without accompanying type signatures.
--- (This list is needed by singletons to strike such definitions.)
-
--- Promoting declarations proceeds in two stages:
--- 1) Promote everything except type signatures
--- 2) Promote type signatures. This must be done in a second pass because
---    a function type signature gets promoted to a type family declaration.
---    Although function signatures do not differentiate between uniform parameters
---    and non-uniform parameters, type family declarations do. We need
---    to process a function's definition to get the count of non-uniform
---    parameters before producing the type family declaration.
---    At this point, any function written without a type signature is rejected
---    and removed.
-promoteDecs :: [Dec] -> Q ([Dec], [Name])
-promoteDecs decls = do
-  checkForRepInDecls decls
-  let vartbl = Map.empty
-  (newDecls, numArgsTable) <- evalForPair $ mapM (promoteDec vartbl) decls
-  (declss, namess) <- mapAndUnzipM (promoteDec' numArgsTable) decls
-  let moreNewDecls = concat declss
-      names = concat namess
-      noTypeSigs = Set.toList $ Set.difference (Map.keysSet $
-                                                  Map.filter (>= 0) numArgsTable)
-                                               (Set.fromList names)
-      noTypeSigsPro = map promoteValName noTypeSigs
-      newDecls' = foldl (\decls name ->
-                          filter (not . (containsName name)) decls)
-                        (concat newDecls) (noTypeSigs ++ noTypeSigsPro)
-  mapM_ (\n -> reportWarning $ "No type binding for " ++ (show (nameBase n)) ++
-                               "; removing all declarations including it")
-        noTypeSigs
-  return (newDecls' ++ moreNewDecls, noTypeSigs)
-
--- produce the type instance for (:==:) for the given pair of constructors
-mkEqTypeInstance :: (Con, Con) -> Q Dec
-mkEqTypeInstance (c1, c2) =
-  if c1 == c2
-  then do
-    let (name, numArgs) = extractNameArgs c1
-    lnames <- replicateM numArgs (newName "a")
-    rnames <- replicateM numArgs (newName "b")
-    let lvars = map VarT lnames
-        rvars = map VarT rnames
-    return $ TySynInstD
-      tyEqName
-      [foldType (PromotedT name) lvars,
-       foldType (PromotedT name) rvars]
-      (tyAll (zipWith (\l r -> foldType (ConT tyEqName) [l, r])
-                      lvars rvars))
-  else do
-    let (lname, lNumArgs) = extractNameArgs c1
-        (rname, rNumArgs) = extractNameArgs c2
-    lnames <- replicateM lNumArgs (newName "a")
-    rnames <- replicateM rNumArgs (newName "b")
-    return $ TySynInstD
-      tyEqName
-      [foldType (PromotedT lname) (map VarT lnames),
-       foldType (PromotedT rname) (map VarT rnames)]
-      falseTy
-  where tyAll :: [Type] -> Type -- "all" at the type level
-        tyAll [] = trueTy
-        tyAll [one] = one
-        tyAll (h:t) = foldType andTy [h, (tyAll t)]
-
--- keeps track of the number of non-uniform parameters to promoted values
-type NumArgsTable = Map.Map Name Int
-type NumArgsQ = QWithAux NumArgsTable
-
--- used when a type is declared as a type synonym, not a type family
--- no need to declare "type family ..." for these
-typeSynonymFlag :: Int
-typeSynonymFlag = -1
-
-promoteDec :: TypeTable -> Dec -> NumArgsQ [Dec]
-promoteDec vars (FunD name clauses) = do
-  let proName = promoteValName name
-      vars' = Map.insert name (promoteVal name) vars
-      numArgs = getNumPats (head clauses) -- count the parameters
-      -- Haskell requires all clauses to have the same number of parameters
-  instDecls <- lift $ mapM (promoteClause vars' proName) clauses
-  addBinding name numArgs -- remember the number of parameters
-  return $ concat instDecls
-  where getNumPats :: Clause -> Int
-        getNumPats (Clause pats _ _) = length pats
-promoteDec vars (ValD pat body decs) = do
-  -- see also the comment for promoteTopLevelPat
-  when (length decs > 0)
-    (fail $ "Promotion of global variable with <<where>> clause " ++
-                "not yet supported")
-  (rhs, decls) <- lift $ evalForPair $ promoteBody vars body
-  (lhss, decls') <- lift $ evalForPair $ promoteTopLevelPat pat
-  if any (flip containsName rhs) (map lhsName lhss)
-    then do -- definition is recursive. use type families & require ty sigs
-      mapM (flip addBinding 0) (map lhsRawName lhss)
-      return $ (map (\(LHS _ nm hole) -> TySynInstD nm [] (hole rhs)) lhss) ++
-               decls ++ decls'
-    else do -- definition is not recursive; just use "type" decls
-      mapM (flip addBinding typeSynonymFlag) (map lhsRawName lhss)
-      return $ (map (\(LHS _ nm hole) -> TySynD nm [] (hole rhs)) lhss) ++
-               decls ++ decls'
-promoteDec vars (DataD cxt name tvbs ctors derivings) = 
-  promoteDataD vars cxt name tvbs ctors derivings
-promoteDec vars (NewtypeD cxt name tvbs ctor derivings) =
-  promoteDataD vars cxt name tvbs [ctor] derivings
-promoteDec vars (TySynD name tvbs ty) =
-  fail "Promotion of type synonym declaration not yet supported"
-promoteDec vars (ClassD cxt name tvbs fundeps decs) =
-  fail "Promotion of class declaration not yet supported"
-promoteDec vars (InstanceD cxt ty decs) =
-  fail "Promotion of instance declaration not yet supported"
-promoteDec vars (SigD name ty) = return [] -- handle in promoteDec'
-promoteDec vars (ForeignD fgn) =
-  fail "Promotion of foreign function declaration not yet supported"
-promoteDec vars (InfixD fixity name)
-  | isUpcase name = return [] -- automatic: promoting a type or data ctor
-  | otherwise     = return [InfixD fixity (promoteValName name)] -- value
-promoteDec vars (PragmaD prag) =
-  fail "Promotion of pragmas not yet supported"
-promoteDec vars (FamilyD flavour name tvbs mkind) =
-  fail "Promotion of type and data families not yet supported"
-promoteDec vars (DataInstD cxt name tys ctors derivings) =
-  fail "Promotion of data instances not yet supported"
-promoteDec vars (NewtypeInstD cxt name tys ctors derivings) =
-  fail "Promotion of newtype instances not yet supported"
-promoteDec vars (TySynInstD name tys ty) =
-  fail "Promotion of type synonym instances not yet supported)"
-
--- only need to check if the datatype derives Eq. The rest is automatic.
-promoteDataD :: TypeTable -> Cxt -> Name -> [TyVarBndr] -> [Con] ->
-                [Name] -> NumArgsQ [Dec]
-promoteDataD vars cxt name tvbs ctors derivings =
-  if any (\n -> (nameBase n) == "Eq") derivings
-    then do
-      let pairs = [ (c1, c2) | c1 <- ctors, c2 <- ctors ]
-      lift $ mapM mkEqTypeInstance pairs
-    else return [] -- the actual promotion is automatic
-
--- second pass through declarations to deal with type signatures
--- returns the new declarations and the list of names that have been
--- processed
-promoteDec' :: NumArgsTable -> Dec -> Q ([Dec], [Name])
-promoteDec' nat (SigD name ty) = case Map.lookup name nat of
-  Nothing -> fail $ "Type declaration is missing its binding: " ++ (show name)
-  Just numArgs -> 
-    -- if there are no args, then use a type synonym, not a type family
-    -- in the type synonym case, we ignore the type signature
-    if numArgs == typeSynonymFlag then return $ ([], [name]) else do 
-      k <- promoteType ty
-      let ks = unravel k
-          (argKs, resultKs) = splitAt numArgs ks -- divide by uniformity
-      resultK <- ravel resultKs -- rebuild the arrow kind
-      tyvarNames <- mapM newName (replicate (length argKs) "a")
-      return ([FamilyD TypeFam
-                       (promoteValName name)
-                       (zipWith KindedTV tyvarNames argKs)
-                       (Just resultK)], [name])
-    where unravel :: Kind -> [Kind] -- get argument kinds from an arrow kind
-          unravel (AppT (AppT ArrowT k1) k2) =
-            let ks = unravel k2 in k1 : ks
-          unravel k = [k]
-          
-          ravel :: [Kind] -> Q Kind
-          ravel [] = fail "Internal error: raveling nil"
-          ravel [k] = return k
-          ravel (h:t) = do
-            k <- ravel t
-            return $ (AppT (AppT ArrowT h) k)
-promoteDec' _ _ = return ([], [])
-
-promoteClause :: TypeTable -> Name -> Clause -> Q [Dec]
-promoteClause vars name (Clause pats body []) = do
-  -- promoting the patterns creates variable bindings. These are passed
-  -- to the function promoted the RHS
-  (types, vartbl) <- evalForPair $ mapM promotePat pats
-  let vars' = Map.union vars vartbl
-  (ty, decls) <- evalForPair $ promoteBody vars' body
-  return $ decls ++ [TySynInstD name types ty]
-promoteClause _ _ (Clause _ _ (_:_)) =
-  fail "A <<where>> clause in a function definition is not yet supported"
-
--- the LHS of a top-level expression is a name and "type with hole"
--- the hole is filled in by the RHS
-data TopLevelLHS = LHS { lhsRawName :: Name -- the unpromoted name
-                       , lhsName :: Name
-                       , lhsHole :: Type -> Type
-                       }
-
--- Treatment of top-level patterns is different from other patterns
--- because type families have type patterns as their LHS. However,
--- it is not possible to use type patterns at the top level, so we
--- have to use other techniques.
-promoteTopLevelPat :: Pat -> QWithDecs [TopLevelLHS]
-promoteTopLevelPat (LitP _) = fail "Cannot declare a global literal."
-promoteTopLevelPat (VarP name) = return [LHS name (promoteValName name) id]
-promoteTopLevelPat (TupP pats) = case length pats of
-  0 -> return [] -- unit as LHS of pattern... ignore
-  1 -> fail "1-tuple encountered during top-level pattern promotion"
-  n -> promoteTopLevelPat (ConP (tupleDataName n) pats)
-promoteTopLevelPat (UnboxedTupP _) =
-  fail "Promotion of unboxed tuples not supported"
-
--- to promote a constructor pattern, we need to create extraction type
--- families to pull out the individual arguments of the constructor
-promoteTopLevelPat (ConP name pats) = do
-  ctorInfo <- lift $ reifyWithWarning name
-  (ctorType, argTypes) <- lift $ extractTypes ctorInfo
-  when (length argTypes /= length pats) $
-    fail $ "Inconsistent data constructor pattern: " ++ (show name) ++ " " ++
-           (show pats)
-  kind <- lift $ promoteType ctorType
-  argKinds <- lift $ mapM promoteType argTypes
-  extractorNamesRaw <- lift $ replicateM (length pats) (newName "Extract")
-
-  -- TH doesn't allow "newName"s to work at the top-level, so we have to
-  -- do this trick to ensure the Extract functions are unique
-  let extractorNames = map (mkName . show) extractorNamesRaw
-  varName <- lift $ newName "a"
-  zipWithM (\nm arg -> addElement $ FamilyD TypeFam
-                                            nm
-                                            [KindedTV varName kind]
-                                            (Just arg))
-           extractorNames argKinds
-  componentNames <- lift $ replicateM (length pats) (newName "a")
-  zipWithM (\extractorName componentName ->
-    addElement $ TySynInstD extractorName
-                            [foldType (promoteDataCon name)
-                                      (map VarT componentNames)]
-                            (VarT componentName))
-    extractorNames componentNames
-
-  -- now we have the extractor families. Use the appropriate families
-  -- in the "holes"
-  promotedPats <- mapM promoteTopLevelPat pats
-  return $ concat $
-    zipWith (\lhslist extractor ->
-               map (\(LHS raw nm hole) -> LHS raw nm
-                                              (hole . (AppT (ConT extractor))))
-                   lhslist)
-            promotedPats extractorNames
-  where extractTypes :: Info -> Q (Type, [Type])
-        extractTypes (DataConI datacon _dataconTy tyname _fixity) = do
-          tyinfo <- reifyWithWarning tyname
-          extractTypesHelper datacon tyinfo
-        extractTypes _ = fail "Internal error: unexpected Info in extractTypes"
- 
-        extractTypesHelper :: Name -> Info -> Q (Type, [Type])
-        extractTypesHelper datacon
-                           (TyConI (DataD _cxt tyname tvbs cons _derivs)) =
-          let mcon = find ((== datacon) . fst . extractNameArgs) cons in
-          case mcon of
-            Nothing -> fail $ "Internal error reifying " ++ (show datacon)
-            Just con -> return (foldType (ConT tyname)
-                                         (map (VarT . extractTvbName) tvbs),
-                                extractConArgs con)
-        extractTypesHelper datacon
-                           (TyConI (NewtypeD cxt tyname tvbs con derivs)) =
-          extractTypesHelper datacon (TyConI (DataD cxt tyname tvbs [con] derivs))
-        extractTypesHelper datacon _ =
-          fail $ "Cannot promote data constructor " ++ (show datacon)
-
-        extractConArgs :: Con -> [Type]
-        extractConArgs = ctor1Case (\_ tys -> tys)
-promoteTopLevelPat (InfixP l name r) = promoteTopLevelPat (ConP name [l, r])
-promoteTopLevelPat (UInfixP _ _ _) =
-  fail "Unresolved infix constructors not supported"
-promoteTopLevelPat (ParensP _) = 
-  fail "Unresolved infix constructors not supported"
-promoteTopLevelPat (TildeP pat) = do
-  lift $ reportWarning "Lazy pattern converted into regular pattern in promotion"
-  promoteTopLevelPat pat
-promoteTopLevelPat (BangP pat) = do
-  lift $ reportWarning "Strict pattern converted into regular pattern in promotion"
-  promoteTopLevelPat pat
-promoteTopLevelPat (AsP name pat) =
-  fail "Promotion of aliased patterns at top level not yet supported"
-promoteTopLevelPat WildP = return []
-promoteTopLevelPat (RecP _ _) =
-  fail "Promotion of record patterns at top level not yet supported"
-
--- must do a similar trick as what is in the ConP case, but this is easier
--- because Lib defined Head and Tail
-promoteTopLevelPat (ListP pats) = do
-  promotedPats <- mapM promoteTopLevelPat pats
-  return $ concat $ snd $
-    mapAccumL (\extractFn lhss ->
-                 ((AppT tailTyFam) . extractFn,
-                  map (\(LHS raw nm hole) ->
-                         LHS raw nm (hole . (AppT headTyFam) . extractFn)) lhss))
-              id promotedPats
-promoteTopLevelPat (SigP pat _) = do
-  lift $ reportWarning $ "Promotion of explicit type annotation in pattern " ++
-                         "not yet supported."
-  promoteTopLevelPat pat
-promoteTopLevelPat (ViewP _ _) =
-  fail "Promotion of view patterns not yet supported"
-
-type TypesQ = QWithAux TypeTable
-
--- promotes a term pattern into a type pattern, accumulating variable
--- binding in the auxiliary TypeTable
-promotePat :: Pat -> TypesQ Type
-promotePat (LitP lit) = fail $ "Promoting literals not supported: " ++ (show lit)
-promotePat (VarP name) = do
-  tyVar <- lift $ newName (nameBase name)
-  addBinding name (VarT tyVar)
-  return $ VarT tyVar
-promotePat (TupP pats) = do
-  types <- mapM promotePat pats
-  let baseTup = PromotedTupleT (length types)
-      tup = foldType baseTup types
-  return tup
-promotePat (UnboxedTupP _) = fail "Unboxed tuples not supported"
-promotePat (ConP name pats) = do
-  types <- mapM promotePat pats
-  let tyCon = foldType (promoteDataCon name) types
-  return tyCon
-promotePat (InfixP pat1 name pat2) = promotePat (ConP name [pat1, pat2])
-promotePat (UInfixP _ _ _) = fail "Unresolved infix constructions not supported"
-promotePat (ParensP _) = fail "Unresolved infix constructions not supported"
-promotePat (TildeP pat) = do
-  lift $ reportWarning "Lazy pattern converted into regular pattern in promotion"
-  promotePat pat
-promotePat (BangP pat) = do
-  lift $ reportWarning "Strict pattern converted into regular pattern in promotion"
-  promotePat pat
-promotePat (AsP name pat) = do
-  ty <- promotePat pat
-  addBinding name ty
-  return ty
-promotePat WildP = do
-  name <- lift $ newName "z"
-  return $ VarT name
-promotePat (RecP _ _) = fail "Promotion of record patterns not yet supported"
-promotePat (ListP pats) = do
-  types <- mapM promotePat pats
-  return $ foldr (\h t -> AppT (AppT PromotedConsT h) t) PromotedNilT types
-promotePat (SigP pat _) = do
-  lift $ reportWarning $ "Promotion of explicit type annotation in pattern " ++
-                         "not yet supported"
-  promotePat pat
-promotePat (ViewP _ _) = fail "View patterns not yet supported"
-
--- promoting a body may produce auxiliary declarations. Accumulate these.
-type QWithDecs = QWithAux [Dec]
-
-promoteBody :: TypeTable -> Body -> QWithDecs Type
-promoteBody vars (NormalB exp) = promoteExp vars exp
-promoteBody vars (GuardedB _) =
-  fail "Promoting guards in patterns not yet supported"
-
-promoteExp :: TypeTable -> Exp -> QWithDecs Type
-promoteExp vars (VarE name) = case Map.lookup name vars of
-  Just ty -> return ty
-  Nothing -> return $ promoteVal name
-promoteExp vars (ConE name) = return $ promoteDataCon name
-promoteExp vars (LitE lit) = fail "Promotion of literal expressions not supported"
-promoteExp vars (AppE exp1 exp2) = do
-  ty1 <- promoteExp vars exp1
-  ty2 <- promoteExp vars exp2
-  return $ AppT ty1 ty2
-promoteExp vars (InfixE mexp1 exp mexp2) =
-  case (mexp1, mexp2) of
-    (Nothing, Nothing) -> promoteExp vars exp
-    (Just exp1, Nothing) -> promoteExp vars (AppE exp exp1)
-    (Nothing, Just exp2) ->
-      fail "Promotion of right-only sections not yet supported"
-    (Just exp1, Just exp2) -> promoteExp vars (AppE (AppE exp exp1) exp2)
-promoteExp vars (UInfixE _ _ _) =
-  fail "Promotion of unresolved infix operators not supported"
-promoteExp vars (ParensE _) = fail "Promotion of unresolved parens not supported"
-promoteExp vars (LamE pats exp) =
-  fail "Promotion of lambda expressions not yet supported"
-promoteExp vars (LamCaseE alts) =
-  fail "Promotion of lambda-case expressions not yet supported"
-promoteExp vars (TupE exps) = do
-  tys <- mapM (promoteExp vars) exps
-  let tuple = PromotedTupleT (length tys)
-      tup = foldType tuple tys
-  return tup
-promoteExp vars (UnboxedTupE _) = fail "Promotion of unboxed tuples not supported"
-promoteExp vars (CondE bexp texp fexp) = do
-  tys <- mapM (promoteExp vars) [bexp, texp, fexp]
-  return $ foldType ifTyFam tys
-promoteExp vars (MultiIfE alts) =
-  fail "Promotion of multi-way if not yet supported"
-promoteExp vars (LetE decs exp) =
-  fail "Promotion of let statements not yet supported"
-promoteExp vars (CaseE exp matches) =
-  fail "Promotion of case statements not yet supported"
-promoteExp vars (DoE stmts) = fail "Promotion of do statements not supported"
-promoteExp vars (CompE stmts) =
-  fail "Promotion of list comprehensions not yet supported"
-promoteExp vars (ArithSeqE _) = fail "Promotion of ranges not supported"
-promoteExp vars (ListE exps) = do
-  tys <- mapM (promoteExp vars) exps
-  return $ foldr (\ty lst -> AppT (AppT PromotedConsT ty) lst) PromotedNilT tys
-promoteExp vars (SigE exp ty) =
-  fail "Promotion of explicit type annotations not yet supported"
-promoteExp vars (RecConE name fields) =
-  fail "Promotion of record construction not yet supported"
-promoteExp vars (RecUpdE exp fields) =
-  fail "Promotion of record updates not yet supported"
diff --git a/Singletons/Singletons.hs b/Singletons/Singletons.hs
deleted file mode 100644
--- a/Singletons/Singletons.hs
+++ /dev/null
@@ -1,602 +0,0 @@
-{- Singletons/Singletons.hs
-
-(c) Richard Eisenberg 2012
-eir@cis.upenn.edu
-
-This file contains functions to refine constructs to work with singleton
-types. It is an internal module to the singletons package.
--}
-
-{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
-
-module Singletons.Singletons where
-
-import Language.Haskell.TH
-import Singletons.Util
-import Singletons.Promote
-import qualified Data.Map as Map
-import Control.Monad
-import Control.Monad.Writer
-import Data.List
-
--- map to track bound variables
-type ExpTable = Map.Map Name Exp
-
--- translating a type gives a type with a hole in it,
--- represented here as a function
-type TypeFn = Type -> Type
-
--- a list of argument types extracted from a type application
-type TypeContext = [Type]
-
-singFamilyName, isSingletonName, forgettableName, comboClassName, witnessName,
-  demoteName, singKindClassName, singInstanceMethName, singInstanceName,
-  sEqClassName, sEqMethName, sconsName, snilName, smartSconsName,
-  smartSnilName, sIfName, undefinedName :: Name
-singFamilyName = mkName "Sing"
-isSingletonName = mkName "SingI"
-forgettableName = mkName "SingE"
-comboClassName = mkName "SingRep"
-witnessName = mkName "sing"
-forgetName = mkName "fromSing"
-demoteName = mkName "Demote"
-singKindClassName = mkName "SingKind"
-singInstanceMethName = mkName "singInstance"
-singInstanceName = mkName "SingInstance"
-sEqClassName = mkName "SEq"
-sEqMethName = mkName "%==%"
-sconsName = mkName "SCons"
-snilName = mkName "SNil"
-smartSconsName = mkName "sCons"
-smartSnilName = mkName "sNil"
-sIfName = mkName "sIf"
-undefinedName = mkName "undefined"
-
-mkTupleName :: Int -> Name
-mkTupleName n = mkName $ "STuple" ++ (show n)
-
-singFamily :: Type
-singFamily = ConT singFamilyName
-
-singKindConstraint :: Kind -> Pred
-singKindConstraint k = ClassP singKindClassName [SigT anyType k]
-
-singInstanceMeth :: Exp
-singInstanceMeth = VarE singInstanceMethName
-
-singInstanceTyCon :: Type
-singInstanceTyCon = ConT singInstanceName
-
-singInstanceDataCon :: Exp
-singInstanceDataCon = ConE singInstanceName
-
-singInstancePat :: Pat
-singInstancePat = ConP singInstanceName []
-
-demote :: Type
-demote = ConT demoteName
-
-anyType :: Type
-anyType = ConT anyTypeName
-
-singDataConName :: Name -> Name
-singDataConName nm = case nameBase nm of
-  "[]" -> snilName
-  ":"  -> sconsName
-  tuple | isTupleString tuple -> mkTupleName (tupleDegree tuple)
-  _ -> prefixUCName "S" ":%" nm
-
-singTyConName :: Name -> Name
-singTyConName name | nameBase name == "[]" = mkName "SList"
-                   | isTupleName name = mkTupleName (tupleDegree $ nameBase name)
-                   | otherwise        = prefixUCName "S" ":%" name
-
-singDataCon :: Name -> Exp
-singDataCon = ConE . singDataConName
-
-smartConName :: Name -> Name
-smartConName = locase . singDataConName
-
-smartCon :: Name -> Exp
-smartCon = VarE . smartConName
-
-singValName :: Name -> Name
-singValName n
-  | nameBase n == "undefined" = undefinedName
-  | otherwise                 = (prefixLCName "s" "%") $ upcase n
-
-singVal :: Name -> Exp
-singVal = VarE . singValName
-
--- generate singleton definitions from an ADT
-genSingletons :: [Name] -> Q [Dec]
-genSingletons names = do
-  checkForRep names
-  infos <- mapM reifyWithWarning names
-  decls <- mapM singInfo infos
-  return $ concat decls
-
-singInfo :: Info -> Q [Dec]
-singInfo (ClassI dec instances) =
-  fail "Singling of class info not supported"
-singInfo (ClassOpI name ty className fixity) =
-  fail "Singling of class members info not supported"
-singInfo (TyConI dec) = singDec dec
-singInfo (FamilyI dec instances) =
-  fail "Singling of type family info not yet supported" -- KindFams
-singInfo (PrimTyConI name numArgs unlifted) =
-  fail "Singling of primitive type constructors not supported"
-singInfo (DataConI name ty tyname fixity) =
-  fail $ "Singling of individual constructors not supported; " ++
-         "single the type instead"
-singInfo (VarI name ty mdec fixity) =
-  fail "Singling of value info not supported"
-singInfo (TyVarI name ty) =
-  fail "Singling of type variable info not supported"
-
--- refine a constructor. the first parameter is the type variable that
--- the singleton GADT is parameterized by
--- runs in the QWithDecs monad because auxiliary declarations are produced
-singCtor :: Type -> Con -> QWithDecs Con 
-singCtor a = ctorCases
-  (\name types -> do
-    let sName = singDataConName name
-        sCon = singDataCon name
-        pCon = promoteDataCon name
-    indexNames <- lift $ replicateM (length types) (newName "n")
-    let indices = map VarT indexNames
-    kinds <- lift $ mapM promoteType types
-    args <- lift $ buildArgTypes types indices
-    let tvbs = zipWith KindedTV indexNames kinds
-        bareKindVars = filter isVarK kinds
-
-    -- SingI instance
-    addElement $ InstanceD ((map singKindConstraint bareKindVars) ++
-                            (map (ClassP comboClassName . return) indices))
-                           (AppT (ConT isSingletonName)
-                                 (foldType pCon (zipWith SigT indices kinds)))
-                           [ValD (VarP witnessName)
-                                 (NormalB $ foldExp sCon (replicate (length types)
-                                                           (VarE witnessName)))
-                                 []]
-
-    -- smart constructor type signature
-    smartConType <- lift $ conTypesToFunType indexNames args kinds
-                                      (AppT singFamily (foldType pCon indices))
-    addElement $ SigD (smartConName name) smartConType
-     
-    -- smart constructor
-    let vars = map VarE indexNames
-        smartConBody = mkSingInstances vars (foldExp (singDataCon name) vars)
-    addElement $ FunD (smartConName name)
-                      [Clause (map VarP indexNames)
-                        (NormalB smartConBody)
-                        []]
-
-    return $ ForallC tvbs
-                     ((EqualP a (foldType (promoteDataCon name) indices)) :
-                       (map (ClassP comboClassName . return) indices) ++
-                       (map singKindConstraint bareKindVars))
-                     (NormalC sName $ map (\ty -> (NotStrict,ty)) args))
-  (\tvbs cxt ctor -> case cxt of
-    _:_ -> fail "Singling of constrained constructors not yet supported"
-    [] -> singCtor a ctor)
-  where buildArgTypes :: [Type] -> [Type] -> Q [Type]
-        buildArgTypes types indices = do
-          typeFns <- mapM (singType False) types
-          return $ zipWith id typeFns indices
-
-        conTypesToFunType :: [Name] -> [Type] -> [Kind] -> Type -> Q Type
-        conTypesToFunType [] [] [] ret = return ret
-        conTypesToFunType (nm : nmtail) (ty : tytail) (k : ktail) ret = do
-          rhs <- conTypesToFunType nmtail tytail ktail ret    
-          let innerty = AppT (AppT ArrowT ty) rhs
-          return $ ForallT [KindedTV nm k]
-                           (if isVarK k then [singKindConstraint k] else [])
-                           innerty
-        conTypesToFunType _ _ _ _ =
-          fail "Internal error in conTypesToFunType"
-
-        mkSingInstances :: [Exp] -> Exp -> Exp
-        mkSingInstances [] exp = exp
-        mkSingInstances (var:tail) exp =
-          CaseE (AppE singInstanceMeth var)
-                [Match singInstancePat (NormalB $ mkSingInstances tail exp) []]
-
--- refine the declarations given
-singletons :: Q [Dec] -> Q [Dec]
-singletons qdec = do
-  decls <- qdec
-  singDecs decls
-
-singDecs :: [Dec] -> Q [Dec]
-singDecs decls = do
-  (promDecls, badNames) <- promoteDecs decls
-  -- need to remove the bad names returned from promoteDecs
-  newDecls <- mapM singDec
-                   (filter (\dec ->
-                     not $ or (map (\f -> f dec)
-                              (map containsName badNames))) decls)
-  return $ decls ++ promDecls ++ (concat newDecls)
-
-singDec :: Dec -> Q [Dec]
-singDec (FunD name clauses) = do
-  let sName = singValName name
-      vars = Map.singleton name (VarE sName)
-  liftM return $ funD sName (map (singClause vars) clauses)
-singDec (ValD _ (GuardedB _) _) =
-  fail "Singling of definitions of values with a pattern guard not yet supported"
-singDec (ValD _ _ (_:_)) =
-  fail "Singling of definitions of values with a <<where>> clause not yet supported"
-singDec (ValD pat (NormalB exp) []) = do
-  (sPat, vartbl) <- evalForPair $ singPat TopLevel pat
-  sExp <- singExp vartbl exp
-  return [ValD sPat (NormalB sExp) []]
-singDec (DataD (_:_) _ _ _ _) =
-  fail "Singling of constrained datatypes not supported"
-singDec (DataD cxt name tvbs ctors derivings) =
-  singDataD False cxt name tvbs ctors derivings
-singDec (NewtypeD cxt name tvbs ctor derivings) =
-  singDataD False cxt name tvbs [ctor] derivings
-singDec (TySynD name tvbs ty) =
-  fail "Singling of type synonyms not yet supported"
-singDec (ClassD cxt name tvbs fundeps decs) =
-  fail "Singling of class declaration not yet supported"
-singDec (InstanceD cxt ty decs) =
-  fail "Singling of class instance not yet supported"
-singDec (SigD name ty) = do
-  tyTrans <- singType True ty
-  return [SigD (singValName name) (tyTrans (promoteVal name))]
-singDec (ForeignD fgn) =
-  let name = extractName fgn in do
-    reportWarning $ "Singling of foreign functions not supported -- " ++
-                    (show name) ++ " ignored"
-    return []
-  where extractName :: Foreign -> Name
-        extractName (ImportF _ _ _ n _) = n
-        extractName (ExportF _ _ n _) = n
-singDec (InfixD fixity name)
-  | isUpcase name = return [InfixD fixity (singDataConName name)]
-  | otherwise     = return [InfixD fixity (singValName name)]
-singDec (PragmaD prag) =
-  let name = extractName prag in do
-    reportWarning $ "Singling of pragmas not supported -- " ++
-                    (show name) ++ " ignored"
-    return []
-  where extractName :: Pragma -> Name
-        extractName (InlineP n _) = n
-        extractName (SpecialiseP n _ _) = n
-singDec (FamilyD flavour name tvbs mkind) =
-  fail "Singling of type and data families not yet supported"
-singDec (DataInstD cxt name tys ctors derivings) = 
-  fail "Singling of data instances not yet supported"
-singDec (NewtypeInstD cxt name tys ctor derivings) =
-  fail "Singling of newtype instances not yet supported"
-singDec (TySynInstD name tys ty) =
-  fail "Singling of type family instances not yet supported"
-
--- the first parameter is True when we're refining the special case "Rep"
--- and false otherwise. We wish to consider the promotion of "Rep" to be *
--- not a promoted data constructor.
-singDataD :: Bool -> Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> Q [Dec]
-singDataD rep cxt name tvbs ctors derivings = do
-  aName <- newName "a"
-  let a = VarT aName
-  let tvbNames = map extractTvbName tvbs
-  k <- promoteType (foldType (ConT name) (map VarT tvbNames))
-  (ctors', ctorInstDecls) <- evalForPair $ mapM (singCtor a) ctors
-  
-  -- instance for SingKind
-  let singKindInst =
-        InstanceD []
-                  (AppT (ConT singKindClassName)
-                        (SigT anyType k))
-                  [FunD singInstanceMethName
-                        (map mkSingInstanceClause ctors')]
-  
-  -- SEq instance
-  let ctorPairs = [ (c1, c2) | c1 <- ctors', c2 <- ctors' ]
-  sEqMethClauses <- mapM mkEqMethClause ctorPairs
-  let sEqInst =
-        InstanceD (map (\k -> ClassP sEqClassName [SigT anyType k])
-                       (getBareKinds ctors'))
-                  (AppT (ConT sEqClassName)
-                        (SigT anyType k))
-                  [FunD sEqMethName sEqMethClauses]
-  
-  -- e.g. type SNat (a :: Nat) = Sing a
-  let kindedSynInst =
-        TySynD (singTyConName name)
-               [KindedTV aName k]
-               (AppT singFamily a)
-
-  -- SingE instance
-  forgetClauses <- mapM mkForgetClause ctors
-  let singEInst =
-        InstanceD []
-                  (AppT (ConT forgettableName) (SigT a k))
-                  [TySynInstD demoteName [a]
-                     (foldType (ConT name)
-                        (map (\kv -> AppT demote (SigT anyType (VarT kv)))
-                             tvbNames)),
-                   FunD forgetName
-                        forgetClauses]
-
-  return $ (if (any (\n -> (nameBase n) == "Eq") derivings)
-            then (sEqInst :)
-            else id) $
-             (DataInstD [] singFamilyName [SigT a k] ctors' []) :
-             singEInst :
-             kindedSynInst :
-             singKindInst :
-             ctorInstDecls
-  where mkSingInstanceClause :: Con -> Clause
-        mkSingInstanceClause = ctor1Case
-          (\nm tys ->
-            Clause [ConP nm (replicate (length tys) WildP)]
-                   (NormalB singInstanceDataCon) [])
-
-        mkEqMethClause :: (Con, Con) -> Q Clause
-        mkEqMethClause (c1, c2) =
-          if c1 == c2
-          then do
-            let (name, numArgs) = extractNameArgs c1
-            lnames <- replicateM numArgs (newName "a")
-            rnames <- replicateM numArgs (newName "b")
-            let lpats = map VarP lnames
-                rpats = map VarP rnames
-                lvars = map VarE lnames
-                rvars = map VarE rnames
-            return $ Clause
-              [ConP name lpats, ConP name rpats]
-              (NormalB $
-                allExp (zipWith (\l r -> foldExp (VarE sEqMethName) [l, r])
-                                lvars rvars))
-              []
-          else do
-            let (lname, lNumArgs) = extractNameArgs c1
-                (rname, rNumArgs) = extractNameArgs c2
-            return $ Clause
-              [ConP lname (replicate lNumArgs WildP),
-               ConP rname (replicate rNumArgs WildP)]
-              (NormalB (singDataCon falseName))
-              []
-
-        mkForgetClause :: Con -> Q Clause
-        mkForgetClause c = do
-          let (name, numArgs) = extractNameArgs c
-          varNames <- replicateM numArgs (newName "a")
-          return $ Clause [ConP (singDataConName name) (map VarP varNames)]
-                          (NormalB $ foldExp
-                             (ConE $ (if rep then reinterpret else id) name)
-                             (map (AppE (VarE forgetName) . VarE) varNames))
-                          []
-
-        getBareKinds :: [Con] -> [Kind]
-        getBareKinds = foldl (\res -> ctorCases
-          (\_ _ -> res) -- must be a constant constructor
-          (\tvbs _ _ -> union res (filter isVarK $ map extractTvbKind tvbs)))
-          []
-
-        allExp :: [Exp] -> Exp
-        allExp [] = singDataCon trueName
-        allExp [one] = one
-        allExp (h:t) = AppE (AppE (singVal andName) h) (allExp t)
-
-singKind :: Kind -> Q (Kind -> Kind)
-singKind (ForallT _ _ _) =
-  fail "Singling of explicitly quantified kinds not yet supported"
-singKind (VarT _) = fail "Singling of kind variables not yet supported"
-singKind (ConT _) = fail "Singling of named kinds not yet supported"
-singKind (TupleT _) = fail "Singling of tuple kinds not yet supported"
-singKind (UnboxedTupleT _) = fail "Unboxed tuple used as kind"
-singKind ArrowT = fail "Singling of unsaturated arrow kinds not yet supported"
-singKind ListT = fail "Singling of list kinds not yet supported"
-singKind (AppT (AppT ArrowT k1) k2) = do
-  k1fn <- singKind k1
-  k2fn <- singKind k2
-  k <- newName "k"
-  return $ \f -> AppT (AppT ArrowT (k1fn (VarT k))) (k2fn (AppT f (VarT k)))
-singKind (AppT _ _) = fail "Singling of kind applications not yet supported"
-singKind (SigT _ _) =
-  fail "Singling of explicitly annotated kinds not yet supported"
-singKind (LitT _) = fail "Type literal used as kind"
-singKind (PromotedT _) = fail "Promoted data constructor used as kind"
-singKind (PromotedTupleT _) = fail "Promoted tuple used as kind"
-singKind PromotedNilT = fail "Promoted nil used as kind"
-singKind PromotedConsT = fail "Promoted cons used as kind"
-singKind StarT = return $ \k -> AppT (AppT ArrowT k) StarT
-singKind ConstraintT = fail "Singling of constraint kinds not yet supported"
-
--- the first parameter is whether or not this type occurs in a positive position
-singType :: Bool -> Type -> Q TypeFn
-singType = singTypeRec []
-
--- the first parameter is the list of types the current type is applied to
--- the second parameter is whether or not this type occurs in a positive position
-singTypeRec :: TypeContext -> Bool -> Type -> Q TypeFn
-singTypeRec ctx pos (ForallT tvbs (_:_) ty) =
-  fail "Singling of constrained functions not yet supported"
-singTypeRec (_:_) pos (ForallT _ _ _) =
-  fail "I thought this was impossible in Haskell. Email me at eir@cis.upenn.edu with your code if you see this message."
-singTypeRec [] pos (ForallT _ [] ty) = -- Sing makes handling foralls automatic
-  singTypeRec [] pos ty
-singTypeRec (_:_) pos (VarT _) =
-  fail "Singling of type variables of arrow kinds not yet supported"
-singTypeRec [] pos (VarT name) = 
-  return $ \ty -> AppT singFamily ty
-singTypeRec ctx pos (ConT name) = -- we don't need to process the context with Sing
-  return $ \ty -> AppT singFamily ty
-singTypeRec ctx pos (TupleT n) = -- just like ConT
-  return $ \ty -> AppT singFamily ty
-singTypeRec ctx pos (UnboxedTupleT n) =
-  fail "Singling of unboxed tuple types not yet supported"
-singTypeRec ctx pos ArrowT = case ctx of
-  [ty1, ty2] -> do
-    t <- newName "t"
-    sty1 <- singTypeRec [] (not pos) ty1
-    sty2 <- singTypeRec [] pos ty2
-    k1 <- promoteType ty1
-    -- need a SingKind constraint on all kind variables that appear
-    -- outside of any kind constructor in a negative position (to the
-    -- left of an odd number of arrows)
-    let polykinds = extractPolyKinds (not pos) k1
-    return (\f -> ForallT [KindedTV t k1]
-                          (map (\k -> ClassP singKindClassName [SigT anyType k]) polykinds)
-                          (AppT (AppT ArrowT (sty1 (VarT t)))
-                                (sty2 (AppT f (VarT t)))))
-    where extractPolyKinds :: Bool -> Kind -> [Kind]
-          extractPolyKinds pos (AppT (AppT ArrowT k1) k2) =
-            (extractPolyKinds (not pos) k1) ++ (extractPolyKinds pos k2)
-          extractPolyKinds False (VarT k) = [VarT k]
-          extractPolyKinds _ _ = []
-  _ -> fail "Internal error in Sing: converting ArrowT with improper context"
-singTypeRec ctx pos ListT =
-  return $ \ty -> AppT singFamily ty
-singTypeRec ctx pos (AppT ty1 ty2) =
-  singTypeRec (ty2 : ctx) pos ty1 -- recur with the ty2 in the applied context
-singTypeRec ctx pos (SigT ty knd) =
-  fail "Singling of types with explicit kinds not yet supported"
-singTypeRec ctx pos (LitT _) = fail "Singling of type-level literals not yet supported"
-singTypeRec ctx pos (PromotedT _) =
-  fail "Singling of promoted data constructors not yet supported"
-singTypeRec ctx pos (PromotedTupleT _) =
-  fail "Singling of type-level tuples not yet supported"
-singTypeRec ctx pos PromotedNilT = fail "Singling of promoted nil not yet supported"
-singTypeRec ctx pos PromotedConsT = fail "Singling of type-level cons not yet supported"
-singTypeRec ctx pos StarT = fail "* used as type"
-singTypeRec ctx pos ConstraintT = fail "Constraint used as type"
-
-singClause :: ExpTable -> Clause -> Q Clause
-singClause vars (Clause pats (NormalB exp) []) = do
-  (sPats, vartbl) <- evalForPair $ mapM (singPat Parameter) pats
-  let vars' = Map.union vartbl vars
-  sBody <- normalB $ singExp vars' exp
-  return $ Clause sPats sBody []
-singClause _ (Clause _ (GuardedB _) _) =
-  fail "Singling of guarded patterns not yet supported"
-singClause _ (Clause _ _ (_:_)) =
-  fail "Singling of <<where>> declarations not yet supported"
-
-type ExpsQ = QWithAux ExpTable
-
--- we need to know where a pattern is to anticipate when
--- GHC's brain might explode
-data PatternContext = LetBinding
-                    | CaseStatement
-                    | TopLevel
-                    | Parameter
-                    | Statement
-                    deriving Eq
-
-checkIfBrainWillExplode :: PatternContext -> ExpsQ ()
-checkIfBrainWillExplode CaseStatement = return ()
-checkIfBrainWillExplode Statement = return ()
-checkIfBrainWillExplode Parameter = return ()
-checkIfBrainWillExplode _ =
-  fail $ "Can't use a singleton pattern outside of a case-statement or\n" ++
-         "do expression: GHC's brain will explode if you try. (Do try it!)"
-
--- convert a pattern, building up the lexical scope as we go
-singPat :: PatternContext -> Pat -> ExpsQ Pat
-singPat patCxt (LitP lit) =
-  fail "Singling of literal patterns not yet supported"
-singPat patCxt (VarP name) =
-  let newName = if patCxt == TopLevel then singValName name else name in do
-    addBinding name (VarE newName)
-    return $ VarP newName
-singPat patCxt (TupP pats) =
-  singPat patCxt (ConP (tupleDataName (length pats)) pats)
-singPat patCxt (UnboxedTupP pats) =
-  fail "Singling of unboxed tuples not supported"
-singPat patCxt (ConP name pats) = do
-  checkIfBrainWillExplode patCxt
-  pats' <- mapM (singPat patCxt) pats
-  return $ ConP (singDataConName name) pats'
-singPat patCxt (InfixP pat1 name pat2) = singPat patCxt (ConP name [pat1, pat2])
-singPat patCxt (UInfixP _ _ _) =
-  fail "Singling of unresolved infix patterns not supported"
-singPat patCxt (ParensP _) =
-  fail "Singling of unresolved paren patterns not supported"
-singPat patCxt (TildeP pat) = do
-  pat' <- singPat patCxt pat
-  return $ TildeP pat'
-singPat patCxt (BangP pat) = do
-  pat' <- singPat patCxt pat
-  return $ BangP pat'
-singPat patCxt (AsP name pat) = do
-  let newName = if patCxt == TopLevel then singValName name else name in do
-    pat' <- singPat patCxt pat
-    addBinding name (VarE newName)
-    return $ AsP name pat'
-singPat patCxt WildP = return WildP
-singPat patCxt (RecP name fields) =
-  fail "Singling of record patterns not yet supported"
-singPat patCxt (ListP pats) = do
-  checkIfBrainWillExplode patCxt
-  sPats <- mapM (singPat patCxt) pats
-  return $ foldr (\elt lst -> ConP sconsName [elt, lst]) (ConP snilName []) sPats
-singPat patCxt (SigP pat ty) =
-  fail "Singling of annotated patterns not yet supported"
-singPat patCxt (ViewP exp pat) =
-  fail "Singling of view patterns not yet supported"
-
-singExp :: ExpTable -> Exp -> Q Exp
-singExp vars (VarE name) = case Map.lookup name vars of
-  Just exp -> return exp
-  Nothing -> return (singVal name)
-singExp vars (ConE name) = return $ smartCon name
-singExp vars (LitE lit) =
-  fail "Singling of literal expressions not yet supported"
-singExp vars (AppE exp1 exp2) = do
-  exp1' <- singExp vars exp1
-  exp2' <- singExp vars exp2
-  return $ AppE exp1' exp2'
-singExp vars (InfixE mexp1 exp mexp2) =
-  case (mexp1, mexp2) of
-    (Nothing, Nothing) -> singExp vars exp
-    (Just exp1, Nothing) -> singExp vars (AppE exp exp1)
-    (Nothing, Just exp2) ->
-      fail "Singling of right-only sections not yet supported"
-    (Just exp1, Just exp2) -> singExp vars (AppE (AppE exp exp1) exp2)
-singExp vars (UInfixE _ _ _) =
-  fail "Singling of unresolved infix expressions not supported"
-singExp vars (ParensE _) =
-  fail "Singling of unresolved paren expressions not supported"
-singExp vars (LamE pats exp) = do
-  (pats', vartbl) <- evalForPair $ mapM (singPat Parameter) pats
-  let vars' = Map.union vartbl vars -- order matters; union is left-biased
-  singExp vars' exp
-singExp vars (LamCaseE matches) = 
-  fail "Singling of case expressions not yet supported"
-singExp vars (TupE exps) = do
-  sExps <- mapM (singExp vars) exps
-  sTuple <- singExp vars (ConE (tupleDataName (length exps)))
-  return $ foldExp sTuple sExps
-singExp vars (UnboxedTupE exps) =
-  fail "Singling of unboxed tuple not supported"
-singExp vars (CondE bexp texp fexp) = do
-  exps <- mapM (singExp vars) [bexp, texp, fexp]
-  return $ foldExp (VarE sIfName) exps
-singExp vars (MultiIfE alts) =
-  fail "Singling of multi-way if statements not yet supported"
-singExp vars (LetE decs exp) =
-  fail "Singling of let expressions not yet supported"
-singExp vars (CaseE exp matches) =
-  fail "Singling of case expressions not yet supported"
-singExp vars (DoE stmts) =
-  fail "Singling of do expressions not yet supported"
-singExp vars (CompE stmts) =
-  fail "Singling of list comprehensions not yet supported"
-singExp vars (ArithSeqE range) =
-  fail "Singling of ranges not yet supported"
-singExp vars (ListE exps) = do
-  sExps <- mapM (singExp vars) exps
-  return $ foldr (\x -> (AppE (AppE (VarE smartSconsName) x)))
-                 (VarE smartSnilName) sExps
-singExp vars (SigE exp ty) =
-  fail "Singling of annotated expressions not yet supported"
-singExp vars (RecConE name fields) =
-  fail "Singling of record construction not yet supported"
-singExp vars (RecUpdE exp fields) =
-  fail "Singling of record updates not yet supported"
diff --git a/Singletons/TypeRepStar.hs b/Singletons/TypeRepStar.hs
deleted file mode 100644
--- a/Singletons/TypeRepStar.hs
+++ /dev/null
@@ -1,31 +0,0 @@
-{- Singletons/TypeRepStar.hs
-
-(c) Richard Eisenberg 2012
-eir@cis.upenn.edu
-
-This file contains the definitions for considering TypeRep to be the demotion
-of *. This is still highly experimental, so expect unusual results!
-
--}
-
-{-# LANGUAGE RankNTypes, TypeFamilies, KindSignatures, FlexibleInstances,
-             GADTs, UndecidableInstances, ScopedTypeVariables #-}
-
-module Singletons.TypeRepStar where
-
-import Singletons.Lib
-import Data.Typeable
-
-data instance Sing (a :: *) where
-  STypeRep :: Typeable a => Sing a
-
-sTypeRep :: forall (a :: *). Typeable a => Sing a
-sTypeRep = STypeRep
-
-instance Typeable a => SingI (a :: *) where
-  sing = STypeRep
-instance SingE (a :: *) where
-  type Demote a = TypeRep
-  fromSing STypeRep = typeOf (undefined :: a)
-instance SingKind (Any :: *) where
-  singInstance STypeRep = SingInstance
diff --git a/Singletons/Util.hs b/Singletons/Util.hs
deleted file mode 100644
--- a/Singletons/Util.hs
+++ /dev/null
@@ -1,165 +0,0 @@
-{- Singletons/Util.hs
-
-(c) Richard Eisenberg 2012
-eir@cis.upenn.edu
-
-This file contains helper functions internal to the singletons package.
-Users of the package should not need to consult this file.
--}
-
-{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
-
-module Singletons.Util where
-
-import Language.Haskell.TH
-import Language.Haskell.TH.Syntax
-import Data.Char
-import Data.Maybe
-import Data.Data
-import Data.List
-import Control.Monad
-import Control.Monad.Writer
-import qualified Data.Map as Map
-import Data.Generics
-
--- reify a declaration, warning the user about splices if the reify fails
-reifyWithWarning :: Name -> Q Info
-reifyWithWarning name = recover
-  (fail $ "Looking up " ++ (show name) ++ " in the list of available " ++
-        "declarations failed.\nThis lookup fails if the declaration " ++
-        "referenced was made in same Template\nHaskell splice as the use " ++
-        "of the declaration. If this is the case, put\nthe reference to " ++
-        "the declaration in a new splice.")
-  (reify name)
-
--- check if a string is the name of a tuple
-isTupleString :: String -> Bool
-isTupleString s =
-  (length s > 1) &&
-  (head s == '(') &&
-  (last s == ')') &&
-  ((length (takeWhile (== ',') (tail s))) == ((length s) - 2))
-
--- check if a name is a tuple name
-isTupleName :: Name -> Bool
-isTupleName = isTupleString . nameBase
-
--- extract the degree of a tuple
-tupleDegree :: String -> Int
-tupleDegree "()" = 0
-tupleDegree s = length s - 1
-
--- reduce the four cases of a 'Con' to just two: monomorphic and polymorphic
--- and convert 'StrictType' to 'Type'
-ctorCases :: (Name -> [Type] -> a) -> ([TyVarBndr] -> Cxt -> Con -> a) -> Con -> a
-ctorCases genFun forallFun ctor = case ctor of
-  NormalC name stypes -> genFun name (map snd stypes)
-  RecC name vstypes -> genFun name (map (\(_,_,ty) -> ty) vstypes)
-  InfixC (_,ty1) name (_,ty2) -> genFun name [ty1, ty2]
-  ForallC [] [] ctor' -> ctorCases genFun forallFun ctor'
-  ForallC tvbs cx ctor' -> forallFun tvbs cx ctor' 
-
--- reduce the four cases of a 'Con' to just 1: a polymorphic Con is treated
--- as a monomorphic one
-ctor1Case :: (Name -> [Type] -> a) -> Con -> a
-ctor1Case mono = ctorCases mono (\_ _ ctor -> ctor1Case mono ctor)
-
--- extract the name and number of arguments to a constructor
-extractNameArgs :: Con -> (Name, Int)
-extractNameArgs = ctor1Case (\name tys -> (name, length tys))
-
--- reinterpret a name. This is useful when a Name has an associated
--- namespace that we wish to forget
-reinterpret :: Name -> Name
-reinterpret = mkName . nameBase
-
--- is an identifier uppercase?
-isUpcase :: Name -> Bool
-isUpcase n = let first = head (nameBase n) in isUpper first || first == ':'
-
--- make an identifier uppercase
-upcase :: Name -> Name
-upcase n =
-  let str = nameBase n 
-      first = head str in
-    if isLetter first
-     then mkName ((toUpper first) : tail str)
-     else mkName (':' : str)
-
--- make an identifier lowercase
-locase :: Name -> Name
-locase n =
-  let str = nameBase n
-      first = head str in
-    if isLetter first
-     then mkName ((toLower first) : tail str)
-     else mkName (tail str) -- remove the ":"
-
--- put an uppercase prefix on a name. Takes two prefixes: one for identifiers
--- and one for symbols
-prefixUCName :: String -> String -> Name -> Name
-prefixUCName pre tyPre n = case (nameBase n) of
-    (':' : rest) -> mkName (tyPre ++ rest)
-    alpha -> mkName (pre ++ alpha)
-
--- put a lowercase prefix on a name. Takes two prefixes: one for identifiers
--- and one for symbols
-prefixLCName :: String -> String -> Name -> Name
-prefixLCName pre tyPre n =
-  let str = nameBase n
-      first = head str in
-    if isLetter first
-     then mkName (pre ++ str)
-     else mkName (tyPre ++ str)
-
--- extract the name from a TyVarBndr
-extractTvbName :: TyVarBndr -> Name
-extractTvbName (PlainTV n) = n
-extractTvbName (KindedTV n _) = n
-
--- extract the kind from a TyVarBndr. Returns '*' by default.
-extractTvbKind :: TyVarBndr -> Kind
-extractTvbKind (PlainTV _) = StarT -- FIXME: This seems wrong.
-extractTvbKind (KindedTV _ k) = k
-
--- apply a type to a list of types
-foldType :: Type -> [Type] -> Type
-foldType = foldl AppT
-
--- apply an expression to a list of expressions
-foldExp :: Exp -> [Exp] -> Exp
-foldExp = foldl AppE
-
--- is a kind a variable?
-isVarK :: Kind -> Bool
-isVarK (VarT _) = True
-isVarK _ = False
-
--- a monad transformer for writing a monoid alongside returning a Q
-type QWithAux m = WriterT m Q
-
--- run a computation with an auxiliary monoid, discarding the monoid result
-evalWithoutAux :: QWithAux m a -> Q a
-evalWithoutAux = liftM fst . runWriterT
-
--- run a computation with an auxiliary monoid, returning only the monoid result
-evalForAux :: QWithAux m a -> Q m
-evalForAux = execWriterT
-
--- run a computation with an auxiliary monoid, return both the result
--- of the computation and the monoid result
-evalForPair :: QWithAux m a -> Q (a, m)
-evalForPair = runWriterT
-
--- in a computation with an auxiliary map, add a binding to the map
-addBinding :: Ord k => k -> v -> QWithAux (Map.Map k v) ()
-addBinding k v = tell (Map.singleton k v)
-
--- in a computation with an auxiliar list, add an element to the list
-addElement :: elt -> QWithAux [elt] ()
-addElement elt = tell [elt]
-
--- does a TH structure contain a name?
-containsName :: Data a => Name -> a -> Bool
-containsName n = everything (||) (mkQ False (== n))
-
diff --git a/singletons.cabal b/singletons.cabal
--- a/singletons.cabal
+++ b/singletons.cabal
@@ -1,5 +1,5 @@
 name:           singletons
-version:        0.8.1
+version:        0.8.2
 cabal-version:  >= 1.8
 synopsis:       A framework for generating singleton types
 homepage:       http://www.cis.upenn.edu/~eir/packages/singletons
@@ -7,7 +7,7 @@
 author:         Richard Eisenberg <eir@cis.upenn.edu>
 maintainer:     Richard Eisenberg <eir@cis.upenn.edu>
 stability:      experimental
-extra-source-files: README
+extra-source-files: README, CHANGES
 license:        BSD3
 license-file:   LICENSE
 build-type:     Simple
@@ -15,8 +15,8 @@
     This library generates singleton types, promoted functions, and singleton
     functions using Template Haskell. It is useful for programmers who wish
     to use dependently typed programming techniques. The library was originally
-    presented in /Dependently typed programming with singletons/, submitted
-    to the Haskell Symposium, 2012.
+    presented in /Dependently Typed Programming with Singletons/, published
+    at the Haskell Symposium, 2012.
     (<http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf>)
 
     As of this release date, Haddock was not able to properly process the code
@@ -31,7 +31,7 @@
       template-haskell >= 2.8,
       containers >= 0.5,
       syb >= 0.3
-  exposed-modules:    Singletons.Lib, Singletons.CustomStar,
-                      Singletons.TypeRepStar
-  other-modules:      Singletons.Promote, Singletons.Singletons,
-                      Singletons.Util
+  exposed-modules:    Data.Singletons, Data.Singletons.CustomStar,
+                      Data.Singletons.TypeRepStar
+  other-modules:      Data.Singletons.Promote, Data.Singletons.Singletons,
+                      Data.Singletons.Util