diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Oliver Charles
+
+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 Oliver Charles 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/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/exhaustive.cabal b/exhaustive.cabal
new file mode 100644
--- /dev/null
+++ b/exhaustive.cabal
@@ -0,0 +1,22 @@
+name:                exhaustive
+version:             1.0.0
+synopsis:            Compile time checks that a computation considers producing data through all possible constructors
+description: For a brief tutorial to @exhaustive@, check out the documentation for "Control.Exhaustive", which contains a small example.
+homepage:            http://github.com/ocharles/exhaustive
+license:             BSD3
+license-file:        LICENSE
+author:              Oliver Charles
+maintainer:          ollie@ocharles.org.uk
+-- copyright:
+category:            Control
+build-type:          Simple
+-- extra-source-files:
+cabal-version:       >=1.10
+
+library
+  exposed-modules:     Control.Exhaustive, Control.Exhaustive.Internal
+  -- other-modules:
+  other-extensions:    ConstraintKinds, FlexibleContexts, FlexibleInstances, FunctionalDependencies, GADTs, RankNTypes, ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances
+  build-depends:       base >=4.7 && <4.8, generics-sop >=0.1 && <0.2, transformers >=0.3 && <0.4
+  hs-source-dirs:      src
+  default-language:    Haskell2010
diff --git a/src/Control/Exhaustive.hs b/src/Control/Exhaustive.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Exhaustive.hs
@@ -0,0 +1,100 @@
+{-|
+
+`exhaustive` is a library that guarantees that when building a parser, or some
+other computation that produces data, /all/ possible constructors in a data type
+are considered. You can think of this library as providing a symmetry to GHC's
+built in @-fwarn-incomplete-patterns@ compile time warning, although this
+library is stricter in that it produces compile time errors if a constructor is
+omitted.
+
+Usage of this library is intended to be straightforward, though admittedly the
+types might have you think the opposite! To understand this library, an example
+may be helpful.
+
+To begin with, consider a simple data type for a "boolean expressions" language:
+
+@
+   import qualified "GHC.Generics" as GHC
+
+   data Expr
+     = ETrue
+     | EFalse
+     | EIf Expr Expr Expr
+     deriving ('Eq', GHC.'GHC.Generic')
+   instance 'Generic' Expr
+@
+
+Note that we have to make our data type an instance of both
+"GHC.Generics".'GHC.Generics.Generic' /and/ "Generics.SOP".'Generic', though this only requires
+boiler-plate code.
+
+Next, we would like to build a parser for this language. Let's assume that we
+have access to a @parsec@-like library, where we have one basic combinator:
+
+* @symbol :: 'String' -> Parser 'String'@
+
+Ordinarily, we would write our parser as
+
+@
+    parseExpr :: Parser Expr
+    parseExpr = 'msum' [ETrue '<$' symbol \"True\"
+                     ,EFalse '<$' symbol \"False\"
+                     ,EIf '<$>' symbol \"if\" '*>' parseExpr
+                          '<*>' symbol \"then\" '*>' parseExpr
+                          '<*>' symbol \"else\" '*>' parseExpr
+                     ]
+@
+
+However, nothing is making sure that we actually considered all constructors in
+@Expr@. We could just as well write
+
+@
+    parseExpr :: Parser Expr
+    parseExpr = 'msum' [ETrue '<$' symbol \"True\"
+                     ,EFalse '<$' symbol \"False\"]
+@
+
+Although this is significantly less useful!
+
+Using @exhaustive@, we can get exhaustivity checks that we are at least
+considering all constructors:
+
+@
+    parseExpr :: Parser Expr
+    parseExpr = 'produceFirst' '$'
+      'construct' (\\f -> f '<$' symbol \"True\") ':*'
+      'construct' (\\f -> f '<$' symbol \"False\") ':*'
+      'construct' (\\f -> f '<$'> symbol "if" '*>' parseExpr
+                         '<*>' symbol "then" '*>' parseExpr
+                         '<*>' symbol "else" '*>' parseExpr) ':*'
+      'Nil'
+@
+
+As you can hopefully see, @exhaustive@ requires only minimal changes to an
+existing parser. Specifically, we need to:
+
+1. Use 'produceFirst' instead of 'msum'
+2. Wrap each constructor application with 'construct'.
+3. Use the provided constructor function, rather than the named constructors in
+the original data type.
+
+-}
+module Control.Exhaustive
+  ( -- * Producing data
+    -- | The following are the main entry points to the API, all providing functionality to produce data.
+    produceM
+  , produceFirst
+  , produceAll
+
+    -- * Constructing Data
+    -- | In order to produce data, you need a way to construct it - once for each constructor in a data type.
+  , construct
+
+    -- * Re-exported
+  , Generic)
+  where
+
+import Control.Applicative
+import Control.Monad
+import Generics.SOP
+import Control.Exhaustive.Internal
diff --git a/src/Control/Exhaustive/Internal.hs b/src/Control/Exhaustive/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Exhaustive/Internal.hs
@@ -0,0 +1,134 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Control.Exhaustive.Internal
+  (Constructor, Producer, FunctorStack, produceM, produceFirst, produceAll, construct, Apply, apply )
+  where
+
+import Data.Maybe
+import Data.Traversable
+import Control.Applicative
+import Data.Foldable
+import Generics.SOP
+import Generics.SOP.NP
+import Data.Functor.Compose
+import Generics.SOP.Constraint
+
+-- | Internal machinery to build n-ary functions. As a user of `exhaustive`, you
+-- generally shouldn't need to worry about this type class, other than knowing
+-- that the type variable @b@ will correspond to a function of all types
+-- mentioned in @a@.
+class Functor f => Apply f a b | f a -> b where
+  apply :: f a -> b
+
+instance Apply ((->) a) b (a -> b) where
+  apply = id
+
+instance Apply I b b where
+  apply (I a) = a
+
+instance (Apply g a b,Apply f b c) => Apply (Compose f g) a c where
+  apply (Compose x) = apply (fmap apply x)
+
+-- | A 'Producer' is a lifted function (in the terms of @generics-sop@) that
+-- instantiates a particular constructor of a data type, possibly using
+-- the side-effects provided by @f@.
+--
+-- Most users will want to create 'Producer's using the smart constructor
+-- 'construct'.
+type Producer f code = Injection (NP I) code -.-> K (f (NS (NP I) code))
+
+-- | A 'Constructor' is an n-ary function from all fields of a specific
+-- constructor in a data type, to a generic representation.
+type Constructor fields = forall r. Apply (FunctorStack fields) (NP I fields) r => r
+
+-- | 'construct' builds a 'Producer' for a single constructor of a data type.
+-- As you can see, the type is a little scary - but there are a few main parts
+-- that will interest you, while the rest are unfortunate implementation
+-- details.
+--
+-- * @f@ is the type of functor who's side effects you can use. For example,
+-- you can choose @f@ to be 'IO', @(MyEnv ->)@, or even more complex
+-- monad transformer stacks.
+--
+-- * @fields@ is a list of types that are used in the constructor.
+--
+--     As an example, given the data type
+--
+--     @data User = User { name :: 'String', age :: 'Int'}@
+--
+--     then @fields@ will correspond to @['String', 'Int']@.
+--
+-- The 'Constructor' argument is what you use to actually create your data type.
+-- A 'Constructor' is an n-ary function from all field types. Continuing the
+-- example with @User@ above, we would have
+--
+-- @Constructor fields@ == @Text -> Int -> out@
+--
+-- Thus a complete call to 'construct' would be
+--
+-- @'construct' (\\f -> f '<$>' parseName '<*>' parseAge)@
+--
+-- For a complete example of how this all fits together, user's are pointed
+-- to the example at the top of this page.
+construct :: forall fields code f.
+             (Applicative f,SingI fields)
+          => (Constructor fields -> f (NP I fields)) -> Producer f code fields
+construct applyCtor =
+  Fn (\(Fn f) ->
+        (K (fmap (unK . f)
+                 (applyCtor (apply (buildF (shape :: Shape fields)))))))
+
+-- | This type family is internal, but provides the building block for building
+-- n-ary functions. Most users will probably not need to work with this
+-- directly.
+type family FunctorStack (args :: [*]) :: * -> * where
+  FunctorStack '[] = I
+  FunctorStack (a ': as) = Compose ((->) a) (FunctorStack as)
+
+data Dict (k :: Constraint) where
+  Dict :: k => Dict k
+
+-- | Prove that a 'FunctorStack' really is a 'Functor'.
+isAFunctor :: Shape xs -> Dict (Functor (FunctorStack xs))
+isAFunctor ShapeNil = Dict
+isAFunctor (ShapeCons s) = case isAFunctor s of Dict -> Dict
+
+-- | Given a list of types, build a stack of reader functors that represents
+-- an n-ary function of all of those types.
+buildF :: Functor (FunctorStack xs) => Shape xs -> FunctorStack xs (NP I xs)
+buildF ShapeNil = I Nil
+buildF (ShapeCons s) = Compose (\x -> case isAFunctor s of Dict -> fmap (I x :*) (buildF s))
+
+-- | Keep attempting to construct a data type until a constructor succeeds. The
+-- first constructor to successfully be constructed (in the order defined in the
+-- original data type) will be returned, or 'empty' if all constructions fail.
+produceFirst
+  :: (code ~ Code a, SingI code, Generic a, Alternative f)
+  => NP (Producer f code) code -> f a
+produceFirst = asum . produceM
+
+-- | Produce all successful constructions of a data-type. If any constructors
+-- fail, they will not be included in the resulting list. If all constructors
+-- fail, this will return 'pure' '[]'.
+produceAll
+  :: (code ~ Code a, SingI code, Generic a, Alternative f)
+  => NP (Producer f code) code -> f [a]
+produceAll = fmap catMaybes . sequenceA . map optional . produceM
+
+-- | Build a list of computations, one for each constructor in a data type.
+produceM
+  :: (code ~ Code a, SingI code, Generic a, Applicative f)
+  => NP (Producer f code) code
+  -> [f a]
+produceM fs =
+  map (fmap (to . SOP))
+            (collapse_NP (fs `hap` injections))