diff --git a/hakaru.cabal b/hakaru.cabal
--- a/hakaru.cabal
+++ b/hakaru.cabal
@@ -3,7 +3,7 @@
 cabal-version:       >=1.16
 build-type:          Simple
 name:                hakaru
-version:             0.6.0
+version:             0.7.0
 synopsis:            A probabilistic programming language
 description:         Hakaru is a simply-typed probabilistic programming language, designed
                      for easy specification of probabilistic models, and inference algorithms.
@@ -16,6 +16,8 @@
 category:            Language
 -- extra-source-files:
 
+tested-with: GHC==8.10.2, GHC==8.6.4, GHC==8.4.4, GHC==8.2.2, GHC==8.0.2, GHC==7.10.3, GHC==7.8.4
+
 ----------------------------------------------------------------
 Source-Repository head
     Type:     git
@@ -30,7 +32,7 @@
 Library
     Hs-Source-Dirs:    haskell
     Default-Language:  Haskell2010
-    GHC-Options:       -Wall -fwarn-tabs -j6 
+    -- GHC-Options:       -Wall -fwarn-tabs -j6 
 
     if flag(traceDisintegrate)
         Cpp-Options:   -D__TRACE_DISINTEGRATE__
@@ -94,6 +96,7 @@
                        Language.Hakaru.Evaluation.ExpectMonad,
                        Language.Hakaru.Expect,
                        Language.Hakaru.Inference,
+                       Language.Hakaru.Repl,
                        Language.Hakaru.Command,
                        Language.Hakaru.CodeGen.Wrapper,
                        Language.Hakaru.CodeGen.Flatten,
@@ -107,33 +110,40 @@
                        Data.Text.Utf8
 
     other-modules:     System.MapleSSH
+                       Text.Parsec.Indentation
+                       Text.Parsec.Indentation.Char
+                       Text.Parsec.Indentation.Token
+                       Text.Parser.Indentation.Implementation
 
+    build-tools:       alex,
+                       happy
+
     build-depends:     base                 >= 4.7  && < 5.0,
                        Cabal                >= 1.16,
-                       ghc-prim             >= 0.3  && < 0.6,
+                       ghc-prim             >= 0.3  && < 0.8,
                        transformers         >= 0.3  && < 0.6,
                        transformers-compat  >= 0.3  && < 0.7,
-                       containers           >= 0.5  && < 0.6,
+                       containers           >= 0.5  && < 0.7,
                        semigroups           >= 0.16,
                        pretty               >= 1.1  && < 1.2,
                        logfloat             >= 0.13 && < 0.14,
-                       math-functions       >= 0.1  && < 0.3,
+                       math-functions       >= 0.1  && < 0.4,
                        vector               >= 0.10,
-                       indentation-parsec   >= 0.0,
                        text                 >= 0.11 && < 1.3,
                        parsec               >= 3.1  && < 3.2,
-                       mwc-random           >= 0.13 && < 0.14,
+                       mwc-random           >= 0.13 && < 0.15,
                        directory            >= 1.2  && < 1.4,
                        integration          >= 0.2.0 && < 0.3.0,
-                       primitive            >= 0.5  && < 0.7,
+                       primitive            >= 0.5  && < 0.8,
                        process              >= 1.1  && < 2.0,
                        HUnit                >= 1.2  && < 2.0,
                        mtl                  >= 2.1,
                        filepath             >= 1.1.0.2,
                        bytestring           >= 0.9,
-                       optparse-applicative >= 0.11 && < 0.15,
+                       optparse-applicative >= 0.11 && < 0.16,
                        syb                  >= 0.6,
-                       exact-combinatorics  >= 0.2.0
+                       exact-combinatorics  >= 0.2.0,
+                       repline              >= 0.4
 
 ----------------------------------------------------------------
 Test-Suite system-testsuite
@@ -141,7 +151,7 @@
     Main-is:           Tests/TestSuite.hs
     Hs-Source-Dirs:    haskell
     Default-Language:  Haskell2010
-    GHC-Options:       -Wall -fwarn-tabs
+    -- GHC-Options:       -Wall -fwarn-tabs
 
     other-modules:     Data.Number.Nat
                        Data.Number.Natural
@@ -212,19 +222,21 @@
                        Tests.TestTools
                        Tests.TypeCheck
 
-    build-depends:     base                 >= 4.6  && < 5.0,
+    build-tools:       alex,
+                       happy
+
+    Build-Depends:     base                 >= 4.6  && < 5.0,
                        Cabal                >= 1.16,
-                       ghc-prim             >= 0.3  && < 0.6,
-                       indentation-parsec   >= 0.0,
+                       ghc-prim             >= 0.3  && < 0.8,
                        transformers         >= 0.3  && < 0.6,
-                       containers           >= 0.5  && < 0.6,
+                       containers           >= 0.5  && < 0.7,
                        semigroups           >= 0.16,
                        logfloat             >= 0.13 && < 0.14,
                        parsec               >= 3.1  && < 3.2,
-                       primitive            >= 0.5  && < 0.7,
+                       primitive            >= 0.5  && < 0.8,
                        pretty               >= 1.1  && < 1.2,
-                       mwc-random           >= 0.13 && < 0.14,
-                       math-functions       >= 0.1  && < 0.3,
+                       mwc-random           >= 0.13 && < 0.15,
+                       math-functions       >= 0.1  && < 0.4,
                        integration          >= 0.2  && < 0.3,
                        HUnit                >= 1.2  && < 2.0,
                        QuickCheck           >= 2.6,
@@ -234,7 +246,7 @@
                        text                 >= 0.11 && < 1.3,
                        bytestring           >= 0.9,
                        directory            >= 1.2  && < 1.4,
-                       optparse-applicative >= 0.11 && < 0.15,
+                       optparse-applicative >= 0.11 && < 0.16,
                        syb                  >= 0.6,
                        filepath             >= 1.1.0.2,
                        exact-combinatorics  >= 0.2.0
@@ -246,12 +258,16 @@
     Default-Language:  Haskell2010
     GHC-Options:       -O2 -Wall -fwarn-tabs
 
+    build-tools:       alex,
+                       happy
+
     build-depends:     base                 >= 4.7  && < 5.0,
-                       mwc-random           >= 0.13 && < 0.14,
+                       mwc-random           >= 0.13 && < 0.15,
                        text                 >= 0.11 && < 1.3,
                        pretty               >= 1.1  && < 1.2,
                        vector               >= 0.10,
-                       optparse-applicative >= 0.11 && < 0.15
+                       optparse-applicative >= 0.11 && < 0.16,
+                       hakaru               >= 0.3
 
 ----------------------------------------------------------------
 Executable compile
@@ -261,11 +277,12 @@
     GHC-Options:       -O2 -Wall -fwarn-tabs
 
     build-depends:     base                 >= 4.7  && < 5.0,
-                       mwc-random           >= 0.13 && < 0.14,
+                       mwc-random           >= 0.13 && < 0.15,
                        text                 >= 0.11 && < 1.3,
                        pretty               >= 1.1  && < 1.2,
                        filepath             >= 1.3,
-                       optparse-applicative >= 0.11 && < 0.15
+                       optparse-applicative >= 0.11 && < 0.16,
+                       hakaru               >= 0.3
 
 ----------------------------------------------------------------
 Executable summary
@@ -275,11 +292,12 @@
     GHC-Options:       -O2 -Wall -fwarn-tabs
 
     build-depends:     base                 >= 4.7  && < 5.0,
-                       mwc-random           >= 0.13 && < 0.14,
+                       mwc-random           >= 0.13 && < 0.15,
                        text                 >= 0.11 && < 1.3,
                        pretty               >= 1.1  && < 1.2,
                        filepath             >= 1.3,
-                       optparse-applicative >= 0.11 && < 0.15
+                       optparse-applicative >= 0.11 && < 0.16,
+                       hakaru               >= 0.3
 
 ----------------------------------------------------------------
 Executable hk-maple
@@ -289,11 +307,12 @@
     GHC-Options:       -O2 -Wall -fwarn-tabs
 
     build-depends:     base                 >= 4.7  && < 5.0,
-                       mwc-random           >= 0.13 && < 0.14,
+                       mwc-random           >= 0.13 && < 0.15,
                        text                 >= 0.11 && < 1.3,
                        pretty               >= 1.1  && < 1.2,
-                       optparse-applicative >= 0.13 && < 0.15,
-                       containers           >= 0.5  && < 0.6
+                       optparse-applicative >= 0.13 && < 0.16,
+                       containers           >= 0.5  && < 0.7,
+                       hakaru               >= 0.3
 
 ----------------------------------------------------------------
 Executable density
@@ -303,9 +322,10 @@
     GHC-Options:       -O2 -Wall -fwarn-tabs
 
     build-depends:     base             >= 4.7  && < 5.0,
-                       mwc-random       >= 0.13 && < 0.14,
+                       mwc-random       >= 0.13 && < 0.15,
                        text             >= 0.11 && < 1.3,
-                       pretty           >= 1.1  && < 1.2
+                       pretty           >= 1.1  && < 1.2,
+                       hakaru           >= 0.3
 
 ----------------------------------------------------------------
 Executable disintegrate
@@ -315,10 +335,11 @@
     GHC-Options:       -O2 -Wall -fwarn-tabs
 
     build-depends:     base                 >= 4.7  && < 5.0,
-                       mwc-random           >= 0.13 && < 0.14,
+                       mwc-random           >= 0.13 && < 0.15,
                        text                 >= 0.11 && < 1.3,
                        pretty               >= 1.1  && < 1.2,
-                       optparse-applicative >= 0.11 && < 0.15
+                       optparse-applicative >= 0.11 && < 0.16,
+                       hakaru               >= 0.3
 
 ----------------------------------------------------------------
 Executable pretty
@@ -330,7 +351,8 @@
     build-depends:     base                 >= 4.7  && < 5.0,
                        text                 >= 0.11 && < 1.3,
                        pretty               >= 1.1  && < 1.2,
-                       optparse-applicative >= 0.11 && < 0.15
+                       optparse-applicative >= 0.11 && < 0.16,
+                       hakaru               >= 0.3
 
 ----------------------------------------------------------------
 Executable prettyinternal
@@ -342,7 +364,8 @@
     build-depends:     base                 >= 4.7  && < 5.0,
                        text                 >= 0.11 && < 1.3,
                        pretty               >= 1.1  && < 1.2,
-                       optparse-applicative >= 0.11 && < 0.15
+                       optparse-applicative >= 0.11 && < 0.16,
+                       hakaru               >= 0.3
 
 ----------------------------------------------------------------
 Executable momiji
@@ -352,7 +375,8 @@
     GHC-Options:       -O2 -Wall -fwarn-tabs
 
     build-depends:     base             >= 4.7  && < 5.0,
-                       text             >= 0.11 && < 1.3
+                       text             >= 0.11 && < 1.3,
+                       hakaru           >= 0.3
 
 ----------------------------------------------------------------
 Executable normalize
@@ -362,10 +386,11 @@
     GHC-Options:       -O2 -Wall -fwarn-tabs
 
     build-depends:     base             >= 4.7  && < 5.0,
-                       mwc-random       >= 0.13 && < 0.14,
+                       mwc-random       >= 0.13 && < 0.15,
                        text             >= 0.11 && < 1.3,
                        mtl              >= 2.1,
-                       pretty           >= 1.1  && < 1.2
+                       pretty           >= 1.1  && < 1.2,
+                       hakaru           >= 0.3
 
 
 ----------------------------------------------------------------
@@ -376,13 +401,14 @@
     GHC-Options:       -O2 -Wall -fwarn-tabs
 
     build-depends:     base                 >= 4.7  && < 5.0,
-                       containers           >= 0.5  && < 0.6,
+                       containers           >= 0.5  && < 0.7,
                        text                 >= 0.11 && < 1.3,
                        mtl                  >= 2.1,
-                       optparse-applicative >= 0.11 && < 0.15,
+                       optparse-applicative >= 0.11 && < 0.16,
                        pretty               >= 1.1  && < 1.2,
                        process              >= 1.1  && < 2.0,
-                       semigroups           >= 0.16
+                       semigroups           >= 0.16,
+                       hakaru               >= 0.3
 
 
 ----------------------------------------------------------------
@@ -393,10 +419,11 @@
     GHC-Options:       -O2 -Wall -fwarn-tabs
 
     build-depends:     base             >= 4.7  && < 5.0,
-                       mwc-random       >= 0.13 && < 0.14,
+                       mwc-random       >= 0.13 && < 0.15,
                        text             >= 0.11 && < 1.3,
                        mtl              >= 2.1,
-                       pretty           >= 1.1  && < 1.2
+                       pretty           >= 1.1  && < 1.2,
+                       hakaru           >= 0.3
 
 ----------------------------------------------------------------
 ----------------------------------------------------------- fin.
diff --git a/haskell/Language/Hakaru/CodeGen/CodeGenMonad.hs b/haskell/Language/Hakaru/CodeGen/CodeGenMonad.hs
--- a/haskell/Language/Hakaru/CodeGen/CodeGenMonad.hs
+++ b/haskell/Language/Hakaru/CodeGen/CodeGenMonad.hs
@@ -431,16 +431,19 @@
   -> (CExpr -> CExpr -> CodeGen ())
   -> CodeGen Ident
 declareReductionCG typ unit mul =
-  do (redId:unitId:mulId:[]) <- mapM genIdent' ["red","unit","mul"]
+  do redId <- genIdent' "red"
+     unitId <- genIdent' "unit"
+     mulId <- genIdent' "mul"
      let declType = typePtrDeclaration typ
 
      inId <- genIdent' "in"
      funCG [CVoid] unitId [declType inId] $
        unit . CVar $ inId
 
-     (outId:in2Id:[]) <- mapM genIdent' ["out","in"]
+     outId <- genIdent' "out"
+     in2Id <- genIdent' "in"
      funCG [CVoid] mulId [declType outId,declType in2Id] $
-       mul (CVar outId) (CVar in2Id)
+         mul (CVar outId) (CVar in2Id)
 
      let typ' = case buildType typ of
                   (x:_) -> x
