diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,5 @@
+#!/usr/bin/env runhaskell
+
+> import Distribution.Simple
+> main = defaultMain
+
diff --git a/dependent-sum.cabal b/dependent-sum.cabal
new file mode 100644
--- /dev/null
+++ b/dependent-sum.cabal
@@ -0,0 +1,29 @@
+name:                   dependent-sum
+version:                0.1
+stability:              provisional
+
+cabal-version:          >= 1.6
+build-type:             Simple
+
+author:                 James Cook <mokus@deepbondi.net>
+maintainer:             James Cook <mokus@deepbondi.net>
+license:                PublicDomain
+homepage:               https://github.com/mokus0/dependent-sum
+
+category:               Data, Dependent Types
+synopsis:               Dependent sum type
+description:            Dependent sums and supporting typeclasses for
+                        comparing and formatting them.
+
+extra-source-files:     examples/*.hs
+
+source-repository head
+  type:     git
+  location: git://github.com/mokus0/dependent-sum.git
+
+Library
+  hs-source-dirs:       src
+  exposed-modules:      Data.Dependent.Sum
+                        Data.GADT.Compare
+                        Data.GADT.Show
+  build-depends:        base >= 3 && <5
diff --git a/examples/FooGADT.hs b/examples/FooGADT.hs
new file mode 100644
--- /dev/null
+++ b/examples/FooGADT.hs
@@ -0,0 +1,103 @@
+{-# LANGUAGE GADTs #-}
+module FooGADT where
+
+import Data.Dependent.Sum
+import Data.GADT.Show
+import Data.GADT.Compare
+
+data Foo a where
+    Foo :: Foo Double
+    Bar :: Foo Int
+    Baz :: Foo String
+    Qux :: Foo Double
+
+instance Eq (Foo a) where
+    (==) = defaultEq
+
+instance GEq Foo where
+    -- either 'geq' or 'maybeEq' are sufficient, but both
+    -- are given here for illustration of how to define them.
+    
+    geq Foo Foo = Just Refl
+    geq Bar Bar = Just Refl
+    geq Baz Baz = Just Refl
+    geq Qux Qux = Just Refl
+    geq _   _   = Nothing
+    
+    maybeEq Foo Foo y n = y
+    maybeEq Bar Bar y n = y
+    maybeEq Baz Baz y n = y
+    maybeEq Qux Qux y n = y
+    maybeEq _   _   y n = n
+    
+
+instance EqTag Foo where
+    eqTagged Foo Foo = (==)
+    eqTagged Bar Bar = (==)
+    eqTagged Baz Baz = (==)
+    eqTagged Qux Qux = (==)
+    eqTagged _   _   = const (const False)
+
+instance GCompare Foo where
+    gcompare Foo Foo = GEQ
+    gcompare Foo _   = GLT
+    gcompare _   Foo = GGT
+    
+    gcompare Bar Bar = GEQ
+    gcompare Bar _   = GLT
+    gcompare _   Bar = GGT
+    
+    gcompare Baz Baz = GEQ
+    gcompare Baz _   = GLT
+    gcompare _   Baz = GGT
+    
+    gcompare Qux Qux = GEQ
+
+instance OrdTag Foo where
+    compareTagged Foo Foo = compare
+    compareTagged Bar Bar = compare
+    compareTagged Baz Baz = compare
+    compareTagged Qux Qux = compare
+    
+    compareTagged _   _   = error "OrdTag (Foo): bad case"
+
+instance Show (Foo a) where
+    showsPrec _ Foo      = showString "Foo"
+    showsPrec _ Bar      = showString "Bar"
+    showsPrec _ Baz      = showString "Baz"
+    showsPrec _ Qux      = showString "Qux"
+
+instance GShow Foo where
+    gshowsPrec = showsPrec
+
+instance ShowTag Foo where
+    showTaggedPrec Foo = showsPrec
+    showTaggedPrec Bar = showsPrec
+    showTaggedPrec Baz = showsPrec
+    showTaggedPrec Qux = showsPrec
+
+
+instance GRead Foo where
+    greadsPrec _ str = case tag of
+        "Foo" -> [(\k -> k Foo, rest)]
+        "Bar" -> [(\k -> k Bar, rest)]
+        "Baz" -> [(\k -> k Baz, rest)]
+        "Qux" -> [(\k -> k Qux, rest)]
+        _     -> []
+        where (tag, rest) = splitAt 3 str
+
+instance ReadTag Foo where
+    readTaggedPrec Foo = readsPrec
+    readTaggedPrec Bar = readsPrec
+    readTaggedPrec Baz = readsPrec
+    readTaggedPrec Qux = readsPrec
+
+
+foo x = Foo :=> x
+bar x = Bar :=> x
+baz x = Baz :=> x
+qux x = Qux :=> x
+
+
+xs = [foo pi, bar 100, baz "hello world", qux (exp 1)]
+xs' = read (show xs) `asTypeOf` xs
diff --git a/src/Data/Dependent/Sum.hs b/src/Data/Dependent/Sum.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Dependent/Sum.hs
@@ -0,0 +1,175 @@
+{-# LANGUAGE ExistentialQuantification, GADTs #-}
+module Data.Dependent.Sum where
+
+import Data.GADT.Show
+import Data.GADT.Compare
+import Data.Typeable
+
+import Data.Maybe (fromMaybe)
+
+-- |A basic dependent sum type; the first component is a tag that specifies 
+-- the type of the second;  for example, think of a GADT such as:
+-- 
+-- > data Tag a where
+-- >    AString :: Tag String
+-- >    AnInt   :: Tag Int
+-- 
+-- Then, we have the following valid expressions of type @DSum Tag@:
+--
+-- > AString :=> "hello!"
+-- > AnInt   :=> 42
+-- 
+-- And we can write functions that consume @DSum Tag@ values by matching, 
+-- such as:
+-- 
+-- > toString :: DSum Tag -> String
+-- > toString (AString :=> str) = str
+-- > toString (AnInt   :=> int) = show int
+-- 
+-- By analogy to the (key => value) construction for dictionary entries in 
+-- many dynamic languages, we use (key :=> value) as the constructor for 
+-- dependent sums.  The :=> operator has very low precedence and binds to 
+-- the right, so if the @Tag@ GADT is extended with an additional constructor
+-- @Rec :: Tag (DSum Tag)@, then @Rec :=> AnInt :=> 3 + 4@ is parsed as
+-- would be expected (@Rec :=> (AnInt :=> (3 + 4))@) and has type @DSum Tag@.
+-- Its precedence is just above that of '$', so @foo bar $ AString :=> "eep"@
+-- is equivalent to @foo bar (AString :=> "eep")@.
+data DSum tag = forall a. !(tag a) :=> a
+infixr 1 :=>
+
+instance Typeable1 t => Typeable (DSum t) where
+    typeOf ds = mkTyConApp dSumCon [typeOfT]
+        where
+            dSumCon = mkTyCon "Data.Dependent.Sum.DSum"
+            typeOfT = typeOf1 $ (undefined :: DSum f -> f a) ds
+
+-- |In order to make a 'Show' instance for @DSum tag@, @tag@ must be able
+-- to show itself as well as any value of the tagged type.  'GShow' together
+-- with this class provides the interface by which it can do so.
+--
+-- @GShow tag => t@ is conceptually equivalent to something like this
+-- imaginary syntax:  @(forall a. Inhabited (tag a) => Show a) => t@,
+-- where 'Inhabited' is an imaginary predicate that characterizes 
+-- non-empty types, and 'a' does not occur free in 't'.
+--
+-- The @Tag@ example type introduced in the 'DSum' section could be given the
+-- following instances:
+-- 
+-- > instance GShow Tag where
+-- >     gshowsPrec _showsValPrec _p AString = showString "AString"
+-- >     gshowsPrec _showsValPrec _p AnInt   = showString "AnInt"
+-- > instance ShowTag Tag where
+-- >     showTaggedPrec AString = showsPrec
+-- >     showTaggedPrec AnInt   = showsPrec
+-- 
+class GShow tag => ShowTag tag where
+    -- |Given a value of type @tag a@, return the 'showsPrec' function for 
+    -- the type parameter @a@.
+    showTaggedPrec :: tag a -> Int ->     a -> ShowS
+
+instance Show a => ShowTag ((:=) a) where
+    showTaggedPrec Refl = showsPrec
+
+-- This instance is questionable.  It works, but is pretty useless.
+instance Show a => ShowTag (GOrdering a) where
+    showTaggedPrec GEQ = showsPrec
+    showTaggedPrec _   = \p _ -> showParen (p > 10)
+        ( showString "error "
+        . shows "type information lost into the mists of oblivion"
+        )
+
+instance ShowTag tag => Show (DSum tag) where
+    showsPrec p (tag :=> value) = showParen (p >= 10)
+        ( gshowsPrec 0 tag
+        . showString " :=> "
+        . showTaggedPrec tag 1 value
+        )
+
+class GRead tag => ReadTag tag where
+    readTaggedPrec :: tag a -> Int -> ReadS a
+
+instance Read a => ReadTag ((:=) a) where
+    readTaggedPrec Refl = readsPrec
+
+-- This instance is questionable.  It works, but is partial (and is also pretty useless)
+-- instance Read a => ReadTag (GOrdering a) where
+--     readTaggedPrec GEQ = readsPrec
+--     readTaggedPrec tag = \p -> readParen (p>10) $ \s ->
+--         [ (error msg, rest')
+--         | let (con, rest) = splitAt 6 s
+--         , con == "error "
+--         , (msg, rest') <- reads rest :: [(String, String)]
+--         ]
+
+instance ReadTag tag => Read (DSum tag) where
+    readsPrec p = readParen (p > 1) $ \s -> 
+        concat
+            [ withTag $ \tag ->
+                [ (tag :=> val, rest'')
+                | (val, rest'') <- readTaggedPrec tag 1 rest'
+                ]
+            | (withTag, rest) <- greadsPrec p s
+            , let (con, rest') = splitAt 5 rest
+            , con == " :=> "
+            ]
+
+-- |In order to test @DSum tag@ for equality, @tag@ must know how to test
+-- both itself and its tagged values for equality.  'EqTag' defines
+-- the interface by which they are expected to do so.
+-- 
+-- Continuing the @Tag@ example from the 'DSum' section, we can define:
+-- 
+-- > instance GEq Tag where
+-- >     geq AString AString = Just Refl
+-- >     geq AString AnInt   = Nothing
+-- >     geq AnInt   AString = Nothing
+-- >     geq AnInt   AnInt   = Just Refl
+-- > instance EqTag Tag where
+-- >     eqTagged AString AString = (==)
+-- >     eqTagged AnInt   AnInt   = (==)
+-- 
+-- Note that 'eqTagged' is not called until after the tags have been
+-- compared, so it only needs to consider the cases where 'gcompare' returns 'GEQ'.
+class GEq tag => EqTag tag where
+    -- |Given two values of type @tag a@ (for which 'gcompare' returns 'GEQ'),
+    -- return the '==' function for the type @a@.
+    eqTagged :: tag a -> tag a -> a -> a -> Bool
+
+instance Eq a => EqTag ((:=) a) where
+    eqTagged Refl Refl = (==)
+
+instance EqTag tag => Eq (DSum tag) where
+    (t1 :=> x1) == (t2 :=> x2)  = fromMaybe False $ do
+        Refl <- geq t1 t2
+        return (eqTagged t1 t2 x1 x2)
+
+-- |In order to compare @DSum tag@ values, @tag@ must know how to compare
+-- both itself and its tagged values.  'OrdTag' defines the 
+-- interface by which they are expected to do so.
+-- 
+-- Continuing the @Tag@ example from the 'EqTag' section, we can define:
+-- 
+-- > instance GCompare Tag where
+-- >     gcompare AString AString = GEQ
+-- >     gcompare AString AnInt   = GLT
+-- >     gcompare AnInt   AString = GGT
+-- >     gcompare AnInt   AnInt   = GEQ
+-- > instance OrdTag Tag where
+-- >     compareTagged AString AString = compare
+-- >     compareTagged AnInt   AnInt   = compare
+-- 
+-- As with 'eqTagged', 'compareTagged' only needs to consider cases where
+-- 'gcompare' returns 'GEQ'.
+class (EqTag tag, GCompare tag) => OrdTag tag where
+    -- |Given two values of type @tag a@ (for which 'gcompare' returns 'GEQ'),
+    -- return the 'compare' function for the type @a@.
+    compareTagged :: tag a -> tag a -> a -> a -> Ordering
+
+instance Ord a => OrdTag ((:=) a) where
+    compareTagged Refl Refl = compare
+
+instance OrdTag tag => Ord (DSum tag) where
+    compare (t1 :=> x1) (t2 :=> x2)  = case gcompare t1 t2 of
+        GLT -> LT
+        GGT -> GT
+        GEQ -> compareTagged t1 t2 x1 x2
diff --git a/src/Data/GADT/Compare.hs b/src/Data/GADT/Compare.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/GADT/Compare.hs
@@ -0,0 +1,165 @@
+{-# LANGUAGE GADTs, TypeOperators, RankNTypes, TypeFamilies, FlexibleInstances #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+module Data.GADT.Compare where
+
+import Data.GADT.Show
+import Data.Typeable
+
+-- |A GADT witnessing equality of two types.  Its only inhabitant is 'Refl'.
+data a := b where
+    -- |A value witnessing the fact that two types are in fact the same.
+    Refl :: a := a
+    deriving Typeable
+
+instance Eq (a := b) where
+    Refl == Refl = True
+
+instance Ord (a := b) where
+    compare Refl Refl = EQ
+
+instance Show (a := b) where
+    showsPrec _ Refl = showString "Refl"
+
+instance GShow ((:=) a) where
+    gshowsPrec _ Refl = showString "Refl"
+
+instance Read (a := a) where
+    readsPrec _ s = case con of
+        "Refl"  -> [(Refl, rest)]
+        _       -> []
+        where (con,rest) = splitAt 4 s
+
+instance GRead ((:=) a) where
+    greadsPrec p s = do
+        (Refl, rest) <- readsPrec p s :: [(x := x, String)]
+        return (\x -> x Refl, rest)
+
+-- |A class for type-contexts which contain enough information
+-- to (at least in some cases) decide the equality of types 
+-- occurring within them.
+-- 
+-- Minimal instance declaration is either 'geq' or 'maybeEq'.
+class GEq f where
+    -- |Produce a witness of type-equality, if one exists.
+    -- 
+    -- A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:
+    -- 
+    -- > extract :: GEq tag => tag a -> DSum tag -> Maybe a
+    -- > extract t1 (t2 :=> x) = do
+    -- >     Refl <- geq t1 t2
+    -- >     return x
+    -- 
+    -- Or in a list comprehension:
+    -- 
+    -- > extractMany :: GEq tag => tag a -> [DSum tag] -> [a]
+    -- > extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)]
+    --
+    -- (Making use of the 'DSum' type from "Data.Dependent.Sum" in both examples)
+    geq :: f a -> f b -> Maybe (a := b)
+    geq x y = maybeEq x y (Just Refl) Nothing
+    
+    -- |An interesting alternative formulation:
+    -- This one is nice because it's purely type-level, which means
+    -- that in some cases the type checker can statically prove
+    -- that the 'f' case is unreachable.  In other cases, it can lead
+    -- to nice concise code such as:
+    -- 
+    -- > extract :: GEq tag => tag a -> DSum tag -> Maybe a
+    -- > extract t1 (t2 :=> x) = maybeEq t1 t2 (Just x) Nothing
+    -- 
+    -- Sometimes, though, it can be hard to get the 'Refl' case's type to unify
+    -- with the assumptions properly.
+    maybeEq :: f a -> f b -> ((a ~ b) => c) -> c -> c
+    maybeEq x y f z = case geq x y of
+        Just Refl   -> f
+        Nothing     -> z
+
+-- |If 'f' has a 'GEq' instance, this function makes a suitable default 
+-- implementation of '(==)'.
+defaultEq :: GEq f => f a -> f b -> Bool
+defaultEq x y = maybeEq x y True False
+
+-- |If 'f' has a 'GEq' instance, this function makes a suitable default 
+-- implementation of '(/=)'.
+defaultNeq :: GEq f => f a -> f b -> Bool
+defaultNeq x y = maybeEq x y False True
+
+instance GEq ((:=) a) where
+    geq Refl Refl = Just Refl
+
+-- This instance seems nice, but it's simply not right:
+-- 
+-- > instance GEq StableName where
+-- >     geq sn1 sn2
+-- >         | sn1 == unsafeCoerce sn2
+-- >             = Just (unsafeCoerce Refl)
+-- >         | otherwise     = Nothing
+-- 
+-- Proof:
+-- 
+-- > x <- makeStableName id :: IO (StableName (Int -> Int))
+-- > y <- makeStableName id :: IO (StableName ((Int -> Int) -> Int -> Int))
+-- > 
+-- > let Just boom = geq x y
+-- > let coerce :: (a := b) -> a -> b; coerce Refl = id
+-- > 
+-- > coerce boom (const 0) id 0
+-- > let "Illegal Instruction" = "QED."
+-- 
+-- The core of the problem is that 'makeStableName' only knows the closure
+-- it is passed to, not any type information.  Together with the fact that
+-- the same closure has the same StableName each time 'makeStableName' is 
+-- called on it, there is serious potential for abuse when a closure can 
+-- be given many incompatible types.
+
+
+-- |A type for the result of comparing GADT constructors; the type parameters
+-- of the GADT values being compared are included so that in the case where 
+-- they are equal their parameter types can be unified.
+data GOrdering a b where
+    GLT :: GOrdering a b
+    GEQ :: GOrdering t t
+    GGT :: GOrdering a b
+    deriving Typeable
+
+-- |TODO: Think of a better name
+--
+-- This operation forgets the phantom types of a 'GOrdering' value.
+weakenOrdering :: GOrdering a b -> Ordering
+weakenOrdering GLT = LT
+weakenOrdering GEQ = EQ
+weakenOrdering GGT = GT
+
+instance Eq (GOrdering a b) where
+    x == y =
+        weakenOrdering x == weakenOrdering y
+
+instance Ord (GOrdering a b) where
+    compare x y = compare (weakenOrdering x) (weakenOrdering y)
+
+instance Show (GOrdering a b) where
+    showsPrec _ GGT = showString "GGT"
+    showsPrec _ GEQ = showString "GEQ"
+    showsPrec _ GLT = showString "GLT"
+
+instance GShow (GOrdering a) where
+    gshowsPrec = showsPrec
+
+instance GRead (GOrdering a) where
+    greadsPrec _ s = case con of
+        "GGT"   -> [(\x -> x GGT, rest)]
+        "GEQ"   -> [(\x -> x GEQ, rest)]
+        "GLT"   -> [(\x -> x GLT, rest)]
+        _       -> []
+        where (con, rest) = splitAt 3 s
+
+-- |Type class for orderable GADT-like structures.  When 2 things are equal,
+-- must return a witness that their parameter types are equal as well (GEQ).
+-- |Type class for comparable GADT-like structures.  When 2 things are equal,
+-- must return a witness that their parameter types are equal as well ('GEQ').
+class GEq f => GCompare f where
+    gcompare :: f a -> f b -> GOrdering a b
+
+instance GCompare ((:=) a) where
+    gcompare Refl Refl = GEQ
+
diff --git a/src/Data/GADT/Show.hs b/src/Data/GADT/Show.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/GADT/Show.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}
+module Data.GADT.Show where
+
+-- |'Show'-like class for 1-type-parameter GADTs
+class GShow t where
+    gshowsPrec :: Int -> t a -> ShowS
+
+
+gshows :: GShow t => t a -> ShowS
+gshows = gshowsPrec (-1)
+
+gshow :: (GShow t) => t a -> String
+gshow x = gshows x ""
+
+
+type GReadS t = String -> [(forall b. (forall a. t a -> b) -> b, String)]
+class GRead t where
+    greadsPrec :: Int -> GReadS t
+
+greads :: GRead t => GReadS t
+greads = greadsPrec (-1)
+
+gread :: GRead t => String -> (forall a. t a -> b) -> b
+gread s = hd [f | (f, "") <- greads s]
+    where
+        hd (x:_) = x
+        hd _ = error "gread: no parse"