diff --git a/Check.lhs b/Check.lhs
new file mode 100644
--- /dev/null
+++ b/Check.lhs
@@ -0,0 +1,214 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators, KindSignatures, GADTs, TypeSynonymInstances,
+>     FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections,
+>     MultiParamTypeClasses #-}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> module Check where
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> import Prelude hiding (elem, all)
+> import Data.Char
+> import Data.List hiding (elem, all)
+> import Data.Monoid
+> import Data.Foldable
+> import Data.Traversable
+> import Control.Applicative
+> import Control.Monad
+> import Control.Newtype
+> import Data.Void
+
+> import Gubbins
+> import Types
+> import Pa
+> import Syntax
+> import Template
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% TError                                                             %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> data TError
+>   = TMissing UpId
+>   | SMissing UpId
+>   | TArity UpId Int [VT]
+>   | SArity UpId Int [VT]
+>   | BadTemplate
+>   | Cockup String
+>   | AmbiguousPats [Pat]
+>   | AmbiguousRaws [Raw]
+>   | BadPat VT Pat
+>   | NoConstructor VT Template
+>   | AppliedPVar String
+>   | RepeatedPVar Template
+>   | PatArityError Template
+>   | RawArityError Template
+>   | BadLhs [Pat]
+>   | UnifyVFail VT VT
+>   | UnifyCFail CT CT
+>   | UnifySFail Sig Sig
+>   | BadBunk
+>   | Useless VT
+>   | CheckR VT Raw
+>   | CantDo Sig [Sig]
+>   | AmbiguousOp Template [Sig]
+>   | ThunkMismatch CT ([Pat], Raw)
+>   | BadMessPat [Pat]
+>   | GuessThunk [([Pat], Raw)]
+>   | BadHandlerType VT
+>   | SynCon
+>   | Line ([Pat], Raw) TError
+>   | Raw VT Raw TError
+>   | Dunno Template [Sig] [Template]
+>   deriving Show
+
+> type Moan = TError :>>: Void
+> type Moaning = Free Moan
+
+> moan :: TError -> Moaning x
+> moan e = com (e :? absurd)
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% checking top level data, signature and function declarations       %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> data TypeInfo = TypeInfo
+>   {  dataDecls  :: [(UpId, (Int, [(Template, [VT])]))]
+>   ,  sigDecls   :: [(UpId, (Int, [(Template, ([VT], VT))]))]
+>   ,  funDecls   :: [(Template, (Int, [VT], [Sig], VT))]
+>   ,  templateT  :: TemplateTable
+>   }  deriving Show
+
+> typeInfo :: Source -> Moaning TypeInfo
+> typeInfo src = do
+>   let dt (n, (xs, cs)) =
+>         (| ~n, (| ~(length xs), traverse (conTemplate src xs) cs|)|)
+>       sg (n, (xs, os)) = (| ~n, (| ~(length xs), traverse oper os|)|) where
+>         oper (vs, v) = (|rass (conTemplate src xs vs) (tScope src xs v)|)
+>         rass (a, b) c = (a, (b, c))
+>       fn stuf@(vs, (ss, v)) = do
+>         let xs = ftvs src stuf
+>         (t, vs') <- conTemplate src xs vs
+>         ss' <- tScope src xs ss
+>         v' <- tScope src xs v
+>         return (t, (length xs, vs', ss', v'))
+>   ds <- (| ~ primitiveTypes ++ traverse dt (sourceData src) |)
+>   ss <- (| ~ primitiveSigs ++ traverse sg (sourceSigs src) |)
+>   fs <- (| ~primitiveFunDecls ++ traverse fn (sourceDecl src) |)
+>   let ts = (| fst (|(snd . snd) ds @ |)
+>             | fst (|(snd . snd) ss @ |)
+>             | fst fs
+>             |)
+>   return $ TypeInfo ds ss fs (TemplateTable ts [] [])
+
+> ftvs :: TMang t => Source -> t -> [UpId]
+> ftvs src = ala' UnionList (ala' Const tMang) (var chk mempty mempty)
+>   where chk u = maybe (maybe [u] (const []) (lookup u primitiveTypes))
+>            (const []) (lookup u (sourceData src))
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% generating a template and domains from a declaration               %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> conTemplate ::  Source -> [UpId] -> [Lump] -> Moaning (Template, [VT])
+> conTemplate src xs vs = do
+>   (bs, us) <- go vs
+>   (|tmp bs, ~us|)
+>   where
+>     go [] = return ([], [])
+>     go (LTy v : vs) = do
+>       u <- tScope src xs v
+>       (bs, us) <- go vs
+>       return (Place : bs, u : us)
+>     go (LNm n : vs) = do
+>       (bs, us) <- go vs
+>       return (Mark n : bs, us)
+>     tmp [] = moan $ BadTemplate
+>     tmp (Mark n : bs) | all place bs = (|[Mark n]|)
+>     tmp bs = (|id (post bs)|)
+>     post [] = (|[]|)
+>     post (Place : Place : bs) = moan $ BadTemplate
+>     post (b : bs) = (| ~b : post bs|)
+>     place Place = True
+>     place _ = False
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% type scope and arity checking                                      %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> class TScope x where
+>   tScope :: Source -> [UpId] -> x -> Moaning x
+
+> instance TScope x => TScope [x] where
+>   tScope src xs = traverse (tScope src xs)
+
+> instance TScope VT where
+>   tScope src xs (D x []) | Just i <- findIndex (==x) xs = return (X i)
+>   tScope src xs (D x vs) = do
+>     a <- maybe
+>            (maybe (moan $ TMissing x) (return . fst) (lookup x primitiveTypes))
+>            (return . length . fst) $
+>          lookup x (sourceData src)
+>     if a == length vs
+>       then (|(D x) (tScope src xs vs)|)
+>       else moan $ TArity x a vs
+>   tScope src xs (M os ss v) =
+>     (|M (tScope src xs os) (tScope src xs ss) (tScope src xs v)|)
+>   tScope src xs Un = return Un
+>   tScope src xs Ze = return Ze
+>   tScope src xs (U c) = (|U (tScope src xs c)|)
+>   tScope src xs (X _) = moan $ Cockup "X already?"
+>   tScope src xs (Q _) = moan $ Cockup "Q already?"
+
+> instance TScope CT where
+>   tScope src xs (v :-> c)  = (|tScope src xs v :-> tScope src xs c|)
+>   tScope src xs (F ss v)   = (|F (tScope src xs ss) (tScope src xs v)|)
+
+> instance TScope Sig where
+>   tScope src xs (s :$ vs) = do
+>     a <- maybe (maybe (moan $ SMissing s)
+>             (pure . fst) (lookup s primitiveSigs))
+>           (pure . length . fst) $
+>           lookup s (sourceSigs src)
+>     if a == length vs
+>       then (| ~s :$ tScope src xs vs|)
+>       else moan $ SArity s a vs
+>   tScope src xs Pure = (|Pure|)
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% prmimitives                                                        %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> primitiveTypes :: [(UpId, (Int, [(Template, [VT])]))]
+> primitiveTypes =
+>   [  (Up "Char", (0, []))
+>   ,  (Up "Bool", (0, [([Mark "tt"], []), ([Mark "ff"], [])]))
+>   ]
+
+> char :: VT
+> char = D (Up "Char") []
+
+> bool :: VT
+> bool = D (Up "Bool") []
+
+> primitiveFunDecls :: [(Template, (Int, [VT], [Sig], VT))]
+> primitiveFunDecls =
+>   [  ([Place, Mark "=Char=", Place], (0, [char, char], [], bool))
+>   ]
+
+> primitiveSigs :: [(UpId, (Int, [(Template, ([VT], VT))]))]
+> primitiveSigs =
+>   [  (Up "Console", (0,
+>      [  ([Mark "inch"], ([], char))
+>      ,  ([Mark "ouch"], ([char], Un))
+>      ]))
+>   ]
diff --git a/Elab.lhs b/Elab.lhs
new file mode 100644
--- /dev/null
+++ b/Elab.lhs
@@ -0,0 +1,388 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators, GADTs, TypeSynonymInstances, KindSignatures,
+>     FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections,
+>     MultiParamTypeClasses #-}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> module Elab where
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> import Debug.Trace
+
+> import Prelude hiding (elem, all, foldr, concat)
+> import Data.Char
+> import Data.List hiding (elem, all, foldr, concat)
+> import Data.Monoid
+> import Data.Foldable
+> import Data.Traversable
+> import Control.Applicative
+> import Control.Monad
+> import Control.Newtype
+> import Control.Arrow
+> import Data.Void
+
+> import Gubbins
+> import Types
+> import Pa
+> import Syntax
+> import ElabMonad
+> import Unify
+> import Template
+> import Check
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Cooked Terms                                                       %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> data PAT
+>   = PV String
+>   | PC Template [PAT]      -- void pattern is |PC [] []|
+>   | PL Char                -- char literal
+>   | PR PAT
+>   | PO Template [PAT] PAT  -- op params continuation
+
+> instance Show PAT where
+>   show (PV x) = x
+>   show (PC t ps) = tempShow t (map show ps)
+>   show (PR p) = "[" ++ show p ++ "]"
+>   show (PO t ps p) =
+>     "[" ++ tempShow t (map show ps) ++ " ? " ++ show p ++ "]"
+
+> data Dir
+>   = CHK
+>   | SYN
+
+> data TM :: {Dir} -> * where
+>   H     :: HD                      -> TM {SYN}
+>   (:/)  :: TM {SYN} -> [TM {CHK}]  -> TM {SYN}
+>   PApp  :: TM {SYN} -> [TM {CHK}]  -> TM {SYN}
+>   HAN   :: TM {SYN} -> TM {CHK}    -> TM {SYN}
+>
+>   E     :: TM {SYN}                -> TM {CHK}
+>   CL    :: Char                    -> TM {CHK}
+>   CN    :: Template -> [TM {CHK}]  -> TM {CHK}
+>   BUNK  :: TM {CHK}                -> TM {CHK}
+>   LAM   :: [([PAT], TM {CHK})]     -> TM {CHK}
+
+> data HD  = VA Int
+>          | FN Template  -- cache the def like a Birdman?
+>          | OP Template
+
+> hTemp :: Bwd Entry -> HD -> Template
+> hTemp g (VA i)  = fst (inx g i)
+> hTemp g (FN f)  = f
+> hTemp g (OP o)  = o
+
+> gShow :: Bwd Entry -> TM {d} -> String
+> gShow g (H h)           = tempShow x ["_" | Place <- x] where x = hTemp g h
+> gShow g (f :/ [])       = gShow g f ++ " !"
+> gShow g (H h :/ ts)     = tempShow (hTemp g h) (map (gShow g) ts)
+> gShow g (f :/ ts)       = "(" ++ show f ++ (ts >>= ((' ' :) . show)) ++ ")"
+> gShow g (PApp f ts)     = "(" ++ show f ++ (ts >>= ((' ' :) . show)) ++ ")"
+> gShow g (HAN h e)       = "(" ++ gShow g h ++ "?" ++ gShow g e ++ ")"
+> gShow g (E t)           = gShow g t
+> gShow g (CN c ts)       = tempShow c (map (gShow g) ts)
+> gShow g (BUNK t)        = "(" ++ gShow g t ++ " {})"
+> gShow g (LAM (a : as))  =
+>   "{" ++ lShow a ++ (as >>= ((" | " ++) . lShow)) ++ "}" where
+>     lShow ([], t) = gShow g t
+>     lShow (ps, t) =
+>       intercalate " " (map show ps) ++ " -> " ++ gShow (patOn g ps) t
+>     patOn g []               = g
+>     patOn g (PV x : ps)      = patOn (bind g x) ps
+>     patOn g (PC _ ps : ps')  = patOn (patOn g ps) ps'
+>     bind g x = g :< ([Mark x] ::: (0, Un))  -- cheeky!
+
+> inx :: Bwd Entry -> Int -> (Template, (Int, VT))
+> inx (_ :< (x ::: (i, j)))  0 = (x, (i, j))
+> inx (g :< (_ ::: _))       i = inx g (i - 1)
+> inx (g :< _)               i = inx g i
+> inx B0                     i = ([Mark ('#' : show i)], (0, Un))
+
+> instance Show (TM {d}) where
+>   show t = gShow B0 t
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Type Checking and Synthesis                                        %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> checkR :: VT -> Raw -> ElabM (TM {CHK})
+> --checkR v r | trace ("checkR " ++ show (v, r)) $ False = undefined
+> checkR v r = hnf v >>= \ v -> err (Raw v r) $ case r of
+>   RVd      -> (|(CN [] []) (-Un =?= v-)|)
+>   RCh c    -> (|(CL c) (-char =?= v-)|)
+>   RTh prs  -> case v of
+>     U c -> (|LAM (traverse (body c) prs)|)
+>     _ -> moanE $ GuessThunk prs
+>   RN n     -> checkR v (RA [RN n])
+>   RBunk    -> moanE BadBunk
+>   RA rs    -> (|ttrCh ~v (|rawTree ~rs ~[] @ |) @ |)
+>   RQ h e   -> do
+>     ss <- getSigsE
+>     (h, z) <- synR h
+>     z <- hnf z
+>     case z of
+>       U (M hs is u :-> F os w) -> do
+>         w =?= v
+>         canDo os
+>         e <- withSigs (sAct hs ss) $ do
+>           canDo is
+>           checkR u e
+>         (|(E (HAN h e))|)
+>       _ -> moanE $ BadHandlerType z
+>   r        -> synR r >>= want v
+
+> synR :: Raw -> ElabM (TM {SYN}, VT)
+> --synR r | trace ("synR " ++ show r) $ False = undefined
+> synR (RN n)     = synR (RA [RN n])
+> synR RVd        = moanE SynCon
+> synR RBunk      = moanE BadBunk
+> synR (RA rs)    = rawTree rs [] >>= \ t -> case t of
+>   TNode f ts -> appSyn f ts
+>   TLeaf r ts -> synR r >>= \ tv -> mention tv ts
+> synR (RTh prs)  = moanE $ GuessThunk prs
+> synR (RQ h e)   = do
+>   ss <- getSigsE
+>   (h, v) <- synR h
+>   v <- hnf v
+>   case v of
+>     U (M hs is u :-> F os w) -> do
+>       canDo os
+>       e <- withSigs (sAct hs ss) $ do
+>         canDo is
+>         checkR u e
+>       (|(HAN h e, w)|)
+>     _ -> moanE $ BadHandlerType v
+
+> isBunk :: TTree Raw -> Bool
+> isBunk (TLeaf RBunk []) = True
+> isBunk _ = False
+
+> ttrCh :: VT -> (TTree Raw) -> ElabM (TM {CHK})
+> --ttrCh v t | trace ("ttrCh " ++ show (v, t)) $ False = undefined
+> ttrCh v (TNode f ts) = if (not (null ts) && isBunk (last ts))
+>   then (|BUNK (ttrCh Ze (TNode f (init ts)))|) else do
+>   info <- getInfoE
+>   (g, _) <- getCxE
+>   let constrs = [ (c, ((u, i), vs))
+>                 | (u, (i , cs)) <- dataDecls info
+>                 , (c, vs) <- cs
+>                 ]
+>   v <- hnf v
+>   case v of
+>     D u vs -> case lookup u (dataDecls info) of
+>       Nothing -> moanE $ TMissing u
+>       Just (i, cs) -> case lookup f cs of
+>         Just ws -> (|(CN f) (ttrsCh f (xsub vs ws) ts)|)
+>         Nothing -> appSyn f ts >>= want v
+>     Q _ -> case (gFetch g f, filter ((f ==) . fst) constrs) of
+>       (Nothing, [(_, ((u, m), vs))]) -> do
+>         ws <- fresh m
+>         ts <- ttrsCh f (xsub ws vs) ts
+>         D u ws =?= v
+>         (|(CN f ts)|)
+>       _ -> appSyn f ts >>= want v
+>     _ -> appSyn f ts >>= want v
+> ttrCh v (TLeaf r []) = checkR v r
+> ttrCh v _ = moanE $ Cockup "oops"
+
+> want :: VT -> (TM {SYN}, VT) -> ElabM (TM {CHK})
+> want v (t, u) = (|(E t) (-u =?= v-)|)
+
+> getOps :: [Sig] -> ElabM [(Template, ([VT], (Sig, VT)))]
+> getOps [] = return []
+> getOps (Pure : _) = return []
+> getOps (s@(u :$ vs) : ss) = do
+>   info <- getInfoE
+>   (| ~[  (ot, xsub vs (ois, (s, oo)))
+>       |  (u', (i, os)) <- sigDecls info, u == u'
+>       ,  (ot, (ois, oo)) <- os
+>       ] ++ getOps ss |)
+
+> mkOpType :: [Sig] -> ([VT], (Sig, VT)) -> VT
+> mkOpType ss (vs, (s, v)) = sAct (U (foldr (:->) (F [s] v) vs)) ss
+
+> appSyn :: Template -> [TTree Raw] -> ElabM (TM {SYN}, VT)
+> --appSyn f ts | trace ("appSyn " ++ show (f, ts)) $ False = undefined
+> appSyn f ts = do
+>   info <- getInfoE
+>   sigs <- getSigsE
+>   ops <-  (|(map (id *** mkOpType sigs)) (getOps sigs)|)
+>   (g, _) <- getCxE
+>   case gFetch g f of
+>     Just (i, (m, v)) -> do
+>       ws <- fresh m
+>       let v' = xsub ws v
+>       --False <- trace ("FOUND: " ++ show f ++ " : " ++ show v') $
+>       --  return False
+>       mention (H (VA i), xsub ws v) ts
+>     Nothing -> case [v | (f', v) <- ops, f == f'] of
+>       (_:_:_) -> moanE $ AmbiguousOp f sigs
+>       [v] -> mention (H (OP f), v) ts
+>       [] -> case lookup f (funDecls info) of
+>         Just (m, vs, sa, v) -> do
+>           ws <- fresh m
+>           mention  (H (FN f),
+>                     sAct (xsub ws (U (foldr (:->) (F sa v) vs))) sigs)
+>                    ts
+>         Nothing -> moanE $ Dunno f sigs (foldMap gnom g)
+
+> gnom :: Entry -> [Template]
+> gnom (x ::: _) = [x]
+> gnom _ = []
+
+> mention :: (TM {SYN}, VT) -> [TTree Raw] -> ElabM (TM {SYN}, VT)
+> mention tv        []  = return tv
+> mention (t, U c)  ts  = use t [] c ts
+> mention (t, v)    ts  = moanE $ Useless v
+
+> use :: TM {SYN} -> [TM {CHK}] -> CT -> [TTree Raw] -> ElabM (TM {SYN}, VT)
+> use f [] (F ss v) (TLeaf RBang [] : ts) = do
+>   canDo ss
+>   mention (f :/ [], v) ts
+> use f as (F ss v) ts = do
+>   canDo ss
+>   mention (f :/ as, v) ts
+> use f as (v :-> c) (t : ts) = do
+>   a <- ttrCh v t
+>   use f (as ++ [a]) c  ts
+> use f as c [] = (|(PApp f as, U c)|)
+
+> canDo :: [Sig] -> ElabM ()
+> canDo [] = return ()
+> canDo (s : ss) = do
+>   ss' <- getSigsE
+>   findSig s ss' ss'
+>   canDo ss
+
+> findSig :: Sig -> [Sig] -> [Sig] -> ElabM ()
+> findSig s [] sd = moanE $ CantDo s sd
+> findSig s@(a :$ us) ((b :$ vs) : ss) sd
+>   | a == b = us =?= vs
+>   | otherwise = findSig s ss sd
+
+> gFetch :: Bwd Entry -> Template -> Maybe (Int, (Int, VT))
+> gFetch B0 _ = Nothing
+> gFetch (g :< (x ::: r)) y
+>   | x == y = Just (0, r)
+>   | otherwise = (|((1 +) *** id) (gFetch g y)|)
+> gFetch (g :< _) y = gFetch g y
+
+> fresh :: Int -> ElabM [VT]
+> fresh m = do
+>     (g, n) <- getCxE
+>     setCxE (grow g n m)
+>     return (map Q (take m [n ..]))
+>   where
+>     grow g n 0 = (g, n)
+>     grow g n m = grow (g :< (n :=? Nothing)) (n + 1) (m - 1)
+
+> ttrsCh :: Template -> [VT] -> [TTree Raw] -> ElabM [TM {CHK}]
+> ttrsCh f [] [] = return []
+> ttrsCh f (v : vs) (t : ts) = (|ttrCh v t : ttrsCh f vs ts|)
+> ttrsCh f _ _ = moanE $ RawArityError f
+
+> body :: CT -> ([Pat], Raw) -> ElabM ([PAT], TM {CHK})
+> body (v :-> c) (p : ps, r) = do
+>   v <- hnf v
+>   (g, p) <- patCh v p
+>   (ps, t) <- cxLocal g $ body c (ps, r)
+>   return (p : ps, t)
+> body (F ss v) ([], r) = do
+>   t <- withSigs ss (checkR v r)
+>   return ([], t)
+> body c (ps, r) = moanE $ ThunkMismatch c (ps, r)
+
+> rawTree :: [Raw] -> [TTree Raw] -> ElabM (TTree Raw)
+> rawTree rs ts = do
+>   tbl <- ttT
+>   case pa (resolve tbl) (map (rawPunc tbl) rs) of
+>     [(t, [])]  -> case t of
+>       TLeaf (RA rs) ts -> rawTree rs ts
+>       t -> return (tApp t ts)
+>     _          -> moanE $ AmbiguousRaws rs
+>   where
+>     rawPunc tbl (RN x) | punc tbl x  = Left x
+>     rawPunc tbl p                    = Right p
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Pattern Checking                                                   %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> patCh :: VT -> Pat -> ElabM (Bwd Entry, PAT)
+> patCh v            (PN x)      = do
+>   info <- getInfoE
+>   if elem [Mark x] (ttTemplates (templateT info))
+>     then ttpCh v (TNode [Mark x] [])
+>     else (|(B0 :< ([Mark x] ::: (0, v)), PV x)|)
+> patCh Un           PVd         = (|(B0, PC [] [])|)
+> patCh (D (Up "Char") []) (PCh c) = (|(B0, PL c)|)
+> patCh (M os ss v)  (PRet p)    = (|(id *** PR) (patCh v p)|)
+> patCh (M os ss v)  (POp ps p)  = patTree ps [] >>= \ z -> case z of
+>   TLeaf p _ -> moanE $ BadMessPat ps
+>   TNode o ts -> do
+>     ops <- getOps os
+>     case [x | (o', x) <- ops, o == o'] of
+>       [(us, (s, u))] -> do
+>         (gz, ps)  <- ttpsCh o us ts
+>         (hz, p)   <- patCh (U (u :-> F (sAct os ss) v)) p
+>         (|disjoin gz hz, ~(PO o ps p)|)
+> patCh v            (PA ps)     = patTree ps [] >>= ttpCh v
+> patCh v            p           = moanE $ BadPat v p
+
+> ttpCh :: VT -> TTree Pat -> ElabM (Bwd Entry, PAT)
+> ttpCh v (TLeaf p []) = patCh v p
+> ttpCh v (TLeaf (PN n) _) = moanE $ AppliedPVar n
+> ttpCh t@(D u vs) (TNode c ps) = do
+>   info <- getInfoE
+>   case lookup u (dataDecls info) of
+>     Nothing -> moanE $ TMissing u
+>     Just (i, cs) ->
+>       case lookup c cs of
+>         Nothing -> moanE $ NoConstructor t c
+>         Just ws -> (|(id *** PC c) (ttpsCh c (xsub vs ws) ps)|)
+> ttpCh v (TNode c _) = moanE $ NoConstructor v c
+
+> ttpsCh ::  Template -> [VT] -> [TTree Pat] -> ElabM (Bwd Entry, [PAT])
+> ttpsCh f [] [] = (| ~B0, ~[] |)
+> ttpsCh f (v : vs) (t : ts) = do
+>   v <- hnf v
+>   (| disjoinC (ttpCh v t) (ttpsCh f vs ts) @ |)
+> ttpsCh f _ _ = moanE $ PatArityError f
+
+> disjoin :: Bwd Entry -> Bwd Entry -> ElabM (Bwd Entry)
+> disjoin ez fz = (|(mappend ez fz) (-traverse chk fz-)|) where
+>   chk e@(x ::: _) = traverse (occ x) ez
+>   chk e = (|B0|)
+>   occ x (y ::: _) | x == y = moanE $ RepeatedPVar x
+>   occ x _ = (|()|)
+
+> disjoinC ::  (Bwd Entry, PAT) -> (Bwd Entry, [PAT]) ->
+>             ElabM (Bwd Entry, [PAT])
+> disjoinC (ez, p) (fz, ps) = (|disjoin ez fz, ~(p : ps)|)
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Patterns for Template Resolution                                   %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> patTree :: [Pat] -> [TTree Pat] -> ElabM (TTree Pat)
+> patTree ps ts = do
+>     tbl <- (|templateT getInfoE|)
+>     case pa (resolve tbl) (map (patPunc tbl) ps) of
+>       [(t, [])]  -> case t of
+>         TLeaf (PA ps) ts -> patTree ps ts
+>         t -> return (tApp t ts)
+>       _          -> moanE $ AmbiguousPats ps
+>   where
+>     patPunc tbl (PN x) | punc tbl x  = Left x
+>     patPunc tbl p                    = Right p
+
diff --git a/ElabMonad.lhs b/ElabMonad.lhs
new file mode 100644
--- /dev/null
+++ b/ElabMonad.lhs
@@ -0,0 +1,160 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators, KindSignatures, GADTs, TypeSynonymInstances,
+>     FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections,
+>     MultiParamTypeClasses #-}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> module ElabMonad where
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> import Debug.Trace
+
+> import Prelude hiding (elem, all, foldr, concat)
+> import Data.Char
+> import Data.List hiding (elem, all, foldr, concat)
+> import Data.Monoid
+> import Data.Foldable
+> import Data.Traversable
+> import Control.Applicative
+> import Control.Monad
+> import Control.Newtype
+> import Control.Arrow
+> import Data.Void
+
+> import Gubbins
+> import Types
+> import Pa
+> import Syntax
+> import Template
+> import Check
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Elaboration Monad and ghastly plumbing                             %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> type GetSigs = () :>>: [Sig]
+> type GetInfo = () :>>: TypeInfo
+> type GetCx = () :>>: Cx
+> type SetCx = Cx :>>: ()
+
+> type ElabM = Free ((Moan :+: (GetCx :+: SetCx)) :+: (GetSigs :+: GetInfo))
+
+> moanE :: TError -> ElabM a
+> moanE e = com (L (L (e :? absurd)))
+
+> getCxE :: ElabM Cx
+> getCxE = com (L (R (L (() :? Ret))))
+
+> setCxE :: Cx -> ElabM ()
+> setCxE g = com (L (R (R (g :? Ret))))
+
+> modCxE :: (Cx -> Cx) -> ElabM ()
+> modCxE f = (|setCxE (|f getCxE|) @ |)
+
+> getSigsE :: ElabM [Sig]
+> getSigsE = com (R (L (() :? Ret)))
+
+> getInfoE :: ElabM TypeInfo
+> getInfoE = com (R (R (() :? Ret)))
+
+ elabUnify :: UnifyM x -> ElabM x
+ elabUnify u = case moc u of
+   Right x -> Ret x
+   Left (L _) -> moanE UnifyFail
+   Left (R (L (_ :? k))) -> getCxE >>= (elabUnify . k)
+   Left (R (R (g :? k))) -> setCxE g >>= (elabUnify . k)
+
+> ttT :: ElabM TemplateTable
+> ttT = do
+>     info <- getInfoE
+>     (g, _) <- getCxE
+>     let tt = templateT info
+>     return (tt {ttTemplates =  cxTemps g (ttTemplates tt)})
+>   where
+>     cxTemps B0                ts  = ts
+>     cxTemps (g :< (x ::: _))  ts  = cxTemps g (x : ts)
+>     cxTemps (g :< _)          ts  = cxTemps g ts
+
+> cxLocal :: Bwd Entry -> ElabM x -> ElabM x
+> cxLocal g c = do
+>     modCxE (((`mappend` g) . (:< Semicolon)) *** id)
+>     x <- c
+>     modCxE (popSemi *** id)
+>     return x
+>  where
+>    popSemi (g :< Semicolon)    = g
+>    popSemi (g :< _)            = popSemi g
+
+> withSigs :: [Sig] -> ElabM x -> ElabM x
+> withSigs ss c = case moc c of
+>   Right x -> Ret x
+>   Left (L (L (e :? k))) -> moanE e
+>   Left (L (R (L (_ :? k)))) -> getCxE >>= (withSigs ss. k)
+>   Left (L (R (R (g :? k)))) -> setCxE g >>= (withSigs ss. k)
+>   Left (R (L (() :? k))) -> withSigs ss (k ss)
+>   Left (R (R (() :? k))) -> getInfoE >>= (withSigs ss . k)   
+
+> baseInfo :: TypeInfo -> ElabM x -> Either TError x
+> baseInfo info = go (B0, 0) where
+>   go g c = case moc c of
+>     Right x -> Right x
+>     Left (L (L (e :? k))) -> Left e
+>     Left (L (R (L (_ :? k)))) -> go g (k g)
+>     Left (L (R (R (g :? k)))) -> go g (k ())
+>     Left (R (L (() :? k))) -> go g (k [Up "" :$ []])  -- the ineffable
+>     Left (R (R (() :? k))) -> go g (k info)
+
+> err :: (TError -> TError) -> ElabM x -> ElabM x
+> err f c = case moc c of
+>   Right x -> Ret x
+>   Left (L (L (e :? k))) -> moanE $ f e
+>   Left (L (R (L (_ :? k)))) -> getCxE >>= (err f . k)
+>   Left (L (R (R (g :? k)))) -> setCxE g >>= (err f . k)
+>   Left (R (L (() :? k))) -> getSigsE >>= (err f . k)
+>   Left (R (R (() :? k))) -> getInfoE >>= (err f . k)   
+
+> hnf :: VT -> ElabM VT
+> hnf (Q i) = do
+>     (g, _) <- getCxE
+>     return $ improve (Q i) g
+>   where
+>     improve (Q i)  (g :< (j :=? Just v)) | i == j  = improve v g
+>     improve (Q i)  (g :< _)                        = improve (Q i) g
+>     improve v      _                               = v
+> hnf v = (|v|)
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Datatypes for contexts                                             %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> data Entry
+>   = Semicolon
+>   | Int :=? Maybe VT
+>   | Template ::: (Int, VT)
+>   deriving Show
+
+> type Cx = (Bwd Entry, Int)  -- a context and a nonce
+
+> instance TMang Entry where
+>   tMang s Semicolon = (|Semicolon|)
+>   tMang s (q :=? mv) = (| ~q :=? tMang s mv|)
+>   tMang s (x ::: iv) = (| ~x ::: tMang s' iv|) where
+>     s' (VX i) = pure (X i)
+>     s' v = s v
+
+> withTopEntry :: (Entry -> ElabM (Bwd Entry)) -> ElabM ()
+> withTopEntry f = getCxE >>= \ (g, i) -> case g of
+>   B0      -> moanE $ Cockup "fell off the bottom of the context"
+>   g :< e  -> do
+>     setCxE (g, i)
+>     h <- f e
+>     modCxE ((`mappend` h) *** id)
+
+
diff --git a/Frank.cabal b/Frank.cabal
--- a/Frank.cabal
+++ b/Frank.cabal
@@ -1,5 +1,5 @@
 name:		Frank
-version:	0.0
+version:	0.1
 synopsis:	An experimental programming language with typed algebraic effects
 description:	An experimental programming language with typed algebraic effects
 license:	PublicDomain
@@ -17,6 +17,7 @@
   build-depends:	base < 5, void, newtype, mtl, she
   extensions:		TypeOperators, KindSignatures, GADTs, TypeSynonymInstances, FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections, FunctionalDependencies, PatternGuards
   ghc-options:		-F -pgmF she
+  other-modules:	Gubbins, Pa, Types, Template, Syntax, Check, ElabMonad, Unify, Elab, Run
 
 source-repository head
   type:		  darcs
diff --git a/Gubbins.lhs b/Gubbins.lhs
new file mode 100644
--- /dev/null
+++ b/Gubbins.lhs
@@ -0,0 +1,143 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-#  LANGUAGE TypeOperators, FlexibleInstances, FunctionalDependencies,
+>      RankNTypes #-}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> module Gubbins where
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> import Control.Applicative
+> import Control.Newtype
+> import Control.Monad.Identity
+> import Data.Void
+> import Data.Monoid
+> import Data.Foldable
+> import Data.Traversable
+> import Data.List
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Newtype instance for Identity                                      %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> instance Newtype (Identity x) x where
+>   pack = Identity
+>   unpack (Identity x) = x
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Higher Kind Show                                                   %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> class ShowStarStar f where
+>   showStarStar :: Show x => f x -> String
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Free Monad, sort of                                                %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> data Free f x
+>    = Ret x
+>    | Com (forall t. (x -> Free f t) -> f (Free f t))
+
+> instance Monad (Free f) where
+>   return = Ret
+>   Ret x  >>= f = f x
+>   Com d  >>= f = Com $ \ k -> d $ \ x -> f x >>= k
+
+> com :: Functor f => f (Free f x) -> Free f x
+> com ffx = Com $ \ k -> fmap (>>= k) ffx
+
+> moc :: Free f x -> Either (f (Free f x)) x
+> moc (Ret x) = Right x
+> moc (Com f) = Left (f Ret)
+
+> instance ShowStarStar f => ShowStarStar (Free f) where
+>   showStarStar c = case moc c of
+>     Right x -> "(Ret " ++ show x ++ ")"
+>     Left ffx -> "(Com " ++ showStarStar ffx ++ ")"
+> instance (ShowStarStar f, Show x) => Show (Free f x) where
+>   show = showStarStar
+
+> data (:>>:) s t x = s :? (t -> x)
+> instance Functor (s :>>: t) where
+>   fmap k (s :? f) = s :? (k . f)
+> instance Show s => ShowStarStar (s :>>: t) where
+>   showStarStar (s :? _) = "(" ++ show s ++ " :? ...)"
+> instance (Show s, Show x) => Show ((s :>>: t) x) where
+>   show = showStarStar
+
+> data (:+:) f g x = L (f x) | R (g x)
+> instance (Functor f, Functor g) => Functor (f :+: g) where
+>   fmap k (L fx)  = L (fmap k fx)
+>   fmap k (R gx)  = R (fmap k gx)
+> instance (ShowStarStar f, ShowStarStar g) => ShowStarStar (f :+: g) where
+>   showStarStar (L fx) = "(L " ++ showStarStar fx ++ ")"
+>   showStarStar (R gx) = "(R " ++ showStarStar gx ++ ")"
+> instance (ShowStarStar f, ShowStarStar g, Show x)
+>   => Show ((f :+: g) x) where
+>   show = showStarStar
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Snoc-lists                                                         %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> data Bwd x = B0 | Bwd x :< x deriving (Show, Eq, Ord)
+> infixl 5 :<
+
+Fish...
+
+> (<><) :: Bwd x -> [x] -> Bwd x
+> xz <>< []        = xz
+> xz <>< (x : xs)  = (xz :< x) <>< xs
+> infixl 5 <><
+
+...and chips
+
+> (<>>) :: Bwd x -> [x] -> [x]
+> B0         <>> xs  = xs
+> (xz :< x)  <>> xs  = xz <>> (x : xs)
+> infixr 5 <>>
+
+> instance Monoid (Bwd x) where
+>   mempty                = B0
+>   mappend xz B0         = xz
+>   mappend xz (yz :< y)  = mappend xz yz :< y
+
+> instance Applicative Bwd where
+>   hiding instance Functor
+>   pure x = pure x :< x
+>   (fz :< f)  <*> (sz :< s)  = (fz <*> sz) :< f s
+>   _          <*> _          = B0
+
+> instance Traversable Bwd where
+>   traverse f B0         = (|B0|)
+>   traverse f (xz :< x)  = (|traverse f xz :< f x|)
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% UnionList                                                          %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> newtype UnionList x = UnionList [x] deriving (Show, Eq)
+> instance Newtype (UnionList x) [x] where
+>   pack = UnionList
+>   unpack (UnionList x) = x
+> instance Eq x => Monoid (UnionList x) where
+>   mempty = UnionList []
+>   mappend (UnionList a) (UnionList b) = UnionList (union a b)
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Missing Traversables                                               %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> instance Traversable ((,) a) where
+>   hiding instance Functor
+>   traverse f (a, b) = (| ~a, f b|)
+
diff --git a/Pa.lhs b/Pa.lhs
new file mode 100644
--- /dev/null
+++ b/Pa.lhs
@@ -0,0 +1,107 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators, FlexibleInstances, TupleSections,
+>     GeneralizedNewtypeDeriving #-}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> module Pa where
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> import Data.Char
+> import Data.Monoid
+> import Control.Applicative
+> import Control.Monad
+
+> import Gubbins
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Brackets and Tokens                                                %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> data Brk = Rnd | Sqr | Crl deriving (Show, Eq)
+
+> data Tok
+>   = TB Brk [Tok] Bool
+>   | TN String
+>   deriving Show
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Chunking (and lexing)                                              %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> chunk :: String -> [[Tok]]
+> chunk = snd . dent . lines where
+>   dent = foldr
+>     (\ s (d, gs) -> let sd = s ++ "\n" ++ d in
+>       if leftA s then ("", lx B0 [] sd : gs) else (sd , gs))
+>     ("", [])
+>   leftA (c : cs) = not (isSpace c)
+>   leftA _ = False
+
+> lx :: Bwd Tok -> [(Brk, Bwd Tok)] -> String -> [Tok]
+> lx tz  []                []         = tz <>> []
+> lx tz  ((b, uz) : bs)    []         = lx (uz :< TB b (tz <>> []) False) bs []
+> lx tz  bs                ('(' : s)  = lx B0 ((Rnd, tz) : bs) s
+> lx tz  ((Rnd, uz) : bs)  (')' : s)  = lx (uz :< TB Rnd (tz <>> []) True) bs s
+> lx tz  bs                ('[' : s)  = lx B0 ((Sqr, tz) : bs) s
+> lx tz  ((Sqr, uz) : bs)  (']' : s)  = lx (uz :< TB Sqr (tz <>> []) True) bs s
+> lx tz  bs                ('{' : s)  = lx B0 ((Crl, tz) : bs) s
+> lx tz  ((Crl, uz) : bs)  ('}' : s)  = lx (uz :< TB Crl (tz <>> []) True) bs s
+> lx tz  bs                ('\'' : c : '\'' : s)
+>   | c /= '\\' = lx (tz :< TN ['\'', c, '\'']) bs s
+> lx tz  bs                (c : s)
+>   | solo c     = lx (tz :< TN [c]) bs s
+>   | isSpace c  = lx tz bs s
+>   | otherwise  = let (s0, s1) = span iddy s in lx (tz :< TN (c : s0)) bs s1
+>   where
+>     solo c = elem c ",;()[]{}!"
+>     iddy c = not (isSpace c || solo c)
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Parser Monad                                                       %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> newtype Pa t x = Pa {pa :: [t] -> [(x, [t])]} deriving Monoid
+> instance Monad (Pa t) where
+>   return x = Pa $ \ ts -> [(x, ts)]
+>   Pa f >>= k = Pa $ \ ts -> do
+>     (x, ts) <- f ts
+>     pa (k x) ts
+> instance MonadPlus (Pa t) where
+>   mzero = mempty
+>   mplus = mappend
+
+> tok :: (t -> [x]) -> Pa t x
+> tok p = Pa $ \ ts -> case ts of
+>   t : ts -> map (, ts) (p t)
+>   _ -> []
+
+> eof :: Pa t ()
+> eof = Pa $ \ ts -> case ts of
+>  [] -> [((), [])]
+>  _ -> []
+
+> sep :: Pa t () -> Pa t x -> Pa t [x]
+> sep s p = (| p : many (|id (-s-) p|)
+>            | []
+>            |)
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Token-Specific Parsers                                             %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> is :: String -> Pa Tok ()
+> is s = tok $ \ t -> case t of
+>   TN s' | s == s' -> [()]
+>   _ -> []
+
+> brk :: Brk -> Pa Tok x -> Pa Tok x
+> brk b p = tok $ \ t -> case t of
+>   TB b' ts True | b == b' -> (|fst (pa (p <* eof) ts)|)
+>   _ -> []
diff --git a/Run.lhs b/Run.lhs
new file mode 100644
--- /dev/null
+++ b/Run.lhs
@@ -0,0 +1,123 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators, KindSignatures, GADTs, TypeSynonymInstances,
+>     FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections,
+>     MultiParamTypeClasses #-}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> module Run where
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> import Prelude hiding (elem, all)
+> import Data.Char
+> import Data.List hiding (elem, all)
+> import Data.Monoid
+> import Data.Foldable
+> import Data.Traversable
+> import Control.Applicative
+> import Control.Monad
+> import Control.Newtype
+> import Data.Void
+> import Control.Arrow
+
+> import Gubbins
+> import Types
+> import Pa
+> import Syntax
+> import Unify
+> import Template
+> import Check
+> import Elab
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Operational Behaviour                                              %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> data VAL
+>   = VC Template [VAL]
+>   | VL Char
+>   | VU COMP
+>   | VR VAL
+>   | VO Template [VAL] VAL
+
+> type COMP = [VAL] -> Free Frank VAL
+
+> type Frank = (Template, [VAL]) :>>: VAL
+
+> type Env = [VAL]
+
+> eval :: [(Template, VAL)] -> Env -> TM {d} -> Free Frank VAL
+> eval fs g (H (VA i)) = (|(g !! i)|)
+> eval fs g (H (FN f)) =
+>   case lookup f fs of
+>     Just v -> (|v|)
+>     Nothing -> error ("Missing definition for " ++ show f)
+> eval fs g (H (OP o)) = (|(VU $ \ vs -> com $ (o, vs) :? Ret)|)
+> eval fs g (f :/ es) = (|apply (eval fs g f) (traverse (eval fs g) es) @ |)
+> eval fs g (PApp f es) = do
+>   f <- eval fs g f
+>   us <- traverse (eval fs g) es
+>   (|(VU $ \ vs -> apply f (us ++ vs))|)
+> eval fs g (HAN h e) = (|handle (eval fs g h) ~(eval fs g e) @ |)
+> eval fs g (E e) = eval fs g e
+> eval fs g (CN c es) = (|(VC c) (traverse (eval fs g) es)|)
+> eval fs g (CL c) = (|(VL c)|)
+> eval fs g (BUNK e) = eval fs g e  -- seeya!
+> eval fs g (LAM pes) = (|(VU (lambda fs g pes))|)
+
+> apply :: VAL -> [VAL] -> Free Frank VAL
+> apply (VU f) vs = f vs
+
+> handle :: VAL -> Free Frank VAL -> Free Frank VAL
+> handle (VU h) e = case moc e of
+>   Right v -> h [VR v]
+>   Left ((o, vs) :? k) -> case moc (h [VO o vs (VU (k . head))]) of
+>     Right v -> Ret v
+>     Left (([Mark "match"], []) :? _) -> com ((o, vs) :? (handle (VU h) . k))
+>     Left c -> com c
+
+> lambda :: [(Template, VAL)] -> Env -> [([PAT], TM {CHK})] -> COMP
+> lambda fs g ((ps, e) : pes) vs = case matches ps vs g of
+>   Just g   -> eval fs g e
+>   Nothing  -> lambda fs g pes vs
+> lambda fs g [] vs = com (([Mark "match"], []) :? undefined)  -- cheeky
+
+> matches :: [PAT] -> [VAL] -> Env -> Maybe Env
+> matches []       []        = return
+> matches (p : ps) (v : vs)  = match p v >=> matches ps vs
+
+> match :: PAT -> VAL -> Env -> Maybe Env
+> match (PV _)       v                     = (|Just (v :)|)
+> match (PC c ps)    (VC d vs) | c == d    = matches ps vs
+> match (PL c)       (VL d) | c == d       = (|Just id|)
+> match (PR p)       (VR v)                = match p v
+> match (PO o ps p)  (VO n vs v) | o == n  = matches ps vs >=> match p v
+> match _            _                     = (|Nothing|)
+
+> instance Show VAL where
+>   show (VC t vs) = tempShow t (map show vs)
+>   show (VL c)    = show c
+>   show (VU _)    = "{...}"
+>   show (VR v)    = "!! VR " ++ show v
+>   show (VO o vs v) = "!! VO " ++ tempShow o (map show vs) ++ " " ++ show v
+
+> display :: Free Frank VAL -> IO String
+> display c = case moc c of
+>   Right v -> return $ show v
+>   Left (([Mark "inch"], []) :? k) -> do
+>     c <- getChar
+>     display (k (VL c))
+>   Left (([Mark "ouch"], [VL c]) :? k) -> do
+>     putChar c
+>     display (k (VC [] []))
+>   Left ((o, vs) :? k) -> return $ "Unhandled: " ++ tempShow o (map show vs)
+
+> primitiveDefs :: [(Template, VAL)]
+> primitiveDefs =
+>   [  ([Place, Mark "=Char=", Place], VU $ \ [VL c, VL d] -> Ret $
+>        if c == d then VC [Mark "tt"] [] else VC [Mark "ff"] [])
+>   ]
diff --git a/Syntax.lhs b/Syntax.lhs
new file mode 100644
--- /dev/null
+++ b/Syntax.lhs
@@ -0,0 +1,231 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators, KindSignatures, GADTs, TypeSynonymInstances,
+>     FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections,
+>     MultiParamTypeClasses #-}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> module Syntax where
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> import Prelude hiding (elem, all)
+> import Data.Char
+> import Data.List hiding (elem, all)
+> import Data.Monoid
+> import Data.Foldable
+> import Data.Traversable
+> import Control.Applicative
+> import Control.Monad
+> import Control.Newtype
+
+> import Types
+> import Pa
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% top level Source                                                   %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> data Source = Source
+>   {  sourceData :: [(UpId, ([UpId], [[Lump]]))]
+>   ,  sourceSigs :: [(UpId, ([UpId], [([Lump], VT)]))]
+>   ,  sourceDecl :: [([Lump], ([Sig], VT))]
+>   ,  sourceDefs :: [([Pat], Raw)]
+>   ,  sourceNote :: [[Tok]]
+>   ,  sourceJunk :: [[Tok]]
+>   }  deriving Show
+
+> instance Monoid Source where
+>   mempty = Source [] [] [] [] [] []
+>   mappend (Source x1 x2 x3 x4 x5 x6) (Source y1 y2 y3 y4 y5 y6) =
+>     Source (x1 ++ y1) (x2 ++ y2) (x3 ++ y3) (x4 ++ y4) (x5 ++ y5) (x6 ++ y6)
+
+> source :: String -> Source
+> source = foldMap ch . chunk where
+>   ch ts = 
+>     case (pa dataP ts, pa sgdP ts, pa declP ts, pa lineP ts, pa noteP ts) of
+>       ([(d, [])], [], [], [], [])  ->  Source [d] [] [] [] [] []
+>       ([], [(s, [])], [], [], [])  ->  Source [] [s] [] [] [] []
+>       ([], [], [(f, [])], [], [])  ->  Source [] [] [f] [] [] []
+>       ([], [], [], [(l, [])], [])  ->  Source [] [] [] [l] [] []
+>       ([], [], [], [], [(n, [])])  ->  Source [] [] [] [] [n] []
+>       _                            ->  Source [] [] [] [] [] [ts]
+
+> data Lump = LNm String | LTy VT
+
+> instance Show Lump where
+>   show (LNm x) = x
+>   show (LTy t) = show t
+
+> instance TMang Lump where
+>   tMang s (LNm x) = (|LNm ~x|)
+>   tMang s (LTy t) = (|LTy (tMang s t)|)
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% datatypes for Raw terms and patterns                               %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> data Raw
+>   = RN String
+>   | RA [Raw]
+>   | RCh Char
+>   | RVd
+>   | RBunk
+>   | RBang
+>   | RTh [([Pat],Raw)]
+>   | RQ Raw Raw
+>   deriving Show
+
+> data Pat
+>   = PN String
+>   | PCh Char
+>   | PVd
+>   | PA [Pat]
+>   | PRet Pat
+>   | POp [Pat] Pat
+>   deriving Show
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% top level chunks                                                   %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> dataP :: Pa Tok (UpId, ([UpId], [[Lump]]))
+> dataP = (| (,) (-is "data"-) upid
+>            (|(,) (many upid) (-is "="-) (sep (is "|") nomTys) (-eof-) |)
+>          |)
+
+> sgdP :: Pa Tok (UpId, ([UpId], [([Lump], VT)]))
+> sgdP = (| (,) (-is "sig"-) upid
+>           (|(,) (many upid) (-is "="-) 
+>              (sep (is "|")
+>                (|nomTys,
+>                  (| id (-brk Sqr eof-) (| id bigVT | Un |) | Un |)|))
+>              (-eof-) |)
+>         |)
+
+> declP :: Pa Tok ([Lump], ([Sig], VT))
+> declP = (|(,) nomTys (|(brk Sqr sigsP), (| id bigVT | Un |) | ([], Un) |)
+>           (-eof-)|)
+
+> lineP :: Pa Tok ([Pat], Raw)
+> lineP = (|(,) (some patP) (-is "="-) bigRaw (-eof-)|)
+
+> noteP :: Pa Tok [Tok]
+> noteP = (|id (-is "note"-) (many (tok return)) (-eof-)|)
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% parsing types                                                      %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> weeVT :: Pa Tok VT
+> weeVT = (| D upid ~[]
+>          | id (brk Sqr (|M sigsP (-is "?"-)
+>                            (| id (brk Sqr sigsP) | [] |) bigVT|))
+>          | Ze (-brk Crl eof-)
+>          | Un (-brk Rnd eof-)
+>          | U (brk Crl bigCT)
+>          | id (brk Rnd bigVT)
+>          |)
+
+> bigVT :: Pa Tok VT
+> bigVT = (| D upid (some weeVT)
+>          | id weeVT
+>          |)
+
+> bigCT :: Pa Tok CT
+> bigCT = (| bigVT :-> (-is "->"-) bigCT
+>          | F (| id (brk Sqr sigsP) | [] |) bigVT
+>          |)
+
+> nomTys :: Pa Tok [Lump]
+> nomTys = some (| LNm nom | LTy weeVT |)
+
+> sigP :: Pa Tok Sig
+> sigP = (| Pure (-brk Crl eof -)
+>         | upid :$ (many weeVT)
+>         |)
+
+> sigsP :: Pa Tok [Sig]
+> sigsP = sep (is ",") sigP
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% keywords and identifiers                                           %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> keywords :: [String]
+> keywords = ["note","sig", "data", "->", ";", ",", "=", "|", "!","?"]
+
+> nom :: Pa Tok String
+> nom = tok $ \ t -> case t of
+>   TN x@(c:_)
+>     | not (c == '\''), not (isUpper c), not (elem x keywords) -> [x]
+>   _ -> []
+
+> upid :: Pa Tok UpId
+> upid = tok $ \ t -> case t of
+>   TN x@(c:_) | isUpper c, not (elem x keywords) -> [Up x]
+>   _ -> []
+
+> lit :: Pa Tok Char
+> lit = tok $ \ t -> case t of
+>     TN ['\'',c,'\'']       | c /= '\\' -> [c]
+>     TN ['\'','\\',c,'\'']  -> [d| (c', d) <- escapees, c' == c]
+>     _ -> []
+>   where
+>     escapees =
+>       [  ('\'', '\'')
+>       ,  ('\"', '\"')
+>       ,  ('\\', '\\')
+>       ,  ('n', '\n')
+>       ,  ('r', '\r')
+>       ,  ('t', '\t')
+>       ,  ('b', '\b')
+>       ]
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% parsing raw terms and patterns                                     %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> bigRaw :: Pa Tok Raw
+> bigRaw = (| RQ medRaw (-is "?"-) bigRaw
+>           | id medRaw
+>           |)
+
+> medRaw :: Pa Tok Raw
+> medRaw = (| RA (|weeRaw : some weeRaw|)
+>           | id weeRaw
+>           |)
+
+> weeRaw :: Pa Tok Raw
+> weeRaw = (| RBang (-is "!"-)
+>           | RN nom
+>           | RCh lit
+>           | RVd (-brk Rnd eof-)
+>           | id (brk Rnd bigRaw)
+>           | RBunk (-brk Crl eof-)
+>           | RTh (brk Crl (|clauseP : many (|id (-is "|"-) clauseP|)|))
+>           |)
+
+> clauseP :: Pa Tok ([Pat], Raw)
+> clauseP = (| some patP, (-is "->"-) bigRaw
+>            | ~[], bigRaw
+>            |)
+
+> patP :: Pa Tok Pat
+> patP = (| PN nom
+>         | PCh lit
+>         | PVd (-brk Rnd eof-)
+>         | PA (brk Rnd (some patP))
+>         | PRet (brk Sqr patP)
+>         | id (brk Sqr (|POp (some patP) (-is "?"-) patP|))
+>         |)
+
+
diff --git a/Template.lhs b/Template.lhs
new file mode 100644
--- /dev/null
+++ b/Template.lhs
@@ -0,0 +1,123 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators, FlexibleInstances, MultiParamTypeClasses #-}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> module Template where
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> import Prelude hiding (elem, any)
+> import Control.Applicative
+> import Control.Monad
+> import Data.Foldable
+> import Data.Monoid
+
+> import Pa
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Templates                                                          %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> type Template = [TBit]
+> data TBit = Place | Mark String deriving (Eq, Ord)
+
+> prefix :: Template -> Bool
+> prefix (Mark _ : _ : _) = True
+> prefix _ = False
+
+> postfix :: Template -> Bool
+> postfix (Place : _) = True
+> postfix _ = False
+
+> tempShow :: Template -> [String] -> String
+> tempShow [Mark c]  [] = c
+> tempShow bs        ss = "(" ++ splice False bs ss ++ ")" where
+>   splice _     []             []        = ""
+>   splice True  bs             ss        = " "  ++  splice False  bs  ss
+>   splice _     []             (s : ss)  = s    ++  splice True   []  ss
+>   splice _     (Mark m : bs)  ss        = m    ++  splice True   bs  ss
+>   splice _     (Place : bs)   (s : ss)  = s    ++  splice True   bs  ss
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Template Tables                                                    %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> data TemplateTable = TemplateTable
+>   {  ttTemplates   :: [Template]              -- what are the templates
+>   ,  ttPrecedence  :: [(Template, Template)]  -- what's outside what
+>   ,  ttAssocs      :: [(Template, Int)]       -- which place associates
+>   }  deriving Show
+
+> punc :: TemplateTable -> String -> Bool
+> punc tt s = elem s [x | bs <- ttTemplates tt, Mark x <- bs]
+
+> gassocs :: TemplateTable -> Template -> (Template, Int)
+> gassocs tbl t = case lookup t (ttAssocs tbl) of
+>   Just i -> (t , i)
+>   _ -> (t , negate 1)
+
+> prLT :: TemplateTable -> ([TBit], Int) -> [TBit] -> Bool
+> prLT tbl ([], _) _ = True
+> prLT tbl (x, 0) y | x == y = True
+> prLT tbl _ [_] = True
+> prLT tbl (x, _) y = grLT (ttPrecedence tbl) x y where
+>   grLT g x y = x /= y && grLE g x y
+>   grLE g x y | x == y = True
+>   grLE g x y = any (grLE g x) [z | (z, y') <- g, y == y']
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Templates                                                          %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> data TTree x
+>   = TLeaf x [TTree x]
+>   | TNode Template [TTree x]
+>   deriving Show
+
+> tApp :: TTree x -> [TTree x] -> TTree x
+> tApp (TLeaf x xs) ys = TLeaf x (xs ++ ys)
+> tApp (TNode t xs) ys = TNode t (xs ++ ys)
+
+> resolve :: TemplateTable -> Pa (Either String x) (TTree x)
+> resolve tbl = big ([], 0) <* eof where
+>   is s = tok $ either (guard . (s ==)) mempty
+>   big ti = (| (mafter ti) medium @ |)
+>   medium = (| safter small @ |) <|>
+>     foldMap (\ t -> (| (TNode t) (tmpl t (gassocs tbl t)) |)) pres
+>   small = tok (either single (return . (`TLeaf` [])))
+>   mafter ti s = (| (mafter ti) more @ | s |) where
+>     more = (| id (foldMap
+>                   (\ t -> (| (TNode t . (s :))
+>                             (tmpl t (dock (gassocs tbl t))) |))
+>                   possibles)
+>             |)
+>     dock (x : xs, i) = (xs, i - 1)
+>     possibles = filter (\ u -> postfix u && prLT tbl ti u && grabs s u)
+>                   (ttTemplates tbl)
+>     grabs (TNode t _) u = prLT tbl (gassocs tbl u) t
+>     grabs _ _ = True
+>   safter s = (| safter (| (tApp s . return) small |) @ | s |) where
+>   tmpl t ([], _) = (|[]|)
+>   tmpl t (Mark s : ts, i) = (| id (-is s-) (tmpl t (ts, i)) |)
+>   tmpl t (Place : ts, i) = (| big (t, i) : tmpl t (ts, i - 1) |)
+>   pres = filter prefix (ttTemplates tbl)
+>   single t  | elem [Mark t] (ttTemplates tbl)
+>             = [TNode [Mark t] []]
+>             | otherwise                        = []
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Show Instances                                                     %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> instance Show TBit where
+>   show Place     = "_"
+>   show (Mark x)  = x
+
+
diff --git a/Types.lhs b/Types.lhs
new file mode 100644
--- /dev/null
+++ b/Types.lhs
@@ -0,0 +1,159 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-# LANGUAGE TypeOperators, FlexibleInstances #-}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> module Types where
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> import Control.Newtype
+> import Control.Applicative
+> import Control.Monad.Identity
+> import Data.Traversable
+> import Data.List
+
+> import Gubbins
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Datatypes for types                                                %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+Frank has *value types*...
+
+> data VT
+>   = Ze                -- empty type                    {}
+>   | Un                -- unit type                     ()
+>   | U CT              -- thunked computation type      {C}
+>   | D UpId [VT]       -- type constructor with params  D V1 .. Vn
+>   | M [Sig] [Sig] VT  -- message from the first bunch
+>   | X Int             -- rigid type variable           X
+>   | Q Int             -- flexible type variable        ?X
+
+... and *computation types*.
+
+> data CT
+>   = VT :-> CT      -- function type                 V -> C
+>   | F [Sig] VT     -- effectful value type          [Ss] V
+> infixr 4 :->
+
+Types are named by UpId identifiers, beginning in uppercase.
+
+> newtype UpId = Up {ui :: String} deriving (Show, Eq, Ord)
+
+Signatures are named and parametrized.
+
+> data Sig
+>   =  (:$) {sigU :: UpId, sigPs :: [VT]}
+>   |  Pure
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% The very nice mangler                                              %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> class TMang t where
+>   tMang :: Applicative f => (Var -> f VT) -> t -> f t
+
+> data Var = VD UpId | VX Int | VQ Int
+> vD :: UpId -> VT
+> vD u = D u []
+> var :: (UpId -> x) -> (Int -> x) -> (Int -> x) -> Var -> x
+> var vd vx vq (VD u) = vd u
+> var vd vx vq (VX i) = vx i
+> var vd vx vq (VQ i) = vq i
+
+> instance TMang VT where
+>   tMang s Ze           = (|Ze|)
+>   tMang s Un           = (|Un|)
+>   tMang s (U c)        = (|U (tMang s c)|)
+>   tMang s (D u [])     = s (VD u)
+>   tMang s (D u vs)     = (|D ~u (tMang s vs)|)
+>   tMang s (M os ss v)  = (|M (tMang s os) (tMang s ss) (tMang s v) |)
+>   tMang s (X i)        = s (VX i)
+>   tMang s (Q i)        = s (VQ i)
+
+> instance TMang CT where
+>   tMang s (v :-> c)  = (|tMang s v :-> tMang s c|)
+>   tMang s (F ss v)   = (|F (tMang s ss) (tMang s v)|)
+
+> instance TMang Sig where
+>   tMang s (u :$ vs) = (| ~u :$ tMang s vs|)
+>   tMang s Pure      = (|Pure|)
+
+> instance TMang x => TMang [x] where
+>   tMang = traverse . tMang
+
+> instance TMang x => TMang (Maybe x) where
+>   tMang = traverse . tMang
+
+> instance (TMang x, TMang y) => TMang (x, y) where
+>   tMang s (x, y) = (|tMang s x, tMang s y|)
+
+> instance TMang Int where
+>   tMang s = pure
+
+> xsub :: (TMang t) => [VT] -> t -> t
+> xsub vs = ala' Identity tMang (var vD (bof vs) Q) where
+>   bof [] i = X i
+>   bof (x : xs) 0 = x
+>   bof (x : xs) i = bof xs (i - 1)
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Sig Action                                                         %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+A signature acts on a collection of signatures by shadowing or
+disabling. (Might add individual disabling?) We lift structurally.
+
+> class SigAct t where
+>   sAct :: t -> [Sig] -> t
+
+> instance SigAct [Sig] where
+>   sAct sa ss = foldr s1 ss sa where
+>     s1 Pure _ = []
+>     s1 s@(f :$ _) ss = s : [s' | s'@(f' :$ _) <- ss, f' /= f]
+
+> instance SigAct VT where
+>   sAct (U c)        ss = U (sAct c ss)
+>   sAct (D n vs)     ss = D n (map (`sAct` ss) vs)  -- really?
+>   sAct (M os sa v)  ss = M os (sAct sa ss) (sAct v ss)
+>   sAct t            ss = t
+
+> instance SigAct CT where
+>   sAct (F sa v)   ss = F (sAct sa ss) (sAct v ss)
+>   sAct (v :-> c)  ss = sAct v ss :-> sAct c ss
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Show instances                                                     %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> instance Show VT where
+>   show Ze           = "{}"
+>   show Un           = "()"
+>   show (U c)        = "{" ++ show c ++ "}"
+>   show (D u [])     = ui u
+>   show (D u vs)     = "(" ++ ui u ++ (vs >>= ((' ' :) . show)) ++ ")"
+>   show (M os ss v)
+>     = "[" ++ intercalate ", " (map show os) ++ " ? "
+>     ++ (if null ss then "" else "[" ++ intercalate ", " (map show ss) ++ "]")
+>     ++ show v ++ "]"
+>   show (X i)        = "#" ++ show i
+>   show (Q i)        = "?" ++ show i
+
+> instance Show CT where
+>   show (v :-> c)       = show v ++ " -> " ++ show c
+>   show (F [] v)        = show v
+>   show (F (s : ss) v)
+>     = "[" ++ show s ++ (ss >>= ((", " ++) . show)) ++ "] " ++ show v
+
+> instance Show Sig where
+>   show (u :$ vs) = ui u ++ (vs >>= ((' ' :) . show))
+>   show Pure = "{}"
diff --git a/Unify.lhs b/Unify.lhs
new file mode 100644
--- /dev/null
+++ b/Unify.lhs
@@ -0,0 +1,114 @@
+> {-# OPTIONS_GHC -F -pgmF she #-}
+> {-#  LANGUAGE TypeOperators, FunctionalDependencies,
+>      FlexibleContexts #-}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> module Unify where
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> import Debug.Trace
+
+> import Control.Newtype
+> import Control.Applicative
+> import Control.Monad
+> import Control.Arrow
+> import Data.Monoid
+> import Data.Void
+> import Data.Function
+> import Data.List
+
+> import Gubbins
+> import Types
+> import Template
+> import Check
+> import ElabMonad
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Unification Class                                                  %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> class Unify t where
+>   (=?=) :: t -> t -> ElabM ()
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Unification Instances                                              %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> instance Unify VT where
+>   --s =?= t | trace (show s ++ " =?= " ++ show t) False = undefined
+>   Ze      =?=  Ze      = return ()
+>   Un      =?=  Un      = return ()
+>   U b     =?=  U c     = b =?= c
+>   D b us  =?=  D c vs  | b == c = us =?= vs
+>   X i     =?=  X j     | i == j = return ()
+>   Q i     =?=  Q j     = if i == j then return () else identify i j
+>   Q i     =?=  v       = solve i [] v
+>   v       =?=  Q i     = solve i [] v
+>   s       =?=  t       = moanE $ UnifyVFail s t
+
+> instance Unify CT where
+>   (u :-> b)  =?=  (v :-> c)  = do u =?= v; b =?= c
+>   F rr u     =?=  F ss v     = do
+>     sortBy (compare `on` sigU) rr =?= sortBy (compare `on` sigU) ss
+>     u =?= v
+>   s          =?=  t          = moanE $ UnifyCFail s t
+
+> instance Unify Sig where
+>   (x :$ us) =?= (y :$ vs) | x == y = us =?= vs
+>   s =?= t = moanE $ UnifySFail s t
+
+> instance Unify t => Unify [t] where
+>   []        =?=  []        = return ()
+>   (a : as)  =?=  (b : bs)  = do a =?= b; as =?= bs
+>   _         =?=  _         = moanE $ Cockup "arity mismatch"
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Occur Check                                                        %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+> qoccur :: TMang t => Int -> t -> Bool
+> qoccur q = ala' Any (ala' Const tMang) $
+>   var (const False) (const False) (q ==)
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%% Identification and Solving                                         %%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+|identify i j| assumes |i| is not |j|
+
+> identify :: Int -> Int -> ElabM ()
+> identify i j = do
+>  --(g, _) <- getCxE
+>  --False <- trace ("IDENTIFY " ++ show g ++ show (i, j)) $ return False
+>  withTopEntry $ \ e -> case e of
+>   k :=? Nothing
+>     | k == i -> return (B0 :< (k :=? Just (Q j)))
+>     | k == j -> return (B0 :< (k :=? Just (Q i)))
+>   k :=? Just v
+>     | k == i -> solve j [] v >> return (B0 :< e)
+>     | k == j -> solve i [] v >> return (B0 :< e)
+>   _ -> identify i j >> return (B0 :< e)
+
+|solve q es v| assumes |v| is not |Q q|
+
+> solve :: Int -> [Entry] -> VT -> ElabM ()
+> solve q es v = do
+>  --(g, _) <- getCxE
+>  --False <- trace ("SOLVE " ++ show g ++ show (q, es, v)) $ return False
+>  withTopEntry $ \ e -> case e of
+>   q' :=? mu | q' == q ->
+>     if qoccur q es || qoccur q v
+>       then moanE $ UnifyVFail (Q q) v
+>       else case mu of
+>         Nothing  -> return (B0 <>< es :< (q :=? Just v))
+>         Just u   -> do modCxE ((<>< es) *** id); u =?= v; return (B0 :< e)
+>   q' :=? _ | qoccur q' es || qoccur q' v -> solve q (e : es) v >> return B0
+>   e -> solve q es v >> return (B0 :< e)