diff --git a/haskell/Language/Hakaru/CodeGen/Flatten.hs b/haskell/Language/Hakaru/CodeGen/Flatten.hs
--- a/haskell/Language/Hakaru/CodeGen/Flatten.hs
+++ b/haskell/Language/Hakaru/CodeGen/Flatten.hs
@@ -822,11 +822,11 @@
   -> CExpr
   -> State [String] [CodeGen ()]
 assignSum' (Inr rest) topIdent =
-  do (_:names) <- get
-     put names
+  do names <- get
+     put (tail names)
      assignSum' rest topIdent
 assignSum' (Inl prod) topIdent =
-  do (name:_) <- get
+  do name <- head <$> get
      return $ assignProd prod topIdent (CVar . Ident $ name)
 
 assignProd
@@ -846,14 +846,14 @@
   -> State [String] [CodeGen ()]
 assignProd' Done _ _ = return []
 assignProd' (Et (Konst d) rest) topIdent (CVar sumIdent) =
-  do (name:names) <- get
-     put names
+  do names <- get
+     put (tail names)
      let varName  = CMember (CMember (CMember topIdent
                                               (Ident "sum")
                                               True)
                                      sumIdent
                                      True)
-                            (Ident name)
+                            (Ident (head names))
                             True
      rest' <- assignProd' rest topIdent (CVar sumIdent)
      return $ [flattenABT d varName] ++ rest'
@@ -1172,7 +1172,9 @@
 gammaCG aE bE =
   \loc -> do
      extDeclareTypes (SMeasure SReal)
-     (_:_:gId:[]) <- mapM reserveIdent ["uniform","normal","gamma"]
+     reserveIdent "uniform"
+     reserveIdent "normal"
+     gId <- reserveIdent "gamma"
      mapM_ (extDeclare . CFunDefExt) [uniformFun,normalFun,gammaFun]
      putExprStat $ loc .=. (CCall (CVar gId) [aE,bE])
 
@@ -1206,7 +1208,9 @@
   \(lam :* End) ->
     \loc ->
       do lamE <- flattenWithName lam
-         (lId:kId:pId:[]) <- mapM genIdent' ["l","k","p"]
+         lId <- genIdent' "l"
+         kId <- genIdent' "k"
+         pId <- genIdent' "p"
          declare SProb lId
          declare SNat  kId
          declare SProb pId
@@ -1439,7 +1443,9 @@
 lseSummateArrayCG body arrayE =
   caseBind body $ \v body' ->
     \loc -> seqDo $ do
-      (maxVId:maxIId:sumId:[]) <- mapM genIdent' ["maxV","maxI","sum"]
+      maxVId <- genIdent' "maxV"
+      maxIId <- genIdent' "maxI"
+      sumId <- genIdent' "sum"
       itId <- createIdent v
       mapM_ (declare SProb) [maxVId,sumId]
       mapM_ (declare SNat)  [maxIId,itId]
@@ -1483,7 +1489,8 @@
 kahanSummationCG body loE hiE =
   caseBind body $ \v body' ->
     \loc -> do
-      (tId:cId:[]) <- mapM genIdent' ["t","c"]
+      tId <- genIdent' "t"
+      cId <- genIdent' "c"
       itId <- createIdent v
       declare SNat itId
       mapM_ (declare SProb) [tId,cId]
@@ -1493,7 +1500,9 @@
       forCG (itE .=. loE)
             (itE .<. hiE)
             (CUnary CPostIncOp itE)
