diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2019, Alejandro Serrano
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * 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.
+
+    * Neither the name of Alejandro Serrano nor the names of other
+      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
+OWNER 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.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,69 @@
+# `simplistic-generics`: generic programming without too many type classes
+
+This library provides a way to do data type-generic programming in GHC,
+re-using almost all the machinery from `GHC.Generics`, but without the need
+to define a different generic type class for each new operation.
+
+Say that you want to define an operation `op` in a generic fashion.
+The [docs of `GHC.Generics`](http://hackage.haskell.org/package/base/docs/GHC-Generics.html)
+tell you that you need to create a new type class whose argument is
+the set of pattern functors that may generate the data type. Then by
+means of a default declaration you bridge the gap between both versions.
+Furthermore, in almost every case the instances of this class follow the
+same pattern:
+
+```haskell
+class GOp (f :: * -> *) where
+  gop :: ...
+instance GOp U1 where ...
+instance (GOp f, GOp g) => GOp (f :+: g) where ...
+instance (GOp f, GOp g) => GOp (f :*: g) where ...
+instance (GOp f) => GOp (M1 i p f) where ...
+instance Op t => GOp (K1 r t) where ...
+
+class Op a where
+  op :: ...
+  default op :: (Generic a, GOp (Rep a)) => ...
+  op = ... gop ...
+```
+
+When using `simplistic-generics` you do *not* introduce such a type class;
+you just write all the cases of the generic function in one go! The only
+thing you need to remember is that you have to pattern match on values of
+the type `SRep w f`, where `f` is the pattern functor from `GHC.Generics`.
+The definition of the previous operation looks then:
+
+```haskell
+gop :: ... SRep w f ...
+gop ... S_U1       ... = ...
+gop ... (S_L1 x)   ... = ...
+gop ... (S_R1 x)   ... = ...
+gop ... (x :**: y) ... = ...
+gop ... (S_M1 x)   ... = ...
+gop ... (S_K1 x)   ... = ...
+```
+
+There is only one missing link here. In the definition of `GOp` using
+type classes we tied the knot by asking the `K1` instance to satisfy `Op`
+recursively. In the case of `SRep` we have a special `OnLeaves` combinator
+which requires a constraint from each `K1` node. The signature for `gop`
+should read then:
+
+```haskell
+gop :: OnLeaves Op f => ... SRep w f ...
+```
+
+The final touch is that instead of using `from` and `to` to convert back and
+forth generic representations, you use `fromS` and `toS` to get a `SRep w f`.
+
+For real examples, check the [`Derive` folder](https://gitlab.com/trupill/simplistic-generics/tree/master/src/Generics/Simplistic/Derive) in the repo.
+
+### Inspiration
+
+This library is inspired by several previous work:
+
+* [Generic Haskell](http://www.cs.uu.nl/research/projects/generic-haskell/compiler/emerald/GHUsersGuide.pdf),
+  described thoroughly in [Andres Löh's thesis](https://www.andres-loeh.de/ExploringGH.pdf),
+  which features type-indexed functions in Haskell.
+* The [`generics-sop` library](http://hackage.haskell.org/package/generics-sop),
+  from which we have copied the `OnLeaves` technique.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/simplistic-generics.cabal b/simplistic-generics.cabal
new file mode 100644
--- /dev/null
+++ b/simplistic-generics.cabal
@@ -0,0 +1,33 @@
+cabal-version:       >=1.10
+name:                simplistic-generics
+version:             0.1.0.0
+synopsis:            Generic programming without too many type classes
+description:         This library provides a representation build on top of 
+                     `GHC.Generics`, which can be used to describe generic
+                     operations on a single function, instead of having
+                     each case defined in an instance of a type class.
+-- bug-reports:
+license:             BSD3
+license-file:        LICENSE
+author:              Alejandro Serrano
+maintainer:          trupill@gmail.com
+-- copyright:
+category:            Data
+build-type:          Simple
+extra-source-files:  README.md
+
+library
+  exposed-modules:     Generics.Simplistic,
+                       Generics.Simplistic.Derive.Eq,
+                       Generics.Simplistic.Derive.Functor,
+                       Generics.Simplistic.Derive.Show
+                       Data.Constraints
+  -- other-modules:
+  -- other-extensions:
+  build-depends:       base >=4.12 && <5, kind-apply, comonad
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+
+source-repository head
+  type:                git
+  location:            https://gitlab.com/trupill/simplistic-generics
diff --git a/src/Data/Constraints.hs b/src/Data/Constraints.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Constraints.hs
@@ -0,0 +1,16 @@
+{-# language MultiParamTypeClasses,
+             UndecidableInstances,
+             QuantifiedConstraints,
+             ConstraintKinds,
+             FlexibleInstances,
+             KindSignatures,
+             PolyKinds #-}
+module Data.Constraints where
+
+import GHC.Exts (Constraint)
+
+class    (c => d) => Implies c d
+instance (c => d) => Implies c d
+
+class    Trivial c
+instance Trivial c
diff --git a/src/Generics/Simplistic.hs b/src/Generics/Simplistic.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Simplistic.hs
@@ -0,0 +1,173 @@
+{-# language GADTs,
+             DataKinds,
+             PolyKinds,
+             TypeOperators,
+             ConstraintKinds,
+             MultiParamTypeClasses,
+             FlexibleContexts,
+             FlexibleInstances,
+             QuantifiedConstraints,
+             UndecidableInstances,
+             KindSignatures,
+             TypeFamilies #-}
+module Generics.Simplistic (
+  -- * From `GHC.Generics.Extra` module
+  Generic, Rep, Generic1, Rep1,
+  V1, U1, (:+:), (:*:), K1, M1, (:=>:),
+  -- * Simplistic representation on `*` types 
+  SMeta(..), SRep(..), GenericSy, fromS, toS, fromI, toI,
+  -- ** Constraints over the leaves of a data type
+  OnLeaves,
+  -- * Simplistic representation on `* -> *` types 
+  SRep1(..), GenericSy1, fromS1, toS1,
+  -- ** Constraints over the leaves of a data type
+  OnLeaves1,
+  -- * Auxiliary constraints
+  Implies, Trivial
+) where
+
+import Control.Comonad
+import Data.Functor.Identity
+import Data.Constraints
+import GHC.Generics.Extra
+import GHC.Exts (Constraint)
+
+data SMeta i t where
+  SM_D :: Datatype    d => SMeta D d
+  SM_C :: Constructor c => SMeta C c
+  SM_S :: Selector    s => SMeta S s
+
+infixr 5 :**:
+data SRep w f where
+  S_U1   ::                          SRep w U1
+  S_L1   ::              SRep w f -> SRep w (f :+: g)
+  S_R1   ::              SRep w g -> SRep w (f :+: g)
+  (:**:) ::  SRep w f -> SRep w g -> SRep w (f :*: g)
+  S_K1   ::              w a      -> SRep w (K1 i a)
+  S_M1   :: SMeta i t -> SRep w f -> SRep w (M1 i t f)
+  S_ST   ::         c => SRep w f -> SRep w (c :=>: f)
+
+type GenericSy a = (Generic a, Sy (Rep a))
+
+fromS :: (GenericSy a, Applicative w) => a -> SRep w (Rep a)
+fromS = fromS' . from
+fromI :: (GenericSy a) => a -> SRep Identity (Rep a)
+fromI = fromS
+toS :: (GenericSy a, Comonad w) => SRep w (Rep a) -> a
+toS = to . toS'
+toI :: (GenericSy a) => SRep Identity (Rep a) -> a
+toI = toS
+
+type family OnLeaves (c :: * -> Constraint) (f :: * -> *) :: Constraint where
+  OnLeaves c V1        = ()
+  OnLeaves c U1        = ()
+  OnLeaves c (f :+: g)  = (OnLeaves c f, OnLeaves c g)
+  OnLeaves c (f :*: g)  = (OnLeaves c f, OnLeaves c g)
+  OnLeaves c (K1 i a)   = c a
+  OnLeaves c (M1 i p f) = OnLeaves c f
+  OnLeaves c (d :=>: f) = Implies d (OnLeaves c f)
+
+infixr 5 :***:
+data SRep1 f x where
+  S1_U1   ::                           SRep1 U1         x
+  S1_L1   ::              SRep1 f x -> SRep1 (f :+: g)  x
+  S1_R1   ::              SRep1 g x -> SRep1 (f :+: g)  x
+  (:***:) :: SRep1 f x -> SRep1 g x -> SRep1 (f :*: g)  x
+  S1_K1   ::          a             -> SRep1 (K1 i a)   x
+  S1_M1   :: SMeta i t -> SRep1 f x -> SRep1 (M1 i t f) x
+  S1_ST   ::        c =>  SRep1 f x -> SRep1 (c :=>: f) x
+  S1_Par  ::          x             -> SRep1 Par1       x
+  S1_Rec  ::          f x           -> SRep1 (Rec1 f)   x
+  S1_Comp ::          f (SRep1 g x) -> SRep1 (f :.: g)  x
+
+type GenericSy1 f = (Generic1 f, Sy1 (Rep1 f))
+
+fromS1 :: (GenericSy1 f) => f a -> SRep1 (Rep1 f) a
+fromS1 = fromS1' . from1
+toS1 :: (GenericSy1 f) => SRep1 (Rep1 f) a -> f a
+toS1 = to1 . toS1'
+
+type family OnLeaves1 (c :: * -> Constraint) (r :: (* -> *) -> Constraint)
+                      (f :: * -> *) :: Constraint where
+  OnLeaves1 c r V1         = ()
+  OnLeaves1 c r U1         = ()
+  OnLeaves1 c r (f :+: g)  = (OnLeaves1 c r f, OnLeaves1 c r g)
+  OnLeaves1 c r (f :*: g)  = (OnLeaves1 c r f, OnLeaves1 c r g)
+  OnLeaves1 c r (K1 i a)   = c a
+  OnLeaves1 c r (M1 i p f) = OnLeaves1 c r f
+  OnLeaves1 c r (d :=>: f) = Implies d (OnLeaves1 c r f)
+  OnLeaves1 c r Par1       = ()
+  OnLeaves1 c r (Rec1 f)   = r f
+  OnLeaves1 c r (f :.: g)  = (r f, OnLeaves1 c r g)
+
+-- Internal instances
+class SMety i t where
+  smeta :: SMeta i t
+instance Datatype d => SMety D d where
+  smeta = SM_D
+instance Constructor c => SMety C c where
+  smeta = SM_C
+instance Selector s => SMety S s where
+  smeta = SM_S
+class Sy f where
+  fromS' :: Applicative w => f a -> SRep w f
+  toS'   :: Comonad     w => SRep w f -> f a
+instance Sy V1 where
+  fromS' = undefined
+  toS'   = undefined
+instance Sy U1 where
+  fromS' U1 = S_U1
+  toS'   S_U1 = U1
+instance (Sy f, Sy g) => Sy (f :+: g) where
+  fromS' (L1 x) = S_L1 (fromS' x)
+  fromS' (R1 y) = S_R1 (fromS' y)
+  toS'   (S_L1 x) = L1 (toS' x)
+  toS'   (S_R1 y) = R1 (toS' y)
+instance (Sy f, Sy g) => Sy (f :*: g) where
+  fromS' (x :*: y) = fromS' x :**: fromS' y
+  toS'   (x :**: y) = toS' x :*: toS' y
+instance Sy (K1 i a) where
+  fromS' (K1 x) = S_K1 (pure x)
+  toS'   (S_K1 x) = K1 (extract x)
+instance (SMety i t, Sy f) => Sy (M1 i t f) where
+  fromS' (M1 x) = S_M1 smeta (fromS' x)
+  toS'   (S_M1 _ x) = M1 (toS' x)
+instance (c => Sy f) => Sy (c :=>: f) where
+  fromS' (SuchThat x) = S_ST (fromS' x)
+  toS'   (S_ST x) = SuchThat (toS' x)
+
+class Sy1 f where
+  fromS1' :: f a -> SRep1 f a
+  toS1'   :: SRep1 f a -> f a
+instance Sy1 V1 where
+  fromS1' = undefined
+  toS1'   = undefined
+instance Sy1 U1 where
+  fromS1' U1 = S1_U1
+  toS1'   S1_U1 = U1
+instance (Sy1 f, Sy1 g) => Sy1 (f :+: g) where
+  fromS1' (L1 x) = S1_L1 (fromS1' x)
+  fromS1' (R1 y) = S1_R1 (fromS1' y)
+  toS1'   (S1_L1 x) = L1 (toS1' x)
+  toS1'   (S1_R1 y) = R1 (toS1' y)
+instance (Sy1 f, Sy1 g) => Sy1 (f :*: g) where
+  fromS1' (x :*: y) = fromS1' x :***: fromS1' y
+  toS1'   (x :***: y) = toS1' x :*: toS1' y
+instance Sy1 (K1 i a) where
+  fromS1' (K1 x) = S1_K1 x
+  toS1'   (S1_K1 x) = K1 x
+instance (SMety i t, Sy1 f) => Sy1 (M1 i t f) where
+  fromS1' (M1 x) = S1_M1 smeta (fromS1' x)
+  toS1'   (S1_M1 _ x) = M1 (toS1' x)
+instance (c => Sy1 f) => Sy1 (c :=>: f) where
+  fromS1' (SuchThat x) = S1_ST (fromS1' x)
+  toS1'   (S1_ST x) = SuchThat (toS1' x)
+instance Sy1 Par1 where
+  fromS1' (Par1 x) = S1_Par x
+  toS1'   (S1_Par x) = Par1 x
+instance Sy1 (Rec1 f) where
+  fromS1' (Rec1 x) = S1_Rec x
+  toS1'   (S1_Rec x) = Rec1 x
+instance (Functor f, Sy1 g) => Sy1 (f :.: g) where
+  fromS1' (Comp1 x) = S1_Comp (fmap fromS1' x)
+  toS1'   (S1_Comp x) = Comp1 (fmap toS1' x)
diff --git a/src/Generics/Simplistic/Derive/Eq.hs b/src/Generics/Simplistic/Derive/Eq.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Simplistic/Derive/Eq.hs
@@ -0,0 +1,23 @@
+{-# language GADTs,
+             TypeFamilies,
+             ConstraintKinds,
+             TypeOperators,
+             FlexibleContexts #-}
+module Generics.Simplistic.Derive.Eq where
+
+import Data.Functor.Identity
+import Generics.Simplistic
+
+geq :: (Applicative w, OnLeaves Eq f)
+    => SRep w f -> SRep w f -> w Bool
+geq S_U1       S_U1       = pure True
+geq (S_L1 x)   (S_L1 y)   = geq x y
+geq (S_R1 x)   (S_R1 y)   = geq x y
+geq (x :**: y) (u :**: v) = (&&) <$> geq x u <*> geq y v
+geq (S_K1 x)   (S_K1 y)   = (==) <$> x <*> y
+geq (S_M1 _ x) (S_M1 _ y) = geq x y
+geq (S_ST x)   (S_ST y)   = geq x y
+geq _          _          = pure False
+
+geq' :: (GenericSy a, OnLeaves Eq (Rep a)) => a -> a -> Bool
+geq' x y = runIdentity $ geq (fromS x) (fromS y)
diff --git a/src/Generics/Simplistic/Derive/Functor.hs b/src/Generics/Simplistic/Derive/Functor.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Simplistic/Derive/Functor.hs
@@ -0,0 +1,23 @@
+{-# language GADTs,
+             TypeOperators,
+             FlexibleContexts #-}
+module Generics.Simplistic.Derive.Functor where
+
+import Generics.Simplistic
+
+gfmap :: OnLeaves1 Trivial Functor f
+      => (a -> b) -> SRep1 f a -> SRep1 f b
+gfmap _ S1_U1       = S1_U1
+gfmap f (S1_L1 x)   = S1_L1 (gfmap f x)
+gfmap f (S1_R1 x)   = S1_R1 (gfmap f x)
+gfmap f (x :***: y) = gfmap f x :***: gfmap f y
+gfmap f (S1_K1 x)   = S1_K1 x
+gfmap f (S1_M1 i x) = S1_M1 i (gfmap f x)
+gfmap f (S1_ST x)   = S1_ST (gfmap f x)
+gfmap f (S1_Par  x) = S1_Par (f x)
+gfmap f (S1_Rec  x) = S1_Rec (fmap f x)
+gfmap f (S1_Comp x) = S1_Comp (fmap (gfmap f) x)
+
+gfmap' :: (GenericSy1 f, OnLeaves1 Trivial Functor (Rep1 f))
+       => (a -> b) -> f a -> f b
+gfmap' f x = toS1 $ gfmap f $ fromS1 x
diff --git a/src/Generics/Simplistic/Derive/Show.hs b/src/Generics/Simplistic/Derive/Show.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Simplistic/Derive/Show.hs
@@ -0,0 +1,99 @@
+{-# language GADTs,
+             TypeFamilies,
+             ConstraintKinds,
+             TypeOperators,
+             FlexibleContexts,
+             ScopedTypeVariables,
+             DeriveGeneric #-}
+module Generics.Simplistic.Derive.Show where
+
+import Data.Functor.Identity
+import Generics.Simplistic
+import GHC.Generics
+
+-- An example
+data MyList a = MyNil | MyCons { hd :: a, tl :: MyList a } deriving Generic
+
+myListValue :: MyList Integer
+myListValue = MyCons 1 (MyCons 2 (MyCons 3 MyNil))
+
+instance Show a => Show (MyList a) where
+  show = gshow
+
+-- Translated from `generic-deriving`
+-- https://github.com/dreixel/generic-deriving/blob/master/src/Generics/Deriving/Show.hs
+
+appPrec :: Int
+appPrec = 2
+
+data Type = Rec | Tup | Pref | Inf String
+
+gshow :: (GenericSy t, OnLeaves Show (Rep t))
+      => t -> String
+gshow v = gshowsPrec Pref 0 v ""
+
+gshowsPrec :: (GenericSy t, OnLeaves Show (Rep t))
+           => Type -> Int -> t -> ShowS
+gshowsPrec t n v = gshowsPrec' t n (fromS v)
+
+gshowsPrec' :: (OnLeaves Show f)
+            => Type -> Int -> SRep Identity f -> ShowS
+-- "Simple" cases
+gshowsPrec' _ _ S_U1       = id
+gshowsPrec' t n (S_L1 x)   = gshowsPrec' t n x
+gshowsPrec' t n (S_R1 x)   = gshowsPrec' t n x
+gshowsPrec' _ n (S_K1 x)   = showsPrec n x
+gshowsPrec' t n (S_ST x)   = gshowsPrec' t n x
+-- The complex case of tuples
+gshowsPrec' t@Rec     n (a :**: b) =
+  gshowsPrec' t n     a . showString ", " . gshowsPrec' t n     b
+gshowsPrec' t@(Inf s) n (a :**: b) =
+  gshowsPrec' t n     a . showString s    . gshowsPrec' t n     b
+gshowsPrec' t@Tup     n (a :**: b) =
+  gshowsPrec' t n     a . showChar ','    . gshowsPrec' t n     b
+gshowsPrec' t@Pref    n (a :**: b) =
+  gshowsPrec' t (n+1) a . showChar ' '    . gshowsPrec' t (n+1) b
+-- The case of metadata
+gshowsPrec' t n (S_M1 (SM_C :: SMeta i c) (x :: SRep Identity f)) = 
+  case fixity of
+    Prefix    -> showParen (n > appPrec && not (isNullary x))
+                  ( showString (conName c)
+                  . if (isNullary x) then id else showChar ' '
+                  . showBraces t (gshowsPrec' t appPrec x))
+    Infix _ m -> showParen (n > m) (showBraces t (gshowsPrec' t m x))
+    where c :: M1 C c f () = undefined
+          fixity = conFixity c
+          t = if (conIsRecord c) then Rec else
+                case (conIsTuple c) of
+                  True -> Tup
+                  False -> case fixity of
+                              Prefix    -> Pref
+                              Infix _ _ -> Inf (show (conName c))
+          showBraces :: Type -> ShowS -> ShowS
+          showBraces Rec     p = showChar '{' . p . showChar '}'
+          showBraces Tup     p = showChar '(' . p . showChar ')'
+          showBraces Pref    p = p
+          showBraces (Inf _) p = p
+          conIsTuple :: C1 c f p -> Bool
+          conIsTuple y = tupleName (conName y) where
+            tupleName ('(':',':_) = True
+            tupleName _ = False
+gshowsPrec' t n (S_M1 (SM_S :: SMeta i c) (x :: SRep Identity f)) 
+  | selName s == "" = --showParen (n > appPrec)
+                      (gshowsPrec' t n x)
+  | otherwise       =   showString (selName s)
+                      . showString " = "
+                      . gshowsPrec' t 0 x
+    where s :: M1 S c f () = undefined
+gshowsPrec' t n (S_M1 _ x) = gshowsPrec' t n x
+
+isNullary :: SRep Identity a -> Bool
+isNullary S_U1       = True
+isNullary (S_L1 x)   = error "unnecessary case"
+isNullary (S_R1 x)   = error "unnecessary case"
+isNullary (x :**: y) = False
+isNullary (S_K1 x)   = False
+isNullary (S_M1 t x) = case t of
+                         SM_S -> isNullary x
+                         _    -> error "unnecessary case"
+isNullary (S_ST x)   = isNullary x