diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# 0.1
+
+* Initial version, more or less based on `singletons-2.5.1`.
+
+* Builds with GHC 8.6.5, GHC 8.8.2, GHCJS 8.6.0.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,33 @@
+Copyright (c) 2020, Renzo Carbonara. All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+this list of conditions and the following disclaimer in the documentation
+and/or other materials provided with the distribution.
+
+3. Neither the name of the author nor the names of its contributors may be
+used to endorse or promote products derived from this software without
+specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+--
+
+This project is based on "singletons", Copyright (c) 2012 Richard
+Eisenberg, licenced under the terms of the BSD-3-Clause license at
+https://hackage.haskell.org/package/singletons-2.5.1/src/LICENSE
+
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,14 @@
+# Singlethongs
+
+Like [singletons](https://hackage.haskell.org/package/singletons), but much
+smaller.
+
+# Development
+
+* Build all with `nix-build`.
+
+* Build with some GHC or GHCJS version with `nix-build -A $xxx`, where `xxx` is
+  one of `ghc865`, `ghc882`, `ghcjs86`.
+
+* Enter a development environment with `nix-shell -A $xxx.env`, where `xxx` is
+  one of `ghc865`, `ghc882`, `ghcjs86`.
diff --git a/lib/Singlethongs.hs b/lib/Singlethongs.hs
new file mode 100644
--- /dev/null
+++ b/lib/Singlethongs.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE DataKinds, GADTs, KindSignatures, TemplateHaskell, TypeFamilies #-}
+
+{- | The goal of
+the [singlethongs](https://hackage.haskell.org/package/singlethongs) library
+is to offer the bare minimum of what
+the [singletons](https://hackage.haskell.org/package/singletons) library offers
+in a small package that's easy to compile across different GHC versions,
+including GHCJS.
+
+This module exports a minimal reproduction of what
+the [singletons](https://hackage.haskell.org/package/singletons) package offers.
+Namely 'Sing', 'SingI', 'SomeSing' and 'SingKind', as well as @TemplateHaskell@
+support for generating the relevant instances for custom types. If there is
+some feature that you thing could be added to this library,
+please [suggest it](https://gitlab.com/k0001/singlethongs/issues).
+
+The types exported by this module are not the same types as the types as the
+one exported by
+the [singletons](https://hackage.haskell.org/package/singletons) package.
+Even if they have the same names and implementation, they are not seen as
+equal by the type-checker. They are only intended to be a drop-in replacement.
+-}
+module Singlethongs
+ ( Sing
+ , SingI(..)
+ , SomeSing(..)
+ , withSomeSing
+ , SingKind(..)
+   -- * Template Haskell
+ , singlethongs
+   -- * Re-exports
+ , TestEquality(testEquality)
+ , (:~:)(Refl)
+ ) where
+
+import Singlethongs.Internal
+import Singlethongs.TH
+import Data.Type.Equality
+
diff --git a/lib/Singlethongs/Internal.hs b/lib/Singlethongs/Internal.hs
new file mode 100644
--- /dev/null
+++ b/lib/Singlethongs/Internal.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE GADTs, KindSignatures, PolyKinds, TypeFamilies, RankNTypes #-}
+module Singlethongs.Internal
+ ( Sing
+ , SingI(sing)
+ , SomeSing(SomeSing)
+ , withSomeSing
+ , SingKind(Demote, fromSing, toSing)
+ ) where
+
+data family Sing (a :: k)
+
+class SingI (a :: k) where
+  sing :: Sing a
+
+data SomeSing k where
+  SomeSing :: Sing (a :: k) -> SomeSing k
+
+withSomeSing :: SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r
+withSomeSing x f = case toSing x of SomeSing x' -> f x'
+{-# INLINE withSomeSing #-}
+
+class SingKind k where
+  type Demote k :: *
+  fromSing :: Sing (a :: k) -> Demote k
+  toSing :: Demote k -> SomeSing k
diff --git a/lib/Singlethongs/TH.hs b/lib/Singlethongs/TH.hs
new file mode 100644
--- /dev/null
+++ b/lib/Singlethongs/TH.hs
@@ -0,0 +1,124 @@
+{-# LANGUAGE CPP, LambdaCase, TemplateHaskell #-}
+module Singlethongs.TH (singlethongs) where
+
+import Data.Type.Equality
+import Language.Haskell.TH
+import Singlethongs.Internal
+
+{-| Generate 'Sing', 'SingI', 'SingKind' and 'TestEquality' instances for a
+datatype.
+
+Given a datatype like @Foo@ below, having one or more unary constructors:
+
+@
+data Foo = Bar | Qux
+
+'singlethongs' ''Foo
+@
+
+The following code will be generated:
+
+@
+data instance 'Sing' (x :: Foo) where
+  SBar :: 'Sing' 'Bar
+  SQux :: 'Sing' 'Qux
+
+instance 'SingKind' Fobo where
+  type 'Demote' Foo = Foo
+  'fromSing' SBar = Bar
+  'fromSing' SQux = Qux
+  'toSing' Bar = 'SomeSing' SBar
+  'toSing' Qux = 'SomeSing' SQux
+
+instance 'SingI' 'Bar where 'sing' = SBar
+instance 'SingI' 'Qux where 'sing' = SQux
+
+instance 'TestEquality' ('Sing' :: Foo -> *) where
+  'testEquality' SBar SBar = 'Just' 'Refl'
+  'testEquality' SQux SQux = 'Just' 'Refl'
+  'testEquality' _ _ = 'Nothing'
+@
+
+In order to use this 'singlethongs' function, you will need to enable the
+following GHC extensions:
+
+@
+\{\-\# LANGUAGE DataKinds, GADTs, KindSignatures, TemplateHaskell, TypeFamilies \#\-\}
+@
+-}
+
+singlethongs :: Name -> Q [Dec]
+singlethongs n0 = reify n0 >>= \case
+  TyConI (DataD [] n1 [] Nothing cons@(_:_) []) -> do
+    nCons <- traverse conName cons
+    out0 <- genDataInstSing n1 nCons
+    out1 <- genInstanceSingKind n1 nCons
+    out2 <- genInstanceTestEquality n1 nCons
+    out3 <- mconcat <$> traverse genInstanceSingI nCons
+    pure (out0 <> out1 <> out2 <> out3)
+  _ -> fail "Only enum types are acceptable"
+
+conName :: Con -> Q Name
+conName = \case
+  NormalC n [] -> pure n
+  _ -> fail "Only enum types are acceptable"
+
+sName :: Name -> Name
+sName a = mkName ("S" <> nameBase a)
+
+genDataInstSing :: Name -> [Name] -> Q [Dec]
+genDataInstSing nTy nCons = do
+  let cons1 = flip fmap nCons $ \nCon ->
+        GadtC [sName nCon] [] (AppT (ConT ''Sing) (PromotedT nCon))
+  pure [mkSingDataInstD nTy cons1]
+
+genInstanceSingI :: Name -> Q [Dec]
+genInstanceSingI nCon = do
+  let singD = FunD (mkName "sing") [Clause [] (NormalB (ConE (sName nCon))) []]
+  pure [InstanceD Nothing [] (AppT (ConT ''SingI) (PromotedT nCon)) [singD]]
+
+genInstanceSingKind :: Name -> [Name] -> Q [Dec]
+genInstanceSingKind nTy nCons = do
+  let fromSingD = FunD (mkName "fromSing") $ flip fmap nCons $ \nCon ->
+        Clause [ConP (sName nCon) []] (NormalB (ConE nCon)) []
+      toSingD = FunD (mkName "toSing") $ flip fmap nCons $ \nCon ->
+        Clause [ConP nCon []]
+               (NormalB (AppE (ConE 'SomeSing) (ConE (sName nCon)))) []
+  pure [InstanceD Nothing [] (AppT (ConT ''SingKind) (ConT nTy))
+         [mkDemoteD nTy, fromSingD, toSingD] ]
+
+genInstanceTestEquality :: Name -> [Name] -> Q [Dec]
+genInstanceTestEquality nTy nCons = do
+  let teD = FunD (mkName "testEquality") $ mconcat
+       [ flip fmap nCons $ \nCon ->
+           let p = ConP (sName nCon) []
+           in Clause [p, p] (NormalB (AppE (ConE 'Just) (ConE 'Refl))) []
+       , case nCons of
+           [_] -> []
+           _ -> [Clause [WildP, WildP] (NormalB (ConE 'Nothing)) []]
+       ]
+  pure [InstanceD Nothing []
+          (AppT (ConT ''TestEquality)
+                (SigT (ConT ''Sing)
+                      (AppT (AppT ArrowT (ConT nTy)) StarT)))
+          [teD ]]
+
+
+mkDemoteD :: Name -> Dec
+mkDemoteD nTy =
+#if MIN_VERSION_template_haskell(2,15,0)
+  TySynInstD (TySynEqn Nothing (AppT (ConT ''Demote) (ConT nTy)) (ConT nTy))
+#else
+  TySynInstD ''Demote (TySynEqn [ConT nTy] (ConT nTy))
+#endif
+
+mkSingDataInstD :: Name -> [Con] -> Dec
+mkSingDataInstD nTy cons =
+#if MIN_VERSION_template_haskell(2,15,0)
+  DataInstD [] Nothing (AppT (ConT ''Sing) (SigT (VarT (mkName "x")) (ConT nTy)))
+            Nothing cons []
+#else
+  DataInstD [] ''Sing [SigT (VarT (mkName "x")) (ConT nTy)] Nothing cons []
+#endif
+
+
diff --git a/singlethongs.cabal b/singlethongs.cabal
new file mode 100644
--- /dev/null
+++ b/singlethongs.cabal
@@ -0,0 +1,42 @@
+cabal-version: 2.4
+name: singlethongs
+version: 0.1
+license: BSD-3-Clause
+license-file: LICENSE
+extra-source-files:  README.md CHANGELOG.md
+author: Renzo Carbonara
+maintainer: renλren.zone
+copyright: Copyright (c) Renzo Carbonara 2020
+category: Data
+build-type: Simple
+synopsis: Like singletons, but much smaller.
+description: Like singletons, but much smaller.
+homepage: https://gitlab.com/k0001/singlethongs
+bug-reports: https://gitlab.com/k0001/singlethongs/issues
+tested-with:
+  GHC == 8.6.0,
+  GHC == 8.6.5,
+  GHC == 8.8.2
+
+library
+  hs-source-dirs: lib
+  ghc-options: -Wall -Werror=incomplete-patterns -O2
+  ghcjs-options: -Wall -Werror=incomplete-patterns -O3
+  default-language: Haskell2010
+  exposed-modules:
+    Singlethongs
+  other-modules:
+    Singlethongs.Internal
+    Singlethongs.TH
+  build-depends:
+    base ==4.*,
+    template-haskell,
+
+test-suite test
+  default-language: Haskell2010
+  type: exitcode-stdio-1.0
+  hs-source-dirs: test
+  main-is: Main.hs
+  build-depends:
+    base,
+    singlethongs,
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE DataKinds, GADTs, KindSignatures, TemplateHaskell, TypeFamilies,
+             ScopedTypeVariables, TypeApplications #-}
+{-# OPTIONS_GHC -ddump-splices #-}
+
+module Main (main) where
+
+import Control.Monad (when)
+
+-- We import qualified to test that TH names don't make silly assumptions.
+import qualified Singlethongs as S
+
+
+data A = Ax deriving (Eq)
+S.singlethongs ''A
+{- =====>
+data instance S.Sing (x :: A) where
+  SAx :: S.Sing 'Ax
+
+instance S.SingKind A where
+  type S.Demote A = A
+  fromSing SAx = Ax
+  toSing Ax = S.SomeSing SAx
+
+instance S.TestEquality (S.Sing :: A -> *) where
+  testEquality SAx SAx = Just S.Refl
+
+instance S.SingI 'Ax where sing = SAx
+-}
+
+t_A :: Bool
+t_A = and
+  [ S.fromSing (SAx :: S.Sing 'Ax) == (Ax :: S.Demote A)
+  , S.withSomeSing @A Ax (\sAx -> S.fromSing sAx == Ax)
+  , S.testEquality SAx SAx == Just S.Refl
+  ]
+
+data B = Bx | By deriving (Eq)
+S.singlethongs ''B
+{- =====>
+
+data instance S.Sing (x :: B) where
+  SBx :: S.Sing 'Bx
+  SBy :: S.Sing 'By
+
+instance S.SingKind B where
+  type S.Demote B = B
+  fromSing SBx = Bx
+  fromSing SBy = By
+  toSing Bx = S.SomeSing SBx
+  toSing By = S.SomeSing SBy
+
+instance S.TestEquality (S.Sing :: B -> *) where
+  testEquality SBx SBx = Just S.Refl
+  testEquality SBy SBy = Just S.Refl
+  testEquality _ _ = Nothing
+
+instance S.SingI  'Bx where sing = SBx
+instance S.SingI  'By where sing = SBy
+-}
+
+t_B :: Bool
+t_B = and
+  [ S.fromSing (SBx :: S.Sing 'Bx) == (Bx :: S.Demote B)
+  , S.withSomeSing @B Bx (\sBx -> S.fromSing sBx == Bx)
+  , S.fromSing (SBy :: S.Sing 'By) == (By :: S.Demote B)
+  , S.withSomeSing @B By (\sBy -> S.fromSing sBy == By)
+  , S.testEquality SBx SBx == Just S.Refl
+  , S.testEquality SBx SBy == Nothing
+  , S.testEquality SBy SBx == Nothing
+  , S.testEquality SBy SBy == Just S.Refl
+  ]
+
+main :: IO ()
+main = do
+  when (not t_A) $ fail "Something wrong with t_A"
+  when (not t_B) $ fail "Something wrong with t_B"