-            (do (xId:yId:zId:[]) <- mapM genIdent' ["x","y","z"]
+            (do xId <- genIdent' "x"
+                yId <- genIdent' "y"
+                zId <- genIdent' "z"
                 mapM_ (declare SProb) [xId,yId,zId]
                 let (xE:yE:zE:[]) = fmap CVar [xId,yId,zId]
                 flattenABT body' xE
diff --git a/haskell/Language/Hakaru/CodeGen/Types.hs b/haskell/Language/Hakaru/CodeGen/Types.hs
--- a/haskell/Language/Hakaru/CodeGen/Types.hs
+++ b/haskell/Language/Hakaru/CodeGen/Types.hs
@@ -278,14 +278,16 @@
   -> State [String] [CDecl]
 datumSum' _ SVoid               = return []
 datumSum' dat (SPlus prod rest) =
-  do (name:names) <- get
-     put names
-     let ident = Ident name
-         mdecl = datumProd dat prod ident
-     rest' <- datumSum' dat rest
-     case mdecl of
-       Nothing -> return rest'
-       Just d  -> return $ [d] ++ rest'
+  do nn <- get
+     case nn of
+      name:names -> do
+       put names
+       let ident = Ident name
+           mdecl = datumProd dat prod ident
+       rest' <- datumSum' dat rest
+       case mdecl of
+         Nothing -> return rest'
+         Just d  -> return $ [d] ++ rest'
 
 datumProd
   :: Sing (HData' t)
@@ -315,13 +317,15 @@
   -> Sing (a :: HakaruFun)
   -> State [String] [CDecl]
 datumPrim dat prim =
-  do (name:names) <- get
-     put names
-     let ident = Ident name
-         decl  = case prim of
-                   SIdent     -> datumDeclaration dat ident
-                   (SKonst k) -> typeDeclaration k ident
-     return [decl]
+  do nn <- get
+     case nn of
+      (name:names) -> do
+       put names
+       let ident = Ident name
+           decl  = case prim of
+                     SIdent     -> datumDeclaration dat ident
+                     (SKonst k) -> typeDeclaration k ident
+       return [decl]
 
 -- index into pair
 datumFst :: CExpr -> CExpr
diff --git a/haskell/Language/Hakaru/Evaluation/DisintegrationMonad.hs b/haskell/Language/Hakaru/Evaluation/DisintegrationMonad.hs
--- a/haskell/Language/Hakaru/Evaluation/DisintegrationMonad.hs
+++ b/haskell/Language/Hakaru/Evaluation/DisintegrationMonad.hs
@@ -96,6 +96,9 @@
 import qualified Data.List.NonEmpty   as NE
 import           Control.Applicative  (Alternative(..))
 import           Control.Monad        (MonadPlus(..),foldM,guard)
+#if __GLASGOW_HASKELL__ > 805
+import           Control.Monad.Fail
+#endif
 import           Data.Text            (Text)
 import qualified Data.Text            as Text
 import           Data.Number.Nat
@@ -580,6 +583,11 @@
 instance Monad (Dis abt) where
     return      = pure
     Dis m >>= k = Dis $ \i c -> m i $ \x -> unDis (k x) i c
+
+#if __GLASGOW_HASKELL__ > 805
+instance MonadFail (Dis abt) where
+    fail        = error
+#endif
 
 instance Alternative (Dis abt) where
     empty           = Dis $ \_ _ _ _ -> []
diff --git a/haskell/Language/Hakaru/Expect.hs b/haskell/Language/Hakaru/Expect.hs
--- a/haskell/Language/Hakaru/Expect.hs
+++ b/haskell/Language/Hakaru/Expect.hs
@@ -201,6 +201,7 @@
         ++ show (pretty_Statements_withTerm ss e)
         ++ "\n") $ return ()
 #endif
+    emitExpectListContext
     w <- pureEvaluate e
     case w of
         -- TODO: if the neutral term is a 'Case_' then we want to go under it
diff --git a/haskell/Language/Hakaru/Parser/Parser.hs b/haskell/Language/Hakaru/Parser/Parser.hs
--- a/haskell/Language/Hakaru/Parser/Parser.hs
+++ b/haskell/Language/Hakaru/Parser/Parser.hs
@@ -1,6 +1,11 @@
 {-# LANGUAGE CPP, OverloadedStrings #-}
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
-module Language.Hakaru.Parser.Parser (parseHakaru, parseHakaruWithImports) where
+module Language.Hakaru.Parser.Parser
+    (
+      parseHakaru
+    , parseHakaruWithImports
+    , parseReplLine
+    ) where
 
 import Prelude hiding (Real)
 
@@ -541,6 +546,24 @@
 
 exprWithImport :: Parser (ASTWithImport' Text)
 exprWithImport = ASTWithImport' <$> (many import_expr) <*> expr
+
+-- Parsing bindings for Hakaru Repl
+type Binding = (AST' Text.Text -> AST' Text.Text)
+
+let_parse :: Parser Binding
+let_parse = Let <$> identifier <* reservedOp "=" <*> expr
+
+bind_parse :: Parser Binding
+bind_parse = Bind <$> identifier <* reservedOp "<~" <*> expr
+
+binding_parse :: Parser Binding
+binding_parse = try let_parse <|> bind_parse
+
+bindingOrExpr :: Parser (Either Binding (AST' Text.Text))
+bindingOrExpr = Left <$> try binding_parse <|> Right <$> expr
+
+parseReplLine :: Text.Text -> Either ParseError (Either Binding (AST' Text.Text))
+parseReplLine x = parseAtTopLevel bindingOrExpr x
 
 -- | A variant of @Text.Parsec.Expr.buildExpressionParser@ (parsec-3.1.11)
 -- that behaves more restrictively when a precedence level contains both
diff --git a/haskell/Language/Hakaru/Pretty/Concrete.hs b/haskell/Language/Hakaru/Pretty/Concrete.hs
--- a/haskell/Language/Hakaru/Pretty/Concrete.hs
+++ b/haskell/Language/Hakaru/Pretty/Concrete.hs
@@ -325,7 +325,7 @@
     parensIf (p > 0) $
     sep [ sep [ text "plate" <+> var
               , text "of" <+> pretty e1 <> colon ]
-        , body ]
+        , nest 2 body ]
 
 ppSCon p Chain = \(e1 :* e2 :* e3 :* End) ->
     let (var, _, body) = ppBinder1 e3 in
@@ -333,7 +333,7 @@
     sep [ sep [ text "chain" <+> var
               , text "from" <+> pretty e2
               , text "of" <+> pretty e1 <> colon ]
-        , body ]
+        , nest 2 body ]
 
 ppSCon p Integrate = \(e1 :* e2 :* e3 :* End) ->
     let (var, _, body) = ppBinder1 e3 in
@@ -341,7 +341,7 @@
     sep [ sep [ text "integrate" <+> var
               , text "from" <+> pretty e1
               , text "to" <+> pretty e2 <> colon ]
-        , body ]
+        , nest 2 body ]
 
 ppSCon p (Summate _ _) = \(e1 :* e2 :* e3 :* End) ->
     let (var, _, body) = ppBinder1 e3 in
@@ -349,7 +349,7 @@
     sep [ sep [ text "summate" <+> var
               , text "from" <+> pretty e1
               , text "to" <+> pretty e2 <> colon ]
-        , body ]
+        , nest 2 body ]
 
 ppSCon p (Product _ _) = \(e1 :* e2 :* e3 :* End) ->
     let (var, _, body) = ppBinder1 e3 in
@@ -357,7 +357,7 @@
     sep [ sep [ text "product" <+> var
               , text "from" <+> pretty e1
               , text "to" <+> pretty e2 <> colon ]
-        , body ]
+        , nest 2 body ]
 
 ppSCon p (Transform_ t) = ppTransform p t
 
@@ -371,7 +371,7 @@
         e1 :* e2 :* End ->
           let (var, _, body) = ppBinder1 e2 in
           parensIf (p > 0) $
-          sep [ text "expect" <+> var <+> pretty e1 <> colon
+          sep [ text "expect" <+> var <+> text "<~" <+> pretty e1 <> colon
               , body ]
     _ -> ppApply p (transformName t) es
 
diff --git a/haskell/Language/Hakaru/Repl.hs b/haskell/Language/Hakaru/Repl.hs
new file mode 100644
--- /dev/null
+++ b/haskell/Language/Hakaru/Repl.hs
@@ -0,0 +1,188 @@
+{-# LANGUAGE CPP
+           , DataKinds
+           , OverloadedStrings
+           , FlexibleContexts
+           , GADTs
+           , RankNTypes
+           #-}
+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
+module Language.Hakaru.Repl where
+
+
+import           Language.Hakaru.Types.Sing
+import           Language.Hakaru.Syntax.ABT
+import qualified Language.Hakaru.Syntax.AST as T
+import           Language.Hakaru.Syntax.AST.Transforms
+import           Language.Hakaru.Syntax.Variable ()
+import qualified Language.Hakaru.Parser.AST as U
+import           Language.Hakaru.Parser.Parser (parseHakaru, parseReplLine)
+import           Language.Hakaru.Parser.SymbolResolve (resolveAST)
+import           Language.Hakaru.Pretty.Concrete
+import           Language.Hakaru.Syntax.TypeCheck
+import           Language.Hakaru.Sample
+import           Language.Hakaru.Syntax.Value
+
+import           Control.Monad.State.Strict (StateT, evalStateT, get, modify)
+import           Control.Monad.IO.Class
+import           Data.List (intercalate)
+import qualified Data.Text      as Text
+import qualified Data.Text.IO   as IO
+import qualified Data.Vector    as V
+import           Text.PrettyPrint (renderStyle, style, mode, Mode(LeftMode))
+import qualified System.Random.MWC as MWC
+import           System.Console.Repline
+
+type Binding = (U.AST' Text.Text -> U.AST' Text.Text)
+type ReplM = HaskelineT (StateT Binding IO)
+
+initialReplState :: Binding
+initialReplState = id
+
+extendBindings :: Binding -> Binding -> Binding
+extendBindings = flip (.)
+
+triv :: TrivialABT T.Term '[] a -> TrivialABT T.Term '[] a
+triv = id
+
+app1 :: a -> U.AST' a -> U.AST' a
+app1 s x = U.Var s `U.App` x
+       
+resolveAndInfer :: U.AST' Text.Text
+              -> Either Text.Text (TypedAST (TrivialABT T.Term))
+resolveAndInfer x = resolveAndInferWithMode x LaxMode
+
+resolveAndInferWithMode
+  :: ABT T.Term abt
+  => U.AST' Text.Text
+  -> TypeCheckMode
+  -> Either Text.Text (TypedAST abt)
+resolveAndInferWithMode x mode' =
+    let m = inferType (resolveAST x) in
+    runTCM m Nothing mode'
+
+               
+splitLines :: Text.Text -> Maybe (V.Vector Text.Text)
+splitLines = Just . V.fromList . Text.lines
+
+whenE :: MonadIO m => Either Text.Text b -> m () -> m ()
+whenE (Left  err) _ = liftIO $ IO.putStrLn err
+whenE (Right _)   m = m 
+             
+illustrate :: Sing a -> MWC.GenIO -> Value a -> IO ()
+illustrate (SMeasure s) g (VMeasure m) = do
+    x <- m (VProb 1) g
+    case x of
+      Just (samp, _) -> illustrate s g samp
+      Nothing        -> illustrate (SMeasure s) g (VMeasure m)
+
+illustrate _ _ x = renderLn x
+
+renderLn :: Value a -> IO ()
+renderLn = putStrLn . renderStyle style {mode = LeftMode} . prettyValue
+             
+runOnce :: MWC.GenIO -> U.AST' Text.Text -> IO ()
+runOnce g prog =
+  case resolveAndInfer prog of
+    Left err -> IO.putStrLn err
+    Right (TypedAST typ ast) ->
+        illustrate typ g (runEvaluate ast)
+
+type_ :: Cmd ReplM
+type_ prog =
+    case parseHakaru (Text.pack prog) of
+      Left err -> liftIO $ putStrLn (show err)
+      Right e  -> do
+        bindings <- get
+        let prog' = bindings (app1 "dirac" e)
+        case resolveAndInfer prog' of
+          Left err -> liftIO $ IO.putStrLn err
+          Right (TypedAST (SMeasure typ) _) -> liftIO $ putStrLn (prettyTypeS typ)
+          _        -> liftIO $ putStrLn "the impossible happened"
+                   
+initM :: ReplM ()
+initM = liftIO $ putStrLn introBanner
+                   
+-- Evaluation
+
+-- No Typechecking of bindings
+cmd :: MWC.GenIO -> String -> ReplM ()
+cmd g x =
+    case parseReplLine (Text.pack x) of
+      Left err         -> liftIO $ putStrLn (show err)
+      Right (Left b)   -> modify (extendBindings b) 
+      Right (Right e)  -> do
+        bindings <- get
+        let prog' = bindings (app1 "dirac" e)
+        liftIO $ runOnce g prog'
+
+
+-- Typecheck bindings before adding them
+cmd2 :: MWC.GenIO -> Cmd ReplM
+cmd2 g x =
+    case parseReplLine (Text.pack x) of
+      Left err  -> liftIO $ putStrLn (show err)
+      Right e   -> do
+        bindings <- get
+        case e of
+          Left b   -> let prog = bindings . b $ (app1 "dirac" U.Unit) in
+                      whenE (resolveAndInfer prog) (modify $ extendBindings b)
+          Right e' -> let prog = bindings (app1 "dirac" e') in
+                      liftIO $ runOnce g prog
+               
+repl :: MWC.GenIO -> IO ()
+repl g = flip evalStateT initialReplState
+        $ evalReplOpts $ ReplOpts
+         { banner           = const (pure ">>> ")
+         , command          = cmd2 g
+         , options          = opts
+         , prefix           = Just ':'
+         , multilineCommand = Nothing
+         , tabComplete      = (Word comp)
+         , initialiser      = initM
+         , finaliser        = return Exit
+         }
+
+                   
+-- Completion
+comp :: Monad m => WordCompleter m
+comp = listWordCompleter [":help", ":expand", ":hist", ":type"]
+
+-- Commands
+help :: Cmd ReplM
+help _ = liftIO $ putStrLn "Help!"
+
+expand :: Cmd ReplM
+expand prog =
+    case parseReplLine (Text.pack prog) of
+      Left err         -> liftIO $ putStrLn (show err)
+      Right (Left b)   -> modify (extendBindings b) 
+      Right (Right e)  -> do
+        bindings <- get
+        let prog' = bindings e
+        case resolveAndInfer prog' of
+          Left err -> liftIO $ IO.putStrLn err
+          Right (TypedAST _ ast) -> liftIO $ print (pretty (expandTransformations ast))
+
+
+hist :: Cmd ReplM
+hist = undefined
+
+opts :: Options ReplM
+opts = [
+    ("help", help),
+    ("expand", expand),
+    ("hist", hist),
+    ("type", type_)
+  ]
+
+introBanner :: String
+introBanner = unlines
+  ["    __  __      __",
+   "   / / / /___ _/ /______ ________  __",
+   "  / /_/ / __ `/ //_/ __ `/ ___/ / / /",
+   " / __  / /_/ / ,< / /_/ / /  / /_/ /",
+   "/_/ /_/\\__,_/_/|_|\\__,_/_/   \\__,_/"
+  ]
+
+main :: IO ()
+main = MWC.createSystemRandom >>= repl
diff --git a/haskell/Language/Hakaru/Simplify.hs b/haskell/Language/Hakaru/Simplify.hs
--- a/haskell/Language/Hakaru/Simplify.hs
+++ b/haskell/Language/Hakaru/Simplify.hs
@@ -50,7 +50,7 @@
 simplifyWithOpts o = sendToMaple o{command=MapleCommand Simplify}
 
 simplify'
-    :: forall abt a
+    :: forall abt
     .  (ABT Term (abt Term)) 
     => TypedAST (abt Term)  -> IO (TypedAST (abt Term))
 simplify' = sendToMaple' defaultMapleOptions{command="Simplify"}
diff --git a/haskell/Language/Hakaru/Syntax/ABT.hs b/haskell/Language/Hakaru/Syntax/ABT.hs
--- a/haskell/Language/Hakaru/Syntax/ABT.hs
+++ b/haskell/Language/Hakaru/Syntax/ABT.hs
@@ -3,6 +3,7 @@
            , GADTs
            , DataKinds
            , PolyKinds
+           , TypeInType
            , TypeOperators
            , Rank2Types
            , MultiParamTypeClasses
@@ -88,6 +89,7 @@
 #endif
 
 import Control.Monad.Identity    
+import Data.Kind
 import Data.Number.Nat
 import Language.Hakaru.Syntax.IClasses
 -- TODO: factor the definition of the 'Sing' type family out from
@@ -131,7 +133,7 @@
 -- smart constructors of the ABT class. But if we don't expose this
 -- type, then clients can't define their own ABT instances (without
 -- reinventing their own copy of this type)...
-data View :: (k -> *) -> [k] -> k -> * where
+data View :: (k -> Type) -> [k] -> k -> Type where
     -- BUG: haddock doesn't like annotations on GADT constructors
     -- <https://github.com/hakaru-dev/hakaru/issues/6>
 
@@ -174,22 +176,22 @@
     traverse12 f (Bind x e) = Bind x <$> traverse12 f e
 
 
-instance (Show1 (Sing :: k -> *), Show1 rec)
-    => Show2 (View (rec :: k -> *))
+instance (Show1 (Sing :: k -> Type), Show1 rec)
+    => Show2 (View (rec :: k -> Type))
     where
     showsPrec2 p (Syn  t)   = showParen_1  p "Syn"  t
     showsPrec2 p (Var  x)   = showParen_1  p "Var"  x
     showsPrec2 p (Bind x v) = showParen_12 p "Bind" x v
 
-instance (Show1 (Sing :: k -> *), Show1 rec)
-    => Show1 (View (rec :: k -> *) xs)
+instance (Show1 (Sing :: k -> Type), Show1 rec)
+    => Show1 (View (rec :: k -> Type) xs)
     where
     showsPrec1 = showsPrec2
     show1      = show2
 
 -- TODO: could weaken the Show1 requirements to Show requirements...
-instance (Show1 (Sing :: k -> *), Show1 rec)
-    => Show (View (rec :: k -> *) xs a)
+instance (Show1 (Sing :: k -> Type), Show1 rec)
+    => Show (View (rec :: k -> Type) xs a)
     where
     showsPrec = showsPrec1
     show      = show1
@@ -197,7 +199,7 @@
 
 -- TODO: neelk includes 'subst' as a method. Any reason we should?
 -- TODO: jon includes instantiation as a method. Any reason we should?
--- TODO: require @(JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Foldable21 syn)@ since all our instances will need those too?
+-- TODO: require @(JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type), Foldable21 syn)@ since all our instances will need those too?
 --
 -- | The class interface for abstract binding trees. The first
 -- argument, @syn@, gives the syntactic signature of the ABT;
@@ -214,7 +216,7 @@
 -- only be able to work for particular @syn@ signatures. This isn't
 -- the case for 'TrivialABT' nor 'MemoizedABT', but isn't too
 -- far-fetched.
-class ABT (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *) | abt -> syn where
+class ABT (syn :: ([k] -> k -> Type) -> k -> Type) (abt :: [k] -> k -> Type) | abt -> syn where
     -- Smart constructors for building a 'View' and then injecting it into the @abt@.
     syn  :: syn abt  a -> abt '[] a
     var  :: Variable a -> abt '[] a
@@ -378,11 +380,11 @@
 -- expensive for this ABT, because we have to traverse the term
 -- every time we want to call them. The 'MemoizedABT' implementation
 -- fixes this.
-newtype TrivialABT (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k) =
+newtype TrivialABT (syn :: ([k] -> k -> Type) -> k -> Type) (xs :: [k]) (a :: k) =
     TrivialABT (View (syn (TrivialABT syn)) xs a)
 
-instance (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Foldable21 syn)
-    => ABT (syn :: ([k] -> k -> *) -> k -> *) (TrivialABT syn)
+instance (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type), Foldable21 syn)
+    => ABT (syn :: ([k] -> k -> Type) -> k -> Type) (TrivialABT syn)
     where
     syn  t                = TrivialABT (Syn  t)
     var  x                = TrivialABT (Var  x)
@@ -434,8 +436,8 @@
 
 
 -- BUG: requires UndecidableInstances
-instance (Show1 (Sing :: k -> *), Show1 (syn (TrivialABT syn)))
-    => Show2 (TrivialABT (syn :: ([k] -> k -> *) -> k -> *))
+instance (Show1 (Sing :: k -> Type), Show1 (syn (TrivialABT syn)))
+    => Show2 (TrivialABT (syn :: ([k] -> k -> Type) -> k -> Type))
     where
     {-
     -- Print the concrete data constructors:
@@ -452,15 +454,15 @@
     showsPrec2 p (TrivialABT (Var  x))   = showParen_1  p "var"  x
     showsPrec2 p (TrivialABT (Bind x v)) = showParen_11 p "bind" x (TrivialABT v)
 
-instance (Show1 (Sing :: k -> *), Show1 (syn (TrivialABT syn)))
-    => Show1 (TrivialABT (syn :: ([k] -> k -> *) -> k -> *) xs)
+instance (Show1 (Sing :: k -> Type), Show1 (syn (TrivialABT syn)))
+    => Show1 (TrivialABT (syn :: ([k] -> k -> Type) -> k -> Type) xs)
     where
     showsPrec1 = showsPrec2
     show1      = show2
 
 -- TODO: could weaken the Show1 requirements to Show requirements...
-instance (Show1 (Sing :: k -> *), Show1 (syn (TrivialABT syn)))
-    => Show (TrivialABT (syn :: ([k] -> k -> *) -> k -> *) xs a)
+instance (Show1 (Sing :: k -> Type), Show1 (syn (TrivialABT syn)))
+    => Show (TrivialABT (syn :: ([k] -> k -> Type) -> k -> Type) xs a)
     where
     showsPrec = showsPrec1
     show      = show1
@@ -489,7 +491,7 @@
 -- N.B., the memoized set of free variables is lazy so that we can
 -- tie-the-knot in 'binder' without interfering with our memos. The
 -- memoized 'nextFree' must be lazy for the same reason.
-data MemoizedABT (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k) =
+data MemoizedABT (syn :: ([k] -> k -> Type) -> k -> Type) (xs :: [k]) (a :: k) =
     MemoizedABT
         { _memoizedFreeVars :: VarSet (KindOf a) -- N.B., lazy!
         , memoizedNextFree  :: Nat -- N.B., lazy!
@@ -502,8 +504,8 @@
 memoizedFreeVars (MemoizedABT xs _ _ _) = xs
 
 
-instance (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Foldable21 syn)
-    => ABT (syn :: ([k] -> k -> *) -> k -> *) (MemoizedABT syn)
+instance (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type), Foldable21 syn)
+    => ABT (syn :: ([k] -> k -> Type) -> k -> Type) (MemoizedABT syn)
     where
     syn t =
         MemoizedABT
@@ -559,8 +561,8 @@
     nextBind = memoizedNextBind
 
 
-instance (Show1 (Sing :: k -> *), Show1 (syn (MemoizedABT syn)))
-    => Show2 (MemoizedABT (syn :: ([k] -> k -> *) -> k -> *))
+instance (Show1 (Sing :: k -> Type), Show1 (syn (MemoizedABT syn)))
+    => Show2 (MemoizedABT (syn :: ([k] -> k -> Type) -> k -> Type))
     where
     showsPrec2 p (MemoizedABT xs nf nb v) =
         showParen (p > 9)
@@ -574,15 +576,15 @@
             . showsPrec1 11 v
             )
 
-instance (Show1 (Sing :: k -> *), Show1 (syn (MemoizedABT syn)))
-    => Show1 (MemoizedABT (syn :: ([k] -> k -> *) -> k -> *) xs)
+instance (Show1 (Sing :: k -> Type), Show1 (syn (MemoizedABT syn)))
+    => Show1 (MemoizedABT (syn :: ([k] -> k -> Type) -> k -> Type) xs)
     where
     showsPrec1 = showsPrec2
     show1      = show2
 
 -- TODO: could weaken the Show1 requirements to Show requirements...
-instance (Show1 (Sing :: k -> *), Show1 (syn (MemoizedABT syn)))
-    => Show (MemoizedABT (syn :: ([k] -> k -> *) -> k -> *) xs a)
+instance (Show1 (Sing :: k -> Type), Show1 (syn (MemoizedABT syn)))
+    => Show (MemoizedABT (syn :: ([k] -> k -> Type) -> k -> Type) xs a)
     where
     showsPrec = showsPrec1
     show      = show1
@@ -595,8 +597,8 @@
 -- Right now this essentially inlines the the TrivialABT instance
 -- but it would be nice if it was abstract in the choice of ABT.
 data MetaABT
-    (meta :: *)
-    (syn  :: ([k] -> k -> *) -> k -> *)
+    (meta :: Type)
+    (syn  :: ([k] -> k -> Type) -> k -> Type)
     (xs   :: [k])
     (a    :: k) =
     MetaABT
@@ -610,8 +612,8 @@
     -> MetaABT meta syn xs a
 withMetadata x (MetaABT _ v) = MetaABT (Just x) v
 
-instance (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Foldable21 syn)
-    => ABT (syn :: ([k] -> k -> *) -> k -> *) (MetaABT meta syn)
+instance (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type), Foldable21 syn)
+    => ABT (syn :: ([k] -> k -> Type) -> k -> Type) (MetaABT meta syn)
     where
     syn t                   = MetaABT Nothing (Syn  t)
     var x                   = MetaABT Nothing (Var  x)
