diff --git a/examples/Binding.lhs b/examples/Binding.lhs
new file mode 100644
--- /dev/null
+++ b/examples/Binding.lhs
@@ -0,0 +1,44 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE GADTs, KindSignatures, TypeOperators, TypeFamilies #-}
+
+> module Binding where
+
+> import Control.Applicative
+
+> import ShePrelude
+
+> data Tm
+>   = V Int
+>   | L Tm
+>   | Tm :$ Tm
+>   deriving Show
+
+> infixl 6 :$
+
+> data Va
+>   = F (Va -> Va)
+>   | [Va] :- Int    -- backwards
+
+> ($$) :: Va -> Va -> Va
+> F f $$ v = f v
+> (vs :- p) $$ v = (v : vs) :- p
+
+> ev :: Tm -> [Va] -> Va
+> ev (V i)     g = g !! i
+> ev (L t)     g = F (\ v -> ev t (v : g))
+> ev (f :$ s)  g = (|ev f $$ ev s|) g
+
+> qu :: Int -> Va -> Tm
+> qu i (F f)     = L (qu (i + 1) (f ([] :- i)))
+> qu i (vs :- j) = foldr (flip (:$)) (V (i - j - 1)) (map (qu i) vs)
+
+> zz :: Tm
+> zz = L [.f. L [.x. V x]]
+> ss :: Tm
+> ss = L [.n. L [.f. L [.x. V f :$ (V n :$ V f :$ V x)]]]
+
+> test3 :: Va
+> test3 = ev [.zz.ss. V ss :$ (V ss :$ (V ss :$ V zz))] [ev ss [],ev zz []]
+
+> norm :: Tm -> Tm
+> norm t = qu 0 (ev t [])
diff --git a/examples/FH.lhs b/examples/FH.lhs
--- a/examples/FH.lhs
+++ b/examples/FH.lhs
@@ -8,6 +8,7 @@
 > import System.IO.Error
 
 > import IFunctor
+> import IMonad
 
 > data FHState = FOpen | FClosed
 > data FHSTATE :: {FHState} -> * where
diff --git a/examples/IFunctor.lhs b/examples/IFunctor.lhs
--- a/examples/IFunctor.lhs
+++ b/examples/IFunctor.lhs
@@ -8,38 +8,3 @@
 > class IFunctor (phi :: ({i} -> *) -> {o} -> *) where
 >   imap :: (s :-> t) -> phi s :-> phi t
 
-> class IFunctor phi => IMonad (phi :: ({i} -> *) -> {i} -> *) where
->   iskip :: s :-> phi s
->   iextend :: (s :-> phi t) -> (phi s :-> phi t)
-
-> iseq :: IMonad phi => (r :-> phi s) -> (s :-> phi t) -> (r :-> phi t)
-> iseq f g = iextend g . f
-
-> (>>-) :: IMonad phi => phi s i -> (s :-> phi t) -> phi t i
-> (>>-) = flip iextend
-
-> data (:*) :: (({i} -> *) -> {i} -> *) -> ({i} -> *) -> {i} -> * where
->   Ret  :: q i -> (phi :* q) i
->   Do   :: phi (phi :* q) i -> (phi :* q) i
-
-> instance IFunctor phi => IFunctor ((:*) phi) where
->   imap f = iextend (iskip . f)
-
-> instance IFunctor phi => IMonad ((:*) phi) where
->   iskip = Ret
->   iextend f (Ret x) = f x
->   iextend f (Do d) = Do (imap (iextend f) d)
-
-Some predicates we like.
-
-> data (:-) :: * -> {x} -> {x} -> * where
->   V :: a -> (a :- x) x
-
-> ret :: IMonad phi => a -> phi (a :- i) i
-> ret a = iskip (V a)
-
-> knownState :: (a -> t i) -> (a :- i) :-> t
-> knownState f (V a) = f a
-
-> (?-) :: IMonad phi => phi (a :- j) i -> (a -> phi t j) -> phi t i
-> c ?- f = c >>- knownState f
diff --git a/examples/IMonad.lhs b/examples/IMonad.lhs
new file mode 100644
--- /dev/null
+++ b/examples/IMonad.lhs
@@ -0,0 +1,42 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE KindSignatures, RankNTypes, TypeOperators, GADTs #-}
+
+> module IMonad where
+
+> import IFunctor
+
+> class IFunctor phi => IMonad (phi :: ({i} -> *) -> {i} -> *) where
+>   iskip :: s :-> phi s
+>   iextend :: (s :-> phi t) -> (phi s :-> phi t)
+
+> iseq :: IMonad phi => (r :-> phi s) -> (s :-> phi t) -> (r :-> phi t)
+> iseq f g = iextend g . f
+
+> (>>-) :: IMonad phi => phi s i -> (s :-> phi t) -> phi t i
+> (>>-) = flip iextend
+
+> data (:*) :: (({i} -> *) -> {i} -> *) -> ({i} -> *) -> {i} -> * where
+>   Ret  :: q i -> (phi :* q) i
+>   Do   :: phi (phi :* q) i -> (phi :* q) i
+
+> instance IFunctor phi => IFunctor ((:*) phi) where
+>   imap f = iextend (iskip . f)
+
+> instance IFunctor phi => IMonad ((:*) phi) where
+>   iskip = Ret
+>   iextend f (Ret x) = f x
+>   iextend f (Do d) = Do (imap (iextend f) d)
+
+My favourite predicate.
+
+> data (:-) :: * -> {x} -> {x} -> * where
+>   V :: a -> (a :- x) x
+
+> ret :: IMonad phi => a -> phi (a :- i) i
+> ret a = iskip (V a)
+
+> knownState :: (a -> t i) -> (a :- i) :-> t
+> knownState f (V a) = f a
+
+> (?-) :: IMonad phi => phi (a :- j) i -> (a -> phi t j) -> phi t i
+> c ?- f = c >>- knownState f
diff --git a/examples/Path.lhs b/examples/Path.lhs
--- a/examples/Path.lhs
+++ b/examples/Path.lhs
@@ -6,6 +6,7 @@
 > import Unsafe.Coerce
 
 > import IFunctor
+> import IMonad
 
 > data Path :: ({i,i} -> *) -> {i,i} -> * where
 >   Nil :: Path r {i,i}
