diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,3 @@
+# Changelog for do-syntax
+
+## Unreleased changes
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Sandy Maguire (c) 2018
+
+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 Author name here 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,46 @@
+# do-notation
+
+[![Build Status](https://travis-ci.org/isovector/do-notation.svg?branch=master)](https://travis-ci.org/isovector/do-notation) | [Hackage][hackage]
+
+[hackage]: https://hackage.haskell.org/package/do-notation
+
+
+## Dedication
+
+> I've just locked an open door. Strange, yet symbolically compelling.
+>
+> Manny Calavera, Grim Fandango
+
+
+## Overview
+
+Have you ever wanted to manage siiiick invariants with indexed monads without
+giving up your regular monads in the process? `do-notation` lets you do this
+with a bunch of type jiggery-pokery behind the scenes.
+
+It also provides the `Ix m` indexed monad which is a free construction over a
+regular monad `m`. Cool.
+
+
+## Usage
+
+```haskell
+{-# LANGUAGE RebindableSyntax #-}
+
+import Language.Haskell.DoNotation
+import Prelude hiding (Monad (..), pure)
+```
+
+
+## Limitations
+
+The implementation doesn't play very nicely with `do`-blocks bound via `let`.
+
+
+## Thanks
+
+Huge shout-outs to [Csongor Kiss][kcsongor] for very patiently walking me
+through the incoherent instance machinery necessary to make this all work.
+
+[kcsongor]: http://kcsongor.github.io/
+
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/do-notation.cabal b/do-notation.cabal
new file mode 100644
--- /dev/null
+++ b/do-notation.cabal
@@ -0,0 +1,54 @@
+-- This file has been generated from package.yaml by hpack version 0.28.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 1c6165d413f70264592696fc50a574b3b258c9311e510f6e59be27738443ed2a
+
+name:           do-notation
+version:        0.1.0.0
+synopsis:       Generalize do-notation to work on monads and indexed monads simultaneously.
+description:    Please see the README on GitHub at <https://github.com/isovector/do-syntax#readme>
+category:       Language
+homepage:       https://github.com/isovector/do-notation#readme
+bug-reports:    https://github.com/isovector/do-notation/issues
+author:         Sandy Maguire
+maintainer:     sandy@sandymaguire.me
+copyright:      2018 Sandy Maguire
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+cabal-version:  >= 1.10
+extra-source-files:
+    ChangeLog.md
+    README.md
+
+source-repository head
+  type: git
+  location: https://github.com/isovector/do-notation
+
+library
+  exposed-modules:
+      Control.Monad.Trans.Ix
+      Language.Haskell.DoNotation
+  other-modules:
+      Paths_do_notation
+  hs-source-dirs:
+      src
+  build-depends:
+      base >=4.7 && <5
+    , indexed
+  default-language: Haskell2010
+
+test-suite do-syntax-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Paths_do_notation
+  hs-source-dirs:
+      test
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.7 && <5
+    , do-notation
+    , indexed
+  default-language: Haskell2010
diff --git a/src/Control/Monad/Trans/Ix.hs b/src/Control/Monad/Trans/Ix.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Trans/Ix.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE InstanceSigs               #-}
+{-# LANGUAGE PolyKinds                  #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE TypeApplications           #-}
+
+module Control.Monad.Trans.Ix
+  ( Ix (..)
+  , liftIx
+  , unsafeLiftIx
+  ) where
+
+import           Control.Monad (MonadPlus (..))
+import           Control.Monad.Indexed
+import           Data.Coerce (coerce)
+import           Data.Kind (Type)
+import qualified Prelude as P
+import           Prelude hiding (Monad (..), pure)
+
+
+------------------------------------------------------------------------------
+-- | The free indexed monad generated from a monad 'm'. Users are not expected
+-- to use 'Ix' directly, but to newtype over it, specializing the kinds of 'i'
+-- and 'j' as necessary.
+--
+-- GeneralizedNewtypeDeriving can be used to get the instances of 'IxFunctor',
+-- 'IxPointed', 'IxApplicative', 'IxMonad', 'IxMonadZero' and 'IxMonadPlus' for
+-- free.
+newtype Ix (m :: Type -> Type) i j a = Ix
+  { runIx :: m a
+  }
+  deriving (Functor, Applicative, P.Monad)
+
+instance Functor m => IxFunctor (Ix m) where
+  imap = fmap
+
+instance Applicative m => IxPointed (Ix m) where
+  ireturn = P.pure
+
+instance Applicative m => IxApplicative (Ix m) where
+  iap
+      :: forall i j k a b
+       . Ix m i j (a -> b)
+      -> Ix m j k a
+      -> Ix m i k b
+  iap = coerce $ (<*>) @m @a @b
+
+instance P.Monad m => IxMonad (Ix m) where
+  ibind
+      :: forall i j k a b
+       . (a -> Ix m j k b)
+      -> Ix m i j a
+      -> Ix m i k b
+  ibind = coerce $ (=<<) @m @a @b
+
+instance MonadPlus m => IxMonadZero (Ix m) where
+  imzero
+      :: forall i j a
+       . Ix m i j a
+  imzero = coerce $ mzero @m @a
+
+instance MonadPlus m => IxMonadPlus (Ix m) where
+  implus
+      :: forall i j a
+       . Ix m i j a
+      -> Ix m i j a
+      -> Ix m i j a
+  implus = coerce $ mplus @m @a
+
+
+------------------------------------------------------------------------------
+-- | Lift an 'm' action into 'Ix m', maintaining the current index.
+liftIx :: m a -> Ix m i i a
+liftIx = coerce
+
+------------------------------------------------------------------------------
+-- | Lift an 'm' action into 'Ix m', changing the current index. 'unsafeLiftIx'
+-- is obviously unsafe due to the fact that it can arbitrarily change the
+-- index.
+unsafeLiftIx :: m a -> Ix m i j a
+unsafeLiftIx = coerce
+
diff --git a/src/Language/Haskell/DoNotation.hs b/src/Language/Haskell/DoNotation.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/DoNotation.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE KindSignatures         #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+------------------------------------------------------------------------------
+-- | This module provides new implementations for '(>>=)', '(>>)', 'pure' and
+-- 'return' so that they will work simultaneously with both regular and indexed
+-- monads.
+--
+-- Intended usage:
+--
+-- @@
+--   {-# LANGUAGE RebindableSyntax #-}
+--
+--   import Language.Haskell.DoNotation
+--   import Prelude hiding (Monad (..), pure)
+-- @@
+module Language.Haskell.DoNotation
+  ( BindSyntax (..)
+  , PureSyntax (..)
+  , P.Monad ()
+  , IxMonad ()
+  ) where
+
+import           Control.Monad.Indexed
+import           Data.Coerce
+import           Data.Kind (Constraint)
+import           Data.Kind (Type)
+import qualified Prelude as P
+import           Prelude hiding (Monad (..), pure)
+import           System.IO (IOMode (..))
+
+
+------------------------------------------------------------------------------
+-- | Typeclass that provides 'pure' and 'return'.
+class PureSyntax (x :: Type -> Type) where
+  pure :: a -> x a
+  pure = return
+
+  return :: a -> x a
+  return = pure
+
+
+instance {-# INCOHERENT #-}
+      P.Monad m => PureSyntax m where
+  pure = P.pure
+
+instance (IxMonad m, j ~ i) => PureSyntax (m i j) where
+  pure = ireturn
+
+
+------------------------------------------------------------------------------
+-- | Typeclass that provides '(>>=)' and '(>>)'.
+class BindSyntax (x :: Type -> Type)
+                 (y :: Type -> Type)
+                 (z :: Type -> Type)
+      | x y -> z
+      , x z -> y
+      , y z -> x where
+  (>>=) :: x a -> (a -> y b) -> z b
+
+  (>>) :: x a -> y b -> z b
+  a >> b = a >>= const b
+
+instance  (P.Monad m, x ~ m) => BindSyntax m x m where
+  (>>=) = (P.>>=)
+
+instance {-# INCOHERENT #-}
+      ( IxMonad m
+      , x ~ m i j
+      , y ~ m j k
+      , z ~ m i k
+      ) => BindSyntax x y z where
+  (>>=) = (>>>=)
+
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,119 @@
+{-# LANGUAGE DataKinds                  #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures             #-}
+{-# LANGUAGE PolyKinds                  #-}
+{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE RebindableSyntax           #-}
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE TypeOperators              #-}
+
+import           Control.Monad (void, fail)
+import           Control.Monad.Indexed
+import           Control.Monad.Trans.Ix
+import           Data.Coerce
+import           Data.Kind (Type)
+import           GHC.TypeLits (Nat, type (+))
+import           Language.Haskell.DoNotation
+import           Prelude hiding (Monad (..), pure)
+import qualified System.IO as SIO
+import           System.IO hiding (openFile, Handle)
+
+
+------------------------------------------------------------------------------
+-- | This module just exists to make sure 'iShouldCompile' actually compiles.
+main :: IO ()
+main = do
+  pure ()
+
+
+------------------------------------------------------------------------------
+-- | Function that uses both monads and indexed monads in do blocks.
+iShouldCompile :: IO ()
+iShouldCompile = do
+  putStrLn "hello"
+  void $ runLinear $ do
+    f <- openFile "not a real file" ReadMode
+    closeFile f
+    pure "goodbye"
+  putStrLn $ do
+    c <- ['a' .. 'z']
+    pure c
+
+
+------------------------------------------------------------------------------
+-- | 'Linear' statically tracks the files you open and makes sure you close them
+-- exactly one time.
+newtype Linear (s :: Type)
+               (i :: LinearState)
+               (j :: LinearState) a = Linear
+  { unsafeRunLinear :: Ix IO i j a
+  }
+  deriving (IxFunctor, IxPointed, IxApplicative, IxMonad)
+
+
+------------------------------------------------------------------------------
+-- | Run the underlying IO action if you've closed all the files you opened.
+runLinear
+    :: (forall s. Linear s ('LinearState 0 '[])
+                           ('LinearState n '[]) a)
+    -> IO a
+runLinear = coerce
+
+
+------------------------------------------------------------------------------
+-- | Data kind for tracking our linear state as the index to 'Linear'.
+data LinearState = LinearState
+  { linearNextKey  :: Nat
+  , linearOpenKeys :: [Nat]
+  }
+
+
+------------------------------------------------------------------------------
+-- | A wrapped 'SIO.Handle' with a phantom parameter for the ST trick.
+newtype Handle (s :: Type) key = Handle
+  { unsafeGetHandle :: SIO.Handle
+  }
+
+
+------------------------------------------------------------------------------
+-- | Open a file and track that you did it in the type system.
+openFile
+    :: FilePath
+    -> IOMode
+    -> Linear s ('LinearState next open)
+                ('LinearState (next + 1) (next ': open))
+                (Handle s next)
+openFile = coerce SIO.openFile
+
+
+------------------------------------------------------------------------------
+-- | Close a file and prove it!
+closeFile
+    :: IsOpen key open ~ 'True
+    => Handle s key
+    -> Linear s ('LinearState next open)
+                ('LinearState next (Close key open))
+                ()
+closeFile = coerce SIO.hClose
+
+
+------------------------------------------------------------------------------
+-- | Type family to detect if a file handle is already opened (ie. if it exists
+-- in the open set.
+type family IsOpen
+      (key :: k)
+      (ts :: [k]) :: Bool where
+  IsOpen key '[]         = 'False
+  IsOpen key (key ': ts) = 'True
+  IsOpen key (_x  ': ts) = IsOpen key ts
+
+
+------------------------------------------------------------------------------
+-- | Type family to remove a file handle from the open set.
+type family Close
+      (key :: k)
+      (ts :: [k]) :: [k] where
+  Close key (key ': ts) = ts
+  Close key (_x  ': ts) =
+    _x ': Close key ts
+