diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Athan Clark
+
+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 Athan Clark 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/dag.cabal b/dag.cabal
new file mode 100644
--- /dev/null
+++ b/dag.cabal
@@ -0,0 +1,83 @@
+Name:                   dag
+Version:                0.0.1
+Author:                 Athan Clark <athan.clark@gmail.com>
+Maintainer:             Athan Clark <athan.clark@gmail.com>
+License:                BSD3
+License-File:           LICENSE
+Synopsis:               Basic type-safe directed acyclic graphs.
+Description:
+  This is a type-safe approach for a directed acyclic graph.
+  .
+  Edge construction is inductive, creating a "schema":
+  .
+  >  import Data.Graph.DAG.Edge
+  >
+  >  -- | Edges are statically defined:
+  >  edges = ECons (Edge :: EdgeValue "foo" "bar") $
+  >    ECons (Edge :: EdgeValue "bar" "baz") $
+  >    ECons (Edge :: EdgeValue "foo" "baz")
+  >    unique -- ENil, but for uniquely edged graphs
+  .
+  Which we use to populate nodes with values:
+  .
+  >  data Cool = AllRight
+  >            | Radical
+  >            | SuperDuper
+  >
+  >  graph = GCons "foo" AllRight $
+  >    GCons "bar" Radical $
+  >    GCons "baz" SuperDuper $
+  >    GNil edges
+  .
+  It's an instance of `Functor`, but we haven't done much here - it will require
+  a lot of reflection that I don't have time to implement right now - there isn't
+  even binding of value-based `GCons` keys and `ECons` edge node labels.
+  .
+  Some type tomfoolery:
+  .
+  >  *Data.Graph.DAG> :t edges
+  >  edges
+  >    :: EdgeSchema
+  >         '['EdgeType "foo" "bar", 'EdgeType "bar" "baz",
+  >           'EdgeType "foo" "baz"] -- Type list of edges
+  >         '['("foo", '["bar", "baz"]), '("bar", '["baz"])] -- potential loops
+  >         'True -- uniqueness
+  .
+  >  *Data.Graph.DAG> :t getSpanningTrees $ edges
+  >  getSpanningTrees $ edges
+  >    :: Data.Proxy.Proxy
+  >         '['Node "foo" '['Node "bar" '['Node "baz" '[]],
+  >                         'Node "baz" '[]],
+  >           'Node "bar" '['Node "baz" '[]],
+  >           'Node "baz" '[]]
+  .
+  This library is still very naive, but it will give us compile-time enforcement
+  of acyclicity (and uniqueness) in these graphs - ideal for dependency graphs.
+
+Cabal-Version:          >= 1.20
+Build-Type:             Simple
+
+Library
+  Default-Language:     Haskell2010
+  HS-Source-Dirs:       src
+  GHC-Options:          -Wall
+  Exposed-Modules:      Data.Graph.DAG
+                        Data.Graph.DAG.Edge
+  Build-Depends:        base >= 4 && < 5
+                      , constraints
+
+Test-Suite spec
+  Type:                 exitcode-stdio-1.0
+  Default-Language:     Haskell2010
+  Hs-Source-Dirs:       src
+                      , test
+  Ghc-Options:          -Wall
+  Main-Is:              Spec.hs
+  Build-Depends:        base
+                      , hspec
+                      , QuickCheck
+                      , quickcheck-instances
+
+Source-Repository head
+  Type:                 git
+  Location:             https://github.com/athanclark/dag
diff --git a/src/Data/Graph/DAG.hs b/src/Data/Graph/DAG.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Graph/DAG.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+
+module Data.Graph.DAG
+        ( module Data.Graph.DAG.Edge
+        , DAG (..)
+        , glookup
+        ) where
+
+import Data.Graph.DAG.Edge
+
+data DAG es a where
+  GNil :: EdgeSchema es x unique -> DAG es a
+  GCons :: (String ~ key) =>
+           key
+        -> a -- value
+        -> DAG es a
+        -> DAG es a
+
+instance Functor (DAG es) where
+  fmap f (GNil e) = GNil e
+  fmap f (GCons k x xs) = GCons k (f x) $
+    fmap f xs
+
+
+glookup :: String -> DAG es a -> Maybe a
+glookup _ (GNil _) = Nothing
+glookup k (GCons k2 a gs) | k == k2   = Just a
+                          | otherwise = glookup k gs
diff --git a/src/Data/Graph/DAG/Edge.hs b/src/Data/Graph/DAG/Edge.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Graph/DAG/Edge.hs
@@ -0,0 +1,179 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module Data.Graph.DAG.Edge where
+
+import Data.Constraint
+import GHC.TypeLits
+import Data.Proxy
+
+-- | We use promoted symbol values for the @from@ and @to@ type parameters. This
+-- is the user-level data type when declaring the list of edges.
+data EdgeValue (from :: Symbol) (to :: Symbol) = Edge
+
+-- | We need this for type-level computation list.
+data EdgeKind = forall from to. EdgeType from to
+
+-- | Some people just want to watch the world burn. Ideally, this shouldn't
+-- exist; poor error messages, and is very square peg - round hole.
+type family Deducible (x :: Bool) :: Constraint where
+  Deducible 'True = ()
+
+-- | @not . elem@ for lists of types, resulting in a constraint.
+type family Excluding (x :: k) (xs :: Maybe [k]) :: Constraint where
+  Excluding a ('Just '[]) = Deducible 'True -- Basis
+  Excluding a 'Nothing    = Deducible 'True -- Basis
+  Excluding a ('Just (a ': ts)) = Deducible 'False -- Reject & Refute
+  Excluding a ('Just (b ': ts)) = Excluding a ('Just ts) -- continue
+
+-- | A simple @Data.List.lookup@ function for type maps.
+type family Lookup (index :: k) ( map :: [(k, k2)] ) :: Maybe k2 where
+  Lookup a ( '( a, v) ': xs ) = 'Just v
+  Lookup a (b ': xs) = Lookup a xs
+  Lookup a '[] = 'Nothing
+
+-- | Trivial inequality for non-reflexivity of edges
+type family (x :: k1) =/= (y :: k2) :: Constraint where
+  a =/= a = Deducible 'False
+  a =/= b = Deducible 'True
+
+-- | Simply reject anything that's been reached in the other direction. We
+-- expect an explicit type signature when uniqueness is needed, otherwise we
+-- will wait until invocation to see if the edges are unique.
+class Acceptable (a :: EdgeKind)
+                 ( oldLoops :: [(Symbol, [Symbol])] )
+                 (unique :: Bool) where
+instance ( Excluding from (Lookup to excludeMap)
+         , from =/= to ) =>
+            Acceptable ('EdgeType from to) excludeMap 'False where
+instance ( Excluding from (Lookup to excludeMap)
+         , Excluding to (Lookup from excludeMap)
+         , from =/= to ) =>
+            Acceptable ('EdgeType from to) excludeMap 'True where
+
+-- | Add an explicit element to the head of a list, if the test is inside that
+-- list.
+type family PrependIfElem (test :: k) (a :: k) (xs :: [k]) :: [k] where
+  PrependIfElem t a (t ': xs) = a ': t ': xs
+  PrependIfElem t a (u ': xs) = u ': (PrependIfElem t a xs)
+  PrependIfElem t a '[]       = '[]
+
+-- | Update the exclusion map with the new edge: the @from@ key gets @to@ added,
+-- likewise with keys that have @from@ in it's value list. We need to track if
+-- the key exists yet.
+type family DisallowIn
+              (new :: EdgeKind)
+              ( oldLoops :: [(Symbol, [Symbol])] )
+              (keyFound :: Bool) :: [(Symbol, [Symbol])] where
+-- When @from ~ key@:
+  DisallowIn ('EdgeType from to) ( '(from, xs) ': es) 'False =
+    '(from, (to ': xs)) ':                      -- add @to@ to transitive reach list
+      (DisallowIn ('EdgeType from to) es 'True) -- continue
+-- When @from ~/~ key@, and @from ~/~ head value@
+  DisallowIn ('EdgeType from to) ( '(key, vs) ': es ) keyFound =
+    '(key, (PrependIfElem from to vs)) ':            -- find the needle if it exists
+        (DisallowIn ('EdgeType from to) es keyFound) -- continue
+-- Basis
+  DisallowIn a '[] 'True = '[] -- search over.
+-- Growth via append
+  DisallowIn ('EdgeType from to) '[] 'False = ('(from, (to ': '[])) ': '[])
+
+-- | @edges@ is a list of types with kind @EdgeKind@, while @nearLoops@ is a
+-- map of the nodes transitively reachable by each node.
+data EdgeSchema (edges :: [EdgeKind])
+                (nearLoops :: [(Symbol, [Symbol])])
+                (unique :: Bool) where
+  ENil :: EdgeSchema '[] '[] unique
+  ECons :: ( Acceptable b oldLoops unique
+           , EdgeValue from to ~ a
+           , EdgeType from to ~ b
+           , DisallowIn b oldLoops 'False ~ c
+           ) => !a
+             -> EdgeSchema old oldLoops unique
+             -> EdgeSchema (b ': old) c unique
+
+-- | Utility for constructing an @EdgeSchema@ granularly
+unique :: EdgeSchema '[] '[] 'True
+unique = ENil
+
+notUnique :: EdgeSchema '[] '[] 'False
+notUnique = ENil
+
+-- | Trivial rose tree for creating spanning trees
+data Tree a = Node a [Tree a]
+
+-- | Adds an empty @c@ tree to the list of trees uniquely
+type family AppendIfNotElemTrees (c :: k) (trees :: [Tree k]) :: [Tree k] where
+  AppendIfNotElemTrees c ((Node c xs) ': xss) = (Node c xs) ': xss
+  AppendIfNotElemTrees c ((Node x xs) ': xss) = (Node x xs) ':
+    (AppendIfNotElemTrees c xss)
+  AppendIfNotElemTrees c '[] = (Node c '[]) ': '[]
+
+-- | Adds @c@ as a child of any tree with a root @t@. Assumes unique roots.
+type family AddChildTo (test :: k)
+                       (child :: k)
+                       (trees :: [Tree k]) :: [Tree k] where
+  AddChildTo t c ((Node t xs) ': xss) =
+    (Node t (AppendIfNotElemTrees c xs)) ': (AddChildTo t c xss)
+  AddChildTo t c ((Node x xs) ': xss) =
+    (Node x (AddChildTo t c xs)) ': (AddChildTo t c xss)
+  AddChildTo t c '[] = '[]
+
+-- | We need to track if @from@ has is a root node or not. TODO: Some code repeat.
+type family AddEdge' (edge :: EdgeKind)
+                     (trees :: [Tree Symbol])
+                     (hasFromRoot :: Bool)
+                     (hasToRoot :: Bool):: [Tree Symbol] where
+  AddEdge' ('EdgeType from to) '[] 'False 'False =
+    (Node from ((Node to '[]) ': '[])) ': (Node to '[]) ': '[]
+
+  AddEdge' ('EdgeType from to) '[] 'True 'False =
+    (Node to                     '[])  ':                  '[]
+
+  AddEdge' ('EdgeType from to) '[] 'False 'True =
+    (Node from ((Node to '[]) ': '[])) ':                  '[]
+
+  AddEdge' x '[] 'True 'True = '[]
+
+  AddEdge' ('EdgeType from to) ((Node from xs) ': xss) hasFromRoot hasToRoot =
+    (Node from (AppendIfNotElemTrees to xs)) ':
+      (AddEdge' ('EdgeType from to) xss 'True hasToRoot)
+
+  AddEdge' ('EdgeType from to) ((Node to xs) ': xss) hasFromRoot hasToRoot =
+    (Node to (AddEdge' ('EdgeType from to) xs 'True 'True)) ':
+      (AddEdge' ('EdgeType from to) xss hasFromRoot 'True)
+
+  -- Go downward, and laterally (I think).
+  AddEdge' ('EdgeType from to) ((Node x xs) ': xss) hasFromRoot hasToRoot =
+    (Node x (AddEdge' ('EdgeType from to) xs 'True 'True)) ':
+      (AddEdge' ('EdgeType from to) xss hasFromRoot hasToRoot)
+
+-- | Add @to@ as a child to every @from@ node in the accumulator.
+type family AddEdge (edge :: EdgeKind)
+                    (trees :: [Tree Symbol]) :: [Tree Symbol] where
+  AddEdge a trees = AddEdge' a trees 'False 'False
+
+-- | Auxilliary function normally defined in a @where@ clause for manual folding.
+type family SpanningTrees' (edges :: [EdgeKind])
+                           (acc :: [Tree Symbol]) :: [Tree Symbol] where
+  SpanningTrees' '[] trees = trees
+  SpanningTrees' (('EdgeType from to) ': es) trees =
+    SpanningTrees' es (AddEdge ('EdgeType from to) trees)
+
+-- | Expects edges to already be type-safe
+type family SpanningTrees (edges :: [EdgeKind]) :: [Tree Symbol] where
+  SpanningTrees edges = SpanningTrees' edges '[]
+
+getSpanningTrees :: EdgeSchema es x unique -> Proxy (SpanningTrees es)
+getSpanningTrees _ = Proxy
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}