@@ -651,10 +653,10 @@
 
 
 
-instance ( Show1 (Sing :: k -> *)
+instance ( Show1 (Sing :: k -> Type)
          , Show1 (syn (MetaABT meta syn))
          , Show  meta)
-    => Show2 (MetaABT meta (syn :: ([k] -> k -> *) -> k -> *))
+    => Show2 (MetaABT meta (syn :: ([k] -> k -> Type) -> k -> Type))
     where
     showsPrec2 p (MetaABT meta v) =
         showParen (p > 9)
@@ -664,18 +666,18 @@
             . showsPrec1 11 v
             )
 
-instance ( Show1 (Sing :: k -> *)
+instance ( Show1 (Sing :: k -> Type)
          , Show1 (syn (MetaABT meta syn))
          , Show  meta)
-    => Show1 (MetaABT meta (syn :: ([k] -> k -> *) -> k -> *) xs)
+    => Show1 (MetaABT meta (syn :: ([k] -> k -> Type) -> k -> Type) xs)
     where
     showsPrec1 = showsPrec2
     show1      = show2
 
-instance ( Show1 (Sing :: k -> *)
+instance ( Show1 (Sing :: k -> Type)
          , Show1 (syn (MetaABT meta syn))
          , Show  meta)
-    => Show (MetaABT meta (syn :: ([k] -> k -> *) -> k -> *) xs a)
+    => Show (MetaABT meta (syn :: ([k] -> k -> Type) -> k -> Type) xs a)
     where
     showsPrec = showsPrec1
     show      = show1
@@ -690,7 +692,7 @@
 -- If it isn't in the set, then just return it.
 -- FIXME: this is actually not used!
 freshen
-    :: (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *))
+    :: (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type))
     => Variable (a :: k)
     -> VarSet (KindOf a)
     -> Variable a
@@ -705,8 +707,8 @@
 --
 -- | Rename a free variable. Does nothing if the variable is bound.
 rename
-    :: forall syn abt (a :: k) xs (b :: k)
-    .  (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Functor21 syn, ABT syn abt)
+    :: forall k syn abt (a :: k) xs (b :: k)
+    .  (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type), Functor21 syn, ABT syn abt)
     => Variable a
     -> Variable a
     -> abt xs b
@@ -755,8 +757,8 @@
 -- to ensure timely throwing of exceptions, the 'Term' and 'ABT'
 -- should have strict 'fmap21' definitions.
 subst
-    :: forall syn abt (a :: k) xs (b :: k)
-    .  (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Traversable21 syn, ABT syn abt)
+    :: forall k syn abt (a :: k) xs (b :: k)
+    .  (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type), Traversable21 syn, ABT syn abt)
     => Variable a
     -> abt '[]  a
     -> abt xs   b
@@ -772,8 +774,8 @@
       varCase = return . var
                      
 substM
-    :: forall syn abt (a :: k) xs (b :: k) m
-    .  (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *),
+    :: forall k syn abt (a :: k) xs (b :: k) m
+    .  (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type),
         Traversable21 syn, ABT syn abt,
         Applicative m, Functor m, Monad m)
     => Variable a
@@ -816,17 +818,17 @@
                
 
 renames
-    :: forall
-        (syn :: ([k] -> k -> *) -> k -> *)
-        (abt :: [k] -> k -> *)
+    :: forall k
+        (syn :: ([k] -> k -> Type) -> k -> Type)
+        (abt :: [k] -> k -> Type)
         (xs  :: [k])
         (a   :: k)
     .   ( ABT syn abt
-        , JmEq1 (Sing :: k -> *)
-        , Show1 (Sing :: k -> *)
+        , JmEq1 (Sing :: k -> Type)
+        , Show1 (Sing :: k -> Type)
         , Functor21 syn
         )
-    => Assocs (Variable :: k -> *)
+    => Assocs (Variable :: k -> Type)
     -> abt xs a
     -> abt xs a
 renames rho0 =
