diff --git a/LICENCE b/LICENCE
new file mode 100644
--- /dev/null
+++ b/LICENCE
@@ -0,0 +1,5 @@
+SHE is written by Conor McBride.
+
+Permission is hereby granted, free of charge, to any person obtaining this work (the "Work"), to deal in the Work without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Work, and to permit persons to whom the Work is furnished to do so.
+
+THE WORK IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE WORK OR THE USE OR OTHER DEALINGS IN THE WORK. 
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,3 @@
+#!/usr/bin/env runhaskell
+> import Distribution.Simple
+> main = defaultMain
diff --git a/examples/FH.lhs b/examples/FH.lhs
new file mode 100644
--- /dev/null
+++ b/examples/FH.lhs
@@ -0,0 +1,57 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators, GADTs, KindSignatures, RankNTypes #-}
+
+> module FH where
+
+> import System.FilePath
+> import System.IO
+> import System.IO.Error
+
+> import IFunctor
+
+> data FHState = FOpen | FClosed
+> data FHSTATE :: {FHState} -> * where
+>   FOPEN    :: FHSTATE {FOpen}
+>   FCLOSED  :: FHSTATE {FClosed}
+
+> data FH :: ({FHState} -> *) -> {FHState} -> * where
+>   FHOpen   :: FilePath -> (FHSTATE :-> q) -> FH q {FClosed}
+>   FHClose  :: q {FClosed} -> FH q {FOpen}
+>   FHRead   :: (Maybe Char -> q {FOpen}) -> FH q {FOpen}
+
+> instance IFunctor FH where
+>   imap f (FHOpen s k) = FHOpen s (f . k)
+>   imap f (FHClose q) = FHClose (f q)
+>   imap f (FHRead k) = FHRead (f . k)
+
+> fhOpen :: FilePath -> (FH :* FHSTATE) {FClosed}
+> fhOpen f = Do $ FHOpen f Ret
+
+> fhClose :: (FH :* (() :- {FClosed})) {FOpen}
+> fhClose = Do . FHClose . Ret $ V ()
+
+> fhRead :: (FH :* (Maybe Char :- {FOpen})) {FOpen}
+> fhRead = Do . FHRead $ \ c -> Ret (V c)
+
+> runFH :: (FH :* (a :- {FClosed})) {FClosed} -> IO a
+> runFH (Ret (V a)) = return a
+> runFH (Do (FHOpen s f)) = catch
+>   (openFile s ReadMode >>= openFH (f FOPEN))
+>   (\ _ -> runFH (f FCLOSED))
+>   where
+>     openFH :: (FH :* (a :- {FClosed})) {FOpen} -> Handle -> IO a
+>     openFH (Do (FHClose k)) h = hClose h >> runFH k
+>     openFH (Do (FHRead f)) h = catch
+>       (hGetChar h >>= \ c -> openFH (f (Just c)) h)
+>       (\ _ -> openFH (f Nothing) h)
+
+> myReadFile :: FilePath -> IO (Maybe String)
+> myReadFile s = runFH $ fhOpen s >>- check where
+>   check :: FHSTATE :-> (FH :* (Maybe String :- {FClosed}))
+>   check FCLOSED = ret Nothing
+>   check FOPEN = grab ?- \ s -> fhClose ?- \ _ -> ret (Just s)
+>   grab :: (FH :* (String :- {FOpen})) {FOpen}
+>   grab = fhRead ?- \ x -> case x of
+>     Nothing -> ret ""
+>     Just c -> grab ?- \ cs -> ret (c : cs)
+
diff --git a/examples/Fix.lhs b/examples/Fix.lhs
new file mode 100644
--- /dev/null
+++ b/examples/Fix.lhs
@@ -0,0 +1,59 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators #-}
+
+> module Fix where
+
+> import Control.Arrow
+
+> data Fix f = In (f (Fix f))
+
+> newtype (:+:) f g x = Plus (Either (f x) (g x))
+> newtype (:*:) f g x = Times (f x, g x)
+> newtype K a x = K a
+> newtype I x = I x
+
+> infixr 4 :+:
+> infixr 5 :*:
+
+> type ListF x = K () :+: (K x :*: I)
+
+> type List x = Fix (ListF x)
+
+> pattern NilF = Plus (Left (K ()))
+> pattern ConsF x xs = Plus (Right (Times (K x, I xs)))
+> pattern Nil = In NilF
+> pattern Cons x xs = In (ConsF x xs)
+
+> foldFix :: Functor f => (f t -> t) -> Fix f -> t
+> foldFix phi (In xs) = phi (fmap (foldFix phi) xs)
+
+> paraFix :: Functor f => (f (Fix f, t) -> t) -> Fix f -> t
+> -- paraFix g = snd . foldFix (\ fxt -> (In (fmap fst fxt), g fxt))
+> paraFix g (In ff) = g (fmap (id &&& paraFix g) ff)
+
+> (+++) :: List x -> List x -> List x
+> xs +++ ys = foldFix phi xs where
+>   phi NilF = ys
+>   phi (ConsF x xs) = Cons x xs
+
+> blat :: List x -> [x]
+> blat = foldFix phi where
+>   phi NilF = []
+>   phi (ConsF x xs) = x : xs
+
+> talb :: [x] -> List x
+> talb = foldr Cons Nil
+
+> instance (Functor f, Functor g) => Functor (f :+: g) where
+>   fmap p (Plus (Left fx)) = Plus (Left (fmap p fx))
+>   fmap p (Plus (Right gx)) = Plus (Right (fmap p gx))
+
+> instance (Functor f, Functor g) => Functor (f :*: g) where
+>   fmap p (Times (fx, gx)) = Times (fmap p fx, fmap p gx)
+
+> instance Functor (K a) where
+>   fmap p (K a) = K a
+
+> instance Functor I where
+>   fmap p (I a) = I (p a)
+
diff --git a/examples/Hig.lhs b/examples/Hig.lhs
new file mode 100644
--- /dev/null
+++ b/examples/Hig.lhs
@@ -0,0 +1,19 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators #-}
+
+> module Hig where
+
+> import -> ExpF where
+>   AddF :: t -> t -> ExpF t
+
+> import -> ExpPS where
+>   pattern Add x y = C (AddF x y)
+
+> import -> FunctorExpF where
+>   fmap f (AddF a b) = AddF (f a) (f b)
+
+> import -> EvAlg where
+>   AddF u v -> u + v
+
+> import -> EvParser where
+>   <|> Add <$ teq '(' <*> pExp <* teq '+' <*> pExp <* teq ')'
diff --git a/examples/IFunctor.lhs b/examples/IFunctor.lhs
new file mode 100644
--- /dev/null
+++ b/examples/IFunctor.lhs
@@ -0,0 +1,45 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE KindSignatures, RankNTypes, TypeOperators, GADTs #-}
+
+> module IFunctor where
+
+> type s :-> t = forall i. s i -> t i
+
+> 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/Jig.lhs b/examples/Jig.lhs
new file mode 100644
--- /dev/null
+++ b/examples/Jig.lhs
@@ -0,0 +1,19 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators #-}
+
+> module Jig where
+
+> import -> ExpF where
+>   NegF :: t -> ExpF t
+
+> import -> ExpPS where
+>   pattern Neg x = C (NegF x)
+
+> import -> FunctorExpF where
+>   fmap f (NegF a) = NegF (f a)
+
+> import -> EvAlg where
+>   NegF u -> negate u
+
+> import -> EvParser where
+>   <|> Neg <$ teq '-' <*> pExp
diff --git a/examples/Parsley.lhs b/examples/Parsley.lhs
new file mode 100644
--- /dev/null
+++ b/examples/Parsley.lhs
@@ -0,0 +1,81 @@
+> module Parsley where
+
+> import Data.Char
+> import Control.Applicative
+> import Control.Monad
+> import Control.Monad.State
+
+> (<*^) :: Applicative f => f (a -> b) -> a -> f b
+> f <*^ s = f <*> pure s
+
+> newtype P t x = P {runP :: [t] -> Maybe ([t], x, [t])}
+
+> instance Monad (P t) where
+>   return x = P $ \ ts -> Just ([], x, ts)
+>   P s >>= f = P $ \ts -> do
+>     (sts, s', ts) <- s ts
+>     (tts, t', ts) <- runP (f s') ts
+>     return (sts ++ tts, t', ts)
+
+> parse :: P t x -> [t] -> Maybe x
+> parse p ts = case runP p ts of
+>   Just (_, x, []) -> Just x
+>   _ -> Nothing
+
+> instance Functor (P t) where
+>   fmap = ap . return
+
+> instance Applicative (P t) where
+>   pure = return
+>   (<*>) = ap
+
+> instance Alternative (P t) where
+>   empty = P $ \ _ -> Nothing
+>   p <|> q = P $ \ ts -> runP p ts <|> runP q ts
+
+> pRest :: P t [t]
+> pRest = P $ \ ts -> Just (ts, ts, [])
+
+> pEnd :: P t ()
+> pEnd = P $ \ ts -> if null ts then Just ([], (), []) else Nothing
+
+> next :: P t t
+> next = P $ \ ts -> case ts of
+>   [] -> Nothing
+>   (t : ts) -> Just ([t], t, ts)
+
+> pExt :: P t x -> P t ([t], x)
+> pExt (P x) = P $ \ ts -> do
+>   (xts, x', ts) <- x ts
+>   return (xts, (xts, x'), ts)
+
+> pOpt :: P t x -> P t (Maybe x)
+> pOpt p = Just <$> p <|> pure Nothing
+
+>{-
+> pPlus :: P t x -> P t [x]
+> pPlus p = (:) <$> p <*> pStar p
+
+> pStar :: P t x -> P t [x]
+> pStar p = pPlus p <|> pure []
+> -}
+
+> pSep :: P t s -> P t x -> P t [x]
+> pSep s p = (:) <$> p <*> many (s *> p) <|> pure []
+
+> grok :: (a -> Maybe b) -> P t a -> P t b
+> grok f p = do
+>   a <- p
+>   case f a of
+>     Just b -> return b
+>     Nothing -> empty
+
+> ok :: (a -> Bool) -> a -> Maybe a
+> ok p a = guard (p a) >> return a
+
+> tok :: (t -> Bool) -> P t t
+> tok p = grok (ok p) next
+
+> teq :: Eq t => t -> P t ()
+> teq t = tok (== t) *> pure ()
+
diff --git a/examples/Path.lhs b/examples/Path.lhs
new file mode 100644
--- /dev/null
+++ b/examples/Path.lhs
@@ -0,0 +1,28 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE KindSignatures, GADTs, RankNTypes, TypeOperators #-}
+
+> module Path where
+
+> import Unsafe.Coerce
+
+> import IFunctor
+
+> data Path :: ({i,i} -> *) -> {i,i} -> * where
+>   Nil :: Path r {i,i}
+>   (:-:) :: r {i,j} -> Path r {j,k} -> Path r {i,k}
+
+> instance IFunctor Path where
+>   imap f Nil = Nil
+>   imap f (r :-: rs) = f r :-: imap f rs
+
+> (+-+) :: Path r {i,j} -> Path r {j,k} -> Path r {i,k}
+> Nil +-+ ps = ps
+> (r :-: rs) +-+ ps = r :-: (rs +-+ ps)
+
+> instance IMonad Path where
+>   iskip = splip $ \ r -> r :-: Nil
+>   iextend f (r :-: rs) = f r +-+ iextend f rs
+
+> splip :: forall (s :: {i,j} -> *) (t :: {i,j} -> *) .
+>            (forall i j . s {i,j} -> t {i,j}) -> s :-> t
+> splip = unsafeCoerce
diff --git a/examples/Pig.lhs b/examples/Pig.lhs
new file mode 100644
--- /dev/null
+++ b/examples/Pig.lhs
@@ -0,0 +1,37 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators, KindSignatures, GADTs #-}
+
+> module Pig where
+
+> import Control.Applicative
+> import Data.Char
+
+> import Parsley
+
+> import Hig
+> import Jig
+
+> data ExpF :: * -> * where
+>   import <- ExpF
+
+> instance Functor ExpF where
+>   import <- FunctorExpF
+
+> data Free :: (* -> *) -> * -> * where
+>   V :: x -> Free f x
+>   C :: f (Free f x) -> Free f x
+
+> fEval :: Functor f => (x -> t) -> (f t -> t) -> Free f x -> t
+> fEval g f (V x)  = g x
+> fEval g f (C fe) = f (fmap (fEval g f) fe)
+
+> type Exp = Free ExpF
+> import <- ExpPS
+
+> eval :: (x -> Int) -> Exp x -> Int
+> eval g = fEval g $ \ e -> case e of
+>   import <- EvAlg
+
+> pExp :: P Char (Exp Char)
+> pExp = V <$> tok isAlpha
+>   import <- EvParser
diff --git a/examples/Tree.lhs b/examples/Tree.lhs
new file mode 100644
--- /dev/null
+++ b/examples/Tree.lhs
@@ -0,0 +1,38 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators #-}
+
+> module Tree where
+
+> import Fix
+
+> type TreeF x = K () :+: (I :*: K x :*: I)
+> type Tree x = Fix (TreeF x)
+
+> pattern LeafF = Plus (Left (K ()))
+> pattern NodeF l x r = Plus (Right (Times (I l, Times (K x, I r))))
+> pattern Leaf = In LeafF
+> pattern Node l x r = In (NodeF l x r)
+
+> spiny :: List x -> Tree x
+> spiny Nil = Leaf
+> spiny (Cons x xs) = Node Leaf x (spiny xs)
+
+> insert :: Ord x => x -> Tree x -> Tree x
+> insert x = paraFix g where
+>   g LeafF = Node Leaf x Leaf
+>   g (NodeF (l, l') y (r, r'))
+>     | x <= y     = Node l' y r
+>     | otherwise  = Node l y r'
+
+> mkTree :: Ord x => List x -> Tree x
+> mkTree = foldFix alg where
+>   alg NilF = Leaf
+>   alg (ConsF x xs) = insert x xs
+
+> flatTree :: Tree x -> List x
+> flatTree = foldFix phi where
+>   phi LeafF = Nil
+>   phi (NodeF l x r) = l +++ (Cons x Nil) +++ r
+
+> treeSort :: Ord x => List x -> List x
+> treeSort = flatTree . mkTree
diff --git a/examples/Vec.lhs b/examples/Vec.lhs
new file mode 100644
--- /dev/null
+++ b/examples/Vec.lhs
@@ -0,0 +1,19 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE GADTs, KindSignatures, TypeOperators #-}
+
+> module Vec where
+
+> import Control.Applicative
+
+> data Nat = Z | S Nat
+
+> data Vec :: {Nat} -> * -> * where
+>   VNil :: Vec {Z} x
+>   (:>) :: x -> Vec {n} x -> Vec {S n} x
+
+> 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
diff --git a/she.cabal b/she.cabal
new file mode 100644
--- /dev/null
+++ b/she.cabal
@@ -0,0 +1,41 @@
+name:               she
+version:            0.0
+homepage:           http://personal.cis.strath.ac.uk/~conor/pub/she
+synopsis:           A Haskell preprocessor adding miscellaneous features
+description:
+    The Strathclyde Haskell Enhancement is a somewhat inglorious bodge,
+    equipping ghc with automatic lifting of types to kinds, pattern
+    synonyms, and some kit for higgledy-piggledy literate programming.
+category:           Language
+license:            PublicDomain
+license-file:       LICENCE
+author:             Conor McBride
+maintainer:         conor@strictlypositive.org
+extra-source-files: src/Makefile
+                    examples/Fix.lhs
+                    examples/FH.lhs
+                    examples/Hig.lhs
+                    examples/IFunctor.lhs
+                    examples/Jig.lhs
+                    examples/Parsley.lhs
+                    examples/Path.lhs
+                    examples/Pig.lhs
+                    examples/Tree.lhs
+                    examples/Vec.lhs
+cabal-version:      >= 1.2
+build-type:         Simple
+
+executable she
+    main-is:            Main.lhs
+
+    build-depends:      base >=4 && < 5,
+                        mtl,
+                        filepath
+    hs-source-dirs:     src
+
+    other-modules:      Aspect
+                        Imports
+                        HaLay
+                        Parsley
+                        Patsy
+                        TypesToKinds
diff --git a/src/Aspect.lhs b/src/Aspect.lhs
new file mode 100644
--- /dev/null
+++ b/src/Aspect.lhs
@@ -0,0 +1,71 @@
+> module Aspect where
+
+> import Prelude hiding (all, minimum)
+> import Control.Applicative
+> import Data.Foldable
+> import Control.Monad
+> import Control.Arrow
+
+> import HaLay
+> import Parsley
+
+> type Higgle = (String, [[Tok]])
+
+> pHiggle :: P Tok Higgle
+> pHiggle = (,) <$ teq (KW "import") <* spc <* teq (Sym "->") <* spc
+>               <*> uid <* spc <*> (outdent <$> pLay "where" pRest)
+
+> higgle :: [Tok] -> ([Higgle], [[Tok]])
+> higgle ts = case parse pHiggle ts of
+>   Just h -> ([h], [])
+>   Nothing -> ([], [ts])
+
+> 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 _ = Nothing
+>   l = skin tss
+>   skin [] = 0
+>   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 _ = Nothing
+
+> dropIn :: [Higgle] -> Int -> String -> [[Tok]]
+> dropIn higs i s = do
+>   (s', tss) <- higs
+>   guard (s == s')
+>   indent i <$> tss
+
+> higOut :: Higgle -> [[Tok]]
+> higOut (s, tss) =
+>   [NL] :
+>   [KW "import", Spc " ", Sym "->", Spc " ", Uid s, Spc " ", KW "where"] :
+>   (indent 2 <$> tss)
+
+> pDent :: P Tok Int
+> pDent = teq NL *> grok spcl next <|> 0 <$ teq NL where
+>   spcl (Spc ss) = Just (length ss)
+>   spcl _ = Nothing
+
+> pPiggle :: P Tok (String, [Tok])
+> pPiggle = (,) <$ teq (KW "import") <* spc <* teq (Sym "<-") <* spc
+>               <*> uid <* spc <*> pRest
+
+> piggle :: [Higgle] -> [[Tok]] -> [[Tok]]
+> piggle higs = mungeLines lp ep where
+>   lp (k : l : tss) = do
+>     i <- parse pDent k
+>     (s, _) <- parse pPiggle l
+>     return $
+>       k : dashOut l : k : dropIn higs i s ++ mungeLines lp ep tss
+>   lp _ = Nothing
+>   ep ts = do
+>     (i, (s, ts)) <- parse ((,) <$> pDent <*> pPiggle) ts
+>     return $
+>       NL : Spc (replicate i ' ') : join (dropIn higs i s)
diff --git a/src/HaLay.lhs b/src/HaLay.lhs
new file mode 100644
--- /dev/null
+++ b/src/HaLay.lhs
@@ -0,0 +1,387 @@
+> {-# LANGUAGE TypeSynonymInstances #-}
+
+> module HaLay where
+
+> import Control.Arrow
+> import Control.Applicative
+> import Data.Char
+> import Data.List
+> import Data.Traversable
+> import Control.Monad
+> import Control.Monad.State
+> import Debug.Trace
+
+> import Parsley
+
+------------------------------------------------------------------------------
+Glom a file like this
+------------------------------------------------------------------------------
+
+> ready :: String -> [[Tok]]
+> ready = map (munge exTyMu) . fst . getLines (Seek NoLay "") [] .
+>         tokenize . (,) 0
+
+------------------------------------------------------------------------------
+Stage 1 : lexing
+------------------------------------------------------------------------------
+
+> tokenize :: (Int, String) -> [(Int, Tok)]
+> tokenize = unfoldr (runStateT ((,) <$> gets fst <*> tokIn))
+
+> data Tok
+>   = Lit String
+>   | Ope BK
+>   | Clo BK
+>   | Uid String
+>   | Lid String
+>   | KW String
+>   | Sym String
+>   | Semi
+>   | Spc String
+>   | Com String
+>   | Urk Char
+>   | NL
+>   | B BK [Tok]          -- a bracket
+>   | L String [[Tok]]    -- some layout
+>   | T Tag [Tok]         -- a tagged region
+>   deriving (Show, Eq)
+
+> 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
+
+> toksOut :: [Tok] -> String
+> toksOut ts = ts >>= tokOut
+> tokssOut :: [[Tok]] -> String
+> tokssOut tss = tss >>= toksOut
+
+> isSpcT :: Tok -> Bool
+> isSpcT (Spc _) = True
+> isSpcT NL      = True
+> isSpcT (Com _) = True
+> isSpcT _       = False
+
+> tokIn :: L Tok
+> tokIn = Lit <$> ((:) <$> ch '\"' <*> slit)
+>     <|> Com <$ stol <*> ((++) <$> traverse ch "#" <*>  spa (not . isNL))
+>     <|> Sym <$>  sym
+>     <|> Com <$> ((++) <$> traverse ch "--" <*>  spa (not . isNL))
+>     <|> Com <$> ((++) <$> traverse ch "{-" <*>  comment 1)
+>     <|> Ope Rnd <$ ch '('
+>     <|> Clo Rnd <$ ch ')'
+>     <|> Ope Sqr <$ ch '['
+>     <|> Clo Sqr <$ ch ']'
+>     <|> Ope Crl <$ ch '{'
+>     <|> Clo Crl <$ ch '}'
+>     <|> Semi <$ ch ';'
+>     <|> Lit <$> ((:) <$> chk isDigit cha <*> spa isDigit)  -- sod FP now
+>     <|> Uid <$> ((:) <$> chk isUpper cha <*> spa isIddy)
+>     <|> klid <$> ((:) <$> chk isLower cha <*> spa isIddy)
+>     <|> Spc  <$> ((:) <$> chk isHSpace cha <*> spa isHSpace)
+>     <|> NL <$ chk isNL cha
+>     <|> Urk <$> cha
+>  where
+>    slit = (:) <$> ch '\\' <*> ((:) <$> cha <*> slit)
+>      <|> return <$> ch '\"'
+>      <|> (:) <$> cha <*> slit
+>    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
+
+------------------------------------------------------------------------
+Stage 2 : Group according to brackets and layout rules
+------------------------------------------------------------------------
+
+> data ChunkMode
+>   = Lay String Int
+>   | Bra BK
+>   | NoLay
+>   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'
+
+> data LineMode
+>   = Bracing
+>   | Seek ChunkMode String
+>   | Edge String Int
+>   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
+
+> 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 (t : ts) = case splendid ts of
+>   (us : sss) -> (t : us) : sss
+
+------------------------------------------------------------------------------
+Stage 3 : tag regions of interest
+------------------------------------------------------------------------------
+
+> data Tag = Ty | Ki | Ex deriving (Show, Eq)
+
+> tender :: Tok -> Bool
+> tender (L _ _ ) = True
+> tender t = elem t [Semi, Sym "=", Sym ",", Sym "|", KW "in"]
+
+> exTyMu :: [Tok] -> Maybe [Tok]
+> exTyMu (t : ts)
+>   | elem t [Sym "::", KW "class", KW "instance"]
+>   = 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?
+>       _ -> t : u : munge exTyMu vs
+>   | elem t [KW "type"]
+>   = Just $ case vs of
+>       Sym "=" : vs -> t : u : Sym "=" : [T Ty (munge tyMu vs)]
+>       _ -> t : u : munge exTyMu vs
+>   where
+>     (u, vs) = first (T Ty . munge tyMu) (span (not . tender) ts)
+> exTyMu _ = Nothing
+
+> tyMu :: [Tok] -> Maybe [Tok]
+> tyMu (Sym "::" : ts) = Just $ Sym "::" : u : munge tyMu vs
+>   where
+>     (u, vs) = first (T Ki . munge kiMu) (span (not . tender) ts)
+> tyMu (B Crl us : ts) = Just $
+>   B Crl [T Ex (munge exTyMu us)] : munge tyMu ts
+> tyMu _ = Nothing
+
+> kiMu :: [Tok] -> Maybe [Tok]
+> kiMu (B Crl us : ts) = Just $
+>   B Crl [T Ty (munge tyMu us)] : munge kiMu ts
+> kiMu (KW "forall" : ts) = case span (/= Sym ".") ts of
+>   (ts, us) -> Just $ KW "forall" : T Ty (munge tyMu ts) : munge kiMu us
+> kiMu _ = Nothing
+
+
+------------------------------------------------------------------------------
+Parsley for layout
+------------------------------------------------------------------------------
+
+> spc :: P Tok ()
+> spc = () <$ many (tok isSpcT)
+
+> uid :: P Tok String
+> uid = grok h next where
+>   h (Uid s) = Just s
+>   h _ = Nothing
+
+> lid :: P Tok String
+> lid = grok h next where
+>   h (Lid s) = Just s
+>   h _ = Nothing
+
+> infC :: P Tok String
+> infC = grok h next where
+>   h (Sym (':' : s)) = Just (':' : s)
+>   h _ = Nothing
+
+> pBr :: BK -> P Tok x -> P Tok x
+> pBr k p = grok pb next where
+>   pb (B j cs) | k == j = parse p cs
+>   pb _ = Nothing
+
+> pLay :: String -> P [Tok] x -> P Tok x
+> pLay k p = grok pb next where
+>   pb (L j tss) | k == j = parse p tss
+>   pb _ = Nothing
+
+> pTag :: Tag -> P Tok x -> P Tok x
+> pTag t p = grok pb next where
+>   pb (T u ts) | t == u = parse p ts
+>   pb _ = Nothing
+
+------------------------------------------------------------------------------
+Mungers
+------------------------------------------------------------------------------
+
+> munge :: ([Tok] -> Maybe [Tok]) -> [Tok] -> [Tok]
+> munge m ts = case m ts of
+>   Just us -> us
+>   Nothing -> case ts of
+>     [] -> []
+>     (B b ss : ts) -> B b (munge m ss) : munge m ts
+>     (L k sss : ts) -> L k (map (munge m) sss) : munge m ts
+>     (T t ss : ts) -> T t (munge m ss) : munge m ts
+>     (t : ts) -> t : munge m ts
+
+> mungeLines :: ([[Tok]] -> Maybe [[Tok]]) -> ([Tok] -> Maybe [Tok]) ->
+>               [[Tok]] -> [[Tok]]
+> mungeLines ms m tss = case ms tss of
+>     Just uss -> uss
+>     Nothing -> case tss of
+>       [] -> []
+>       (ts : tss) -> munge help ts : mungeLines ms m tss
+>   where
+>     help ts = m ts <|>
+>       case ts of
+>         (L k sss : ts) -> Just (L k (mungeLines ms m sss) : munge help ts)
+>         _ -> Nothing
+
+> dashOut :: [Tok] -> [Tok]
+> dashOut ts = [Com ("-- " ++ easy ts)] where
+>   easy [] = []
+>   easy (B _ _ : _) = []
+>   easy (L _ _ : _) = []
+>   easy (t : ts) = tokOut t ++ easy ts
+
+> dental :: [[Tok]] -> [Tok]
+> dental [] = [NL]
+> 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 (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) =
+>   redent l ls ++ ms
+> preamble ls (m : ms) = m : preamble ls ms
+
+
+------------------------------------------------------------------------------
+Classifiers, odds and ends
+------------------------------------------------------------------------------
+
+> isNL :: Char -> Bool
+> isNL b = elem b "\r\n"
+
+> isHSpace :: Char -> Bool
+> isHSpace c = isSpace c && not (isNL c)
+
+> isIddy :: Char -> Bool
+> isIddy b = isAlphaNum b || elem b "_'"
+
+> isInfy :: Char -> Bool
+> isInfy b = elem b "!#$%&*+-.:/<=>?@\\^|~"
+
+> data BK = Rnd | Sqr | Crl deriving (Show, Eq)
+
+> ope :: BK -> String
+> ope Rnd = "("
+> ope Sqr = "["
+> ope Crl = "{"
+
+> clo :: BK -> String
+> clo Rnd = ")"
+> clo Sqr = "]"
+> clo Crl = "}"
+
+> keywords :: [String]
+> keywords = ["module", "import", "type", "data", "newtype", "pattern", "kind",
+>             "let", "in", "case", "of", "do", "forall", "class", "instance",
+>             "family", "where", "if", "then", "else"]
+
+> lakeys :: [String]
+> lakeys = ["let", "of", "do", "where"]
+
+> width :: [Tok] -> Int
+> width ts = case span (/= NL) ts of
+>   (ts, []) -> length (ts >>= tokOut)
+>   (_, NL : ts) -> width ts
+
+------------------------------------------------------------------------
+The lexer monad
+------------------------------------------------------------------------
+
+> type L = StateT (Int, String) Maybe
+
+> instance Alternative L where
+>   empty = StateT $ \ is -> empty
+>   p <|> q = StateT $ \ is -> runStateT p is <|> runStateT q is
+
+> instance Applicative L where
+>   pure = return
+>   (<*>) = ap
+
+> 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))
+
+> stol :: L ()
+> stol = do
+>   i <- gets fst
+>   guard (i == 0)
+
+> chk :: (t -> Bool) -> L t -> L t
+> chk p l = do t <- l ; if p t then return t else empty
+
+> ch :: Char -> L Char
+> ch c = chk (== c) cha
+
+> spa :: (Char -> Bool) -> L String
+> spa p = (:) <$> chk p cha <*> spa p  <|> pure []
+
+> sym :: L String
+> sym = StateT $ \ (i, s) -> case h s of
+>   ("", _) -> Nothing
+>   ("--", _) -> Nothing
+>   (s, t) -> Just (s, (i + length s, t))
+>  where
+>   h (s@('-':'}':_)) = ("", s)
+>   h (c : s) | isInfy c = first (c :) (h s)
+>   h s = ([], s)
diff --git a/src/Imports.lhs b/src/Imports.lhs
new file mode 100644
--- /dev/null
+++ b/src/Imports.lhs
@@ -0,0 +1,30 @@
+> module Imports where
+
+> import Control.Applicative
+> import System.IO.Error
+> import System.FilePath
+> import Data.Foldable
+> import Data.Monoid
+
+> import HaLay
+> import Parsley
+
+> tryReadFile :: FilePath -> IO String
+> tryReadFile s = catch (readFile s) $ \ e ->
+>  if isDoesNotExistError e then return "" else ioError e
+
+> pImport :: P Tok [String]
+> pImport = teq (KW "import") *> spc *> pSep (teq (Sym ".")) uid <* pRest
+
+> grokImports :: [Tok] -> [[FilePath]]
+> grokImports cs = foldMap pure $ parse pImport cs
+
+> getHers :: [String] -> IO [[Tok]]
+> getHers p = ready <$>  tryReadFile (joinPath p <.> "hers")
+
+> storySoFar :: [[Tok]] -> IO [[Tok]]
+> storySoFar hs = foldMap getHers (hs >>= grokImports)
+
+> instance Monoid x => Monoid (IO x) where
+>   mempty = pure mempty
+>   mappend x y = mappend <$> x <*> y
diff --git a/src/Main.lhs b/src/Main.lhs
new file mode 100644
--- /dev/null
+++ b/src/Main.lhs
@@ -0,0 +1,49 @@
+> module Main where
+
+> import System.Environment
+> import System.FilePath
+> import Data.Char
+> import Data.Traversable
+> import Data.Foldable
+
+> import HaLay
+> import Imports
+> import Aspect
+> import Patsy
+> import TypesToKinds
+
+> sheGoes :: [[Tok]] -> [[Tok]] -> ([[Tok]], [[Tok]])
+> sheGoes hersi0 hs0 =
+>   let nl = dental hs0
+>       (higs0, hersi1) = foldMap higgle hersi0
+>       (higs1, hs1) = foldMap higgle hs0
+>       higs = higs0 ++ higs1
+>       herso0 = higs >>= higOut
+>       hs2 = piggle higs hs1
+>       ((ps0, herso1), _) = traverse getPatsy hersi1
+>       ((ps1, herso2), hs3) = traverse getPatsy hs2
+>       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)
+
+> hsAndHers :: String -> IO (String, String)
+> hsAndHers s = do
+>   let ihs = ready s
+>   pcs <- storySoFar ihs
+>   let (hers, hs) = sheGoes pcs ihs
+>   return (tokssOut hs, tokssOut hers)
+
+> main :: IO ()
+> main = do
+>   x : y : z : _ <- getArgs
+>   let x' = replaceExtension x ".hers"
+>   putStrLn x
+>   putStrLn y
+>   putStrLn z
+>   f <- readFile y
+>   (f', h) <- hsAndHers f
+>   writeFile x' h
+>   writeFile z f'
+
diff --git a/src/Makefile b/src/Makefile
new file mode 100644
--- /dev/null
+++ b/src/Makefile
@@ -0,0 +1,7 @@
+default: she
+
+she: Main.lhs Parsley.lhs Patsy.lhs TypesToKinds.lhs HaLay.lhs Imports.lhs Aspect.lhs
+	ghc --make Main -o she
+
+install: she
+	sudo cp she /usr/local/bin/
diff --git a/src/Parsley.lhs b/src/Parsley.lhs
new file mode 100644
--- /dev/null
+++ b/src/Parsley.lhs
@@ -0,0 +1,81 @@
+> module Parsley where
+
+> import Data.Char
+> import Control.Applicative
+> import Control.Monad
+> import Control.Monad.State
+
+> (<*^) :: Applicative f => f (a -> b) -> a -> f b
+> f <*^ s = f <*> pure s
+
+> newtype P t x = P {runP :: [t] -> Maybe ([t], x, [t])}
+
+> instance Monad (P t) where
+>   return x = P $ \ ts -> Just ([], x, ts)
+>   P s >>= f = P $ \ts -> do
+>     (sts, s', ts) <- s ts
+>     (tts, t', ts) <- runP (f s') ts
+>     return (sts ++ tts, t', ts)
+
+> parse :: P t x -> [t] -> Maybe x
+> parse p ts = case runP p ts of
+>   Just (_, x, []) -> Just x
+>   _ -> Nothing
+
+> instance Functor (P t) where
+>   fmap = ap . return
+
+> instance Applicative (P t) where
+>   pure = return
+>   (<*>) = ap
+
+> instance Alternative (P t) where
+>   empty = P $ \ _ -> Nothing
+>   p <|> q = P $ \ ts -> runP p ts <|> runP q ts
+
+> pRest :: P t [t]
+> pRest = P $ \ ts -> Just (ts, ts, [])
+
+> pEnd :: P t ()
+> pEnd = P $ \ ts -> if null ts then Just ([], (), []) else Nothing
+
+> next :: P t t
+> next = P $ \ ts -> case ts of
+>   [] -> Nothing
+>   (t : ts) -> Just ([t], t, ts)
+
+> pExt :: P t x -> P t ([t], x)
+> pExt (P x) = P $ \ ts -> do
+>   (xts, x', ts) <- x ts
+>   return (xts, (xts, x'), ts)
+
+> pOpt :: P t x -> P t (Maybe x)
+> pOpt p = Just <$> p <|> pure Nothing
+
+>{-
+> pPlus :: P t x -> P t [x]
+> pPlus p = (:) <$> p <*> pStar p
+
+> pStar :: P t x -> P t [x]
+> pStar p = pPlus p <|> pure []
+> -}
+
+> pSep :: P t s -> P t x -> P t [x]
+> pSep s p = (:) <$> p <*> many (s *> p) <|> pure []
+
+> grok :: (a -> Maybe b) -> P t a -> P t b
+> grok f p = do
+>   a <- p
+>   case f a of
+>     Just b -> return b
+>     Nothing -> empty
+
+> ok :: (a -> Bool) -> a -> Maybe a
+> ok p a = guard (p a) >> return a
+
+> tok :: (t -> Bool) -> P t t
+> tok p = grok (ok p) next
+
+> teq :: Eq t => t -> P t ()
+> teq t = tok (== t) *> pure ()
+
diff --git a/src/Patsy.lhs b/src/Patsy.lhs
new file mode 100644
--- /dev/null
+++ b/src/Patsy.lhs
@@ -0,0 +1,115 @@
+> module Patsy where
+
+> import Data.Char
+> import Data.List
+> import Control.Applicative
+
+> import Parsley
+> import HaLay
+
+> type Patsy = (String, ([String], [Tok]))
+
+> pPatsy :: P Tok Patsy
+> pPatsy = teq (KW "pattern") *> spc *>
+>   ((,) <$> uid
+>        <*> ((,) <$> many (spc *> lid) <* (spc <* teq (Sym "=") <* spc)
+>                 <*> pRest))
+
+> getPatsy :: [Tok] -> (([Patsy], [[Tok]]), [Tok])
+> getPatsy cs = case parse pPatsy cs of
+>   Just p -> (([p], [cs,[NL]]), jigger p)
+>   _      -> (([], []), cs)
+
+> jigger :: Patsy -> [Tok]
+> jigger (s, (as, cs)) =
+>   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 (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
+>   recs _ [] = []
+>   recs False (Sym "=" : cs) = Sym "=" : recs True cs
+>   recs True (Sym "," : cs) = Sym "," : recs False cs
+>   recs False (c : cs) = c : recs False cs
+>   recs True (c : cs) = subst xcs c : recs True cs
+> subst xcs c = c
+
+> args :: [Patsy] -> [String] -> [Tok] ->
+>         ([(String, Tok)], [String], [Tok])
+> args ps [] cs = ([], [], cs)
+> args ps xs [] = ([], xs, [])
+> args ps xs (c : cs) | isSpcT c = args ps xs cs
+> args ps (x : xs) (Lid a : Sym "@" : B Rnd cs : ds) =
+>   let (xcs, ys, cs') = args ps xs ds
+>   in  ((x, B Rnd [Lid a, Sym "@", B Rnd (processes ps cs)]) : xcs, ys, cs')
+> args ps (x : xs) (c : cs) = case process ps c of
+>   Just c' -> let (xcs, ys, cs') = args ps xs cs in ((x, c') : xcs, ys, cs')
+>   _ -> ([], x : xs, c : cs)
+
+> abstract :: [String] -> [Tok] -> Tok
+> abstract [] [Lid y] = Lid y
+> abstract [] cs =  B Rnd cs
+> abstract xs cs =  B Rnd $
+>     [Sym "\\", Spc " "] ++
+>     concat [[Lid x, Spc " "] | x <- xs] ++
+>     [Sym "->", Spc " "] ++ cs
+
+> 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)
+>   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)
+> process ps (Lit s) = Just (Lit s)
+> process ps c = Nothing
+
+> processes :: [Patsy] -> [Tok] -> [Tok]
+> processes ps = munge big where
+>   big (Uid c : cs) = case lookup c ps of
+>     Just (xs, bs) ->
+>       let (xcs, ys, ds) = args ps xs cs
+>       in  Just $ abstract ys (map (subst xcs) bs) : munge big ds
+>     _ -> Nothing
+>   big (Lid l : cs) = Just $ Lid l : wee cs
+>   big (B b cs : ds) = Just $ B b (munge big cs) : wee ds
+>   big (T Ty cs : ds) = Just $ T Ty (munge off cs) : munge big ds
+>   big _ = Nothing
+>   wee [] = []
+>   wee (c : cs) | isSpcT c = c : wee cs
+>   wee (c : cs) = case process ps c of
+>     Just c' -> c' : wee cs
+>     Nothing -> munge big (c : cs)
+>   off (T Ex cs : ds) = Just $ T Ex (munge big cs) : munge off ds
+>   off _ = Nothing
+
+> freeCons :: Tok -> [String]
+> freeCons (Uid s) = [s]
+> freeCons (B _ cs) = nub (cs >>= freeCons)
+> freeCons _ = []
+
+> topSort :: Eq x => (y -> [x]) -> [(x, y)] -> Maybe [(x, y)]
+> topSort fr [] = Just []
+> topSort fr (xy : xys) =
+>   do xys <- topSort fr xys
+>      topInsert xy xys
+>   where
+>     topInsert (x, y) xys@(h@(_, y') : t)
+>       | any ((`elem` (fr y)) . fst) xys
+>       = if elem x (fr y') then Nothing else (h :) <$> topInsert (x, y) t
+>     topInsert xy xys = Just (xy : xys)
+
+> prep1 :: [Patsy] -> Patsy -> [Patsy]
+> prep1 ps (p, (xs, cs)) = (p, (xs, processes ps cs)) : ps
+
+> prepare :: [Patsy] -> Maybe [Patsy]
+> prepare ps0 = do
+>   ps1 <- topSort ((>>= freeCons) . snd) ps0
+>   return $ foldl prep1 [] ps1
+
diff --git a/src/TypesToKinds.lhs b/src/TypesToKinds.lhs
new file mode 100644
--- /dev/null
+++ b/src/TypesToKinds.lhs
@@ -0,0 +1,85 @@
+> module TypesToKinds where
+
+> import Control.Applicative
+
+> import HaLay
+> import Parsley
+
+> dataGrok :: [Tok] -> [[Tok]]
+> dataGrok cs@(KW "newtype" : T Ty _ : ds)
+>    = map blat (fillet ds)
+> dataGrok cs@(KW "data" : T Ty _ : ds)
+>    = map blat (fillet ds)
+> dataGrok cs = []
+
+> 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)]))
+
+> fillet :: [Tok] -> [(Tok, Int)]
+> fillet [] = []
+> fillet (Sym "=" : [T Ty cs]) =
+>   case parse (pSep (spc *> teq (Sym "|")) (spc *> pOldSyn)) cs of
+>     Just sis -> sis
+>     _ -> []
+> fillet (L "where" css : _)     = css >>= gadtSyn
+> fillet (_ : cs) = fillet cs
+
+> pOldSyn :: P Tok (Tok, Int)
+> pOldSyn = (\s -> (jig s, 2)) <$ pArg <*> infC <* pArg
+>       <|> (,) <$> pCId
+>               <*> (length <$> many pArg <|> pBr Crl pFields)
+>               <* spc
+
+> jig :: String -> Tok
+> jig s = (B Rnd [Sym (":$#$#$#" ++ s)])
+
+> pArg :: P Tok ()
+> pArg = spc <* (
+>   () <$ lid <|>
+>   () <$ uid <|>
+>   pBr Rnd (() <$ pRest) <|>
+>   pBr Sqr (() <$ pRest) <|>
+>   teq (Sym "!") *> pArg
+>   )
+
+> pFields :: P Tok Int
+> pFields = 0 <$ pEnd <|> (1 +) <$ lid <*> pFields <|> next *> pFields
+
+> gadtSyn :: [Tok] -> [(Tok, Int)]
+> gadtSyn cs = case parse pGDecl cs of
+>   Just (ss, i) -> map (flip (,) i) ss
+>   _ -> []
+
+> pGDecl :: P Tok ([Tok], Int)
+> pGDecl = (,) <$> pSep (spc *> teq (Sym ",")) pCId <* spc <* teq (Sym "::")
+>              <*> pTag Ty pArity <* pRest
+
+> pCId :: P Tok Tok
+> pCId = Uid <$> (("SheTy" ++) <$> uid)
+>    <|> jig <$> pBr Rnd (spc *> infC <* spc)
+
+> pArity :: P Tok Int
+> pArity = 0 <$ pEnd
+>      <|> (1 +) <$ teq (Sym "->") <*> pArity
+>      <|> next *> pArity
+
+> 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 _ = Nothing
+
+> ttkMu :: [Tok] -> Maybe [Tok]
+> ttkMu (T Ty us : ts) = Just $ T Ty (munge tyTTK us) : munge ttkMu ts
+> ttkMu _ = Nothing
+
+> exTTK :: [Tok] -> Maybe [Tok]
+> 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)