diff --git a/examples/Vec.lhs b/examples/Vec.lhs
--- a/examples/Vec.lhs
+++ b/examples/Vec.lhs
@@ -1,19 +1,66 @@
 > {-# OPTIONS_GHC -F -pgmF she #-}
-> {-# LANGUAGE GADTs, KindSignatures, TypeOperators #-}
+> {-# LANGUAGE GADTs, KindSignatures, TypeOperators, TypeFamilies, FlexibleContexts,
+>     MultiParamTypeClasses, UndecidableInstances, ScopedTypeVariables,
+>     RankNTypes #-}
 
 > module Vec where
 
 > import Control.Applicative
 
-> data Nat = Z | S Nat
+> import ShePrelude
 
+> data Nat :: * where
+>   Z :: Nat
+>   S :: Nat -> Nat
+>   deriving (SheSingleton)
+
+> {-
+> data Down :: ({Nat} -> *) -> {Nat} -> * where
+>   DNil :: Down x {Z}
+>   DCons :: x {n} -> Down x {n} -> Down x {S n}
+> -}
+
 > data Vec :: {Nat} -> * -> * where
 >   VNil :: Vec {Z} x
 >   (:>) :: x -> Vec {n} x -> Vec {S n} x
+>   deriving ()
 
+> instance Show x => Show (Vec {n} x) where
+>   show VNil       = "VNil"
+>   show (x :> xs)  = show x ++ " :> " ++ show xs
+
 > vtail :: Vec {S n} x -> Vec {n} x
 > vtail (x :> xs) = xs
 
-> vapp :: Vec {n} (s -> t) -> Vec {n} s -> Vec {n} t
-> vapp VNil VNil = VNil
-> vapp (f :> fs) (s :> ss) = f s :> vapp fs ss
+> type family (m :: {Nat}) :+ (n :: {Nat}) :: {Nat}
+> type instance {Z} :+ n = n
+> type instance {S m} :+ n = {S} (m :+ n)
+
+> instance Functor (Vec {n}) where
+>   fmap f VNil = VNil
+>   fmap f (x :> xs) = f x :> fmap f xs
+
+> vappend :: Vec m x -> Vec n x -> Vec (m :+ n) x
+> vappend VNil ys = ys
+> vappend (x :> xs) ys = x :> vappend xs ys
+
+> instance {:n :: Nat:} => Applicative (Vec {n}) where
+>   pure = vec {:n :: Nat:} where
+>     vec :: forall x. pi (n :: Nat). x -> Vec {n} x
+>     vec {Z}    x = VNil
+>     vec {S n}  x = x :> vec n x
+>   (<*>) = vapp where
+>     vapp :: Vec {m} (s -> t) -> Vec {m} s -> Vec {m} t
+>     vapp VNil VNil = VNil
+>     vapp (f :> fs)  (s :> ss) = f s :> vapp fs ss
+
+> fiveByFive :: Vec {S (S (S (S (S Z))))} Int
+> fiveByFive = pure 5
+
+> vtake :: forall x. pi (m :: Nat). pi (n :: Nat). Vec ({m} :+ {n}) x -> Vec {m} x
+> vtake {Z}   {n} xs         = VNil
+> vtake {S m} {n} (x :> xs)  = x :> vtake {m} {n} xs
+
+> listVec :: [a] -> (pi (n :: Nat). Vec {n} a -> t) -> t
+> listVec [] f = f {Z} VNil
+> listVec (x : xs) f = listVec xs (\ n ys -> f {S n} (x :> ys))
diff --git a/she.cabal b/she.cabal
--- a/she.cabal
+++ b/she.cabal
@@ -1,5 +1,5 @@
 name:               she
-version:            0.0
+version:            0.1
 homepage:           http://personal.cis.strath.ac.uk/~conor/pub/she
 synopsis:           A Haskell preprocessor adding miscellaneous features
 description:
@@ -12,30 +12,45 @@
 author:             Conor McBride
 maintainer:         conor@strictlypositive.org
 extra-source-files: src/Makefile
+                    examples/Binding.lhs
                     examples/Fix.lhs
                     examples/FH.lhs
                     examples/Hig.lhs
                     examples/IFunctor.lhs
+                    examples/IMonad.lhs
                     examples/Jig.lhs
                     examples/Parsley.lhs
                     examples/Path.lhs
                     examples/Pig.lhs
                     examples/Tree.lhs
                     examples/Vec.lhs
-cabal-version:      >= 1.2
+cabal-version:      >= 1.6
 build-type:         Simple
 
 executable she
     main-is:            Main.lhs
 
-    build-depends:      base >=4 && < 5,
+    build-depends:      base >=3 && < 5,
                         mtl,
                         filepath
     hs-source-dirs:     src
 
     other-modules:      Aspect
+                        DeBruijn
+                        IdiomBrackets
                         Imports
                         HaLay
                         Parsley
                         Patsy
                         TypesToKinds
+
+library
+    exposed-modules:    ShePrelude
+    build-depends:      base >=3 && < 5,
+                        mtl,
+                        filepath
+    hs-source-dirs:     src    
+
+source-repository head
+  type:     darcs
+  location: http://personal.cis.strath.ac.uk/~conor/pub/she
diff --git a/src/Aspect.lhs b/src/Aspect.lhs
--- a/src/Aspect.lhs
+++ b/src/Aspect.lhs
@@ -22,18 +22,18 @@
 
 > outdent :: [[Tok]] -> [[Tok]]
 > outdent tss = map (munge nip) tss where
->   nip (NL : Spc ss : ts) = Just $
->     NL : Spc (replicate (length ss - l) ' ') : munge nip ts
+>   nip (NL fl : Spc ss : ts) = Just $
+>     NL fl : Spc (replicate (length ss - l) ' ') : munge nip ts
 >   nip _ = Nothing
 >   l = skin tss
 >   skin [] = 0
->   skin ([NL, Spc ss] : (t : _) : _) | not (isSpcT t) = length ss
+>   skin ([NL _, Spc ss] : (t : _) : _) | not (isSpcT t) = length ss
 >   skin (_ : tss) = skin tss
 
 > indent :: Int -> [Tok] -> [Tok]
 > indent i = munge dent where
->   dent (NL : Spc ss : ts) = Just $
->     NL : Spc (replicate i ' ' ++ ss) : munge dent ts
+>   dent (NL fl : Spc ss : ts) = Just $
+>     NL fl : Spc (replicate i ' ' ++ ss) : munge dent ts
 >   dent _ = Nothing
 
 > dropIn :: [Higgle] -> Int -> String -> [[Tok]]
@@ -44,12 +44,12 @@
 
 > higOut :: Higgle -> [[Tok]]
 > higOut (s, tss) =
->   [NL] :
->   [KW "import", Spc " ", Sym "->", Spc " ", Uid s, Spc " ", KW "where"] :
->   (indent 2 <$> tss)
+>   [ [NL ("Dunno.lhs", 0)]
+>   , [KW "import", Spc " ", Sym "->", Spc " ", Uid s, Spc " ", L "where" (indent 4 <$> tss)]
+>   ]
 
 > pDent :: P Tok Int
-> pDent = teq NL *> grok spcl next <|> 0 <$ teq NL where
+> pDent = pNL *> grok spcl next <|> 0 <$ pNL where
 >   spcl (Spc ss) = Just (length ss)
 >   spcl _ = Nothing
 
@@ -68,4 +68,4 @@
 >   ep ts = do
 >     (i, (s, ts)) <- parse ((,) <$> pDent <*> pPiggle) ts
 >     return $
->       NL : Spc (replicate i ' ') : join (dropIn higs i s)
+>       NL ("Dunno.lhs", 0): Spc (replicate i ' ') : join (dropIn higs i s) ++ ts
diff --git a/src/DeBruijn.lhs b/src/DeBruijn.lhs
new file mode 100644
--- /dev/null
+++ b/src/DeBruijn.lhs
@@ -0,0 +1,25 @@
+> module DeBruijn where
+
+> import Data.List
+> import Control.Applicative
+
+> import Parsley
+> import HaLay
+
+> deBruijnMu :: [String] -> [Tok] -> Maybe [Tok]
+> deBruijnMu xs (B Sqr ss : ts)
+>   = (:) <$> parse jig ss <*> pure (munge (deBruijnMu xs) ts) where
+>     jig :: P Tok Tok
+>     jig = teq (Sym ".") *>
+>           (shf xs <$> some (lid <* teq (Sym ".")) <*> pRest)
+>     shf xs [] ts = B Rnd (wang xs : KW "in" : Spc " " :
+>                           munge (deBruijnMu xs) ts)
+>     shf xs (y : ys) ts = shf (y : xs) ys ts
+>     wang xs = L "let"  ([Ope Crl] :
+>                        intersperse [Semi] (zipWith dang xs [0..]) ++
+>                        [[Clo Crl]])
+>     dang x i = [Lid x, Sym "=", Lit (show i)]
+> deBruijnMu _ _ = Nothing
+
+> deBruijn :: [[Tok]] -> [[Tok]]
+> deBruijn = map (munge (deBruijnMu []))
diff --git a/src/HaLay.lhs b/src/HaLay.lhs
--- a/src/HaLay.lhs
+++ b/src/HaLay.lhs
@@ -2,7 +2,7 @@
 
 > module HaLay where
 
-> import Control.Arrow
+> import Control.Arrow (first)
 > import Control.Applicative
 > import Data.Char
 > import Data.List
@@ -17,17 +17,19 @@
 Glom a file like this
 ------------------------------------------------------------------------------
 
-> ready :: String -> [[Tok]]
-> ready = map (munge exTyMu) . fst . getLines (Seek NoLay "") [] .
->         tokenize . (,) 0
+> ready :: String -> String -> [[Tok]]
+> ready f = map (munge exTyMu) . fst . getLines (Seek NoLay "") [] .
+>           tokenize . (,) ((f, 0), 0)
 
 ------------------------------------------------------------------------------
 Stage 1 : lexing
 ------------------------------------------------------------------------------
 
-> tokenize :: (Int, String) -> [(Int, Tok)]
-> tokenize = unfoldr (runStateT ((,) <$> gets fst <*> tokIn))
+> type Position = (({-file-}String, {-line-}Int), {-col-}Int)
 
+> tokenize :: (Position, String) -> [(Int, Tok)]
+> tokenize = unfoldr (runStateT ((,) <$> lCol <*> tokIn))
+
 > data Tok
 >   = Lit String
 >   | Ope BK
@@ -40,7 +42,7 @@
 >   | Spc String
 >   | Com String
 >   | Urk Char
->   | NL
+>   | NL (String, Int)    -- file and new line
 >   | B BK [Tok]          -- a bracket
 >   | L String [[Tok]]    -- some layout
 >   | T Tag [Tok]         -- a tagged region
@@ -48,21 +50,22 @@
 
 > tokOut :: Tok -> String
 > tokOut t = case t of
->   Lit s -> s
->   Ope b -> ope b
->   Clo b -> clo b
->   Uid s -> s
->   Lid s -> s
->   KW  s -> s
->   Sym s -> s
->   Semi  -> ";"
->   Spc s -> s
->   Com s -> s
->   Urk c -> [c]
->   NL    -> "\n"
->   B b ts -> ope b ++ toksOut ts ++ clo b
->   L s tss -> s ++ tokssOut tss
->   T _ ts -> toksOut ts
+>   Lit s      -> s
+>   Ope b      -> ope b
+>   Clo b      -> clo b
+>   Uid s      -> s
+>   Lid s      -> s
+>   KW  s      -> s
+>   Sym s      -> s
+>   Semi       -> ";"
+>   Spc s      -> s
+>   Com s      -> s
+>   Urk c      -> [c]
+>   NL (f, l)  | isSuffixOf ".hers" f -> "\n"
+>              | otherwise -> "{-# LINE " ++ show l ++ " " ++ show f ++ " #-}\n"
+>   B b ts     -> ope b ++ toksOut ts ++ clo b
+>   L s tss    -> s ++ tokssOut tss
+>   T _ ts     -> toksOut ts
 
 > toksOut :: [Tok] -> String
 > toksOut ts = ts >>= tokOut
@@ -70,13 +73,16 @@
 > tokssOut tss = tss >>= toksOut
 
 > isSpcT :: Tok -> Bool
-> isSpcT (Spc _) = True
-> isSpcT NL      = True
-> isSpcT (Com _) = True
-> isSpcT _       = False
+> isSpcT (Spc _)  = True
+> isSpcT (NL _)   = True
+> isSpcT (Com _)  = True
+> isSpcT _        = False
 
 > tokIn :: L Tok
 > tokIn = Lit <$> ((:) <$> ch '\"' <*> slit)
+>     <|> Lit <$> ((:) <$> ch '\'' <*> haha)
+>     <|> NL <$ traverse ch "{-# LINE " <*> whur <* traverse ch "\" #-}" <*
+>           some (chk isNL cha)
 >     <|> Com <$ stol <*> ((++) <$> traverse ch "#" <*>  spa (not . isNL))
 >     <|> Sym <$>  sym
 >     <|> Com <$> ((++) <$> traverse ch "--" <*>  spa (not . isNL))
@@ -90,20 +96,26 @@
 >     <|> Semi <$ ch ';'
 >     <|> Lit <$> ((:) <$> chk isDigit cha <*> spa isDigit)  -- sod FP now
 >     <|> Uid <$> ((:) <$> chk isUpper cha <*> spa isIddy)
->     <|> klid <$> ((:) <$> chk isLower cha <*> spa isIddy)
+>     <|> klid <$> ((:) <$> chk (\ b -> isLower b || b == '_') cha <*> spa isIddy)
 >     <|> Spc  <$> ((:) <$> chk isHSpace cha <*> spa isHSpace)
->     <|> NL <$ chk isNL cha
+>     <|> NL <$ some (chk isNL cha) <*> lFLine
 >     <|> Urk <$> cha
 >  where
 >    slit = (:) <$> ch '\\' <*> ((:) <$> cha <*> slit)
 >      <|> return <$> ch '\"'
 >      <|> (:) <$> cha <*> slit
+>    haha = (:) <$> ch '\\' <*> ((:) <$> cha <*> slit)
+>      <|> return <$> ch '\''
+>      <|> (:) <$> cha <*> haha
 >    klid s = if elem s keywords then KW s else Lid s
 >    comment 0 = pure ""
 >    comment i = (++) <$> traverse ch "{-" <*> comment (i + 1)
 >            <|> (++) <$> traverse ch "-}" <*> comment (i - 1)
 >            <|> (++) <$> ((:) <$> ch '\"' <*> slit) <*> comment i
 >            <|> (:) <$> cha <*> comment i
+>    whur = flip (,) <$> (read <$> some (chk isDigit cha))
+>             <* traverse ch " \""
+>             <*> spa (not . (=='\"'))
 
 ------------------------------------------------------------------------
 Stage 2 : Group according to brackets and layout rules
@@ -116,20 +128,42 @@
 >   deriving (Show, Eq)
 
 > getChunks :: ChunkMode -> [Tok] -> [(Int, Tok)] -> ([Tok], [(Int, Tok)])
-> getChunks _ acc [] = (reverse acc, [])
-> getChunks m acc its@((i, t) : its') = case (m, t) of
->   _ | isSpcT t -> getChunks m (t : acc) its'
->   (Lay _ j, _) | not (null acc) && i <= j -> (reverse acc, its)
->   (Lay _ _, Semi) -> (reverse (t : acc), its')
->   (Lay k _, KW e) | elem (k, e) layDKillaz -> (reverse acc, its)
->   (Lay _ _, Clo _) -> (reverse acc, its)
->   (Bra b, Clo b') | b == b' -> (reverse acc, its')
->   (m, Ope b) -> case getChunks (Bra b) [] its' of
->     (cs, its) -> getChunks m (B b cs : acc) its
->   (m, KW e) | elem e lakeys -> case getLines (Seek m e) [] its' of
->     (css, its) -> getChunks m ((L e css) : acc) its
->   _ -> getChunks m (t : acc) its'
+> getChunks m acc its =
+>   let (iss, ius) = span gappy its
+>       gappy (_, s) = isSpcT s
+>       acss = case iss of
+>         [] -> acc
+>         _  -> reverse (map snd iss) ++ acc
+>   in case ius of
+>        [] -> (reverse acc, its)
+>        ((i, t) : its') -> case (m, t) of
+>          (Lay _ j, _) | not (null acc) && i <= j -> (reverse acc, its)
+>          (Lay _ _, Semi) -> (reverse acc, its)
+>          (Lay k _, KW e) | elem (k, e) layDKillaz -> (reverse acc, its)
+>          (Lay _ _, Clo _) -> (reverse acc, its)
+>          (Bra b, Clo b') | b == b' -> (reverse acss, its')
+>          (m, Ope b) -> case getChunks (Bra b) [] its' of
+>            (cs, its) -> getChunks m (B b cs : acss) its
+>          (m, KW e) | elem e lakeys -> case getLines (Seek m e) [] its' of
+>            (css, its) -> getChunks m ((L e css) : acss) its
+>          _ -> getChunks m (t : acss) its'
 
+ getChunks :: ChunkMode -> [Tok] -> [(Int, Tok)] -> ([Tok], [(Int, Tok)])
+ getChunks _ acc [] = (reverse acc, [])
+ getChunks m acc its@((i, t) : its') = case (m, t) of
+   _ | isSpcT t -> getChunks m (t : acc) its'
+   (Lay _ j, _) | not (null acc) && i <= j -> (reverse acc, its)
+   (Lay _ _, Semi) -> (reverse (t : acc), its')
+   (Lay k _, KW e) | elem (k, e) layDKillaz -> (reverse acc, its)
+   (Lay _ _, Clo _) -> (reverse acc, its)
+   (Bra b, Clo b') | b == b' -> (reverse acc, its')
+   (m, Ope b) -> case getChunks (Bra b) [] its' of
+     (cs, its) -> getChunks m (B b cs : acc) its
+   (m, KW e) | elem e lakeys -> case getLines (Seek m e) [] its' of
+     (css, its) -> getChunks m ((L e css) : acc) its
+   _ -> getChunks m (t : acc) its'
+
+
 > data LineMode
 >   = Bracing
 >   | Seek ChunkMode String
@@ -137,34 +171,73 @@
 >   deriving (Show, Eq)
 
 > getLines :: LineMode -> [[Tok]] -> [(Int, Tok)] -> ([[Tok]], [(Int, Tok)])
-> getLines _ acc [] = (reverse acc, [])
-> getLines m acc ((_, s) : its) | isSpcT s = eat [s] its where
->   eat sacc ((_, s) : its) | isSpcT s = eat (s : sacc) its
->   eat sacc its = getLines m (reverse (splendid (reverse sacc)) ++ acc) its
-> getLines m acc its@((i, t) : its') = case (m, t) of
->   (Edge k j, _)
->     | i == j -> case getChunks (Lay k i) [] its of
->       ([], its) -> (reverse acc, its)
->       (cs, its) -> getLines (Edge k i) (reverse (splendid cs) ++ acc) its
->     | otherwise -> (reverse acc, its)
->   (Seek m s, Ope Crl) -> getLines Bracing ([Ope Crl] : acc) its'
->   (Seek (Lay k j) s, _)
->     | j < i -> getLines (Edge s i) acc its
->     | otherwise -> (reverse acc, its)
->   (Seek NoLay s, _) -> getLines (Edge s i) acc its
->   (Bracing, Clo Crl) -> (reverse ([Clo Crl] : acc), its')
->   (Bracing, _) -> case getChunks NoLay [] its of
->       ([], its) -> (reverse acc, its)
->       (cs, its) -> getLines Bracing (cs : acc) its
+> getLines m acc its =
+>   let (iss, ius) = span gappy its
+>       gappy (_, Semi) = True
+>       gappy (_, s) = isSpcT s
+>       acss = case iss of
+>         [] -> acc
+>         _  -> reverse (splendid (map snd iss)) ++ acc
+>   in case ius of
+>        [] -> (reverse acc, its)
+>        ((i, t) : its') -> case (m, t) of
+>          (Bracing, Clo Crl) -> (reverse ([Clo Crl] :  acss), its')
+>          (_, Clo _) -> (reverse acc, its)
+>          (Edge k j, _)
+>            | i >= j -> case getChunks (Lay k i) [] ius of
+>              ([], _) -> (reverse acc, its)
+>              (cs, ius) -> getLines (Edge k i) (reverse (splendid cs) ++ acss) ius
+>            | otherwise -> (reverse acc, its)
+>          (Seek m s, Ope Crl) | properBrace its'
+>            -> getLines Bracing ([Ope Crl] : acss) its'
+>          (Seek (Lay k j) s, _)
+>            | j < i -> getLines (Edge s i) acss ius
+>            | otherwise -> (reverse acc, its)
+>          (Seek (Bra b) s,_) -> getLines (Edge s i) acss ius
+>          (Seek NoLay s, _) -> getLines (Edge s i) acss ius
+>          (Bracing, _) -> case getChunks NoLay [] its of
+>             ([], _) -> (reverse acc, its)
+>             (cs, ius) -> getLines Bracing (cs : acss) ius
 
+> properBrace :: [(Int, Tok)] -> Bool
+> properBrace [] = True
+> properBrace ((_, Clo Crl) : _) = False
+> properBrace ((_, Semi) : _) = True
+> properBrace ((_, Sym s) : _) | elem s ["->", "<-", "="] = True
+> properBrace (_ : its) = properBrace its
+
+
+ getLines :: LineMode -> [[Tok]] -> [(Int, Tok)] -> ([[Tok]], [(Int, Tok)])
+ getLines _ acc [] = (reverse acc, [])
+ getLines m acc ((_, s) : its) | isSpcT s = eat [s] its where
+   eat sacc ((_, s) : its) | isSpcT s = eat (s : sacc) its
+   eat sacc its = getLines m (reverse (splendid (reverse sacc)) ++ acc) its
+ getLines m acc its@((i, t) : its') = case (m, t) of
+   (Bracing, Clo Crl) -> (reverse ([Clo Crl] : acc), its')
+   (_, Clo _) -> (reverse acc, its)
+   (Edge k j, _)
+     | i == j -> case getChunks (Lay k i) [] its of
+       ([], its) -> (reverse acc, its)
+       (cs, its) -> getLines (Edge k i) (reverse (splendid cs) ++ acc) its
+     | otherwise -> (reverse acc, its)
+   (Seek m s, Ope Crl) -> getLines Bracing ([Ope Crl] : acc) its'
+   (Seek (Lay k j) s, _)
+     | j < i -> getLines (Edge s i) acc its
+     | otherwise -> (reverse acc, its)
+   (Seek (Bra b) s,_) -> getLines (Edge s i) acc its
+   (Seek NoLay s, _) -> getLines (Edge s i) acc its
+   (Bracing, _) -> case getChunks NoLay [] its of
+       ([], its) -> (reverse acc, its)
+       (cs, its) -> getLines Bracing (cs : acc) its
+
 > layDKillaz :: [(String, String)]
 > layDKillaz = [("of", "where"), ("do", "where"), ("let", "in")]
 
 > splendid :: [Tok] -> [[Tok]]
 > splendid [] = [[]]
-> splendid (NL : ts) = case splendid ts of
->   (ss : sss) | all isSpcT ss  -> [] : (NL : ss) : sss
->              | otherwise      -> (NL : ss) : sss
+> splendid (NL fl : ts) = case splendid ts of
+>   (ss : sss) | all isSpcT ss  -> [] : (NL fl : ss) : sss
+>              | otherwise      -> (NL fl : ss) : sss
 > splendid (t : ts) = case splendid ts of
 >   (us : sss) -> (t : us) : sss
 
@@ -176,7 +249,7 @@
 
 > tender :: Tok -> Bool
 > tender (L _ _ ) = True
-> tender t = elem t [Semi, Sym "=", Sym ",", Sym "|", KW "in"]
+> tender t = elem t [Semi, Sym "=", Sym ",", Sym "|", KW "in", KW "deriving"]
 
 > exTyMu :: [Tok] -> Maybe [Tok]
 > exTyMu (t : ts)
@@ -184,7 +257,7 @@
 >   = Just $ t : u : munge exTyMu vs
 >   | elem t [KW "data", KW "newtype"]
 >   = Just $ case vs of
->       Sym "=" : vs -> t : u : Sym "=" : [T Ty vs]  -- dodgy or what?
+>       Sym "=" : vs -> t : u : Sym "=" : oldStyle vs
 >       _ -> t : u : munge exTyMu vs
 >   | elem t [KW "type"]
 >   = Just $ case vs of
@@ -194,6 +267,22 @@
 >     (u, vs) = first (T Ty . munge tyMu) (span (not . tender) ts)
 > exTyMu _ = Nothing
 
+> oldStyle :: [Tok] -> [Tok]
+> oldStyle ts = case parse (pSep (teq (Sym "|")) (many (tok (/= Sym "|")))) ts of
+>     Just tss -> intercalate [Sym "|"] (map go tss)
+>   where
+>     noInfT (Sym (':':_)) = False
+>     noInfT _ = True
+>     go ts = case span noInfT ts of
+>       (as, (t : bs)) -> [T Ty (munge tyMu as), t, T Ty (munge tyMu bs)]
+>       _ -> case span isSpcT ts of
+>         (ss, t : ts) -> ss ++ t : map ho ts
+>         _ -> ts
+>     ho s | isSpcT s = s
+>     ho (Sym s) = Sym s
+>     ho (B Crl ts) = B Crl (munge exTyMu ts)
+>     ho t = T Ty (munge tyMu [t])
+
 > tyMu :: [Tok] -> Maybe [Tok]
 > tyMu (Sym "::" : ts) = Just $ Sym "::" : u : munge tyMu vs
 >   where
@@ -217,6 +306,11 @@
 > spc :: P Tok ()
 > spc = () <$ many (tok isSpcT)
 
+> pNL :: P Tok ()
+> pNL = grok h next where
+>   h (NL _)  = Just ()
+>   h _       = Nothing
+
 > uid :: P Tok String
 > uid = grok h next where
 >   h (Uid s) = Just s
@@ -282,18 +376,18 @@
 >   easy (t : ts) = tokOut t ++ easy ts
 
 > dental :: [[Tok]] -> [Tok]
-> dental [] = [NL]
-> dental (l@(NL : _) : (c : _) : _) | not (isSpcT c) = l
+> dental [] = [NL ("Dunno.lhs", 0)]
+> dental (l@(NL _ : _) : (c : _) : _) | not (isSpcT c) = l
 > dental (l : ls) = dental ls
 
 > redent :: [Tok] -> [[Tok]] -> [[Tok]]
-> redent nl ((NL : _) : tss) = redent nl tss
+> redent nl ((NL _ : _) : tss) = redent nl tss
 > redent nl (ts : tss) = nl : ts : redent nl tss
 > redent nl [] = []
 
 > preamble :: [[Tok]] -> [[Tok]] -> [[Tok]]
 > preamble ls [] = ls
-> preamble ls ms@(l@(NL : _) : (c : _) : _) | not (isSpcT c) =
+> preamble ls ms@(l@(NL _ : _) : (c : _) : _) | not (isSpcT c) =
 >   redent l ls ++ ms
 > preamble ls (m : ms) = m : preamble ls ms
 
@@ -312,7 +406,7 @@
 > isIddy b = isAlphaNum b || elem b "_'"
 
 > isInfy :: Char -> Bool
-> isInfy b = elem b "!#$%&*+-.:/<=>?@\\^|~"
+> isInfy b = elem b "!#$%&*+-,.:/<=>?@\\^|~"
 
 > data BK = Rnd | Sqr | Crl deriving (Show, Eq)
 
@@ -329,25 +423,33 @@
 > keywords :: [String]
 > keywords = ["module", "import", "type", "data", "newtype", "pattern", "kind",
 >             "let", "in", "case", "of", "do", "forall", "class", "instance",
->             "family", "where", "if", "then", "else"]
+>             "family", "where", "if", "then", "else", "deriving"]
 
 > lakeys :: [String]
 > lakeys = ["let", "of", "do", "where"]
 
 > width :: [Tok] -> Int
-> width ts = case span (/= NL) ts of
+> width ts = case span noNL ts of
 >   (ts, []) -> length (ts >>= tokOut)
->   (_, NL : ts) -> width ts
+>   (_, NL _ : ts) -> width ts
+>   where noNL (NL _)  = False
+>         noNL _       = True
 
 ------------------------------------------------------------------------
 The lexer monad
 ------------------------------------------------------------------------
 
-> type L = StateT (Int, String) Maybe
+> type L =  StateT  (Position, String) Maybe
 
+> lFLine :: L (String, Int)
+> lFLine = gets $ \ ((fl, _), _) -> fl
+
+> lCol :: L Int
+> lCol = gets $ \ ((_, c), _) -> c
+
 > instance Alternative L where
->   empty = StateT $ \ is -> empty
->   p <|> q = StateT $ \ is -> runStateT p is <|> runStateT q is
+>   empty    = StateT $ \ is -> empty
+>   p <|> q  = StateT $ \ is -> runStateT p is <|> runStateT q is
 
 > instance Applicative L where
 >   pure = return
@@ -356,15 +458,15 @@
 > cha :: L Char
 > cha = StateT moo where
 >   moo (i, []) = Nothing
->   moo (i, c : s) | isNL c = Just (c, (0, s))
->                  | c == '\t'
->                  = if mod i 8 == 7 then Just (' ', (i + 1, s))
->                                    else Just (' ', (i + 1, c : s))
->                  | otherwise = Just (c, (i + 1, s))
+>   moo ((fl@(f,l),i), c : s)
+>     | isNL c     = Just (c, (((f, l + 1), 0), s))
+>     | c == '\t'  = if mod i 8 == 7  then Just (' ', ((fl, i + 1), s))
+>                                     else Just (' ', ((fl, i + 1), c : s))
+>     | otherwise  = Just (c, ((fl, i + 1), s))
 
 > stol :: L ()
 > stol = do
->   i <- gets fst
+>   i <- lCol
 >   guard (i == 0)
 
 > chk :: (t -> Bool) -> L t -> L t
@@ -377,10 +479,10 @@
 > spa p = (:) <$> chk p cha <*> spa p  <|> pure []
 
 > sym :: L String
-> sym = StateT $ \ (i, s) -> case h s of
+> sym = StateT $ \ ((fl, i), s) -> case h s of
 >   ("", _) -> Nothing
 >   ("--", _) -> Nothing
->   (s, t) -> Just (s, (i + length s, t))
+>   (s, t) -> Just (s, ((fl, i + length s), t))
 >  where
 >   h (s@('-':'}':_)) = ("", s)
 >   h (c : s) | isInfy c = first (c :) (h s)
diff --git a/src/IdiomBrackets.lhs b/src/IdiomBrackets.lhs
new file mode 100644
--- /dev/null
+++ b/src/IdiomBrackets.lhs
@@ -0,0 +1,78 @@
+> module IdiomBrackets where
+
+> import Control.Applicative
+
+> import HaLay
+> import Parsley
+
+> pIBAlts :: P Tok [[Tok]]
+> pIBAlts = teq (Sym "|") *> many (many (tok (/= Sym "|")) <* teq (Sym "|"))
+
+> pInfA :: P Tok ([Tok], Tok, [Tok])
+> pInfA = (,,) <$> many (tok (not . infSym)) <*> tok infSym <*> pRest where
+>   infSym (Sym s) = not (elem s ["~", "@"])
+>   infSym _ = False
+
+> ia :: Tok -> String -> Tok -> Tok
+> ia x o y = B Rnd [x, Spc " ", Sym o, Spc " ", y]
+
+> ip :: Tok -> Tok
+> ip t = B Rnd [Lid "pure", Spc " ", t]
+
+> iGrok :: Tok -> [Tok] -> Tok
+> iGrok f [] = f
+> iGrok f (s : ts) | isSpcT s = iGrok f ts
+> iGrok f (Sym "@" : ts) = iGrok (B Rnd [Lid "join", Spc " ", f]) ts
+> iGrok f (Sym "~" : Spc _ : ts) = iGrok f (Sym "~" : ts)
+> iGrok f (Sym "~" : t : ts) = iGrok (ia f "<*>" (ip t)) ts
+> iGrok f (B Rnd (Sym "%" : us) : ts) = iGrok (ia f "<*" (iGnore "%" us)) ts
+> iGrok f (B Rnd (Sym "-" : us) : ts) = iGrok (ia f "<*" (iGnore "-" us)) ts
+> iGrok f (t : ts) = iGrok (ia f "<*>" t) ts
+
+> iGnore :: String -> [Tok] -> Tok
+> iGnore z ts = case parse (pSep (teq Semi) (many (tok notSep)) <* teq (Sym z)) ts of
+>     Nothing -> ip (B Rnd [])
+>     Just [] -> ip (B Rnd [])
+>     Just [ts] -> B Rnd ts
+>     Just (ts : tss) -> foldl (\ a bs -> ia a "<*" (B Rnd bs)) (B Rnd ts) tss
+>   where
+>     notSep Semi = False
+>     notSep (Sym x) | x == z = False
+>     notSep _ = True
+
+> iStart :: [Tok] -> Tok
+> iStart [] = ip (B Rnd [])
+> iStart (s : ts) | isSpcT s = iStart ts
+> iStart (B Rnd (Sym "%" : us) : ts) = ia (iGnore "%" us) "*>" (iStart ts)
+> iStart (B Rnd (Sym "-" : us) : ts) = ia (iGnore "-" us) "*>" (iStart ts)
+> iStart (t : ts) = iGrok (ip t) ts
+
+> iIA :: Tok -> [Tok] -> Tok
+> iIA f [] = f
+> iIA f (s : ts) | isSpcT s = iIA f ts
+> iIA f (Sym "@" : ts) = iIA (B Rnd [Lid "join", Spc " ", f]) ts
+> iIA f (Sym "~" : Spc _ : ts) = iIA f (Sym "~" : ts)
+> iIA f (Sym "~" : t : ts) = iIA (ia f "<*>" (ip t)) ts
+> iIA f (B Rnd (Sym "%" : us) : ts) = iIA (ia f "<*" (iGnore "%" us)) ts
+> iIA f (B Rnd (Sym "-" : us) : ts) = iIA (ia f "<*" (iGnore "-" us)) ts
+> iIA f (t : ts) = let (us, vs) = span yum ts in iIA (ia f "<*>" (B Rnd (t : us))) vs
+>   where yum (B Rnd (Sym "%" : _)) = False
+>         yum (Sym "@") = False
+>         yum _ = True
+
+> iPro :: [Tok] -> Tok
+> iPro ts = case parse pInfA ts of
+>   Nothing -> iStart ts
+>   Just (as, o, bs) -> iIA (iIA (ip (B Rnd [o])) as) bs
+
+> rejig :: [[Tok]] -> Tok
+> rejig [] = Lid "empty"
+> rejig [ts] = iPro ts
+> rejig (ts : tss) = ia (iPro ts) "<|>" (rejig tss)
+
+> idiomBrackets :: [Tok] -> [Tok]
+> idiomBrackets = munge ibMu where
+>   ibMu (B Rnd us : ts) = case parse pIBAlts us of
+>     Just uss -> Just $ rejig (map (munge ibMu) uss) : munge ibMu ts
+>     Nothing -> Nothing
+>   ibMu _ = Nothing
diff --git a/src/Imports.lhs b/src/Imports.lhs
--- a/src/Imports.lhs
+++ b/src/Imports.lhs
@@ -3,8 +3,9 @@
 > import Control.Applicative
 > import System.IO.Error
 > import System.FilePath
-> import Data.Foldable
+> import Data.Foldable hiding (elem)
 > import Data.Monoid
+> import Data.Maybe
 
 > import HaLay
 > import Parsley
@@ -20,10 +21,26 @@
 > grokImports cs = foldMap pure $ parse pImport cs
 
 > getHers :: [String] -> IO [[Tok]]
-> getHers p = ready <$>  tryReadFile (joinPath p <.> "hers")
+> getHers p = ready f <$> tryReadFile f where f = joinPath p <.> "hers"
 
 > storySoFar :: [[Tok]] -> IO [[Tok]]
-> storySoFar hs = foldMap getHers (hs >>= grokImports)
+> storySoFar hs = oneOfEach [] <$> foldMap getHers (hs >>= grokImports)
+
+> pModule :: P Tok String
+> pModule = (teq (KW "module") *> spc *> uid) <* pRest
+
+> oneOfEach :: [String] -> [[Tok]] -> [[Tok]]
+> oneOfEach xs [] = []
+> oneOfEach xs (ts : tss) = case parse pModule ts of
+>   Just x | elem x xs  -> oneOfEach xs tss
+>          | otherwise  -> ts : oneOfEach (x : xs) tss
+>   Nothing -> ts : oneOfEach xs tss
+
+> pModuleGuts :: P Tok [[Tok]]
+> pModuleGuts = teq (KW "module") *> spc *> uid *> spc *> pLay "where" pRest
+
+> getGuts :: [[Tok]] -> [[Tok]]
+> getGuts = foldMap (fromMaybe [] . parse pModuleGuts)
 
 > instance Monoid x => Monoid (IO x) where
 >   mempty = pure mempty
diff --git a/src/Main.lhs b/src/Main.lhs
--- a/src/Main.lhs
+++ b/src/Main.lhs
@@ -5,34 +5,47 @@
 > import Data.Char
 > import Data.Traversable
 > import Data.Foldable
+> import Data.List
+> import Debug.Trace
 
 > import HaLay
 > import Imports
 > import Aspect
+> import DeBruijn
 > import Patsy
 > import TypesToKinds
+> import IdiomBrackets
 
-> sheGoes :: [[Tok]] -> [[Tok]] -> ([[Tok]], [[Tok]])
-> sheGoes hersi0 hs0 =
+> sheGoes :: FilePath -> [[Tok]] -> [[Tok]] -> ([[Tok]], [[Tok]])
+> sheGoes mo inh hs0 =
 >   let nl = dental hs0
->       (higs0, hersi1) = foldMap higgle hersi0
+>       hersi0 = getGuts inh
+>       (higs0, _) = foldMap higgle hersi0
 >       (higs1, hs1) = foldMap higgle hs0
 >       higs = higs0 ++ higs1
->       herso0 = higs >>= higOut
+>       herso0 = higs1 >>= higOut
 >       hs2 = piggle higs hs1
->       ((ps0, herso1), _) = traverse getPatsy hersi1
->       ((ps1, herso2), hs3) = traverse getPatsy hs2
+>       hs2'5 = deBruijn hs2
+>       hs2'75 = map idiomBrackets hs2'5
+>       ((ps0, _), _) = traverse getPatsy hersi0
+>       ((ps1, herso1), hs3) = traverse getPatsy hs2'75
 >       hs4 = case prepare (ps0 ++ ps1) of
 >               Nothing -> hs3
 >               Just ps -> map (processes ps) hs3
->       hs5 = typesToKinds hs4 ++ redent nl (hs4 >>= dataGrok)
->   in  (herso0 ++ [[NL]] ++ herso1 ++ [[NL]] ++ herso2, hs5)
+>       hs5 = typesToKinds (noDerSing hs4) ++
+>             redent nl ((hs4 >>= dataGrok) ++ (hs4 >>= singGrok))
+>   in  (inh ++
+>        [[NL (mo ++ ".hers", 0)],
+>         [KW "module", Spc " ", Uid mo, Spc " ", L "where"
+>           (redent [NL (mo ++ ".hers", 0), Spc "  "]
+>            (herso0 ++ [[NL (mo ++ ".hers", 0)]] ++ herso1))]]
+>       , hs5)
 
-> hsAndHers :: String -> IO (String, String)
-> hsAndHers s = do
->   let ihs = ready s
+> hsAndHers :: String -> FilePath -> String -> IO (String, String)
+> hsAndHers f mo s = do
+>   let ihs = ready f s
 >   pcs <- storySoFar ihs
->   let (hers, hs) = sheGoes pcs ihs
+>   let (hers, hs) = sheGoes mo pcs ihs
 >   return (tokssOut hs, tokssOut hers)
 
 > main :: IO ()
@@ -43,7 +56,7 @@
 >   putStrLn y
 >   putStrLn z
 >   f <- readFile y
->   (f', h) <- hsAndHers f
+>   (f', h) <- hsAndHers x (takeBaseName x) f
 >   writeFile x' h
 >   writeFile z f'
 
diff --git a/src/Makefile b/src/Makefile
--- a/src/Makefile
+++ b/src/Makefile
@@ -5,3 +5,34 @@
 
 install: she
 	sudo cp she /usr/local/bin/
+# DO NOT DELETE: Beginning of Haskell dependencies
+Parsley.o : Parsley.lhs
+HaLay.o : HaLay.lhs
+HaLay.o : Parsley.hi
+Imports.o : Imports.lhs
+Imports.o : Parsley.hi
+Imports.o : HaLay.hi
+Aspect.o : Aspect.lhs
+Aspect.o : Parsley.hi
+Aspect.o : HaLay.hi
+DeBruijn.o : DeBruijn.lhs
+DeBruijn.o : HaLay.hi
+DeBruijn.o : Parsley.hi
+Patsy.o : Patsy.lhs
+Patsy.o : HaLay.hi
+Patsy.o : Parsley.hi
+TypesToKinds.o : TypesToKinds.lhs
+TypesToKinds.o : Parsley.hi
+TypesToKinds.o : HaLay.hi
+IdiomBrackets.o : IdiomBrackets.lhs
+IdiomBrackets.o : Parsley.hi
+IdiomBrackets.o : HaLay.hi
+Main.o : Main.lhs
+Main.o : IdiomBrackets.hi
+Main.o : TypesToKinds.hi
+Main.o : Patsy.hi
+Main.o : DeBruijn.hi
+Main.o : Aspect.hi
+Main.o : Imports.hi
+Main.o : HaLay.hi
+# DO NOT DELETE: End of Haskell dependencies
diff --git a/src/Patsy.lhs b/src/Patsy.lhs
--- a/src/Patsy.lhs
+++ b/src/Patsy.lhs
@@ -17,19 +17,19 @@
 
 > getPatsy :: [Tok] -> (([Patsy], [[Tok]]), [Tok])
 > getPatsy cs = case parse pPatsy cs of
->   Just p -> (([p], [cs,[NL]]), jigger p)
+>   Just p -> (([p], [cs,[NL ("Dunno.lhs", 0)]]), jigger p)
 >   _      -> (([], []), cs)
 
 > jigger :: Patsy -> [Tok]
 > jigger (s, (as, cs)) =
->   Lid ("patsy" ++ s) : (as >>= \a -> [Spc " ", Lid a]) ++
+>   Lid ("-- patsy" ++ s) : (as >>= \a -> [Spc " ", Lid a]) ++
 >   [Spc " ", Sym "=", Spc " "] ++ cs
 
 > subst :: [(String, Tok)] -> Tok -> Tok
 > subst xcs (Lid x) = case lookup x xcs of
 >   Just c -> c
 >   Nothing -> Lid x
-> subst xcs (Spc _) = Spc " "
+> subst xcs s | isSpcT s = Spc " "
 > subst xcs (B Rnd cs) = B Rnd (map (subst xcs) cs)
 > subst xcs (B Sqr cs) = B Sqr (map (subst xcs) cs)
 > subst xcs (B Crl cs) = B Crl (recs False cs) where
@@ -63,7 +63,7 @@
 > process :: [Patsy] -> Tok -> Maybe Tok
 > process ps (Lid y) = Just (Lid y)
 > process ps (Uid c) = case lookup c ps of
->   Just (xs, cs) -> Just (abstract xs cs)
+>   Just (xs, cs) -> Just (abstract xs (map (subst []) cs))
 >   Nothing -> Just (Uid c)
 > process ps (B Rnd cs) = Just $ B Rnd (processes ps cs)
 > process ps (B Sqr cs) = Just $ B Sqr (processes ps cs)
diff --git a/src/ShePrelude.lhs b/src/ShePrelude.lhs
new file mode 100644
--- /dev/null
+++ b/src/ShePrelude.lhs
@@ -0,0 +1,42 @@
+> {-# LANGUAGE TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses, GADTs,
+>     ScopedTypeVariables, FlexibleContexts
+> #-}
+
+> module ShePrelude where
+
+> data SheProxy (ty :: *) (tm :: *) where SheProxy :: SheProxy ty tm
+> class SheChecks (ty :: *) (tm :: *) where
+>   sheTypes :: SheProxy ty tm -> SheSingleton ty tm
+> data family SheSingleton ty :: * -> *
+
+> data SheTyLeft x = SheTyLeft x
+> data SheTyRight x = SheTyRight x
+> data instance SheSingleton (Either s t) dummy where
+>   SheWitLeft   :: SheSingleton s x -> SheSingleton (Either s t) (SheTyLeft x)
+>   SheWitRight  :: SheSingleton t x -> SheSingleton (Either s t) (SheTyRight x)
+> instance SheChecks s x => SheChecks (Either s t) (SheTyLeft x) where
+>   sheTypes _ = SheWitLeft (sheTypes (SheProxy :: SheProxy s x))
+> instance SheChecks t x => SheChecks (Either s t) (SheTyRight x) where
+>   sheTypes _ = SheWitRight (sheTypes (SheProxy :: SheProxy t x))
+
+> data SheTyTrue = SheTyTrue
+> data SheTyFalse = SheTyFalse
+> data instance SheSingleton Bool dummy where
+>   SheWitTrue   :: SheSingleton Bool SheTyTrue
+>   SheWitFalse  :: SheSingleton Bool SheTyFalse
+> instance SheChecks Bool SheTyTrue where
+>   sheTypes _ = SheWitTrue
+> instance SheChecks Bool SheTyFalse where
+>   sheTypes _ = SheWitFalse
+
+> data SheSpecialNil = SheSpecialNil
+> data (:$#$#$#:) x y = (:$#$#$#:) x y
+> data instance SheSingleton [t] dummy where
+>   SheSpecialWitNil :: SheSingleton [t] SheSpecialNil
+>   (:$%$%$%:) :: SheSingleton t x -> SheSingleton [t] xs ->
+>                 SheSingleton [t] (x :$#$#$#: xs)
+> instance SheChecks [t] SheSpecialNil where
+>   sheTypes _ = SheSpecialWitNil
+> instance (SheChecks t x, SheChecks [t] xs) => SheChecks [t] (x :$#$#$#: xs) where
+>   sheTypes _ = (sheTypes (SheProxy :: SheProxy t x)) :$%$%$%:
+>                (sheTypes (SheProxy :: SheProxy [t] xs))
diff --git a/src/TypesToKinds.lhs b/src/TypesToKinds.lhs
--- a/src/TypesToKinds.lhs
+++ b/src/TypesToKinds.lhs
@@ -1,6 +1,7 @@
 > module TypesToKinds where
 
 > import Control.Applicative
+> import Data.List
 
 > import HaLay
 > import Parsley
@@ -14,12 +15,14 @@
 
 > blat :: (Tok, Int) -> [Tok]
 > blat (c, j) =
->     [KW "data", T Ty (cxs ++ [Spc " "]), Sym "=", T Ty cxs] where
->   cxs = Spc " " : c : ([1 .. j] >>= (\k -> [Spc " ", Lid ("x" ++ show k)]))
+>     [KW "data", T Ty (cxs id ++ [Spc " "]), Sym "="] ++ cxs ty where
+>   cxs f = Spc " " : c :
+>           ([1 .. j] >>= (\k -> [Spc " ", f (Lid ("x" ++ show k))]))
+>   ty t = T Ty [t]
 
 > fillet :: [Tok] -> [(Tok, Int)]
 > fillet [] = []
-> fillet (Sym "=" : [T Ty cs]) =
+> fillet (Sym "=" : cs) =
 >   case parse (pSep (spc *> teq (Sym "|")) (spc *> pOldSyn)) cs of
 >     Just sis -> sis
 >     _ -> []
@@ -27,25 +30,25 @@
 > fillet (_ : cs) = fillet cs
 
 > pOldSyn :: P Tok (Tok, Int)
-> pOldSyn = (\s -> (jig s, 2)) <$ pArg <*> infC <* pArg
+> pOldSyn = (\s -> (jig s, 2)) <$ pArg <* spc <*> infC <* pArg
 >       <|> (,) <$> pCId
->               <*> (length <$> many pArg <|> pBr Crl pFields)
 >               <* spc
+>               <*> (pBr Crl pFields <|> length <$> many pArg)
+>               <* spc
 
 > jig :: String -> Tok
 > jig s = (B Rnd [Sym (":$#$#$#" ++ s)])
 
 > pArg :: P Tok ()
 > pArg = spc <* (
->   () <$ lid <|>
->   () <$ uid <|>
->   pBr Rnd (() <$ pRest) <|>
->   pBr Sqr (() <$ pRest) <|>
+>   (() <$ pTag Ty pRest) <|>
 >   teq (Sym "!") *> pArg
 >   )
 
 > pFields :: P Tok Int
-> pFields = 0 <$ pEnd <|> (1 +) <$ lid <*> pFields <|> next *> pFields
+> pFields = 0 <$ pEnd
+>       <|> (1 +) <$ lid <*> pFields  -- right, assuming types are chunked
+>       <|> next *> pFields
 
 > gadtSyn :: [Tok] -> [(Tok, Int)]
 > gadtSyn cs = case parse pGDecl cs of
@@ -65,21 +68,260 @@
 >      <|> (1 +) <$ teq (Sym "->") <*> pArity
 >      <|> next *> pArity
 
+> pTele :: P Tok ([(String, [Tok])], [Tok])
+> pTele = (,)  <$> some (spc *> pBr Rnd piB) <* spc <* teq (Sym ".")
+>              <*> pRest
+>              where
+>    piB :: P Tok (String, [Tok])
+>    piB = (,) <$ spc <*> lid <* spc <* teq (Sym "::") <* spc <*> pRest
+
 > tyTTK :: [Tok] -> Maybe [Tok]
-> tyTTK (B Crl [T Ex us] : ts) =
->   Just $ B Rnd (munge exTTK us) : munge tyTTK ts
-> tyTTK (B Crl [T Ty us] : ts) =
->   Just $ Sym "*" : munge tyTTK ts
+> tyTTK (B Crl [T Ex (Sym ":" : us)] : ts) = case parse pProxyRequest us of
+>   Just (tm, ty) -> Just $
+>     [Uid "SheChecks", Spc " ", B Rnd ty, Spc " ", B Rnd (munge exTTK tm)]
+>     ++ munge tyTTK ts
+>   _ -> Nothing
+> tyTTK (B Crl [T Ex us] : ts)  = Just $ B Rnd (munge exTTK us) : munge tyTTK ts
+> tyTTK (B Rnd us : ts) = (: munge tyTTK ts) <$> (sing <$> parse pSing us) where
+>   sing t = B Rnd [Uid "SheSingleton", Spc " ", B Rnd t]
+>   pSing = spc *> teq (Sym "::") *> pTag Ki pRest
+> tyTTK (Lid "pi" : ts)         = pity <$> parse pTele ts where
+>   pity :: ([(String, [Tok])], [Tok]) -> [Tok]
+>   pity (xss, ts) =
+>     [KW "forall", Spc " "] ++
+>     (xss >>= \ (x, _) -> [Lid x, Spc " "]) ++
+>     [Sym ".", Spc " "] ++
+>     (xss >>= \ (x, ss) ->
+>       [Uid "SheSingleton", Spc " ", B Rnd (munge tyTTK ss), Spc " ", Lid x,
+>        Spc " ", Sym "->", Spc " "]) ++
+>     munge tyTTK ts
+> tyTTK (T Ki us : ts)          = Just $ T Ki (munge kiTTK us) : munge tyTTK ts
 > tyTTK _ = Nothing
 
+> kiTTK :: [Tok] -> Maybe [Tok]
+> kiTTK (B Crl [T Ty us] : ts)  = Just $ Sym "*" : munge kiTTK ts
+> kiTTK (Lid "pi" : ts)         = piki <$> parse pTele ts where
+>   piki :: ([(String, [Tok])], [Tok]) -> [Tok]
+>   piki (xks, ts) =
+>     (xks >>= \ (_, ks) ->
+>       [B Rnd (munge kiTTK ks), Spc " ", Sym "->", Spc " "]) ++
+>     munge kiTTK ts
+> kiTTK (KW "forall" : ts)      = case span (/= Sym ".") ts of
+>   (_, _ : ts) -> Just $ munge kiTTK ts
+>   _ -> Nothing
+> kiTTK _ = Nothing
+
 > ttkMu :: [Tok] -> Maybe [Tok]
 > ttkMu (T Ty us : ts) = Just $ T Ty (munge tyTTK us) : munge ttkMu ts
+> ttkMu (B Crl (Sym ":" : us) : ts) = case parse pProxyRequest us of
+>   Just (tm, ty) -> Just $ proxyRequest tm ty : munge ttkMu ts
+>   _ -> Nothing
+> ttkMu (B Crl us : ts)
+>   | piArg us = Just $ B Rnd (munge witMu us) : munge ttkMu ts
+>   where
+>     piArg xs | elem (Sym "=") xs = False
+>     piArg xs | elem (Sym "::") xs = False
+>     piArg _ = True
 > ttkMu _ = Nothing
 
+> pProxyRequest :: P Tok ([Tok], [Tok])
+> pProxyRequest = (,) <$> some (tok (/= Sym "::")) <* teq (Sym "::") <* spc
+>                     <*> pTag Ty (some (tok (/= Sym ":")) <* teq (Sym ":"))
+
+> witMu :: [Tok] -> Maybe [Tok]
+> witMu (B Sqr us : ts) = Just $ mkL (munge witMu us) : munge witMu ts where
+>   mkL [] = Uid "SheSpecialWitNil"
+>   mkL ts = case span (/= Sym ",") ts of
+>     (ss, []) ->
+>       B Rnd [B Rnd ss, Spc " ", Sym ":$%$%$%:", Spc " ", Uid "SheSpecialNil"]
+>     (ss, _ : ts) ->
+>       B Rnd [B Rnd ss, Spc " ", Sym ":$%$%$%:", Spc " ", mkL ts]
+> witMu (Uid s : ts) = Just $ Uid ("SheWit" ++ s) : munge witMu ts
+> witMu (Sym (':' : s) : ts) = Just $ Sym (":$%$%$%:" ++ s) : munge witMu ts
+> witMu _ = Nothing
+
 > exTTK :: [Tok] -> Maybe [Tok]
+> exTTK (B Sqr us : ts) = Just $ mkL (munge exTTK us) : munge exTTK ts where
+>   mkL [] = Uid "SheSpecialNil"
+>   mkL ts = case span (/= Sym ",") ts of
+>     (ss, []) ->
+>       B Rnd [B Rnd ss, Spc " ", Sym ":$#$#$#:", Spc " ", Uid "SheSpecialNil"]
+>     (ss, _ : ts) ->
+>       B Rnd [B Rnd ss, Spc " ", Sym ":$#$#$#:", Spc " ", mkL ts]
 > exTTK (Uid s : ts) = Just $ Uid ("SheTy" ++ s) : munge exTTK ts
 > exTTK (Sym (':' : s) : ts) = Just $ Sym (":$#$#$#:" ++ s) : munge exTTK ts
 > exTTK _ = Nothing
 
 > typesToKinds :: [[Tok]] -> [[Tok]]
 > typesToKinds = map (munge ttkMu)
+
+> data ConTy = ConTy
+>   { cName     :: String
+>   , cForall   :: [Tok]
+>   , cInst     :: [Tok]
+>   , cArgs     :: [[Tok]]
+>   , cFam      :: [Tok]
+>   , cIndices  :: [Tok]
+>   } deriving (Show)
+
+> sing :: ConTy -> ConTy
+> sing (ConTy
+>   { cName     = c
+>   , cForall   = xs
+>   , cInst     = is
+>   , cArgs     = as
+>   , cFam      = ds
+>   , cIndices  = ss
+>   }) = ConTy
+>   { cName     = "SheWit" ++ c
+>   , cForall   = xs ++ (vs >>= (\v -> [Spc " ", Lid v]))
+>  -- , cInst     = is 
+>   , cInst     = cook is (zipWith constra as vs)
+>   , cArgs     = zipWith singa as vs
+>   , cFam      = [B Rnd ([Uid "SheSingleton", Spc " "] ++ ds ++ Spc " " : ss)]
+>   , cIndices  = ss  ++ [Spc " ",
+>                     B Rnd  (mkPref (sheTy c) :
+>                            (vs >>= (\ v -> [Spc " ", Lid v])))]
+>   } where
+>   vs = zipWith (\ _ i -> "sha" ++ show i) as [0..]
+>   singa ts v = [Uid "SheSingleton", Spc " ", B Rnd ts, Spc " ", Lid v]
+>   constra ts v = [Uid "SheChecks", Spc " ", B Rnd ts, Spc " ", Lid v]
+>   cook is [] | all isSpcT is = is
+>   cook (B Rnd is : _) cs = cook is cs
+>   cook is cs
+>     | all isSpcT is = [B Rnd (intercalate [Sym ",", Spc " "] cs)]
+>     | otherwise = [B Rnd (intercalate [Sym ",", Spc " "] (is : cs))]
+
+> conTyOut :: ConTy -> [Tok]
+> conTyOut (ConTy
+>   { cName     = c
+>   , cForall   = xs
+>   , cInst     = is
+>   , cArgs     = as
+>   , cFam      = ds
+>   , cIndices  = ss
+>   }) = [Uid c, Spc " ", Sym "::", Spc " ", T Ty (
+>        fao xs ++
+>        cio is ++
+>        (as >>= \ ts -> ts ++ [Spc " ", Sym "->", Spc " "]) ++
+>        ds ++ Spc " " : ss)]
+>   where
+>     fao xs | all isSpcT xs = xs
+>            | otherwise = [KW "forall", Spc " "] ++ xs ++ [Sym ".", Spc " "]
+>     cio xs | all isSpcT xs = xs
+>            | otherwise = xs ++ [Spc " ", Sym "=>", Spc " "]
+
+> pGConTy :: P Tok ConTy
+> pGConTy = (ConTy <$ spc <*> uid <* spc <* teq (Sym "::") <* spc) >>= \f ->
+>           pTag Ty (f <$> pFA <*> pCI <*> many pARG <* spc <*> (((:[]). Uid) <$> uid)
+>                    <*> pRest)
+>   where
+>     pFA = spc *> (
+>             teq (KW "forall") *> some (tok (/= Sym ".")) <* teq (Sym ".")
+>             <|> [] <$ spc)
+>     pCI = some (tok (/= Sym "=>")) <* teq (Sym "=>")
+>           <|> [] <$ spc
+>     pARG = some (tok (/= Sym "->")) <* teq (Sym "->")
+
+> mkPref :: Tok -> Tok
+> mkPref t@(Sym _) = B Rnd [t]
+> mkPref t = t
+
+> sheTy :: String -> Tok
+> sheTy (':' : s) = Sym (":$#$#$#:" ++ s)
+> sheTy s = Uid ("SheTy" ++ s)
+
+> pGADT :: P Tok ((String, Int), ([ConTy], [String]))
+> pGADT = (,)
+>   <$   tok (`elem` [KW "data", KW "newtype"]) <* spc
+>   <*>  pTag Ty ((,) <$ spc <*> uid <* spc <*>  pGArity <* pRest) <* spc
+>   <*>  pLay "where" ((,) <$> pGCons <*> pDer)
+>   <*   pRest
+>   where
+>     pGArity = length <$> many (lid <* spc)
+>               <|> (teq (Sym "::") *> spc *> pTag Ki pArity)
+>     pGCons = tok (all isSpcT) *> pGCons
+>              <|> (:) <$> grok (parse pGConTy) next <*> pGCons
+>              <|> pure []
+>     pDer = grok (parse pDeriving) next <* pRest <|> pure []
+
+> pDeriving :: P Tok [String]
+> pDeriving = teq (KW "deriving") *> spc *>
+>             (pure <$> uid <|>
+>             pBr Rnd (spc *> pSep (spc *> teq (Sym ",") *> spc) uid <* spc))
+
+ singGrok :: [Tok] -> [[Tok]]
+ singGrok ts = case parse pGADT ts of
+   Just ((s, i), (cs, ds)) | elem "SheSingleton" ds ->
+    let vs = [1..i] >>= \v -> [Spc " ", Lid ("x" ++ show i)] in
+    [[KW "type",
+      T Ty [Spc " ", KW "instance", Spc " ", Uid "SheSingleton", Spc " ",
+           B Rnd (Uid s : vs), Spc " "],
+      Sym "=",
+      T Ty (Spc " " : Uid ("SheSing" ++ s) : vs)],[NL ("Dunno.lhs",0)],
+     [KW "data", Spc " ", Uid ("SheSing" ++ s), Spc " ", Sym "::",
+      T Ki (concat (replicate i [Spc " ", Sym "*", Spc " ", Sym "->"]) ++
+           [Spc " ", Sym "*", Spc " ", Sym "->", Spc " ", Sym "*", Spc " "]),
+      L "where" (cs >>= \ c -> [[NL ("Dunno.lhs",0), Spc "    "], conTyOut (sing c)])],[NL ("Dunno.lhs",0)]] ++
+     (cs >>= \ c -> [checkI c, [NL ("Dunno.lhs",0)]])
+   _ -> []
+
+> singGrok :: [Tok] -> [[Tok]]
+> singGrok ts = case parse pGADT ts of
+>   Just ((s, i), (cs, ds)) | elem "SheSingleton" ds ->
+>    let vs = [1..i] >>= \v -> [Spc " ", Lid ("x" ++ show i)] in
+>     [[KW "data",
+>       T Ty [Spc " ", KW "instance", Spc " ", Uid "SheSingleton", Spc " ",
+>            B Rnd (Uid s : vs), Spc " ", Uid "dummy", Spc " ",
+>       L "where" (cs >>= \ c -> [[NL ("Dunno.lhs",0), Spc "    "], conTyOut (sing c)])]],
+>      [NL ("Dunno.lhs",0)]] ++
+>      (cs >>= \ c -> [checkI c, [NL ("Dunno.lhs",0)]])
+>   _ -> []
+
+> checkI :: ConTy -> [Tok]
+> checkI  (ConTy
+>   { cName     = c
+>   , cForall   = xs
+>   , cInst     = is
+>   , cArgs     = as
+>   , cFam      = ds
+>   , cIndices  = ss
+>   }) =
+>   [KW "instance",
+>    T Ty (Spc " " : prems ais ++
+>     [Uid "SheChecks", Spc " ", B Rnd (ds ++ Spc " " : ss), Spc " ",
+>      B Rnd (mkPref (sheTy c) : (ais >>= (\ (_, v) -> [Spc " ", Lid v]))),
+>      Spc " "]),
+>    L "where" [[Spc " "],
+>      [Lid "sheTypes", Spc " ", Lid "_", Spc " ", Sym "=", Spc " ",
+>       Uid ("SheWit" ++ c)] ++ (ais >>= poxy)
+>      ]
+>   ]
+>   where
+>     ais = zipWith (\ty i -> (ty, "sha" ++ show i)) as [0..]
+>     prems [] = []
+>     prems [tyv] = cnstr tyv ++ [Spc " " , Sym "=>", Spc " "]
+>     prems (tyv : tyvs) =
+>       [B Rnd (cnstr tyv ++
+>               (tyvs >>= \tyv -> [Sym ",", Spc " "] ++ cnstr tyv)),
+>        Spc " " , Sym "=>", Spc " "]
+>     cnstr (ty, v) = [Uid "SheChecks", Spc " ", B Rnd ty, Spc " ", Lid v]
+>     poxy (ty, v) = [Spc " ", proxyRequest [Lid v] ty]
+
+> proxyRequest :: [Tok] -> [Tok] -> Tok
+> proxyRequest tm ty = B Rnd [
+>       Lid "sheTypes", Spc " ", B Rnd [
+>         Uid "SheProxy", Spc " ", Sym "::", T Ty [Spc " ",
+>           Uid "SheProxy", Spc " ", B Rnd ty, Spc " ", B Rnd (munge exTTK tm)
+>       ]]]
+
+> noDerSing :: [[Tok]] -> [[Tok]]
+> noDerSing = map (munge ndsMu) where
+>   ndsMu ts = case parse pDeriving ts of
+>     Just xs -> Just $ mkDer (filter (/= "SheSingleton") xs)
+>     _ -> Nothing
+>   mkDer [] = []
+>   mkDer [x] = [KW "deriving", Spc " ", Uid x]
+>   mkDer (x : xs) =
+>     [KW "deriving", Spc " ",
+>      B Rnd (Uid x : (xs >>= \x -> [Sym ",", Spc " ", Uid x]))]