@@ -837,8 +839,8 @@
 -- called (//) in Jon's abt library. We use this textual name so we can also have 'insts' for the n-ary version, rather than iterating the unary version. Or we could use something like (!) and (!!), albeit those names tend to be used to mean other things. It'd be nice to do (@) and (@@), but the first one is illegal.
 inst
     :: forall syn abt (a :: k) xs (b :: k)
-    .   ( JmEq1 (Sing :: k -> *)
-        , Show1 (Sing :: k -> *)
+    .   ( JmEq1 (Sing :: k -> Type)
+        , Show1 (Sing :: k -> Type)
         , Functor21 syn
         , ABT syn abt
         )
@@ -854,14 +856,14 @@
 -- BUG: This appears to have both capture and escape issues as demonstrated by 'Tests.Disintegrate.test0' and commented on at 'Language.Hakaru.Evaluation.Types.runM'.
 -- | The parallel version of 'subst' for performing multiple substitutions at once.
 substs
-    :: forall
-        (syn :: ([k] -> k -> *) -> k -> *)
-        (abt :: [k] -> k -> *)
+    :: forall k
+        (syn :: ([k] -> k -> Type) -> k -> Type)
+        (abt :: [k] -> k -> Type)
         (xs  :: [k])
         (a   :: k)
     .   ( ABT syn abt
-        , JmEq1 (Sing :: k -> *)
-        , Show1 (Sing :: k -> *)
+        , JmEq1 (Sing :: k -> Type)
+        , Show1 (Sing :: k -> Type)
         , Traversable21 syn
         )
     => Assocs (abt '[])
@@ -1028,10 +1030,10 @@
 -- need access to the original ABT, then this function has somewhat
 -- less overhead.
 cataABT
-    :: forall
-        (abt :: [k] -> k -> *)
-        (syn :: ([k] -> k -> *) -> k -> *)
-        (r   :: [k] -> k -> *)
+    :: forall k
+        (abt :: [k] -> k -> Type)
+        (syn :: ([k] -> k -> Type) -> k -> Type)
+        (r   :: [k] -> k -> Type)
     .  (ABT syn abt, Functor21 syn)
     => (forall a.      Variable a -> r '[] a)
     -> (forall x xs a. Variable x -> r xs a -> r (x ': xs) a)
@@ -1053,11 +1055,11 @@
 -- inputs, which allows the @bind@ and @syn@ operations to update the monadic
 -- context in which the subterms are evaluated if need be.
 cataABTM
-    :: forall
-        (abt :: [k] -> k -> *)
-        (syn :: ([k] -> k -> *) -> k -> *)
-        (r   :: [k] -> k -> *)
-        (f   :: * -> *)
+    :: forall k
+        (abt :: [k] -> k -> Type)
+        (syn :: ([k] -> k -> Type) -> k -> Type)
+        (r   :: [k] -> k -> Type)
+        (f   :: Type -> Type)
     .  (ABT syn abt, Traversable21 syn, Applicative f)
     => (forall a.      Variable a  -> f (r '[] a))
     -> (forall x xs a. Variable x  -> f (r xs a) -> f (r (x ': xs) a))
@@ -1090,10 +1092,10 @@
 -- this is a top-down function; however, if you treat them strictly
 -- then it becomes a bottom-up function.
 paraABT
-    :: forall
-        (abt :: [k] -> k -> *)
-        (syn :: ([k] -> k -> *) -> k -> *)
-        (r   :: [k] -> k -> *)
+    :: forall k
+        (abt :: [k] -> k -> Type)
+        (syn :: ([k] -> k -> Type) -> k -> Type)
+        (r   :: [k] -> k -> Type)
     .  (ABT syn abt, Functor21 syn)
     => (forall a.      Variable a -> r '[] a)
     -> (forall x xs a. Variable x -> abt xs a -> r xs a -> r (x ': xs) a)
@@ -1119,7 +1121,7 @@
 -- | If the expression is a variable, then look it up. Recursing
 -- until we can finally return some syntax.
 resolveVar
-    :: (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), ABT syn abt)
+    :: (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type), ABT syn abt)
     => abt '[] (a :: k)
     -> Assocs (abt '[])
     -> Either (Variable a) (syn abt a)
diff --git a/haskell/Language/Hakaru/Syntax/TypeCheck.hs b/haskell/Language/Hakaru/Syntax/TypeCheck.hs
--- a/haskell/Language/Hakaru/Syntax/TypeCheck.hs
+++ b/haskell/Language/Hakaru/Syntax/TypeCheck.hs
@@ -134,7 +134,7 @@
 
     -- In general (according to Dunfield & Pientka), we should be
     -- able to infer the result of a fully saturated primop by
-    -- looking up it's type and then checking all the arguments.
+    -- looking up its type and then checking all the arguments.
     go (U.PrimOp_  _ _)   = False
     go (U.ArrayOp_ _ es)  = F.all mustCheck es
 
@@ -479,22 +479,26 @@
        U.Summate_ e1 e2 e3 -> do
            TypedAST typ1 e1' <- inferType e1
            e2' <- checkType_ typ1 e2
-           inferBinder typ1 e3 $ \typ2 ee' ->
-               case (hDiscrete_Sing typ1, hSemiring_Sing typ2) of
-                 (Just h1, Just h2) ->
+           case hDiscrete_Sing typ1 of
+             Nothing -> failwith_ "Summate given bounds which are not discrete"
+             Just h1 -> inferBinder typ1 e3 $ \typ2 ee' ->
+               case hSemiring_Sing typ2 of
+                 Nothing -> failwith_ "Summate given summands which are not in a semiring"
+                 Just h2 ->
                      return . TypedAST typ2 $
                             syn (Summate h1 h2 :$ e1' :* e2' :* ee' :* End)
-                 _                  -> failwith_ "Summate given bounds which are not discrete"
 
        U.Product_ e1 e2 e3 -> do
            TypedAST typ1 e1' <- inferType e1
            e2' <- checkType_ typ1 e2
-           inferBinder typ1 e3 $ \typ2 e3' ->
-               case (hDiscrete_Sing typ1, hSemiring_Sing typ2) of
-                 (Just h1, Just h2) ->
+           case hDiscrete_Sing typ1 of
+             Nothing -> failwith_ "Product given bounds which are not discrete"
+             Just h1 -> inferBinder typ1 e3 $ \typ2 e3' ->
+               case hSemiring_Sing typ2 of
+                 Nothing -> failwith_ "Product given factors which are not in a semiring"
+                 Just h2 ->
                      return . TypedAST typ2 $
                             syn (Product h1 h2 :$ e1' :* e2' :* e3' :* End)
-                 _                  -> failwith_ "Product given bounds which are not discrete"
 
        U.Bucket_ e1 e2 r1 -> do
            e1' <- checkType_ SNat e1
@@ -1113,17 +1117,37 @@
                          sourceSpan
                          "infinity can only be checked against nat or prob"
 
+        U.Product_ e1 e2 e3 ->
+           case hSemiring_Sing typ0 of
+             Nothing -> failwith_ "Product given factors which are not in a semiring"
+             Just h2 -> do
+               TypedAST typ1 e1' <- inferType e1
+               e2' <- checkType_ typ1 e2
+               case hDiscrete_Sing typ1 of
+                 Nothing -> failwith_ "Product given bounds which are not discrete"
+                 Just h1 -> do
+                     e3' <- checkBinder typ1 typ0 e3
+                     return $ syn (Product h1 h2 :$ e1' :* e2' :* e3' :* End)
+
         U.NaryOp_ op es -> do
             mode <- getMode
             case mode of
               StrictMode -> safeNaryOp typ0
               LaxMode    -> safeNaryOp typ0
-              UnsafeMode -> do
+              UnsafeMode -> case op of
+               U.Prod -> do
                 op' <- make_NaryOp typ0 op
                 (bads, goods) <-
-                  fmap partitionEithers . T.forM es $
-                  \e -> fmap (maybe (Left e) Right)
-                             (tryWith LaxMode (checkType_ typ0 e))
+                  fmap partitionEithers . T.forM es $ \e -> do
+                    r <- tryWith LaxMode (checkType_ typ0 e)
+                    case r of
+                      Just er -> return (Right er)
+                      Nothing -> do
+                        r <- try (do TypedAST t p <- inferType e
+                                     checkOrCoerce sourceSpan p t typ0)
+                        case r of
+                          Just er -> return (Right er)
+                          Nothing -> return (Left e)
                 if null bads
                 then return $ syn (NaryOp_ op' (S.fromList goods))
                 else do TypedAST typ bad <- inferType (case bads of
@@ -1133,6 +1157,13 @@
                         return (case bad:goods of
                           [e] -> e
                           es' -> syn $ NaryOp_ op' (S.fromList es'))
+               _ -> do
+                es' <- tryWith LaxMode (safeNaryOp typ0)
+                case es' of
+                  Just es'' -> return es''
+                  Nothing   -> do
+                    TypedAST typ e0' <- inferType (syn $ U.NaryOp_ op es)
+                    checkOrUnsafeCoerce sourceSpan e0' typ typ0
             where
             safeNaryOp :: forall c. Sing c -> TypeCheckMonad (abt '[] c)
             safeNaryOp typ = do
diff --git a/haskell/Language/Hakaru/Syntax/TypeCheck/TypeCheckMonad.hs b/haskell/Language/Hakaru/Syntax/TypeCheck/TypeCheckMonad.hs
--- a/haskell/Language/Hakaru/Syntax/TypeCheck/TypeCheckMonad.hs
+++ b/haskell/Language/Hakaru/Syntax/TypeCheck/TypeCheckMonad.hs
@@ -34,6 +34,9 @@
 import           Control.Applicative   (Applicative(..), (<$>))
 import           Data.Monoid           (Monoid(..))
 #endif
+#if __GLASGOW_HASKELL__ > 805
+import           Control.Monad.Fail
+#endif
 import qualified Language.Hakaru.Parser.AST as U
 
 import Language.Hakaru.Syntax.IClasses
@@ -84,6 +87,11 @@
         TCM $ \ctx input mode ->
         unTCM mx ctx input mode >>= \x ->
         unTCM (k x) ctx input mode
+
+#if __GLASGOW_HASKELL__ > 805
+instance MonadFail TypeCheckMonad where
+    fail = error
+#endif
 
 {-
 -- We could provide this instance, but there's no decent error
diff --git a/haskell/Language/Hakaru/Syntax/Variable.hs b/haskell/Language/Hakaru/Syntax/Variable.hs
--- a/haskell/Language/Hakaru/Syntax/Variable.hs
+++ b/haskell/Language/Hakaru/Syntax/Variable.hs
@@ -5,6 +5,7 @@
            , FlexibleContexts
            , DeriveDataTypeable
            , ExistentialQuantification
+           , TypeInType
            , UndecidableInstances
            , ScopedTypeVariables
            #-}
@@ -66,6 +67,7 @@
 
 import           Data.Proxy        (KProxy(..))
 import           Data.Typeable     (Typeable)
+import           Data.Kind
 import           Data.Text         (Text)
 import           Data.IntMap       (IntMap)
 import qualified Data.IntMap       as IM
@@ -123,7 +125,7 @@
 -- TODO: instance Read (Variable a)
 
 -- HACK: this requires UndecidableInstances
-instance Show1 (Sing :: k -> *) => Show1 (Variable :: k -> *) where
+instance Show1 (Sing :: k -> Type) => Show1 (Variable :: k -> Type) where
     showsPrec1 p (Variable hint i typ) =
         showParen (p > 9)
             ( showString "Variable "
@@ -197,7 +199,7 @@
 -- Whichever interpretation we choose, we must make sure that typing
 -- contexts, binding environments, and so on all behave consistently.
 varEq
-    :: (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *))
+    :: (Show1 (Sing :: k -> Type), JmEq1 (Sing :: k -> Type))
     => Variable (a :: k)
     -> Variable (b :: k)
     -> Maybe (TypeEq a b)
@@ -233,7 +235,7 @@
 -- when 'varEq' chooses the second interpretation.
 data VarEqTypeError where
     VarEqTypeError
-        :: (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *))
+        :: (Show1 (Sing :: k -> Type), JmEq1 (Sing :: k -> Type))
         => {-# UNPACK #-} !(Variable (a :: k))
         -> {-# UNPACK #-} !(Variable (b :: k))
         -> VarEqTypeError
@@ -278,7 +280,7 @@
 
 
 -- This instance requires the 'JmEq1' and 'Show1' constraints because we use 'varEq'.
-instance (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *))
+instance (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type))
     => Eq (SomeVariable (kproxy :: KProxy k))
     where
     SomeVariable x == SomeVariable y =
@@ -288,7 +290,7 @@
 
 
 -- This instance requires the 'JmEq1' and 'Show1' constraints because 'Ord' requires the 'Eq' instance, which in turn requires those constraints.
-instance (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *))
+instance (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type))
     => Ord (SomeVariable (kproxy :: KProxy k))
     where
     SomeVariable x `compare` SomeVariable y =
@@ -298,7 +300,7 @@
 -- TODO: instance Read SomeVariable
 
 
-instance Show1 (Sing :: k -> *)
+instance Show1 (Sing :: k -> Type)
     => Show (SomeVariable (kproxy :: KProxy k))
     where
     showsPrec p (SomeVariable v) =
@@ -313,7 +315,7 @@
 newtype VarSet (kproxy :: KProxy k) =
     VarSet { unVarSet :: IntMap (SomeVariable kproxy) }
 
-instance Show1 (Sing :: k -> *) => Show (VarSet (kproxy :: KProxy k)) where
+instance Show1 (Sing :: k -> Type) => Show (VarSet (kproxy :: KProxy k)) where
     showsPrec p (VarSet xs) =
         showParen (p > 9)
             ( showString "VarSet "
@@ -412,7 +414,7 @@
 
 
 memberVarSet
-    :: (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *))
+    :: (Show1 (Sing :: k -> Type), JmEq1 (Sing :: k -> Type))
     => Variable (a :: k)
     -> VarSet (kproxy :: KProxy k)
     -> Bool
@@ -429,16 +431,16 @@
 -- What is the best behaviour when we have two variables with
 -- different types in the set?
 unionVarSet
-    :: forall (kproxy :: KProxy k)
-    .  (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *))
+    :: forall k (kproxy :: KProxy k)
+    .  (Show1 (Sing :: k -> Type), JmEq1 (Sing :: k -> Type))
     => VarSet kproxy
     -> VarSet kproxy
     -> VarSet kproxy
 unionVarSet (VarSet s1) (VarSet s2) = VarSet (IM.union s1 s2)
 
 intersectVarSet
-    :: forall (kproxy :: KProxy k)
-    .  (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *))
+    :: forall k (kproxy :: KProxy k)
+    .  (Show1 (Sing :: k -> Type), JmEq1 (Sing :: k -> Type))
     => VarSet kproxy
     -> VarSet kproxy
     -> VarSet kproxy
@@ -454,12 +456,12 @@
 -- <https://github.com/hakaru-dev/hakaru/issues/6>
 --
 -- | A pair of variable and term, both of the same Hakaru type.
-data Assoc (ast :: k -> *)
+data Assoc (ast :: k -> Type)
     = forall (a :: k) . Assoc
         {-# UNPACK #-} !(Variable a)
         !(ast a)
 
-instance (Show1 (Sing :: k -> *), Show1 (ast :: k -> *))
+instance (Show1 (Sing :: k -> Type), Show1 (ast :: k -> Type))
     => Show (Assoc ast)
     where
     showsPrec p (Assoc x e) =
@@ -485,7 +487,7 @@
 -- then the implementation must be updated.
 newtype Assocs ast = Assocs { unAssocs :: IntMap (Assoc ast) }
 
-instance (Show1 (Sing :: k -> *), Show1 (ast :: k -> *))
+instance (Show1 (Sing :: k -> Type), Show1 (ast :: k -> Type))
     => Show (Assocs ast)
     where
     showsPrec p rho =
@@ -581,7 +583,7 @@
 --
 -- N.B., this function is robust to all interpretations of 'varEq'.
 lookupAssoc
-    :: (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *))
+    :: (Show1 (Sing :: k -> Type), JmEq1 (Sing :: k -> Type))
     => Variable (a :: k)
     -> Assocs ast
     -> Maybe (ast a)
diff --git a/haskell/Tests/RoundTrip.hs b/haskell/Tests/RoundTrip.hs
--- a/haskell/Tests/RoundTrip.hs
+++ b/haskell/Tests/RoundTrip.hs
@@ -206,22 +206,52 @@
     
 testStdChiSqRelations :: Test
 testStdChiSqRelations = test [
+    "t_stdChiSq_superposition" ~: testConcreteFiles "tests/RoundTrip2/t_stdChiSq_superposition.0.hk" "tests/RoundTrip2/t_stdChiSq_superposition.expected.hk",
+    "t_uniform_to_stdChiSq" ~: testConcreteFiles "tests/RoundTrip2/t_uniform_to_stdChiSq.0.hk" "tests/RoundTrip2/t_uniform_to_stdChiSq.expected.hk",
+    "t_stdChiSq_to_beta" ~: testConcreteFiles "tests/RoundTrip2/t_stdChiSq_to_beta.0.hk" "tests/RoundTrip2/t_stdChiSq_to_beta.expected.hk",
     "t_stdChiSq_to_gamma"   ~: testConcreteFiles "tests/RoundTrip/t_stdChiSq_to_gamma.0.hk" "tests/RoundTrip/t_stdChiSq_to_gamma.expected.hk",
     "t_stdChiSq_to_exponential" ~: testConcreteFiles "tests/RoundTrip2/t_stdChiSq_to_exponential.0.hk" "tests/RoundTrip2/t_stdChiSq_to_exponential.expected.hk",
     "t_rayleigh_to_stdChiSq"     ~: testConcreteFiles "tests/RoundTrip2/t_rayleigh_to_stdChiSq.0.hk" "tests/RoundTrip2/t_rayleigh_to_stdChiSq.expected.hk"        
     ]
 
+
+testCauchyRelations :: Test 
+testCauchyRelations = test [
+    "t_cauchy_add_transformation" ~: testConcreteFiles "tests/RoundTrip2/t_cauchy_add_transformation.0.hk" "tests/RoundTrip2/t_cauchy_add_transformation.expected.hk",
+    "t_cauchy_sub_transformation" ~: testConcreteFiles "tests/RoundTrip2/t_cauchy_sub_transformation.0.hk" "tests/RoundTrip2/t_cauchy_sub_transformation.expected.hk"
+    ]
+
 testExponentialRelations :: Test 
-testExponentialRelations = test [ 
-    "t_exponential_to_stdChiSq"     ~: testConcreteFiles "tests/RoundTrip/t_exponential_to_stdChiSq.0.hk" "tests/RoundTrip/t_exponential_to_stdChiSq.expected.hk"
+testExponentialRelations = test [
+    "t_pareto_to_exponential"        ~: testConcreteFiles "tests/RoundTrip/t_pareto_to_exponential.0.hk" "tests/RoundTrip/t_pareto_to_exponential.expected.hk",
+    "t_exponential_to_pareto"        ~: testConcreteFiles "tests/RoundTrip/t_exponential_to_pareto.0.hk" "tests/RoundTrip/t_exponential_to_pareto.expected.hk",
+    "t_exponential_to_laplace"        ~: testConcreteFiles "tests/RoundTrip/t_exponential_to_laplace.0.hk" "tests/RoundTrip/t_exponential_to_laplace.expected.hk",
+    "t_exponential_to_beta"        ~: testConcreteFiles "tests/RoundTrip/t_exponential_to_beta.0.hk" "tests/RoundTrip/t_exponential_to_beta.expected.hk",
+
+    "t_exponential_sum_to_erlang"        ~: testConcreteFiles "tests/RoundTrip/t_exponential_sum_to_erlang.0.hk" "tests/RoundTrip/t_exponential_sum_to_erlang.expected.hk",
+
+    "t_exp_erlang_to_pareto"        ~: testConcreteFiles "tests/RoundTrip/t_exp_erlang_to_pareto.0.hk" "tests/RoundTrip/t_exp_erlang_to_pareto.expected.hk",
+    "t_exponential_sum_rates"        ~: testConcreteFiles "tests/RoundTrip/t_exponential_sum_rates.0.hk" "tests/RoundTrip/t_exponential_sum_rates.expected.hk",
+    "t_exponential_to_stdChiSq"     ~: testConcreteFiles "tests/RoundTrip/t_exponential_to_stdChiSq.0.hk" "tests/RoundTrip/t_exponential_to_stdChiSq.expected.hk",
+    "t_exponential_scale_closure"   ~: testConcreteFiles "tests/RoundTrip/t_exponential_scale_closure.0.hk" "tests/RoundTrip/t_exponential_scale_closure.expected.hk"
     ]
 
 testErlangRelations :: Test
 testErlangRelations = test [
-        "t_erlang_to_pareto"   ~: testConcreteFiles "tests/RoundTrip2/t_erlang_to_pareto.0.hk" "tests/RoundTrip2/t_erlang_to_pareto.expected.hk",
-    "t_erlang_to_stdChiSq"   ~: testConcreteFiles "tests/RoundTrip2/t_erlang_to_stdChiSq.0.hk" "tests/RoundTrip2/t_erlang_to_stdChiSq.expected.hk"        
+    "t_erlang_to_erlang"   ~: testConcreteFiles "tests/RoundTrip/t_erlang_to_erlang.0.hk" "tests/RoundTrip/t_erlang_to_erlang.expected.hk",
+    "t_erlang_to_erlang_2"   ~: testConcreteFiles "tests/RoundTrip/t_erlang_to_erlang_1.0.hk" "tests/RoundTrip/t_erlang_to_erlang_1.expected.hk",
+    "t_exponential_to_erlang"   ~: testConcreteFiles "tests/RoundTrip/t_exponential_to_erlang.0.hk" "tests/RoundTrip/t_exponential_to_erlang.expected.hk",
+    "t_erlang_to_pareto"   ~: testConcreteFiles "tests/RoundTrip2/t_erlang_to_pareto.0.hk" "tests/RoundTrip2/t_erlang_to_pareto.expected.hk",
+    "t_erlang_to_stdChiSq"   ~: testConcreteFiles "tests/RoundTrip2/t_erlang_to_stdChiSq.0.hk" "tests/RoundTrip2/t_erlang_to_stdChiSq.expected.hk"
     ]
 
+testRayleighRelations :: Test 
+testRayleighRelations = test [
+    "t_exponential_to_rayleigh" ~: testConcreteFiles "tests/RoundTrip2/t_exponential_to_rayleigh.0.hk" "tests/RoundTrip2/t_exponential_to_rayleigh.expected.hk",
+    "t_gamma_to_rayleigh" ~: testConcreteFiles "tests/RoundTrip2/t_gamma_to_rayleigh.0.hk" "tests/RoundTrip2/t_gamma_to_rayleigh.expected.hk",
+    "t_weibull_to_rayleigh" ~: testConcreteFiles "tests/RoundTrip2/t_weibull_to_rayleigh.0.hk" "tests/RoundTrip2/t_weibull_to_rayleigh.expected.hk"
+    ]
+
 testOther :: Test
 testOther = test [
     "t82"              ~: testConcreteFiles "tests/RoundTrip/t82.0.hk" "tests/RoundTrip/t82.expected.hk",
@@ -265,7 +295,10 @@
     , testMeasureInt
     , testErlangRelations
     , testStdChiSqRelations
+    , testCauchyRelations
     , testExponentialRelations
+    , testRayleighRelations
+    , testCauchyRelations
     , testOther
     ]
 
diff --git a/haskell/Tests/TestTools.hs b/haskell/Tests/TestTools.hs
--- a/haskell/Tests/TestTools.hs
+++ b/haskell/Tests/TestTools.hs
@@ -3,6 +3,7 @@
            , RankNTypes
            , GADTs
            , PolyKinds
+           , TypeInType
            , ScopedTypeVariables
            , FlexibleContexts #-}
 {-# OPTIONS_GHC -Wall -fwarn-tabs #-}
@@ -33,6 +34,7 @@
 
 import Data.Maybe (isJust)
 import Data.List
+import Data.Kind
 import qualified Data.Text    as T
 import qualified Data.Text.Utf8 as IO
 import Data.Typeable (Typeable)
@@ -129,7 +131,7 @@
 assertAlphaEq preface a b =
    unless (alphaEq a b) (assertFailure $ mismatchMessage pretty preface a b)
 
-mismatchMessage :: forall (k :: q -> *) . (forall a . k a -> Doc) -> String -> forall a b . k a -> k b -> String 
+mismatchMessage :: forall q (k :: q -> Type) . (forall a . k a -> Doc) -> String -> forall a b . k a -> k b -> String 
 mismatchMessage k preface a b = msg 
  where msg = concat [ p
                     , "expected:\n"
diff --git a/haskell/Text/Parsec/Indentation.hs b/haskell/Text/Parsec/Indentation.hs
new file mode 100644
--- /dev/null
+++ b/haskell/Text/Parsec/Indentation.hs
@@ -0,0 +1,209 @@
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances, TupleSections #-}
+{-# OPTIONS -Wall  #-}
+module Text.Parsec.Indentation (module Text.Parsec.Indentation, I.IndentationRel(..), Indentation, infIndentation) where
+
+-- Implements "Indentation Senstivie Parising: Landin Revisited"
+--
+-- Primary functions are:
+--  - 'localIndent':
+--  - 'absoluteIndent':
+--  - 'localTokenMode':
+--
+-- Primary driver functions are:
+--  - TODO
+
+-- TODO:
+--   Grace style indentation stream
+
+import Control.Monad
+--import Text.Parsec.Prim
+import Text.Parsec.Prim (ParsecT, mkPT, runParsecT,
+                         Stream(..), Consumed(..), Reply(..),
+                         State(..), getInput, setInput)
+import Text.Parsec.Error (Message (Message), addErrorMessage)
+import Text.Parser.Indentation.Implementation as I
+
+------------------------
+-- Indentable Stream
+------------------------
+
+data IndentStream s = IndentStream { indentationState :: !IndentationState, tokenStream :: !s } deriving (Show)
+--data IndentationToken t = IndentationToken !t | InvalidIndentation String
+type IndentationToken t = t
+
+{-# INLINE mkIndentStream #-}
+mkIndentStream :: Indentation -> Indentation -> Bool -> IndentationRel -> s -> IndentStream s
+mkIndentStream lo hi mode rel s = IndentStream (mkIndentationState lo hi mode rel) s
+
+instance (Monad m, Stream s m (t, Indentation)) => Stream (IndentStream s) m (IndentationToken t) where
+  uncons (IndentStream is s) = do
+    x <- uncons s
+    case x of
+      Nothing -> return Nothing
+      Just ((t, i), s') -> return $ updateIndentation is i ok err where
+        ok is' = Just ({-IndentationToken-} t, IndentStream is' s')
+        err _ = Nothing --(InvalidIndentation msg, IndentStream is s)
+        -- HACK: Sigh! We have no way to properly signal the
+        -- sort of failure that occurs here.  We would do 'fail
+        -- "Invalid indentation.  "++msg', but that triggers a
+        -- non-backtracking error.  'return Nothing' will make
+        -- Parsec think the stream is empty (which is wrong),
+        -- but at least it is a backtracking error.  The
+        -- fundamental problem is that 'm' *not* ParsecT (where
+        -- we could signal a parsing error) but is whatever
+        -- monad 'm' happens to be the argument to ParsecT.
+
+{-# INLINE localState #-}
+localState :: (Monad m) => LocalState (ParsecT (IndentStream s) u m a)
+localState pre post m = do
+  IndentStream is s <- getInput
+  setInput (IndentStream (pre is) s)
+  x <- m
+  IndentStream is' s' <- getInput
+  setInput (IndentStream (post is is') s')
+  return x
+
+{-# INLINE localStateUnlessAbsMode #-}
+localStateUnlessAbsMode :: (Monad m) => LocalState (ParsecT (IndentStream s) u m a)
+localStateUnlessAbsMode pre post m = do
+  a <- liftM (indentationStateAbsMode . indentationState) getInput
+  if a then m else localState pre post m
+
+
+------------------------
+-- Operations
+------------------------
+
+{-# INLINE localTokenMode #-}
+localTokenMode :: (Monad m) => (IndentationRel -> IndentationRel) -> ParsecT (IndentStream s) u m a -> ParsecT (IndentStream s) u m a
+localTokenMode = I.localTokenMode localState
+
+{-# INLINE localIndentation #-}
+localIndentation :: (Monad m) => IndentationRel -> ParsecT (IndentStream s) u m a -> ParsecT (IndentStream s) u m a
+localIndentation = I.localIndentation localStateUnlessAbsMode
+
+{-# INLINE absoluteIndentation #-}
+absoluteIndentation :: (Monad m) => ParsecT (IndentStream s) u m a -> ParsecT (IndentStream s) u m a
+absoluteIndentation = I.absoluteIndentation localState
+--  post _  i2 = when (absMode i2) (fail "absoluteIndent: no tokens consumed") >>
+
+{-# INLINE ignoreAbsoluteIndentation #-}
+ignoreAbsoluteIndentation :: (Monad m) => ParsecT (IndentStream s) u m a -> ParsecT (IndentStream s) u m a
+ignoreAbsoluteIndentation = I.ignoreAbsoluteIndentation localState
+
+{-# INLINE localAbsoluteIndentation #-}
+localAbsoluteIndentation :: (Monad m) => ParsecT (IndentStream s) u m a -> ParsecT (IndentStream s) u m a
+localAbsoluteIndentation = I.localAbsoluteIndentation localState
+
+------------------------
+-- Indent Stream Impls
+------------------------
+
+streamToList :: (Monad m, Stream s m t) => s -> m [t]
+streamToList s = do
+  x <- uncons s
+  case x of
+    Nothing -> return []
+    Just (c, s') -> do s'' <- streamToList s'
+                       return (c : s'')
+
+----------------
+-- SourcePos
+
+{-
+mkSourcePosIndentStream s = SourcePosIndentStream s
+newtype SourcePosIndentStream s = SourcePosIndentStream s
+instance (Stream s m t) => Stream (SourcePosIndentStream s) m (Indent, t) where
+  uncons (SourcePosIndentStream s) = do
+    col <- liftM sourceColumn $ getPosition
+    x <- uncons s
+    case x of
+      Nothing -> return Nothing
+      Just x -> return (Just ((col, x), SourcePosIndentStream s))
+-}
+
+
+----------------
+-- TODO: parser based on first non-whitespace char
+
+----------------
+-- First token of line indents
+
+----------------
+-- Based on Indents
+
+-- Note that if 'p' consumes input but is at the wrong indentation, then
+-- 'indentStreamParser p' signals an error but does *not* consume input.
+-- This allows Parsec primitives like 'string' to be properly backtracked.
+{-# INLINE indentStreamParser #-}
+indentStreamParser :: (Monad m) => ParsecT s u m (t, Indentation) -> ParsecT (IndentStream s) u m (IndentationToken t)
+indentStreamParser p = mkPT $ \state ->
+  let IndentStream is s = stateInput state
+      go f (Ok (a, i) state' e) = updateIndentation is i ok err where
+        ok is' = return $ f $ return (Ok ({-IndentationToken-} a) (state' {stateInput = IndentStream is' (stateInput state') }) e)
+        err msg = return $ Empty $ return $ Error (Message ("Invalid indentation.  "++msg++show ((stateInput state) { tokenStream = ""})) `addErrorMessage` e)
+      go f (Error e) = return $ f $ return (Error e)
+  in runParsecT p (state { stateInput = s }) >>= consumed (go Consumed) (go Empty)
+
+{-# INLINE consumed #-}
+consumed :: (Monad m) => (a -> m b) -> (a -> m b) -> Consumed (m a) -> m b
+consumed c _ (Consumed m) = m >>= c
+consumed _ e (Empty m)    = m >>= e
+
+-- lifting operator
+-- token, tokens, tokenPrim, tokenPrimEx ???
+-- whiteSpace
+-- ByteString
+-- ByteString.Lazy
+-- Text
+
+{-
+delimitedLayout :: Stream (IndentStream s) m t =>
+  ParsecT (IndentStream s) u m open -> Bool ->
+  ParsecT (IndentStream s) u m close -> Bool ->
+  ParsecT (IndentStream s) u m a -> ParsecT (IndentStream s) u m a
+delimitedLayout open openAny close closeAny body = between open' close' (localIndent (Const 0) body) where
+  open'  | openAny = localIndent (Const 0) open
+         | otherwise = open
+  close' | closeAny = localIndent (Const 0) close
+         | otherwise = close
+
+indentedLayout :: Stream (IndentStream s) m t =>
+  (Maybe (ParsecT (IndentStream s) u m sep)) ->
+  ParsecT (IndentStream s) u m a -> ParsecT (IndentStream s) u m [a]
+indentedLayout (Nothing ) clause = localIndent Gt $ many $ absoluteIndent $ clause
+indentedLayout (Just sep) clause = liftM concat $ localIndent Gt $ many $ absoluteIndent $ sepBy1 clause sep
+-}
+
+{-
+layout p = delimitedLayout (symbol "{") False (symbol "}") True (semiSep p)
+       <|> indentedLayout (Just semi) p
+
+identifier pred = liftM fromString $ try $ identifier >>= \x -> guard (pred x) >> return x
+operator pred = liftM fromString $ try $ operator >>= \x -> guard (pred x) >> return x
+
+reserved name = (if name `elem` middleKeywords then localFirstTokenMode (const Ge) else id) $ reserved name
+
+Numbers, Integers and Naturals are custom
+
+dotSep
+dotSep1
+
+-}
+
+{-
+test :: String
+test = foo where
+          foo = "abc \
+\def" ++ ""
+
+test2 :: Int
+test2 = foo where
+          foo = let { x = 1;
+ } in x
+
+
+--- All code indented?
+  foo = 3
+  bar = 4
+-}
diff --git a/haskell/Text/Parsec/Indentation/Char.hs b/haskell/Text/Parsec/Indentation/Char.hs
new file mode 100644
--- /dev/null
+++ b/haskell/Text/Parsec/Indentation/Char.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
+module Text.Parsec.Indentation.Char where
+
+import Text.Parsec.Prim (ParsecT, mkPT, runParsecT,
+                         Stream(..),
+                         Consumed(..), Reply(..),
+                         State(..))
+import Text.Parsec.Pos (sourceColumn)
+import Text.Parser.Indentation.Implementation (Indentation)
+
+----------------
+-- Unicode char
+-- newtype UnicodeIndentStream
+
+----------------
+-- Based on Char
+{-# INLINE mkCharIndentStream #-}
+mkCharIndentStream :: s -> CharIndentStream s
+mkCharIndentStream s = CharIndentStream 1 s
+data CharIndentStream s = CharIndentStream { charIndentStreamColumn :: {-# UNPACK #-} !Indentation,
+                                             charIndentStreamStream :: !s } deriving (Show)
+
+instance (Stream s m Char) => Stream (CharIndentStream s) m (Char, Indentation) where
+  uncons (CharIndentStream i s) = do
+    x <- uncons s
+    case x of
+      Nothing -> return Nothing
+      Just (c, cs) -> return (Just ((c, i), CharIndentStream (updateColumn i c) cs))
+
+{-# INLINE updateColumn #-}
+updateColumn :: Integral a => a -> Char -> a
+updateColumn _ '\n' = 1
+updateColumn i '\t' = i + 8 - ((i-1) `mod` 8)
+updateColumn i _    = i + 1
+
+{-# INLINE charIndentStreamParser #-}
+charIndentStreamParser :: (Monad m) => ParsecT s u m t -> ParsecT (CharIndentStream s) u m (t, Indentation)
+charIndentStreamParser p = mkPT $ \state ->
+  let go (Ok a state' e) = return (Ok (a, sourceColumn $ statePos state) (state' { stateInput = CharIndentStream (sourceColumn $ statePos state') (stateInput state') }) e)
+      go (Error e) = return (Error e)
+  in runParsecT p (state { stateInput = charIndentStreamStream (stateInput state) })
+         >>= consumed (return . Consumed . go) (return . Empty . go)
+
+{-# INLINE consumed #-}
+consumed :: (Monad m) => (a -> m b) -> (a -> m b) -> Consumed (m a) -> m b
+consumed c _ (Consumed m) = m >>= c
+consumed _ e (Empty m)    = m >>= e
diff --git a/haskell/Text/Parsec/Indentation/Token.hs b/haskell/Text/Parsec/Indentation/Token.hs
new file mode 100644
--- /dev/null
+++ b/haskell/Text/Parsec/Indentation/Token.hs
@@ -0,0 +1,400 @@
+{-# LANGUAGE FlexibleContexts, NoMonomorphismRestriction #-}
+{-# OPTIONS -Wall -fno-warn-unused-do-bind -fno-warn-name-shadowing #-}
+module Text.Parsec.Indentation.Token where
+
+import Control.Monad.Identity
+import Data.Char
+import Data.List (nub, sort)
+import Text.Parsec
+import Text.Parsec.Token
+
+import Text.Parsec.Indentation
+import Text.Parsec.Indentation.Char (CharIndentStream(..), charIndentStreamParser)
+
+type IndentLanguageDef st = GenLanguageDef (IndentStream (CharIndentStream String)) st Identity
+
+makeIndentLanguageDef :: (Monad m) => GenLanguageDef s st m -> GenLanguageDef (IndentStream (CharIndentStream s)) st m
+makeIndentLanguageDef l = l {
+  identStart = indentStreamParser (charIndentStreamParser (identStart l)),
+  identLetter = indentStreamParser (charIndentStreamParser (identLetter l)),
+  opStart = indentStreamParser (charIndentStreamParser (opStart l)),
+  opLetter = indentStreamParser (charIndentStreamParser (opLetter l))
+  }
+
+-- TODO: makeTokenParser :: (Stream (IndentStream s) m Char)
+makeTokenParser :: (Stream s m (Char, Indentation))
+                => GenLanguageDef (IndentStream s) u m -> GenTokenParser (IndentStream s) u m
+makeTokenParser languageDef
+    = TokenParser{ identifier = identifier
+                 , reserved = reserved
+                 , operator = operator
+                 , reservedOp = reservedOp
+
+                 , charLiteral = charLiteral
+                 , stringLiteral = stringLiteral
+                 , natural = natural
+                 , integer = integer
+                 , float = float
+                 , naturalOrFloat = naturalOrFloat
+                 , decimal = decimal
+                 , hexadecimal = hexadecimal
+                 , octal = octal
+
+                 , symbol = symbol
+                 , lexeme = lexeme
+                 , whiteSpace = whiteSpace
+                 , parens = parens
+                 , braces = braces
+                 , angles = angles
+                 , brackets = brackets
+                 , squares = brackets
+                 , semi = semi
+                 , comma = comma
+                 , colon = colon
+                 , dot = dot
+                 , semiSep = semiSep
+                 , semiSep1 = semiSep1
+                 , commaSep = commaSep
+                 , commaSep1 = commaSep1
+                 }
+    where
+
+    -----------------------------------------------------------
+    -- Bracketing
+    -----------------------------------------------------------
+    parens p        = between (symbol "(") (symbol ")") p
+    braces p        = between (symbol "{") (symbol "}") p
+    angles p        = between (symbol "<") (symbol ">") p
+    brackets p      = between (symbol "[") (symbol "]") p
+
+    semi            = symbol ";"
+    comma           = symbol ","
+    dot             = symbol "."
+    colon           = symbol ":"
+
+    commaSep p      = sepBy p comma
+    semiSep p       = sepBy p semi
+
+    commaSep1 p     = sepBy1 p comma
+    semiSep1 p      = sepBy1 p semi
+
+
+    -----------------------------------------------------------
+    -- Chars & Strings
+    -----------------------------------------------------------
+    charLiteral     = lexeme (between (char '\'')
+                                      (char '\'' <?> "end of character")
+                                      characterChar )
+                    <?> "character"
+
+    characterChar   = charLetter <|> charEscape
+                    <?> "literal character"
+
+    charEscape      = do{ char '\\'; escapeCode }
+    charLetter      = satisfy (\c -> (c /= '\'') && (c /= '\\') && (c > '\026'))
+
+
+
+    stringLiteral   = lexeme (
+                      do{ str <- between (char '"')
+                                         (localTokenMode (const Any) (char '"' <?> "end of string"))
+                                         (localTokenMode (const Any) (many stringChar))
+                        ; return (foldr (maybe id (:)) "" str)
+                        }
+                      <?> "literal string")
+
+    stringChar      =   do{ c <- stringLetter; return (Just c) }
+                    <|> stringEscape
+                    <?> "string character"
+
+    stringLetter    = satisfy (\c -> (c /= '"') && (c /= '\\') && (c > '\026'))
+
+    stringEscape    = do{ char '\\'
+                        ;     do{ escapeGap  ; return Nothing }
+                          <|> do{ escapeEmpty; return Nothing }
+                          <|> do{ esc <- escapeCode; return (Just esc) }
+                        }
+
+    escapeEmpty     = char '&'
+    escapeGap       = do{ many1 space
+                        ; char '\\' <?> "end of string gap"
+                        }
+
+
+
+    -- escape codes
+    escapeCode      = charEsc <|> charNum <|> charAscii <|> charControl
+                    <?> "escape code"
+
+    charControl     = do{ char '^'
+                        ; code <- upper
+                        ; return (toEnum (fromEnum code - fromEnum 'A'))
+                        }
+
+    charNum         = do{ code <- decimal
+                                  <|> do{ char 'o'; number 8 octDigit }
+                                  <|> do{ char 'x'; number 16 hexDigit }
+                        ; return (toEnum (fromInteger code))
+                        }
+
+    charEsc         = choice (map parseEsc escMap)
+                    where
+                      parseEsc (c,code)     = do{ char c; return code }
+
+    charAscii       = choice (map parseAscii asciiMap)
+                    where
+                      parseAscii (asc,code) = try (do{ string asc; return code })
+
+
+    -- escape code tables
+    escMap          = zip ("abfnrtv\\\"\'") ("\a\b\f\n\r\t\v\\\"\'")
+    asciiMap        = zip (ascii3codes ++ ascii2codes) (ascii3 ++ ascii2)
+
+    ascii2codes     = ["BS","HT","LF","VT","FF","CR","SO","SI","EM",
+                       "FS","GS","RS","US","SP"]
+    ascii3codes     = ["NUL","SOH","STX","ETX","EOT","ENQ","ACK","BEL",
+                       "DLE","DC1","DC2","DC3","DC4","NAK","SYN","ETB",
+                       "CAN","SUB","ESC","DEL"]
+
+    ascii2          = ['\BS','\HT','\LF','\VT','\FF','\CR','\SO','\SI',
+                       '\EM','\FS','\GS','\RS','\US','\SP']
+    ascii3          = ['\NUL','\SOH','\STX','\ETX','\EOT','\ENQ','\ACK',
+                       '\BEL','\DLE','\DC1','\DC2','\DC3','\DC4','\NAK',
+                       '\SYN','\ETB','\CAN','\SUB','\ESC','\DEL']
+
+
+    -----------------------------------------------------------
+    -- Numbers
+    -----------------------------------------------------------
+    naturalOrFloat  = lexeme (natFloat) <?> "number"
+
+    float           = lexeme floating   <?> "float"
+    integer         = lexeme int        <?> "integer"
+    natural         = lexeme nat        <?> "natural"
+
+
+    -- floats
+    floating        = do{ n <- decimal
+                        ; fractExponent n
+                        }
+
+
+    natFloat        = do{ char '0'
+                        ; zeroNumFloat
+                        }
+                      <|> decimalFloat
+
+    zeroNumFloat    =  do{ n <- hexadecimal <|> octal
+                         ; return (Left n)
+                         }
+                    <|> decimalFloat
+                    <|> fractFloat 0
+                    <|> return (Left 0)
+
+    decimalFloat    = do{ n <- decimal
+                        ; option (Left n)
+                                 (fractFloat n)
+                        }
+
+    fractFloat n    = do{ f <- fractExponent n
+                        ; return (Right f)
+                        }
+
+    fractExponent n = do{ fract <- fraction
+                        ; expo  <- option 1.0 exponent'
+                        ; return ((fromInteger n + fract)*expo)
+                        }
+                    <|>
+                      do{ expo <- exponent'
+                        ; return ((fromInteger n)*expo)
+                        }
+
+    fraction        = do{ char '.'
+                        ; digits <- many1 digit <?> "fraction"
+                        ; return (foldr op 0.0 digits)
+                        }
+                      <?> "fraction"
+                    where
+                      op d f    = (f + fromIntegral (digitToInt d))/10.0
+
+    exponent'       = do{ oneOf "eE"
+                        ; f <- sign
+                        ; e <- decimal <?> "exponent"
+                        ; return (power (f e))
+                        }
+                      <?> "exponent"
+                    where
+                       power e  | e < 0      = 1.0/power(-e)
+                                | otherwise  = fromInteger (10^e)
+
+
+    -- integers and naturals
+    int             = do{ f <- lexeme sign
+                        ; n <- nat
+                        ; return (f n)
+                        }
+
+    sign            =   (char '-' >> return negate)
+                    <|> (char '+' >> return id)
+                    <|> return id
+
+    nat             = zeroNumber <|> decimal
+
+    zeroNumber      = do{ char '0'
+                        ; hexadecimal <|> octal <|> decimal <|> return 0
+                        }
+                      <?> ""
+
+    decimal         = number 10 digit
+    hexadecimal     = do{ oneOf "xX"; number 16 hexDigit }
+    octal           = do{ oneOf "oO"; number 8 octDigit  }
+
+    number base baseDigit
+        = do{ digits <- many1 baseDigit
+            ; let n = foldl (\x d -> base*x + toInteger (digitToInt d)) 0 digits
+            ; seq n (return n)
+            }
+
+    -----------------------------------------------------------
+    -- Operators & reserved ops
+    -----------------------------------------------------------
+    reservedOp name =
+        lexeme $ try $
+        do{ string name
+          ; notFollowedBy (opLetter languageDef) <?> ("end of " ++ show name)
+          }
+
+    operator =
+        lexeme $ try $
+        do{ name <- oper
+          ; if (isReservedOp name)
+             then unexpected ("reserved operator " ++ show name)
+             else return name
+          }
+
+    oper =
+        do{ c <- (opStart languageDef)
+          ; cs <- many (opLetter languageDef)
+          ; return (c:cs)
+          }
+        <?> "operator"
+
+    isReservedOp name =
+        isReserved (sort (reservedOpNames languageDef)) name
+
+
+    -----------------------------------------------------------
+    -- Identifiers & Reserved words
+    -----------------------------------------------------------
+    reserved name =
+        lexeme $ try $
+        do{ caseString name
+          ; notFollowedBy (identLetter languageDef) <?> ("end of " ++ show name)
+          }
+
+    caseString name
+        | caseSensitive languageDef  = string name
+        | otherwise               = do{ walk name; return name }
+        where
+          walk []     = return ()
+          walk (c:cs) = do{ caseChar c <?> msg; walk cs }
+
+          caseChar c  | isAlpha c  = char (toLower c) <|> char (toUpper c)
+                      | otherwise  = char c
+
+          msg         = show name
+
+
+    identifier =
+        lexeme $ try $
+        do{ name <- ident
+          ; if (isReservedName name)
+             then unexpected ("reserved word " ++ show name)
+             else return name
+          }
+
+
+    ident
+        = do{ c <- identStart languageDef
+            ; cs <- many (identLetter languageDef)
+            ; return (c:cs)
+            }
+        <?> "identifier"
+
+    isReservedName name
+        = isReserved theReservedNames caseName
+        where
+          caseName      | caseSensitive languageDef  = name
+                        | otherwise               = map toLower name
+
+
+    isReserved names name
+        = scan names
+        where
+          scan []       = False
+          scan (r:rs)   = case (compare r name) of
+                            LT  -> scan rs
+                            EQ  -> True
+                            GT  -> False
+
+    theReservedNames
+        | caseSensitive languageDef  = sort reserved
+        | otherwise                  = sort . map (map toLower) $ reserved
+        where
+          reserved = reservedNames languageDef
+
+
+
+    -----------------------------------------------------------
+    -- White space & symbols
+    -----------------------------------------------------------
+    symbol name
+        = lexeme (string name)
+
+    lexeme p
+        = do{ x <- p; whiteSpace; return x  }
+
+    whiteSpace = ignoreAbsoluteIndentation (localTokenMode (const Any) whiteSpace')
+    whiteSpace'
+        | noLine && noMulti  = skipMany (simpleSpace <?> "")
+        | noLine             = skipMany (simpleSpace <|> multiLineComment <?> "")
+        | noMulti            = skipMany (simpleSpace <|> oneLineComment <?> "")
+        | otherwise          = skipMany (simpleSpace <|> oneLineComment <|> multiLineComment <?> "")
+        where
+          noLine  = null (commentLine languageDef)
+          noMulti = null (commentStart languageDef)
+
+    simpleSpace =
+        skipMany1 (satisfy isSpace)
+
+    oneLineComment =
+        do{ try (string (commentLine languageDef))
+          ; skipMany (satisfy (/= '\n'))
+          ; return ()
+          }
+
+    multiLineComment =
+        do { try (string (commentStart languageDef))
+           ; inComment
+           }
+
+    inComment
+        | nestedComments languageDef  = inCommentMulti
+        | otherwise                = inCommentSingle
+
+    inCommentMulti
+        =   do{ try (string (commentEnd languageDef)) ; return () }
+        <|> do{ multiLineComment                     ; inCommentMulti }
+        <|> do{ skipMany1 (noneOf startEnd)          ; inCommentMulti }
+        <|> do{ oneOf startEnd                       ; inCommentMulti }
+        <?> "end of comment"
+        where
+          startEnd   = nub (commentEnd languageDef ++ commentStart languageDef)
+
+    inCommentSingle
+        =   do{ try (string (commentEnd languageDef)); return () }
+        <|> do{ skipMany1 (noneOf startEnd)         ; inCommentSingle }
+        <|> do{ oneOf startEnd                      ; inCommentSingle }
+        <?> "end of comment"
+        where
+          startEnd   = nub (commentEnd languageDef ++ commentStart languageDef)
diff --git a/haskell/Text/Parser/Indentation/Implementation.hs b/haskell/Text/Parser/Indentation/Implementation.hs
new file mode 100644
--- /dev/null
+++ b/haskell/Text/Parser/Indentation/Implementation.hs
@@ -0,0 +1,338 @@
+module Text.Parser.Indentation.Implementation where
+
+-- Implements common code for "Indentation Senstivie Parising: Landin Revisited"
+--
+-- Primary functions are:
+--  - TODO
+-- Primary driver functions are:
+--  - TODO
+
+-- TODO:
+--   Grace style indentation stream
+--   Haskell style indentation stream
+
+--import Control.Monad
+
+------------------------
+-- Indentations
+------------------------
+
+-- We use indent 1 for the first column.  Not only is this consistent
+-- with how Parsec counts columns, but it also allows 'Gt' to refer to
+-- the first column by setting the indent to 0.
+--data Indentation = Indentation# Int# deriving (Eq, Ord)
+type Indentation = Int
+data IndentationRel = Eq | Any | Const Indentation | Ge | Gt deriving (Show, Eq)
+
+{-# INLINE infIndentation #-}
+infIndentation :: Indentation
+infIndentation = maxBound
+
+{-
+instance Num Indentation where
+
+instance Show Indentation where
+  show i@(Indentation# i') | i' == maxBound = "Infinity"
+                           | otherwise = show (Int# i')
+-}
+
+------------------------
+-- Indentable Stream
+------------------------
+
+-- We store state information about the current indentation in the
+-- Stream.  Encoding the indentation state in the Stream is weird, but
+-- the other two places where we could put it don't work.  The monad
+-- isn't rolledback when backtracking happens (which we need the
+-- indentation state to do), and the user state isn't available when
+-- we do an 'uncons'.
+
+{-# INLINE mkIndentationState #-}
+mkIndentationState :: Indentation -> Indentation -> Bool -> IndentationRel -> IndentationState
+mkIndentationState lo hi mode rel
+  | lo == infIndentation = error "mkIndentationState: minimum indentation 'infIndentation' is out of bounds"
+  | lo > hi = error "mkIndentationState: minimum indentation is greater than maximum indent"
+  | otherwise = IndentationState lo hi mode rel
+
+-- THEOREM: indent sets are all describable by upper and lower bounds (maxBound is infinity)
+-- GLOBAL INVARIANT: minIndentation /= infIndentation
+-- GLOBAL INVARIANT: minIndentation <= maxIndentation
+-- GLOBAL INVARIENT: lo <= lo' where lo and lo' are minIndentation respectively before and after a monadic action
+-- GLOBAL INVARIENT: hi' <= hi where hi and hi' are maxIndentation respectively before and after a monadic action
+
+data IndentationState = IndentationState {
+  minIndentation :: {-# UNPACK #-} !Indentation, -- inclusive, must not equal infIndentation
+  maxIndentation :: {-# UNPACK #-} !Indentation, -- inclusive, infIndentation (i.e., maxBound) means infinity
+  absMode :: !Bool, -- true if we are in 'absolute' mode
+  tokenRel :: !IndentationRel
+  } deriving (Show)
+  -- Our representation of maxIndentation will get us in trouble if things
+  -- overflow.  In future we may want to use a type representing
+  -- Integer+Infinity However, this bug triggers *only* when there are
+  -- a large number of nested 'Gt' indentations which shouldn't be all
+  -- that common and 'local'
+
+{-# INLINE indentationStateAbsMode #-}
+indentationStateAbsMode :: IndentationState -> Bool
+indentationStateAbsMode x = absMode x
+
+{-# INLINE updateIndentation #-}
+-- PRIVATE: Use assertIndentation instead
+updateIndentation :: IndentationState -> Indentation -> (IndentationState -> a) -> (String -> a) -> a
+updateIndentation (IndentationState lo hi mode rel) i ok err = updateIndentation' lo hi (if mode then Eq else rel) i ok' err' where
+  ok' lo' hi' = ok (IndentationState lo' hi' False rel)
+  err' = err
+
+{-# INLINE updateIndentation' #-}
+updateIndentation' :: Indentation -> Indentation -> IndentationRel -> Indentation -> (Indentation -> Indentation -> a) -> (String -> a) -> a
+updateIndentation' lo hi rel i ok err =
+  case rel of
+    Any                          -> ok lo hi
+    Const c | c  == i            -> ok lo hi
+            | otherwise          -> err' $ "indentation "++show c
+    Eq      | lo <= i && i <= hi -> ok i i
+            | otherwise          -> err' $ "an indentation between "++show lo++" and "++show hi
+    Gt      | lo <  i            -> ok lo (min (i-1) hi)
+            | otherwise          -> err' $ "an indentation greater than "++show lo
+    Ge      | lo <= i            -> ok lo (min i hi)
+            | otherwise          -> err' $ "an indentation greater than or equal to "++show lo
+  where err' place = err $ "Found a token at indentation "++show i++".  Expecting a token at "++place++"."
+
+-- TODO: error when hi is maxIndentation
+
+-- There is no way to query the current indentation because multiple
+-- indentations are tried in parallel and later parsing may disqualify
+-- one of these indentations.  However, we can assert that the current
+-- indentation must have a particular relation, 'r', to a given
+-- indentation, 'i'.  The call 'assertIndent r i' does this.  Calling
+-- 'assertIndent r i' is equivalent to consuming a pseudo-token that has
+-- been annotated with the relation 'r' at indentation 'i'.
+--
+-- Note that the absolute indentation mode may override 'r'.
+{-
+assertIndent :: (Monad m, Stream (IndentStream s) m t) => IndentRel -> Indent -> ParsecT (IndentStream s) u m ()
+assertIndent r i = do
+  IndentStream lo hi mode rel s <- getInput
+  let ok s' = setInput (s' { absMode = mode }) -- Update input sets mode to False by default
+      --ok lo' hi' = setInput (IndentStream lo' hi' mode rel s)
+      err msg = unexpected $ "Indentation assertion '"++show r++" "++show i++"' failed.  "++msg
+  updateIndent lo hi mode r i s ok err
+  --updateIndent lo hi (if mode then Eq else r) i ok err
+-}
+
+{-
+{-# INLINE askTokenMode #-}
+askTokenMode :: (Monad m) => ParsecT (IndentStream s) u m IndentRel
+askTokenMode = liftM tokenRel getInput
+-}
+
+------------------------
+-- Token Modes
+------------------------
+
+-- Token modes determine how the current indentation must relate to
+-- the indentation of a token.  Because several languages have special
+-- rules for the first token of the production, we split the token
+-- mode into two parts.  The first part is the mode for the first
+-- token in a grammatical form while the second part is the mode for
+-- the other tokens in a grammatical form.
+--
+-- Because of this split, while token modes generally follow a reader
+-- monad pattern, there is one important exception.  Namely the
+-- first-token mode may follow a state monad pattern.  (Thus we have
+-- the divergent names for the first-token and other-token query
+-- operators.)
+
+-- THEOREM: tokenMode == tokenMode'
+-- THEOREM: firstTokenMode' == firstTokenMode \/ firstTokenMode' == otherTokenMode
+
+type LocalState a = (IndentationState -> IndentationState) -- pre
+                  -> (IndentationState {-old-} -> IndentationState {-new-} -> IndentationState) -- post
+                  -> a -> a
+
+{-# INLINE localTokenMode #-}
+localTokenMode :: (LocalState a)
+               -> (IndentationRel -> IndentationRel)
+               -> a -> a
+localTokenMode localState f_rel = localState pre post where
+  pre  i1    = i1 { tokenRel = f_rel (tokenRel i1) }
+  post i1 i2 = i2 { tokenRel =        tokenRel i1  }
+
+{-# INLINE absoluteIndentation #-}
+absoluteIndentation :: LocalState a -> a -> a
+absoluteIndentation localState = localState pre post where
+  pre  i1    = i1 { absMode = True }
+  post i1 i2 = i2 { absMode = absMode i1 && absMode i2 }
+
+{-# INLINE ignoreAbsoluteIndentation #-}
+ignoreAbsoluteIndentation :: LocalState a -> a -> a
+ignoreAbsoluteIndentation localState = localState pre post where
+  pre  i1    = i1 { absMode = False }
+  post i1 i2 = i2 { absMode = absMode i1 }
+
+{-# INLINE localAbsoluteIndentation #-}
+localAbsoluteIndentation :: LocalState a -> a -> a
+localAbsoluteIndentation localState = localState pre post where
+  pre  i1    = i1 { absMode = True }
+  post i1 i2 = i2 { absMode = absMode i1 }
+
+--{-# INLINE askTokenMode #-}
+--askTokenMode :: (Monad m) => ParsecT (IndentationStream s) u m IndentationRel
+--askTokenMode = liftM tokenRel getInput
+-- TODO: assertNotAbsMod/askAbsMode
+-- when (absMode i2) (fail "absoluteIndentation: no tokens consumed") >>
+
+------------------------
+-- Local Indentations
+------------------------
+
+{-# INLINE localIndentation' #-}
+-- PRIVATE: locally violates global invariants but used in a way that does not
+localIndentation' :: LocalState a -> (Indentation -> Indentation) -> (Indentation -> Indentation) -> (Indentation -> Indentation -> Indentation) -> a -> a
+localIndentation' localState f_lo f_hi f_hi' m = localState pre post m
+  where pre (IndentationState lo hi mode rel) = IndentationState (f_lo lo) (f_hi hi) mode rel
+        post (IndentationState lo hi _ _) i2 = i2 { minIndentation = lo, maxIndentation = f_hi' hi (maxIndentation i2) }
+--        post (IndentationStream lo hi mode rel s) i2 = IndentationStream lo (f_hi' hi (maxIndentation i2)) mode rel s
+
+-- 'localIndentation r p' specifies that the current indentation for 'p' must have relation 'r'
+-- relative to the current indentation of the context in which 'localIndentation r p' is called.
+{-# INLINE localIndentation #-}
+-- NOTE: it is the responsibility of 'localState' to *not* use it's arguments if we are in absMode
+localIndentation :: LocalState a -> IndentationRel -> a -> a
+localIndentation _localState Eq m = m
+localIndentation localState Any m = localIndentation' localState (const 0) (const infIndentation) (const) m
+localIndentation localState (Const c) m
+    | c == infIndentation = error "localIndentation: Const indentation 'infIndentation' is out of bounds"
+    | otherwise = localIndentation' localState (const c) (const c) (const) m
+localIndentation localState Ge m = localIndentation' localState (id) (const infIndentation) (flip const) m
+localIndentation localState Gt m = localIndentation' localState (+1) (const infIndentation) (f) ({-TODO: checkOverflow >>-} m) where
+  f hi hi' | hi' == infIndentation || hi < hi' = hi
+           | hi' > 0 = hi' - 1 -- Safe only b/c hi' > 0
+           | otherwise = error "localIndentation: assertion failed: hi' > 0"
+{-
+  checkOverflow = do
+    IndentationStream { minIndentation = lo } <- getState
+    when (lo == infIndentation) $ fail "localIndentation: Overflow in indentation lower bound."
+-}
+
+----------------
+-- SourcePos
+
+{-
+mkSourcePosIndentStream s = SourcePosIndentStream s
+newtype SourcePosIndentStream s = SourcePosIndentStream s
+instance (Stream s m t) => Stream (SourcePosIndentStream s) m (Indent, t) where
+  uncons (SourcePosIndentStream s) = do
+    col <- liftM sourceColumn $ getPosition
+    x <- uncons s
+    case x of
+      Nothing -> return Nothing
+      Just x -> return (Just ((col, x), SourcePosIndentStream s))
+-}
+
+----------------
+-- Unicode char
+-- newtype UnicodeIndentStream
+
+{-
+----------------
+-- Based on Char
+mkCharIndentStream :: s -> CharIndentStream s
+mkCharIndentStream s = CharIndentStream 1 s
+data CharIndentStream s = CharIndentStream { charIndentStreamColumn :: !Indent,
+                                             charIndentStreamStream :: s } deriving (Show)
+
+instance (Stream s m Char) => Stream (CharIndentStream s) m (Indent, Char) where
+  uncons (CharIndentStream i s) = do
+    x <- uncons s
+    case x of
+      Nothing -> return Nothing
+      Just (c, cs) -> return (Just ((i, c), CharIndentStream (f c) cs)) where
+        f '\n' = 1
+        f '\t' = i + 8 - ((i-1) `mod` 8)
+        f _    = i + 1
+
+charIndentStreamParser :: (Monad m) => ParsecT s u m t -> ParsecT (CharIndentStream s) u m (Indent, t)
+charIndentStreamParser p = mkPT $ \state ->
+  let go (Ok a state' e) = return (Ok (sourceColumn $ statePos state, a) (state' { stateInput = CharIndentStream (sourceColumn $ statePos state') (stateInput state') }) e)
+      go (Error e) = return (Error e)
+  in runParsecT p (state { stateInput = charIndentStreamStream (stateInput state) })
+         >>= consumed (return . Consumed . go) (return . Empty . go)
+
+----------------
+-- TODO: parser based on first non-whitespace char
+
+----------------
+-- First token of line indents
+
+----------------
+-- Based on Indents
+
+-- Note that if 'p' consumes input but is at the wrong indentation, then
+-- 'indentStreamParser p' signals an error but does *not* consume input.
+-- This allows Parsec primitives like 'string' to be properly backtracked.
+indentStreamParser :: (Monad m) => ParsecT s u m (Indent, t) -> ParsecT (IndentStream s) u m t
+indentStreamParser p = mkPT $ \state ->
+  let IndentStream lo hi mode rel _ = stateInput state
+      go f (Ok (i, a) state' e) = updateIndent lo hi (if mode then Eq else rel) i ok err where
+        ok lo' hi' = return $ f $ return (Ok a (state' {stateInput = IndentStream lo' hi' False rel (stateInput state') }) e)
+        err msg = return $ Empty $ return $ Error (Message ("Invalid indentation.  "++msg++show ((stateInput state) { tokenStream = ""})) `addErrorMessage` e)
+      go f (Error e) = return $ f $ return (Error e)
+  in runParsecT p (state { stateInput = tokenStream (stateInput state) }) >>= consumed (go Consumed) (go Empty)
+
+-- lifting operator
+-- token, tokens, tokenPrim, tokenPrimEx ???
+-- whiteSpace
+-- ByteString
+-- ByteString.Lazy
+-- Text
+
+delimitedLayout :: Stream (IndentStream s) m t =>
+  ParsecT (IndentStream s) u m open -> Bool ->
+  ParsecT (IndentStream s) u m close -> Bool ->
+  ParsecT (IndentStream s) u m a -> ParsecT (IndentStream s) u m a
+delimitedLayout open openAny close closeAny body = between open' close' (localIndent (Const 0) body) where
+  open'  | openAny = localIndent (Const 0) open
+         | otherwise = open
+  close' | closeAny = localIndent (Const 0) close
+         | otherwise = close
+
+indentedLayout :: Stream (IndentStream s) m t =>
+  (Maybe (ParsecT (IndentStream s) u m sep)) ->
+  ParsecT (IndentStream s) u m a -> ParsecT (IndentStream s) u m [a]
+indentedLayout (Nothing ) clause = localIndent Gt $ many $ absoluteIndent $ clause
+indentedLayout (Just sep) clause = liftM concat $ localIndent Gt $ many $ absoluteIndent $ sepBy1 clause sep
+
+{-
+layout p = delimitedLayout (symbol "{") False (symbol "}") True (semiSep p)
+       <|> indentedLayout (Just semi) p
+
+identifier pred = liftM fromString $ try $ identifier >>= \x -> guard (pred x) >> return x
+operator pred = liftM fromString $ try $ operator >>= \x -> guard (pred x) >> return x
+
+reserved name = (if name `elem` middleKeywords then localFirstTokenMode (const Ge) else id) $ reserved name
+
+Numbers, Integers and Naturals are custom
+
+dotSep
+dotSep1
+
+-}
+
+{-
+test :: String
+test = foo where
+          foo = "abc \
+\def" ++ ""
+
+test2 :: Int
+test2 = foo where
+          foo = let { x = 1;
+ } in x
+
+
+--- All code indented?
+  foo = 3
+  bar = 4
+-}
+-}
