diff --git a/Language/Javascript/JMacro.hs b/Language/Javascript/JMacro.hs
--- a/Language/Javascript/JMacro.hs
+++ b/Language/Javascript/JMacro.hs
@@ -69,7 +69,8 @@
 module Language.Javascript.JMacro (
   module Language.Javascript.JMacro.QQ,
   module Language.Javascript.JMacro.Base,
-  module Language.Javascript.JMacro.Prelude
+  module Language.Javascript.JMacro.Prelude,
+  module Language.Javascript.JMacro.Types
  ) where
 
 import Prelude hiding (tail, init, head, last, minimum, maximum, foldr1, foldl1, (!!), read)
@@ -77,3 +78,4 @@
 import Language.Javascript.JMacro.Base hiding (expr2stat)
 import Language.Javascript.JMacro.QQ
 import Language.Javascript.JMacro.Prelude
+import Language.Javascript.JMacro.Types (JType(..))
diff --git a/Language/Javascript/JMacro/Base.hs b/Language/Javascript/JMacro/Base.hs
--- a/Language/Javascript/JMacro/Base.hs
+++ b/Language/Javascript/JMacro/Base.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances, TypeFamilies, RankNTypes, DeriveDataTypeable, StandaloneDeriving, FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances, TypeFamilies, RankNTypes, DeriveDataTypeable, StandaloneDeriving, FlexibleContexts, TypeSynonymInstances #-}
 
 -----------------------------------------------------------------------------
 {- |
@@ -14,7 +14,7 @@
 
 module Language.Javascript.JMacro.Base (
   -- * ADT
-  JStat(..), JExpr(..), JVal(..), Ident(..),
+  JStat(..), JExpr(..), JVal(..), Ident(..), IdentSupply(..),
   -- * Generic traversal (via compos)
   JMacro(..), MultiComp(..), Compos(..),
   composOp, composOpM, composOpM_, composOpFold,
@@ -27,16 +27,18 @@
   -- * Literals
   jsv,
   -- * Occasionally helpful combinators
-  jLam, jVar, jFor, jForIn, jForEachIn, jTryCatchFinally,
+  jLam, jVar, jVarTy, jFor, jForIn, jForEachIn, jTryCatchFinally,
   expr2stat, ToStat(..), nullStat,
   -- * Hash combinators
   jhEmpty, jhSingle, jhAdd, jhFromList,
   -- * Utility
-  jsSaturate
+  jsSaturate, jtFromList
   ) where
 import Prelude hiding (tail, init, head, last, minimum, maximum, foldr1, foldl1, (!!), read)
 import Control.Applicative hiding (empty)
 import Data.Function
+import Data.Maybe (fromMaybe)
+import qualified Data.Set as S
 import qualified Data.Map as M
 import Text.PrettyPrint.HughesPJ
 import Control.Monad.State.Strict
@@ -45,10 +47,42 @@
 import Data.Generics
 import Data.Monoid
 
+import Language.Javascript.JMacro.Types
+
 {--------------------------------------------------------------------
   ADTs
 --------------------------------------------------------------------}
 
+newtype IdentSupply a = IS {runIdentSupply :: State [Ident] a} deriving Typeable
+
+inIdentSupply f x = IS $ f (runIdentSupply x)
+
+instance Data a => Data (IdentSupply a)
+instance Functor IdentSupply where
+    fmap f x = inIdentSupply (fmap f) x
+
+takeOne :: State [Ident] Ident
+takeOne = do
+  (x:xs) <- get
+  put xs
+  return x
+
+newIdentSupply :: Maybe String -> [Ident]
+newIdentSupply Nothing     = newIdentSupply (Just "jmId")
+newIdentSupply (Just pfx') = [StrI (pfx ++ show x) | x <- [(0::Integer)..]]
+    where pfx = pfx'++['_']
+
+sat_ :: IdentSupply a -> a
+sat_ x = evalState (runIdentSupply x) $ newIdentSupply (Just "<<unsatId>>")
+
+instance Eq a => Eq (IdentSupply a) where
+    (==) = (==) `on` sat_
+instance Ord a => Ord (IdentSupply a) where
+    compare = compare `on` sat_
+instance Show a => Show (IdentSupply a) where
+    show x = "(" ++ show (sat_ x) ++ ")"
+
+
 --switch
 --Yield statement?
 --destructuring/pattern matching functions --pattern matching in lambdas.
@@ -56,7 +90,7 @@
 --add postfix stat
 
 -- | Statements
-data JStat = DeclStat   Ident
+data JStat = DeclStat   Ident (Maybe JLocalType)
            | ReturnStat JExpr
            | IfStat     JExpr JStat JStat
            | WhileStat  JExpr JStat
@@ -67,11 +101,13 @@
            | ApplStat   JExpr [JExpr]
            | PostStat   String JExpr
            | AssignStat JExpr JExpr
-           | UnsatBlock (State [Ident] JStat)
+           | UnsatBlock (IdentSupply JStat)
            | AntiStat   String
+           | ForeignStat Ident JLocalType
            | BreakStat
              deriving (Eq, Ord, Show, Data, Typeable)
 
+
 instance Monoid JStat where
     mempty = BlockStat []
     mappend (BlockStat xs) (BlockStat ys) = BlockStat $ xs ++ ys
@@ -79,6 +115,8 @@
     mappend xs (BlockStat ys) = BlockStat $ xs : ys
     mappend xs ys = BlockStat [xs,ys]
 
+
+-- TODO: annotate expressions with type
 -- | Expressions
 data JExpr = ValExpr    JVal
            | SelExpr    JExpr Ident
@@ -88,8 +126,9 @@
            | IfExpr     JExpr JExpr JExpr
            | NewExpr    JExpr
            | ApplExpr   JExpr [JExpr]
-           | UnsatExpr  (State [Ident] JExpr)
+           | UnsatExpr  (IdentSupply JExpr)
            | AntiExpr   String
+           | TypeExpr   Bool JExpr JLocalType
              deriving (Eq, Ord, Show, Data, Typeable)
 
 -- | Values
@@ -101,17 +140,17 @@
           | JRegEx   String
           | JHash    (M.Map String JExpr)
           | JFunc    [Ident] JStat
-          | UnsatVal (State [Ident] JVal)
+          | UnsatVal (IdentSupply JVal)
             deriving (Eq, Ord, Show, Data, Typeable)
 
 -- | Identifiers
 newtype Ident = StrI String deriving (Eq, Ord, Show, Data, Typeable)
 
 
-deriving instance Typeable2 State
-deriving instance Data (State [Ident] JVal)
-deriving instance Data (State [Ident] JExpr)
-deriving instance Data (State [Ident] JStat)
+--deriving instance Typeable2 (StateT [Ident] Identity)
+--deriving instance Data (State [Ident] JVal)
+--deriving instance Data (State [Ident] JExpr)
+--deriving instance Data (State [Ident] JStat)
 
 
 
@@ -122,6 +161,7 @@
 expr2stat (AntiExpr x) = AntiStat x
 expr2stat _ = nullStat
 
+
 {--------------------------------------------------------------------
   Compos
 --------------------------------------------------------------------}
@@ -152,8 +192,6 @@
 composOpFold z c f = unC . compos (\_ -> C z) (\(C x) (C y) -> C (c x y)) (C . f)
 newtype C b a = C { unC :: b }
 
-
-
 instance JMacro Ident where
     toMC = MIdent
     fromMC (MIdent x) = x
@@ -183,7 +221,7 @@
     compos ret app f' v = case v of
         MIdent _ -> ret v
         MStat v' -> ret MStat `app` case v' of
-           DeclStat i -> ret DeclStat `app` f i
+           DeclStat i t -> ret DeclStat `app` f i `app` ret t
            ReturnStat i -> ret ReturnStat `app` f i
            IfStat e s s' -> ret IfStat `app` f e `app` f s `app` f s'
            WhileStat e s -> ret WhileStat `app` f e `app` f s
@@ -197,6 +235,7 @@
            AssignStat e e' -> ret AssignStat `app` f e `app` f e'
            UnsatBlock _ -> ret v'
            AntiStat _ -> ret v'
+           ForeignStat i t -> ret ForeignStat `app` f i `app` ret t
            BreakStat -> ret BreakStat
         MExpr v' -> ret MExpr `app` case v' of
            ValExpr e -> ret ValExpr `app` f e
@@ -208,6 +247,7 @@
            NewExpr e -> ret NewExpr `app` f e
            ApplExpr e xs -> ret ApplExpr `app` f e `app` mapM' f xs
            AntiExpr _ -> ret v'
+           TypeExpr b e t -> ret (TypeExpr b) `app` f e `app` ret t
            UnsatExpr _ -> ret v'
         MVal v' -> ret MVal `app` case v' of
            JVar i -> ret JVar `app` f i
@@ -225,51 +265,44 @@
         mapM' g = foldr (app . app (ret (:)) . g) (ret [])
         f x = ret fromMC `app` f' (toMC x)
 
+instance Compos JType where
+    compos ret app f v =
+        case v of
+          JTFunc args body -> ret JTFunc `app` mapM' f args `app` f body
+          JTForall vars t -> ret JTForall `app` ret vars `app` f t
+          JTList t -> ret JTList `app` f t
+          JTMap t -> ret JTMap `app` f t
+          JTRecord t m -> ret JTRecord `app` f t `app` m'
+              where (ls,ts) = unzip $ M.toList m
+                    m' = ret (M.fromAscList . zip ls) `app` mapM' f ts
+          x -> ret x
+      where
+        mapM' g = foldr (app . app (ret (:)) . g) (ret [])
 
+
 {--------------------------------------------------------------------
   New Identifiers
 --------------------------------------------------------------------}
 
-sat_ :: State [Ident] a -> a
-sat_ x = evalState x $ newIdentSupply (Just "<<unsatId>>")
-
-instance Eq a => Eq (State [Ident] a) where
-    (==) = (==) `on` sat_
-instance Ord a => Ord (State [Ident] a) where
-    compare = compare `on` sat_
-instance Show a => Show (State [Ident] a) where
-    show x = "(" ++ show (sat_ x) ++ ")"
-
 class ToSat a where
-    toSat_ :: a -> [Ident] -> State [Ident] (JStat, [Ident])
+    toSat_ :: a -> [Ident] -> IdentSupply (JStat, [Ident])
 
 instance ToSat [JStat] where
-    toSat_ f vs = return $ (BlockStat f, reverse vs)
+    toSat_ f vs = IS $ return $ (BlockStat f, reverse vs)
 
 instance ToSat JStat where
-    toSat_ f vs = return $ (f, reverse vs)
+    toSat_ f vs = IS $ return $ (f, reverse vs)
 
 instance ToSat JExpr where
-    toSat_ f vs = return $ (expr2stat f, reverse vs)
+    toSat_ f vs = IS $ return $ (expr2stat f, reverse vs)
 
 instance ToSat [JExpr] where
-    toSat_ f vs = return $ (BlockStat $ map expr2stat f, reverse vs)
+    toSat_ f vs = IS $ return $ (BlockStat $ map expr2stat f, reverse vs)
 
 instance (ToSat a, b ~ JExpr) => ToSat (b -> a) where
-    toSat_ f vs = do
+    toSat_ f vs = IS $ do
       x <- takeOne
-      toSat_ (f (ValExpr $ JVar x)) (x:vs)
-
-takeOne :: (Monad m, MonadState [b] m) => m b
-takeOne = do
-  (x:xs) <- get
-  put xs
-  return x
-
-newIdentSupply :: Maybe String -> [Ident]
-newIdentSupply Nothing     = newIdentSupply (Just "jmId")
-newIdentSupply (Just pfx') = [StrI (pfx ++ show x) | x <- [(0::Integer)..]]
-    where pfx = pfx'++['_']
+      runIdentSupply $ toSat_ (f (ValExpr $ JVar x)) (x:vs)
 
 {-
 splitIdentSupply :: ([Ident] -> ([Ident], [Ident]))
@@ -285,14 +318,14 @@
 -- | Given an optional prefix, fills in all free variable names with a supply
 -- of names generated by the prefix.
 jsSaturate :: (JMacro a) => Maybe String -> a -> a
-jsSaturate str x = evalState (jsSaturate_ x) (newIdentSupply str)
+jsSaturate str x = evalState (runIdentSupply $ jsSaturate_ x) (newIdentSupply str)
 
-jsSaturate_ :: (JMacro a) => a -> State [Ident] a
-jsSaturate_ e = fromMC <$> go (toMC e)
+jsSaturate_ :: (JMacro a) => a -> IdentSupply a
+jsSaturate_ e = IS $ fromMC <$> go (toMC e)
     where go v = case v of
-                   MStat (UnsatBlock us) -> go =<< (MStat <$> us)
-                   MExpr (UnsatExpr  us) -> go =<< (MExpr <$> us)
-                   MVal  (UnsatVal   us) -> go =<< (MVal  <$> us)
+                   MStat (UnsatBlock us) -> go =<< (MStat <$> runIdentSupply us)
+                   MExpr (UnsatExpr  us) -> go =<< (MExpr <$> runIdentSupply us)
+                   MVal  (UnsatVal   us) -> go =<< (MVal  <$> runIdentSupply us)
                    _ -> composOpM go v
 
 {--------------------------------------------------------------------
@@ -308,8 +341,8 @@
           mp = M.fromList xs
 
 --only works on fully saturated things
-jsUnsat_ :: JMacro a => [Ident] -> a -> State [Ident] a
-jsUnsat_ xs e = do
+jsUnsat_ :: JMacro a => [Ident] -> a -> IdentSupply a
+jsUnsat_ xs e = IS $ do
   (idents,is') <- splitAt (length xs) <$> get
   put is'
   return $ jsReplace_ (zip xs idents) e
@@ -324,7 +357,7 @@
               MExpr _  -> toMC $ UnsatExpr  (coerceMC <$> jsUnsat_ is' x'')
               MVal  _  -> toMC $ UnsatVal   (coerceMC <$> jsUnsat_ is' x'')
               MIdent _ -> toMC $ f x
-    where (x', (StrI l:_)) = runState (jsSaturate_ x) is
+    where (x', (StrI l:_)) = runState (runIdentSupply $ jsSaturate_ x) is
           x'' = f x'
           is = newIdentSupply (Just "inSat")
           lastVal = readNote "inSat" (drop 6 l) :: Int
@@ -343,14 +376,14 @@
                    (MStat (BlockStat ss)) -> MStat . BlockStat <$>
                                              blocks ss
                        where blocks [] = return []
-                             blocks (DeclStat (StrI i) : xs) =  case i of
-                                ('!':'!':i') -> (DeclStat (StrI i'):) <$> blocks xs
-                                ('!':i') -> (DeclStat (StrI i'):) <$> blocks xs
+                             blocks (DeclStat (StrI i) t : xs) =  case i of
+                                ('!':'!':i') -> (DeclStat (StrI i') t:) <$> blocks xs
+                                ('!':i') -> (DeclStat (StrI i') t:) <$> blocks xs
                                 _ -> do
                                   (newI:st) <- get
                                   put st
                                   rest <- blocks xs
-                                  return $ [DeclStat newI `mappend` jsReplace_ [(StrI i, newI)] (BlockStat rest)]
+                                  return $ [DeclStat newI t `mappend` jsReplace_ [(StrI i, newI)] (BlockStat rest)]
                              blocks (x':xs) = (fromMC <$> go (toMC x')) <:> blocks xs
                              (<:>) = liftM2 (:)
                    (MStat (ForInStat b (StrI i) e s)) -> do
@@ -396,7 +429,10 @@
     jsToDoc (IfStat cond x y) = text "if" <> parens (jsToDoc cond) $$ braceNest' (jsToDoc x) $$ mbElse
         where mbElse | y == BlockStat []  = empty
                      | otherwise = text "else" $$ braceNest' (jsToDoc y)
-    jsToDoc (DeclStat x) = text "var" <+> jsToDoc x
+    jsToDoc (DeclStat x t) = text "var" <+> jsToDoc x <> rest
+        where rest = case t of
+                       Nothing -> text ""
+                       Just tp -> text " /* ::" <+> jsToDoc tp <+> text "*/"
     jsToDoc (WhileStat p b)  = text "while" <> parens (jsToDoc p) $$ braceNest' (jsToDoc b)
     jsToDoc (UnsatBlock e) = jsToDoc $ sat_ e
     jsToDoc BreakStat = text "break"
@@ -416,6 +452,7 @@
     jsToDoc (AssignStat i x) = jsToDoc i <+> char '=' <+> jsToDoc x
     jsToDoc (PostStat op x) = jsToDoc x <> text op
     jsToDoc (AntiStat s) = text $ "`(" ++ s ++ ")`"
+    jsToDoc (ForeignStat i t) = text "//foriegn" <+> jsToDoc i <+> text "::" <+> jsToDoc t
     jsToDoc (BlockStat xs) = jsToDoc (flattenBlocks xs)
         where flattenBlocks (BlockStat y:ys) = flattenBlocks y ++ flattenBlocks ys
               flattenBlocks (y:ys) = y : flattenBlocks ys
@@ -426,11 +463,15 @@
     jsToDoc (SelExpr x y) = cat [jsToDoc x <> char '.', jsToDoc y]
     jsToDoc (IdxExpr x y) = jsToDoc x <> brackets (jsToDoc y)
     jsToDoc (IfExpr x y z) = parens (jsToDoc x <+> char '?' <+> jsToDoc y <+> char ':' <+> jsToDoc z)
-    jsToDoc (InfixExpr op x y) = parens $ sep [jsToDoc x, text op, jsToDoc y]
+    jsToDoc (InfixExpr op x y) = parens $ sep [jsToDoc x, text op', jsToDoc y]
+        where op' | op == "++" = "+"
+                  | otherwise = op
+
     jsToDoc (PostExpr op x) = jsToDoc x <> text op
     jsToDoc (ApplExpr je xs) = jsToDoc je <> (parens . fsep . punctuate comma $ map jsToDoc xs)
     jsToDoc (NewExpr e) = text "new" <+> jsToDoc e
     jsToDoc (AntiExpr s) = text $ "`(" ++ s ++ ")`"
+    jsToDoc (TypeExpr b e t)  = parens $ jsToDoc e <+> text (if b then "/* ::!" else "/* ::") <+> jsToDoc t <+> text "*/"
     jsToDoc (UnsatExpr e) = jsToDoc $ sat_ e
 
 instance JsToDoc JVal where
@@ -455,10 +496,50 @@
 instance JsToDoc [JStat] where
     jsToDoc = vcat . map ((<> semi) . jsToDoc)
 
+instance JsToDoc JType where
+    jsToDoc JTNum = text "Num"
+    jsToDoc JTString = text "String"
+    jsToDoc JTBool = text "Bool"
+    jsToDoc JTStat = text "()"
+    jsToDoc JTImpossible = text "_|_" -- "⊥"
+    jsToDoc (JTForall vars t) = text "forall" <+> fsep  (punctuate comma (map ppRef vars)) <> text "." <+> jsToDoc t
+    jsToDoc (JTFunc args ret) = fsep . punctuate (text " ->") . map ppType $ args' ++ [ret]
+        where args'
+               | null args = [JTStat]
+               | otherwise = args
+    jsToDoc (JTList t) = brackets $ jsToDoc t
+    jsToDoc (JTMap t) = text "Map" <+> ppType t
+    jsToDoc (JTRecord t mp) = braces (fsep . punctuate comma . map (\(x,y) -> text x <+> text "::" <+> jsToDoc y) $ M.toList mp) <+> text "[" <> jsToDoc t <> text "]"
+    jsToDoc (JTFree ref) = ppRef ref
+    jsToDoc (JTRigid ref cs) = text "[" <> ppRef ref <> text "]"
+{-
+        maybe (text "") (text " / " <>)
+                  (ppConstraintList . map (\x -> (ref,x)) $ S.toList cs) <>
+        text "]"
+-}
+
+instance JsToDoc JLocalType where
+    jsToDoc (cs,t) = maybe (text "") (<+> text "=> ") (ppConstraintList cs) <> jsToDoc t
+
+ppConstraintList cs
+    | null cs = Nothing
+    | otherwise = Just . parens . fsep . punctuate comma $ map go cs
+    where
+      go (vr,Sub   t') = ppRef vr   <+> text "<:" <+> jsToDoc t'
+      go (vr,Super t') = jsToDoc t' <+> text "<:" <+> ppRef vr
+
+
+ppRef (Just n,_) = text n
+ppRef (_,i) = text $ "t_"++show i
+ppType x@(JTFunc _ _) = parens $ jsToDoc x
+ppType x@(JTMap _) = parens $ jsToDoc x
+ppType x = jsToDoc x
+
 {--------------------------------------------------------------------
   ToJExpr Class
 --------------------------------------------------------------------}
 
+
 -- | Things that can be marshalled into javascript values.
 -- Instantiate for any necessary data structures.
 class ToJExpr a where
@@ -547,8 +628,8 @@
 -- Usage:
 -- @jLam $ \ x y -> {JExpr involving x and y}@
 jLam :: (ToSat a) => a -> JExpr
-jLam f = ValExpr . UnsatVal $ do
-           (block,is) <- toSat_ f []
+jLam f = ValExpr . UnsatVal . IS $ do
+           (block,is) <- runIdentSupply $ toSat_ f []
            return $ JFunc is block
 
 -- | Introduce a new variable into scope for the duration
@@ -556,31 +637,44 @@
 -- Usage:
 -- @jVar $ \ x y -> {JExpr involving x and y}@
 jVar :: (ToSat a) => a -> JStat
-jVar f = UnsatBlock $ do
-           (block, is) <- toSat_ f []
+jVar f = UnsatBlock . IS $ do
+           (block, is) <- runIdentSupply $ toSat_ f []
            let addDecls (BlockStat ss) =
-                  BlockStat $ map DeclStat is ++ ss
+                  BlockStat $ map (\x -> DeclStat x Nothing) is ++ ss
                addDecls x = x
            return $ addDecls block
 
 
+-- | Introduce a new variable with optional type into scope for the duration
+-- of the enclosed expression. The result is a block statement.
+-- Usage:
+-- @jVar $ \ x y -> {JExpr involving x and y}@
+jVarTy :: (ToSat a) => a -> (Maybe JLocalType) -> JStat
+jVarTy f t = UnsatBlock . IS $ do
+           (block, is) <- runIdentSupply $ toSat_ f []
+           let addDecls (BlockStat ss) =
+                  BlockStat $ map (\x -> DeclStat x t) is ++ ss
+               addDecls x = x
+           return $ addDecls block
+
+
 -- | Create a for in statement.
 -- Usage:
 -- @jForIn {expression} $ \x -> {block involving x}@
 jForIn :: ToSat a => JExpr -> (JExpr -> a) -> JStat
-jForIn e f = UnsatBlock $ do
-               (block, is) <- toSat_ f []
+jForIn e f = UnsatBlock . IS $ do
+               (block, is) <- runIdentSupply $ toSat_ f []
                return $ ForInStat False (headNote "jForIn" is) e block
 
 -- | As with "jForIn" but creating a \"for each in\" statement.
 jForEachIn :: ToSat a => JExpr -> (JExpr -> a) -> JStat
-jForEachIn e f = UnsatBlock $ do
-               (block, is) <- toSat_ f []
+jForEachIn e f = UnsatBlock . IS $ do
+               (block, is) <- runIdentSupply $ toSat_ f []
                return $ ForInStat True (headNote "jForIn" is) e block
 
 jTryCatchFinally :: (ToSat a) => JStat -> a -> JStat -> JStat
-jTryCatchFinally s f s2 = UnsatBlock $ do
-                     (block, is) <- toSat_ f []
+jTryCatchFinally s f s2 = UnsatBlock . IS $ do
+                     (block, is) <- runIdentSupply $ toSat_ f []
                      return $ TryStat s (headNote "jTryCatch" is) block s2
 
 jsv :: String -> JExpr
@@ -603,6 +697,9 @@
 
 jhFromList :: [(String, JExpr)] -> JVal
 jhFromList = JHash . M.fromList
+
+jtFromList :: JType -> [(String, JType)] -> JType
+jtFromList t y = JTRecord t $ M.fromList y
 
 nullStat :: JStat
 nullStat = BlockStat []
diff --git a/Language/Javascript/JMacro/Executable.hs b/Language/Javascript/JMacro/Executable.hs
--- a/Language/Javascript/JMacro/Executable.hs
+++ b/Language/Javascript/JMacro/Executable.hs
@@ -27,6 +27,6 @@
 
     fixIdent x = fromMC $ composOp go (toMC x) :: JStat
         where go v = case v of
-                       (MStat (DeclStat (StrI ('!':'!':i')))) -> MStat (DeclStat (StrI i'))
-                       (MStat (DeclStat (StrI ('!':i')))) -> MStat (DeclStat (StrI i'))
+                       (MStat (DeclStat (StrI ('!':'!':i')) t)) -> MStat (DeclStat (StrI i') t)
+                       (MStat (DeclStat (StrI ('!':i')) t)) -> MStat (DeclStat (StrI i') t)
                        _ -> composOp go v
diff --git a/Language/Javascript/JMacro/ParseTH.hs b/Language/Javascript/JMacro/ParseTH.hs
--- a/Language/Javascript/JMacro/ParseTH.hs
+++ b/Language/Javascript/JMacro/ParseTH.hs
@@ -1,19 +1,21 @@
-module Language.Javascript.JMacro.ParseTH where
+module Language.Javascript.JMacro.ParseTH (parseHSExp) where
 
---import Language.Haskell.Meta.Parse
+import Language.Haskell.Meta.Parse
 import qualified Language.Haskell.TH as TH
-import Language.Haskell.Exts.Translate
-import Language.Haskell.Exts.Parser
-import Language.Haskell.Exts.Extension
-import Language.Haskell.Exts.Annotated.Fixity
-import qualified Language.Haskell.Exts.Syntax as Hs
+-- import Language.Haskell.Exts.Translate
+-- import Language.Haskell.Exts.Parser
+-- import Language.Haskell.Exts.Extension
+-- import Language.Haskell.Exts.Annotated.Fixity
+-- import qualified Language.Haskell.Exts.Syntax as Hs
 
 parseHSExp :: String -> Either String TH.Exp
-parseHSExp = fmap toExp . parseResultToEither . parseExpWithMode myDefaultParseMode
+--for haskell-src-exts-qq
+--parseHSExp = fmap toExp . parseResultToEither . parseExpWithMode myDefaultParseMode
 
 --for Language.Haskell.Meta
---parseHSExp = parseExp
+parseHSExp = parseExp
 
+{-
 parseResultToEither :: ParseResult a -> Either String a
 parseResultToEither (ParseOk a) = Right a
 parseResultToEither (ParseFailed loc e)
@@ -39,3 +41,4 @@
                       ,RankNTypes
                       ,MultiParamTypeClasses
                       ,RecursiveDo]
+-}
diff --git a/Language/Javascript/JMacro/QQ.hs b/Language/Javascript/JMacro/QQ.hs
--- a/Language/Javascript/JMacro/QQ.hs
+++ b/Language/Javascript/JMacro/QQ.hs
@@ -37,9 +37,10 @@
 import Text.Regex.PCRE.Light (compileM)
 
 import Language.Javascript.JMacro.Base
+import Language.Javascript.JMacro.Types
 import Language.Javascript.JMacro.ParseTH
 
--- import Debug.Trace
+import Debug.Trace
 
 {--------------------------------------------------------------------
   QuasiQuotation
@@ -47,11 +48,11 @@
 
 -- | QuasiQuoter for a block of JMacro statements.
 jmacro :: QuasiQuoter
-jmacro = QuasiQuoter quoteJMExp quoteJMPat
+jmacro = QuasiQuoter {quoteExp = quoteJMExp, quotePat = quoteJMPat}
 
 -- | QuasiQuoter for a JMacro expression.
 jmacroE :: QuasiQuoter
-jmacroE = QuasiQuoter quoteJMExpE quoteJMPatE
+jmacroE = QuasiQuoter {quoteExp = quoteJMExpE, quotePat = quoteJMPatE}
 
 quoteJMPat :: String -> TH.PatQ
 quoteJMPat s = case parseJM s of
@@ -89,7 +90,7 @@
 antiIdent :: JMacro a => String -> a -> a
 antiIdent s e = fromMC $ go (toMC e)
     where go (MExpr (ValExpr (JVar (StrI s'))))
-             | s == s' = MExpr (AntiExpr s)
+             | s == s' = MExpr (AntiExpr $ fixIdent s)
           go (MExpr (SelExpr x i)) =
               MExpr (SelExpr (antiIdent s x) i)
           go x = composOp go x
@@ -98,12 +99,21 @@
 antiIdents ss x = foldr antiIdent x ss
 
 
+fixIdent css@(c:_)
+    | isUpper c = '_' : escapeDollar css
+    | otherwise = escapeDollar css
+  where
+    escapeDollar = map (\x -> if x =='$' then 'dž' else x)
+fixIdent _ = "_"
+
+
 jm2th :: Data a => a -> TH.ExpQ
 jm2th v = dataToExpQ (const Nothing
                       `extQ` handleStat
                       `extQ` handleExpr
                       `extQ` handleVal
                       `extQ` handleStr
+                      `extQ` handleTyp
                      ) v
 
     where handleStat :: JStat -> Maybe (TH.ExpQ)
@@ -112,29 +122,32 @@
                                       TH.listE (blocks ss)
               where blocks :: [JStat] -> [TH.ExpQ]
                     blocks [] = []
-                    blocks (DeclStat (StrI i):xs) = case i of
-                     ('!':'!':i') -> jm2th (DeclStat (StrI i')) : blocks xs
+                    blocks (DeclStat (StrI i) t:xs) = case i of
+                     ('!':'!':i') -> jm2th (DeclStat (StrI i') t) : blocks xs
                      ('!':i') ->
                         [TH.appE (TH.lamE [TH.varP . mkName . fixIdent $ i'] $
                                  appConstr "BlockStat"
                                  (TH.listE . (ds:) . blocks $ xs)) (TH.appE (TH.varE $ mkName "jsv")
                                                                             (TH.litE $ TH.StringL i'))]
-                        where ds = TH.appE (TH.conE $ mkName "DeclStat")
-                                           (TH.appE (TH.conE $ mkName "StrI")
-                                                  (TH.litE $ TH.StringL i'))
+                        where ds =
+                                  TH.appE
+                                        (TH.appE (TH.conE $ mkName "DeclStat")
+                                               (TH.appE (TH.conE $ mkName "StrI")
+                                                      (TH.litE $ TH.StringL i')))
+                                        (jm2th t)
                      _ ->
-                        [TH.appE (TH.varE $ mkName "jVar")
-                              (TH.lamE [TH.varP . mkName . fixIdent $ i] $
-                                 appConstr "BlockStat"
-                                 (TH.listE $ blocks $ map (antiIdent i) xs))]
+                        [TH.appE
+                           (TH.appE (TH.varE $ mkName "jVarTy")
+                                  (TH.lamE [TH.varP . mkName . fixIdent $ i] $
+                                     appConstr "BlockStat"
+                                     (TH.listE $ blocks $ map (antiIdent i) xs)))
+                           (jm2th t)
+                        ]
 
                     blocks (x:xs) = jm2th x : blocks xs
 
 
-                    fixIdent css@(c:_)
-                        | isUpper c = '_' : css
-                        | otherwise = css
-                    fixIdent _ = "_"
+
           handleStat (ForInStat b (StrI i) e s) = Just $
                  appFun (TH.varE $ forFunc)
                         [jm2th e,
@@ -159,6 +172,7 @@
                                       Right ans -> Just $ TH.appE (TH.varE (mkName "toStat"))
                                                                   (return ans)
                                       Left err -> Just $ fail err
+
           handleStat _ = Nothing
 
           handleExpr :: JExpr -> Maybe (TH.ExpQ)
@@ -182,6 +196,13 @@
           handleStr :: String -> Maybe (TH.ExpQ)
           handleStr x = Just $ TH.litE $ TH.StringL x
 
+          handleTyp :: JType -> Maybe (TH.ExpQ)
+          handleTyp (JTRecord t mp) = Just $
+                                    TH.appE (TH.appE (TH.varE $ mkName "jtFromList") (jm2th t))
+                                          (jm2th $ M.toList mp)
+
+          handleTyp _ = Nothing
+
           appFun x = foldl (TH.appE) x
           appConstr n = TH.appE (TH.conE $ mkName n)
 
@@ -204,8 +225,8 @@
 
 jsLang :: P.LanguageDef ()
 jsLang = javaStyle {
-           P.reservedNames = ["var","return","if","else","while","for","in","break","new","function","switch","case","default","fun","try","catch","finally"],
-           P.reservedOpNames = ["--","*","/","+","-",".","%","?","=","==","!=","<",">","&&","||","++","===",">=","<=","->"],
+           P.reservedNames = ["var","return","if","else","while","for","in","break","new","function","switch","case","default","fun","try","catch","finally","foreign"],
+           P.reservedOpNames = ["--","*","/","+","-",".","%","?","=","==","!=","<",">","&&","||","++","===",">=","<=","->","::","::!"],
            P.identLetter = alphaNum <|> oneOf "_$",
            P.identStart  = letter <|> oneOf "_$",
            P.commentLine = "//",
@@ -259,14 +280,25 @@
   return (StrI i)
 -}
 
-varidentdecl :: JMParser Ident
+
+getType = do
+  isForce <- (reservedOp "::!" >> return True) <|> (reservedOp "::" >> return False)
+  t <- runTypeParser
+  return (isForce, t)
+
+addForcedType (Just (True,t)) e = TypeExpr True e t
+addForcedType _ e = e
+
+--function !foo or function foo or var !x or var x, with optional type
+varidentdecl :: JMParser (Ident, Maybe (Bool, JLocalType))
 varidentdecl = do
   i <- identifierWithBang
   when ("jmId_" `isPrefixOf` i || "!jmId_" `isPrefixOf` i) $ fail "Illegal use of reserved jmId_ prefix in variable name."
   when (i=="this" || i=="!this") $ fail "Illegal attempt to name variable 'this'."
-  return (StrI i)
-
+  t <- optionMaybe getType
+  return (StrI i, t)
 
+--any other identifier decl
 identdecl :: JMParser Ident
 identdecl = do
   i <- identifier
@@ -274,14 +306,15 @@
   when (i=="this") $ fail "Illegal attempt to name variable 'this'."
   return (StrI i)
 
+--varidentdecls can take types!
 identAssignDecl :: JMParser [JStat]
-identAssignDecl = varidentdecl >>= \i ->
-                  (do
+identAssignDecl = do
+  (i,mbTyp) <- varidentdecl
+  optAssignStat <- optionMaybe $ do
                     reservedOp "="
                     e <- expr
-                    return [DeclStat i, AssignStat (ValExpr (JVar (clean i))) e]
-                  )
-                  <|> return [DeclStat i]
+                    return $ AssignStat (ValExpr (JVar (clean i))) (addForcedType mbTyp e)
+  return $ DeclStat i (fmap snd mbTyp) : maybe [] (:[]) optAssignStat
     where clean (StrI ('!':x)) = StrI x
           clean x = x
 
@@ -297,6 +330,7 @@
 statement = declStat
             <|> funDecl
             <|> functionDecl
+            <|> foreignStat
             <|> returnStat
             <|> ifStat
             <|> whileStat
@@ -313,26 +347,37 @@
       declStat = do
         reserved "var"
         res <- concat <$> commaSep1 identAssignDecl
-        semi
+        _ <- semi
         return res
 
       functionDecl = do
         reserved "function"
-        n <- varidentdecl
+
+        (i,mbTyp) <- varidentdecl
         as <- parens (commaSep identdecl) <|> many1 identdecl
         b <- try (ReturnStat <$> braces expr) <|> (l2s <$> statement)
-        return $ [DeclStat n, AssignStat (ValExpr $ JVar (clean n)) (ValExpr $ JFunc as b)]
+        return $ [DeclStat i (fmap snd mbTyp),
+                  AssignStat (ValExpr $ JVar (clean i)) (addForcedType mbTyp $ ValExpr $ JFunc as b)]
             where clean (StrI ('!':x)) = StrI x
                   clean x = x
 
       funDecl = do
         reserved "fun"
         n <- identdecl
+        mbTyp <- optionMaybe getType
         as <- many identdecl
         b <- try (ReturnStat <$> braces expr) <|> (l2s <$> statement) <|> (symbol "->" >> ReturnStat <$> expr)
-        return $ [DeclStat (addBang n), AssignStat (ValExpr $ JVar n) (ValExpr $ JFunc as b)]
+        return $ [DeclStat (addBang n) (fmap snd mbTyp),
+                  AssignStat (ValExpr $ JVar n) (addForcedType mbTyp $ ValExpr $ JFunc as b)]
+
             where addBang (StrI x) = StrI ('!':'!':x)
 
+      foreignStat = do
+          reserved "foreign"
+          i <- try $ identdecl <* reservedOp "::"
+          t <- runTypeParser
+          return [ForeignStat i t]
+
       returnStat =
         reserved "return" >> (:[]) . ReturnStat <$> expr
 
@@ -420,6 +465,7 @@
           e2 <- expr
           return [AssignStat e1 e2]
 
+
       applStat = expr2stat' =<< expr
 
 --fixme: don't handle ifstats
@@ -448,26 +494,33 @@
 
 expr :: JMParser JExpr
 expr = do
-    e <- expr'
-    addIf e <|> return e
-  where addIf e = do
-          symbol "?"
-          t <- expr
-          colon
-          el <- expr
+  e <- exprWithIf
+  addType e
+  where
+    addType e = do
+         optTyp <- optionMaybe getType
+         case optTyp of
+           (Just (b,t)) -> return $ TypeExpr b e t
+           Nothing -> return e
+    exprWithIf = do
+         e <- rawExpr
+         addIf e <|> return e
+    addIf e = do
+          reservedOp "?"
+          t <- exprWithIf
+          _ <- colon
+          el <- exprWithIf
           let ans = (IfExpr e t el)
           addIf ans <|> return ans
-
-        expr' = buildExpressionParser table dotExpr <?> "expression"
-
-        table = [[iop "*", iop "/", iop "%"],
-                 [iop "+", iop "-"],
-                 [iope "==", iope "!=", iope "<", iope ">",
-                  iope ">=", iope "<=", iope "==="],
-                 [iop "&&", iop "||"]
-                ]
-        iop  s  = Infix (reservedOp s >> return (InfixExpr s)) AssocLeft
-        iope s  = Infix (reservedOp s >> return (InfixExpr s)) AssocNone
+    rawExpr = buildExpressionParser table dotExpr <?> "expression"
+    table = [[iop "*", iop "/", iop "%"],
+             [iop "++", iop "+", iop "-"],
+             [iope "==", iope "!=", iope "<", iope ">",
+              iope ">=", iope "<=", iope "==="],
+             [iop "&&", iop "||"]
+            ]
+    iop  s  = Infix (reservedOp s >> return (InfixExpr s)) AssocLeft
+    iope s  = Infix (reservedOp s >> return (InfixExpr s)) AssocNone
 
 dotExpr :: JMParser JExpr
 dotExpr = do
@@ -483,13 +536,15 @@
     addNxt e = do
             nxt <- (Just <$> lookAhead anyChar <|> return Nothing)
             case nxt of
-              Just '.' -> addNxt =<< (dot >> (SelExpr e <$> ident'))
+              Just '.' -> addNxt =<< (dot >> (SelExpr e <$> (ident' <|> numIdent)))
               Just '[' -> addNxt =<< (IdxExpr e <$> brackets' expr)
               Just '(' -> addNxt =<< (ApplExpr e <$> args')
               Just '-' -> try (reservedOp "--" >> return (PostExpr "--" e)) <|> return e
               Just '+' -> try (reservedOp "++" >> return (PostExpr "++" e)) <|> return e
               _   -> return e
 
+    numIdent = StrI <$> many1 digit
+
     notExpr = try (symbol "!" >> dotExpr) >>= \e ->
               return (ApplExpr (ValExpr (JVar (StrI "!"))) [e])
 
@@ -598,7 +653,7 @@
     fraction        = char '.' >> (foldr op 0.0 <$> many1 digit <?> "fraction")
                     where
                       op d f    = (f + fromIntegral (digitToInt d))/10.0
-    exponent'       = do oneOf "eE"
+    exponent'       = do _ <- oneOf "eE"
                          f <- sign
                          power . f <$> decimal
                     where
@@ -617,9 +672,9 @@
 
 myStringLiteral :: Char -> JMParser String
 myStringLiteral t = do
-    char t
+    _ <- char t
     x <- concat <$> many myChar
-    char t
+    _ <- char t
     return x
  where myChar = do
          c <- noneOf [t]
@@ -632,9 +687,9 @@
 
 myStringLiteralNoBr :: Char -> JMParser String
 myStringLiteralNoBr t = do
-    char t
+    _ <- char t
     x <- concat <$> many myChar
-    char t
+    _ <- char t
     return x
  where myChar = do
          c <- noneOf [t,'\n']
diff --git a/Language/Javascript/JMacro/Rpc.hs b/Language/Javascript/JMacro/Rpc.hs
--- a/Language/Javascript/JMacro/Rpc.hs
+++ b/Language/Javascript/JMacro/Rpc.hs
@@ -30,10 +30,17 @@
 > testRPCCall :: String -> JExpr -> JExpr -> JExpr
 > (testRPC, testRPCCall) = mkWebRPC "test" $ \x y -> asIO $ return (x + (y::Int))
 
+This code uses a simple request/response type based on strings to be as agnostic as possible about choice of web service stack. It can be used as is, or used as a model for code which targets a particular web stack (Happstack, Snap, FastCGI, etc.).
+
+The jQuery Javascript library is used to handle ajax requests, and hence pages which embed RPC calls must have the jQuery javascript library loaded.
+
 -}
 
 module Language.Javascript.JMacro.Rpc (
-   mkWebRPC, asIO, Request, Response(..)
+  -- * API
+  mkWebRPC, asIO, Request, Response(..), WebRPCDesc,
+  -- * Helper Classes
+  CallWebRPC(..),ToWebRPC(..)
 ) where
 
 import Prelude hiding (tail, init, head, last, minimum, maximum, foldr1, foldl1, (!!), read)
@@ -50,7 +57,7 @@
 -- | A String containing a json representation of function arguments encoded as a list of parameters. Generally would be passed as part of an HTTP request.
 type Request = String
 
--- | Either a success or failure (with code). Generally would be turned back into a propre HTTP response.
+-- | Either a success or failure (with code). Generally would be turned back into a proper HTTP response.
 data Response = GoodResponse String
               | BadResponse Int String
 
@@ -59,29 +66,29 @@
 respCode c e = BadResponse c e
 badData e = return $ respCode 400 ("Bad Data format: " ++ e)
 
-class ToWebRPC_ a where
+class ToWebRPC a where
     toWebRPC_ :: a -> ([JSValue] -> IO Response)
 
-instance (JSON b) => ToWebRPC_ (IO b) where
+instance (JSON b) => ToWebRPC (IO b) where
     toWebRPC_ f _ =  returnResp =<< f
 
-instance (JSON a, ToWebRPC_ b) => ToWebRPC_ (a -> b) where
+instance (JSON a, ToWebRPC b) => ToWebRPC (a -> b) where
     toWebRPC_ f (x:xs) = case readJSON x of
                            Ok v -> toWebRPC_ (f v) xs
                            Error s -> badData s
     toWebRPC_ _ _ = badData "missing parameter"
 
-toWebRPC :: ToWebRPC_ a => a -> Request -> IO Response
+toWebRPC :: ToWebRPC a => a -> Request -> IO Response
 toWebRPC f = \req -> case runGetJSON readJSArray req of
                        (Right (JSArray xs)) ->f' xs
                        (Left e) -> badData e
                        _ -> badData "toWebRPC error"
     where f' = toWebRPC_ f
 
-class CallWebRPC_ a b | a -> b where
+class CallWebRPC a b | a -> b where
     callWebRPC_ :: [JExpr] -> String -> a -> b
 
-instance CallWebRPC_ (IO b) JExpr where
+instance CallWebRPC (IO b) JExpr where
     callWebRPC_ xs serverLoc _ =
         [$jmacroE|
          (\() { var res;
@@ -96,14 +103,14 @@
                 return res;
                }())|]
 
-instance (CallWebRPC_ b c, ToJExpr d) => CallWebRPC_ (a -> b) (d -> c) where
+instance (CallWebRPC b c, ToJExpr d) => CallWebRPC (a -> b) (d -> c) where
     callWebRPC_ xs serverLoc f = \x -> callWebRPC_ (toJExpr x : xs) serverLoc (f undefined)
 
-callWebRPC :: (CallWebRPC_ a b) => String -> a -> b
+callWebRPC :: (CallWebRPC a b) => String -> a -> b
 callWebRPC s f = callWebRPC_ [] s f
 
 -- | Produce a pair of (ServerFunction, ClientFunction) from a function in IO
-mkWebRPC :: (ToWebRPC_ a, CallWebRPC_ a b) => String -> a -> (WebRPCDesc, String -> b)
+mkWebRPC :: (ToWebRPC a, CallWebRPC a b) => String -> a -> (WebRPCDesc, String -> b)
 mkWebRPC name rpcFun = ((name,toWebRPC rpcFun), \server -> callWebRPC (server ++ "/" ++ name) rpcFun)
 
 
diff --git a/Language/Javascript/JMacro/TypeCheck.hs b/Language/Javascript/JMacro/TypeCheck.hs
new file mode 100644
--- /dev/null
+++ b/Language/Javascript/JMacro/TypeCheck.hs
@@ -0,0 +1,915 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving, FlexibleInstances, PatternGuards #-}
+
+module Language.Javascript.JMacro.TypeCheck where
+
+import Language.Javascript.JMacro.Base
+import Language.Javascript.JMacro.Types
+import Language.Javascript.JMacro.QQ
+
+import Control.Applicative
+import Control.Arrow((&&&))
+import Control.Monad
+import Control.Monad.State
+import Control.Monad.Reader
+import Control.Monad.Writer
+import Control.Monad.Error
+import Data.Either
+import Data.Map (Map)
+import Data.Maybe(catMaybes, fromMaybe)
+import Data.List(intercalate, nub, transpose)
+import qualified Data.Traversable as T
+import qualified Data.Foldable as F
+import qualified Data.Map as M
+import Data.Set(Set)
+import qualified Data.Set as S
+
+import Text.PrettyPrint.HughesPJ
+
+import Debug.Trace
+
+-- Utility
+
+isLeft (Left _) = True
+isLeft _ = False
+
+partitionOut :: (a -> Maybe b) -> [a] -> ([b],[a])
+partitionOut f xs' = foldr go ([],[]) xs'
+    where go x ~(bs,as)
+             | Just b <- f x = (b:bs,as)
+             | otherwise = (bs,x:as)
+
+zipWithOrChange :: (a -> a -> b) -> (a -> b) -> [a] -> [a] -> [b]
+zipWithOrChange f g xss yss = go xss yss
+    where go (x:xs) (y:ys) = f x y : go xs ys
+          go xs@(_:_) _ = map g xs
+          go _ ys = map g ys
+
+zipWithOrIdM :: Monad m => (a -> a -> m a) -> [a] -> [a] -> m [a]
+zipWithOrIdM f xs ys = sequence $ zipWithOrChange f return xs ys
+
+unionWithM :: (Monad m, Ord key) => (val -> val -> m val) -> Map key val -> Map key val -> m (Map key val)
+unionWithM f m1 m2 = T.sequence $ M.unionWith (\xm ym -> join $ liftM2 f xm ym) (M.map return m1) (M.map return m2)
+
+intersectionWithM :: (Monad m, Ord key) => (val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
+intersectionWithM f m1 m2 = T.sequence $ M.intersectionWith f m1 m2
+
+-- Basic Types and TMonad
+data StoreVal = SVType JType
+              | SVConstrained (Set Constraint)
+              -- | SVFreshType Int
+                deriving Show
+
+data TCState = TCS {tc_env :: [Map Ident JType],
+                    tc_vars :: Map Int StoreVal,
+                    tc_stack :: [Set Int],
+                    tc_frozen :: Set Int,
+                    tc_varCt :: Int,
+                    tc_context :: [TMonad String]}
+
+instance Show TCState where
+    show (TCS env vars stack frozen varCt cxt) =
+        "env: " ++ show env ++ "\n" ++
+        "vars: " ++ show vars ++ "\n" ++
+        "stack: " ++ show stack ++ "\n" ++
+        "frozen: " ++ show frozen ++ "\n" ++
+        "varCt: " ++ show varCt
+
+tcStateEmpty = TCS [M.empty] M.empty [S.empty] S.empty 0 []
+
+newtype TMonad a = TMonad (ErrorT String (State TCState) a) deriving (Functor, Monad, MonadState TCState, MonadError String)
+
+instance Applicative TMonad where
+    pure = return
+    (<*>) = ap
+
+class JTypeCheck a where
+    typecheck :: a -> TMonad JType
+
+evalTMonad (TMonad x) = evalState (runErrorT x) tcStateEmpty
+
+runTMonad (TMonad x) = runState (runErrorT x) tcStateEmpty
+
+withContext :: TMonad a -> TMonad String -> TMonad a
+withContext act cxt = do
+  cs <- tc_context <$> get
+  modify (\s -> s {tc_context = cxt : cs})
+  res <- act
+  modify (\s -> s {tc_context = cs})
+  return res
+
+traversem_ :: (F.Foldable t, Monad f) => (a -> f b) -> t a -> f ()
+traversem_ f = F.foldr ((>>) . f) (return ())
+
+--assums x is resolved
+freeVarsWithNames :: JType -> TMonad (Map Int String)
+freeVarsWithNames x =
+  intsToNames . (\(a,_,_) -> a) <$>
+       execStateT (go x) (M.empty, S.empty, 0)
+    where
+      go :: JType -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
+      go (JTFree vr) = handleVR vr
+      go (JTRigid vr cs) = handleVR vr >> traversem_ (go . fromC) cs
+      go v = composOpM_ go v
+
+      handleVR (mbName, ref) = do
+        (m,ns,ct) <- get
+        case M.lookup ref m of
+          Just (Left _) -> return ()
+          Just (Right _) -> case mbName of
+                              Just name -> putName name ref
+                              Nothing -> return ()
+          Nothing -> do
+            case mbName of
+              Just name -> putName name ref
+              Nothing -> put (M.insert ref (Right ct) m, ns, ct + 1)
+            mapM_ (go . fromC) =<< lift (lookupConstraintsList (mbName, ref))
+
+      putName n ref = do
+        (m,ns,ct) <- get
+        let n' = mkUnique ns n 0
+        put (M.insert ref (Left n') m, S.insert n' ns, ct)
+
+      mkUnique ns n i
+          | n' `S.member` ns = mkUnique ns n (i + 1)
+          | otherwise = n'
+          where n' | i == 0 = n
+                   | otherwise = n ++ show i
+
+      fromC (Sub t) = t
+      fromC (Super t) = t
+
+      intsToNames x = fmap (either id go) x
+          where go i = mkUnique (S.fromList $ lefts $ M.elems x) (int2Name i) 0
+                int2Name i | q == 0 = [letter]
+                           | otherwise = letter : show q
+                    where (q,r) = divMod i 26
+                          letter = toEnum (fromEnum 'a' + r)
+
+prettyType x = do
+  xt <- resolveType x
+  names <- freeVarsWithNames xt
+  let replaceNames (JTFree ref) = JTFree $ fixRef ref
+      replaceNames (JTForall refs t) = JTForall (map fixRef refs) $ replaceNames t
+      replaceNames v = composOp replaceNames v
+
+      fixRef (_,ref) = (M.lookup ref names, ref)
+
+      prettyConstraints ref = map go <$> lookupConstraintsList (Nothing, ref)
+          where
+            myName = case M.lookup ref names of
+                       Just n -> n
+                       Nothing -> "t_"++show ref
+            go (Sub t) = myName ++ " <: " ++ (show $ jsToDoc $ replaceNames t)
+            go (Super t) = (show $ jsToDoc $ replaceNames t) ++ " <: " ++ myName
+
+  constraintStrings <- nub . concat <$> mapM prettyConstraints (M.keys names)
+
+  let constraintStr
+          | null constraintStrings = ""
+          | otherwise = "(" ++ intercalate ", " constraintStrings ++ ") => "
+
+  return $ constraintStr ++ (show . jsToDoc $ replaceNames xt)
+
+tyErr0 :: String -> TMonad a
+tyErr0 x = throwError x
+
+tyErr1 :: String -> JType -> TMonad b
+tyErr1 s t = do
+  st <- prettyType t
+  throwError $ s ++ ": " ++ st
+
+tyErr2ext :: String -> String -> String -> JType -> JType -> TMonad a
+tyErr2ext s s1 s2 t t' = do
+  st <- prettyType t
+  st' <- prettyType t'
+  throwError $ s ++ ". " ++ s1 ++ ": " ++ st ++ ", " ++ s2 ++ ": " ++ st'
+
+tyErr2Sub :: JType -> JType -> TMonad a
+tyErr2Sub t t' = tyErr2ext "Couldn't apply subtype relation" "Subtype" "Supertype" t t'
+
+prettyEnv :: TMonad [Map Ident String]
+prettyEnv = mapM (T.mapM prettyType) . tc_env =<< get
+
+runTypecheckRaw x = runTMonad (typecheckMain x)
+
+runTypecheckFull x = runTMonad $ do
+                       r <- prettyType =<< typecheckMain x
+                       e <- prettyEnv
+                       return (r,e)
+
+runTypecheck x = evalTMonad $ prettyType =<< typecheckMain x
+
+evalTypecheck x = evalTMonad $ do
+                    _ <- typecheckMain x
+                    e <- prettyEnv
+                    return e
+
+typecheckMain x = go `catchError` handler
+    where go = do
+            r <- typecheck x
+            setFrozen . S.unions . tc_stack =<< get
+            tryCloseFrozenVars
+            return r
+          handler e = do
+                 cxt <- tc_context <$> get
+                 throwError =<< (unlines . (e:) <$> sequence cxt)
+
+-- Manipulating VarRefs and Constraints
+
+addToStack v (s:ss) = S.insert v s : ss
+addToStack _ _ = error "addToStack: no sets" --[S.singleton v]
+
+newVarRef :: TMonad VarRef
+newVarRef = do
+  v <- tc_varCt <$> get
+  modify (\s -> s {tc_varCt = v + 1,
+                   tc_stack = addToStack v (tc_stack s)})
+  return $ (Nothing, v)
+
+newTyVar :: TMonad JType
+newTyVar = JTFree <$> newVarRef
+
+mapConstraint :: (Monad m, Functor m) => (JType -> m JType) -> Constraint -> m Constraint
+mapConstraint f (Sub t) = Sub <$> f t
+mapConstraint f (Super t) = Super <$> f t
+
+partitionCs [] = ([],[])
+partitionCs (Sub t:cs) = (t:subs,sups)
+    where (subs,sups) = partitionCs cs
+partitionCs (Super t:cs) = (subs,t:sups)
+    where (subs,sups) = partitionCs cs
+
+
+--add mutation
+lookupConstraintsList :: VarRef -> TMonad [Constraint]
+lookupConstraintsList vr@(_,ref) = do
+    vars <- tc_vars <$> get
+    case M.lookup ref vars of
+      (Just (SVConstrained cs)) -> filter notLoop . nub <$> mapM (mapConstraint resolveType) (S.toList cs)
+      (Just (SVType t)) -> tyErr1 "lookupConstraints on instantiated type" t
+      Nothing -> return []
+  where
+    notLoop (Super (JTFree (_,ref'))) | ref == ref' = False
+    notLoop (Sub   (JTFree (_,ref'))) | ref == ref' = False
+    notLoop _ = True
+
+-- if we instantiate a var to itself, then there's a good chance this results from a looping constraint -- we should be helpful and get rid of any such constraints.
+instantiateVarRef :: VarRef -> JType -> TMonad ()
+instantiateVarRef vr@(_,ref) (JTFree (_,ref')) | ref == ref' = do
+    cs <- lookupConstraintsList vr
+    let cs' = simplify cs
+    modify (\s -> s {tc_vars = M.insert ref (SVConstrained (S.fromList cs')) (tc_vars s)})
+  where simplify (Sub   (JTFree (_,r)):cs) | r == ref = cs
+        simplify (Super (JTFree (_,r)):cs) | r == ref = cs
+        simplify (c:cs) = c : simplify cs
+        simplify x = x
+
+instantiateVarRef vr@(_,ref) t = do
+  occursCheck ref t
+  cs <- lookupConstraintsList vr
+  modify (\s -> s {tc_vars = M.insert ref (SVType t) (tc_vars s)})
+  checkConstraints t cs
+
+occursCheck :: Int -> JType -> TMonad ()
+occursCheck ref (JTFree (_,i))
+  | i == ref = tyErr1 "Occurs check: cannot construct infinite type" (JTFree (Nothing,i))
+occursCheck ref x = composOpM_ (occursCheck ref) x
+
+checkConstraints :: JType -> [Constraint] -> TMonad ()
+checkConstraints t cs = mapM_ go cs
+    where go (Sub t2) = t <: t2
+          go (Super t2) = t2 <: t
+
+addConstraint :: VarRef -> Constraint -> TMonad ()
+addConstraint vr@(_,ref) c = case c of
+       Sub t -> case t of
+                  JTFree _ -> addC c
+
+                  JTForall vars t -> normalizeConstraints . (c : ) =<< lookupConstraintsList vr
+
+                  JTFunc args res -> do
+                         mapM_ (occursCheck ref) (res:args)
+                         normalizeConstraints . (c :) =<< lookupConstraintsList vr
+
+                  JTRecord t m -> occursCheck ref t >>
+                                  F.mapM_ (occursCheck ref) m >>
+                                  addRecConstraint (Left (m,t))
+
+                  JTList t' -> do
+                         vr' <- newVarRef
+                         addConstraint vr' (Sub t')
+                         instantiateVarRef vr (JTList (JTFree vr'))
+
+                  JTMap t' -> do
+                         vr' <- newVarRef
+                         addConstraint vr' (Sub t')
+                         instantiateVarRef vr (JTMap (JTFree vr'))
+
+                  JTRigid _ cs -> do
+                         (subs,sups) <- partitionCs <$> lookupConstraintsList vr
+                         let (subs1,sups1) = partitionCs $ S.toList cs
+                         when ((null sups1 && (not . null) sups) ||
+                               (null subs1 && (not . null) subs)) $ tyErr2Sub (JTFree vr) t
+                         mapM_ (uncurry (<:)) [(x,y) | x <- subs, y <- subs1]
+                         mapM_ (uncurry (<:)) [(y,x) | x <- sups, y <- sups1]
+
+                         modify (\s -> s {tc_vars = M.insert ref (SVType t) (tc_vars s)}) --can all this be subsumed by a call to instantiate varref and casing on jtrigid carefully in the <: relationship?
+                         -- a polymorphic var is a subtype of another if it is "bigger" on the lattice -- its subtypes are lower and supertypes are higher. sups a > sups b, subs a < subs b
+                  _ -> instantiateVarRef vr t
+
+       Super t -> case t of
+                  JTFree _ -> addC c
+
+                  JTForall vars t -> normalizeConstraints . (c : ) =<< lookupConstraintsList vr
+
+                  JTFunc args res -> do
+                         mapM_ (occursCheck ref) (res:args)
+                         normalizeConstraints . (c :) =<< lookupConstraintsList vr
+
+                  JTRecord t m -> occursCheck ref t >>
+                                  F.mapM_ (occursCheck ref) m >>
+                                  addRecConstraint (Right (m,t))
+
+                  JTList t' -> do
+                         vr' <- newVarRef
+                         addConstraint vr' (Super t')
+                         instantiateVarRef vr (JTList (JTFree vr'))
+
+                  JTMap t' -> do
+                         vr' <- newVarRef
+                         addConstraint vr' (Super t')
+                         instantiateVarRef vr (JTMap (JTFree vr'))
+
+                  JTRigid _ cs -> do
+                         (subs,sups) <- partitionCs <$> lookupConstraintsList vr
+                         let (subs1,sups1) = partitionCs $ S.toList cs
+                         when ((null sups1 && (not . null) sups) ||
+                               (null subs1 && (not . null) subs)) $ tyErr2Sub (JTFree vr) t
+                         mapM_ (uncurry (<:)) [(y,x) | x <- subs, y <- subs1]
+                         mapM_ (uncurry (<:)) [(x,y) | x <- sups, y <- sups1]
+
+                         modify (\s -> s {tc_vars = M.insert ref (SVType t) (tc_vars s)}) --can all this be subsumed by a call to instantiate varref and casing on jtrigid carefully in the <: relationship?
+                         -- a polymorphic var is a subtype of another if it is "bigger" on the lattice -- its subtypes are lower and supertypes are higher. sups a > sups b, subs a < subs b
+
+                  _ -> instantiateVarRef vr t
+    where
+      putCs cs =
+        modify (\s -> s {tc_vars = M.insert ref (SVConstrained $ S.fromList $ cs) (tc_vars s)})
+
+      addC constraint = do
+        cs <- lookupConstraintsList vr
+        modify (\s -> s {tc_vars = M.insert ref (SVConstrained (S.fromList $ constraint:cs)) (tc_vars s)})
+
+      findRecordSubs cs = partitionOut go cs
+          where go (Sub (JTRecord t m)) = Just (m,t)
+                go _ = Nothing
+
+      findRecordSups cs = partitionOut go cs
+          where go (Super (JTRecord t m)) = Just (m,t)
+                go _ = Nothing
+
+      --left is sub, right is super
+      --There really should be at most one existing sub and sup constraint
+      addRecConstraint eM = do
+        (subs,restCs) <- findRecordSubs <$> lookupConstraintsList vr
+        let (sups,restCs') = findRecordSups restCs
+
+            mergeSubs [] = return Nothing
+            mergeSubs [m] = return $ Just m
+            mergeSubs (m:ms) = Just <$> foldM (\(mp,t) (mp',t') -> do
+                                                  mp'' <- unionWithM (\x y -> someLowerBound [x,y]) mp mp'
+                                                  t'' <- someLowerBound [t,t']
+                                                  return (mp'',t'')
+                                              ) m ms
+            mergeSups [] = return Nothing
+            mergeSups [m] = return $ Just m
+            mergeSups (m:ms) = Just <$> foldM (\(mp,t) (mp',t') -> do
+                                                                mp'' <- intersectionWithM (\x y -> someUpperBound [x,y]) mp mp'
+                                                                t'' <- someUpperBound [t,t']
+                                                                return (mp'',t'')
+                                                            ) m ms
+        mbSub <- mergeSubs $ case eM of
+                               Left mt -> mt : subs
+                               _ -> subs
+        mbSup <- mergeSups $ case eM of
+                               Right mt -> mt : sups
+                               _ -> sups
+        normalizeConstraints =<< case (mbSub, mbSup) of
+          (Just (subm,subt), Just (supm,supt)) -> do
+            when (not $ M.isSubmapOfBy (\_ _ -> True) subm supm) $ tyErr2ext "Incompatible constraints" "Subtype constraint" "Supertype constraint" (JTRecord subt subm) (JTRecord supt supm)
+            _ <- intersectionWithM (\x y -> y <: x) subm supm
+            _ <- supt <: subt
+            return $ Sub (JTRecord subt subm) : Super (JTRecord supt supm) : restCs'
+          (Just (subm,subt), Nothing)  -> return $ Sub (JTRecord subt subm) : restCs'
+          (Nothing , Just (supm,supt)) -> return $ Super (JTRecord supt supm) : restCs'
+          _ -> return restCs'
+
+      --There really should be at most one existing sub and sup constraint
+      normalizeConstraints cl = putCs =<< cannonicalizeConstraints cl
+
+
+cannonicalizeConstraints constraintList = do
+        -- trace ("ccl: " ++ show constraintList) $ return ()
+        let (subs,restCs)  = findForallSubs constraintList
+            (sups,restCs') = findForallSups restCs
+        mbSub <- mergeSubs subs
+        mbSup <- mergeSups sups
+        case (mbSub, mbSup) of
+          (Just sub, Just sup) -> do
+            sup <: sub
+            return $ Sub sub : Super sup : restCs'
+          (Just sub, Nothing)  -> return $ Sub sub : restCs'
+          (Nothing , Just sup) -> return $ Super sup : restCs'
+          _ -> return restCs'
+  where
+
+    findForallSubs cs = partitionOut go cs
+      where go (Sub (JTForall vars t)) = Just (vars,t)
+            go (Sub (JTFree _)) = Nothing
+            go (Sub x) = Just ([],x)
+            go _ = Nothing
+
+    findForallSups cs = partitionOut go cs
+      where go (Super (JTForall vars t)) = Just (vars,t)
+            go (Super (JTFree _)) = Nothing
+            go (Super x) = Just ([],x)
+            go _ = Nothing
+
+    findFuncs cs = partitionOut go cs
+        where go (JTFunc args ret) = Just (args, ret)
+              go _ = Nothing
+
+    mergeSubs [] = return Nothing
+    mergeSubs [([],t)] = return $ Just $ t
+    mergeSubs [s] = return $ Just $ uncurry JTForall s
+    mergeSubs ss = do
+      rt <- newTyVar
+      (_,frame) <- withLocalScope $ do
+          instantiatedTypes <- mapM (uncurry instantiateScheme) ss
+          let (funcTypes, otherTypes) = findFuncs instantiatedTypes
+          when (not . null $ funcTypes) $ do
+                     let (argss,rets) = unzip funcTypes
+                         lft = length funcTypes
+                     args' <- mapM someUpperBound $ filter ((== lft) . length) $ transpose argss
+                     ret'  <- someLowerBound rets
+                     rt <: JTFunc args' ret'
+          mapM_ (rt <:) otherTypes
+--        ((args',ret'):_,o:_) -> tyErr2ext "Incompatible Subtype Constraints" "Subtype constraint" "Subtype constraint" (JTFunc args' ret') o
+      rt' <- resolveType rt
+      case rt' of
+        (JTFunc args res) -> do
+          freeVarsInArgs <- S.unions <$> mapM freeVars args
+          freeVarsInRes  <- freeVars res
+          setFrozen $ frame `S.difference` (freeVarsInArgs `S.intersection` freeVarsInRes)
+        _ -> setFrozen frame
+      -- tryCloseFrozenVars
+      Just <$> resolveType (JTForall (frame2VarRefs frame) rt')
+
+    mergeSups [] = return Nothing
+    mergeSups [([],t)] = return $ Just $ t
+    mergeSups [s] = return $ Just $ uncurry JTForall s
+    mergeSups ss = do
+      rt <- newTyVar
+      (_,frame) <- withLocalScope $ do
+           instantiatedTypes <- mapM (uncurry instantiateScheme) ss
+           let (funcTypes, otherTypes) = findFuncs instantiatedTypes
+           when (not . null $ funcTypes) $ do
+                     let (argss,rets) = unzip funcTypes
+                     args' <- mapM someLowerBound $ transpose argss
+                     ret'  <- someUpperBound rets
+                     rt <: JTFunc args' ret'
+           mapM_ (<: rt) otherTypes
+--        ((args',ret'):_,o:_) -> tyErr2ext "Incompatible Supertype Constraints" "Supertype constraint" ("Supertype constraint" ++ show o) (JTFunc args' ret') o
+      rt' <- resolveType rt
+
+      case rt' of
+        (JTFunc args res) -> do
+          freeVarsInArgs <- S.unions <$> mapM freeVars args
+          freeVarsInRes  <- freeVars res
+          setFrozen $ frame `S.difference` (freeVarsInArgs `S.intersection` freeVarsInRes)
+        _ -> setFrozen frame
+      -- tryCloseFrozenVars
+      Just <$> resolveType (JTForall (frame2VarRefs frame) rt')
+
+
+tryCloseFrozenVars :: TMonad ()
+tryCloseFrozenVars = runReaderT (loop . tc_frozen =<< get) []
+    where
+      loop frozen = do
+        mapM_ go $ S.toList frozen
+        newFrozen <- tc_frozen <$> lift get
+        if S.null (newFrozen  `S.difference` frozen)
+           then return ()
+           else loop newFrozen
+      go :: Int -> ReaderT [Either Int Int] TMonad ()
+      go i = do
+        s <- ask
+        case findLoop i s of
+          -- if no set is returned, then that means we just return (i.e. the constraint is dull)
+          Just Nothing  -> return ()
+          -- if a set is returned, then all vars in the set should be tied together
+          Just (Just vrs) -> unifyGroup vrs
+          Nothing       -> do
+              t <- lift $ resolveTypeShallow (JTFree (Nothing, i))
+              case t of
+                (JTFree vr) -> do
+                     l <- tryClose vr
+                     case l of
+                       [] -> return ()
+                       cl -> do
+                         mapM_ (go' vr) cl
+                         lift (mapM_ (mapConstraint resolveType) cl)
+                          -- not clear if we need to call again. if we resolve any constraints, they should point us back upwards...
+                         --if cl remains free, recannonicalize it?
+                _ -> return ()
+      -- Left is super, right is sub
+      go' (_,ref) (Sub (JTFree (_,i)))
+          | i == ref = return ()
+          | otherwise = -- trace (show ("super: " ++ show (ref,i))) $
+                        local (\s -> Left ref : s) $ go i
+      go' (_,ref) (Super (JTFree (_,i)))
+          | i == ref = return ()
+          | otherwise = -- trace (show ("sub: " ++ show (ref,i))) $
+                        local (\s -> Right ref : s) $ go i
+      go' _ _ = return ()
+
+      unifyGroup :: [Int] -> ReaderT [Either Int Int] TMonad ()
+      unifyGroup (vr:vrs) = lift $ mapM_ (\x -> instantiateVarRef (Nothing, x) (JTFree (Nothing,vr))) vrs
+
+      findLoop i cs@(c:_) = go [] cs
+          where
+            cTyp = isLeft c
+            go accum (r:rs)
+               | either id id r == i && isLeft r == cTyp = Just $ Just (either id id r : accum)
+                  -- i.e. there's a cycle to close
+               | either id id r == i = Just Nothing
+                  -- i.e. there's a "dull" cycle
+               | isLeft r /= cTyp = Nothing -- we stop looking for a cycle because the chain is broken
+               | otherwise = go (either id id r : accum) rs
+            go _ [] = Nothing
+
+      findLoop i [] = Nothing
+
+      tryClose vr@(_,i) = do
+        cl <- lift$ cannonicalizeConstraints =<< lookupConstraintsList vr
+        -- trace ("tryclose: " ++ show vr) $ trace (show cl) $ return ()
+        case partitionCs cl of
+          (_,[s]) -> lift (instantiateVarRef vr s) >> go i >> return [] -- prefer lower bound (supertype constraint)
+          ([s],_) -> lift (instantiateVarRef vr s) >> go i >> return []
+          _ -> return cl
+
+-- Manipulating the environment
+withLocalScope :: TMonad a -> TMonad (a, Set Int)
+withLocalScope act = do
+  modify (\s -> s {tc_env   = M.empty : tc_env s,
+                   tc_stack = S.empty : tc_stack s})
+  res <- act
+  frame <- head . tc_stack <$> get
+  modify (\s -> s {tc_env   = drop 1 $ tc_env s,
+                   tc_stack = drop 1 $ tc_stack s})
+  return (res, frame)
+
+setFrozen :: Set Int -> TMonad ()
+setFrozen x = modify (\s -> s {tc_frozen = tc_frozen s `S.union` x})
+
+-- addRefsToStack x = modify (\s -> s {tc_stack = F.foldr addToStack (tc_stack s) x })
+
+frame2VarRefs frame = (\x -> (Nothing,x)) <$> S.toList frame
+
+addEnv :: Ident -> JType -> TMonad ()
+addEnv ident typ = do
+  envstack <- tc_env <$> get
+  case envstack of
+    (e:es) -> modify (\s -> s {tc_env = M.insert ident typ e : es}) -- we clobber/shadow var names
+    _ -> throwError "empty env stack (this should never happen)"
+
+newVarDecl :: Ident -> TMonad JType
+newVarDecl ident = do
+  v <- newTyVar
+  addEnv ident v
+  return v
+
+resolveTypeGen :: ((JType -> TMonad JType) -> JType -> TMonad JType) -> JType -> TMonad JType
+resolveTypeGen f typ = go typ
+    where
+      go :: JType -> TMonad JType
+      go x@(JTFree (_, ref)) = do
+        vars <- tc_vars <$> get
+        case M.lookup ref vars of
+          Just (SVType t) -> do
+            res <- go t
+            when (res /= t) $ modify (\s -> s {tc_vars = M.insert ref (SVType res) $ tc_vars s}) --mutation, shortcuts pointer chasing
+            return res
+          _ -> return x
+
+      -- | Eliminates resolved vars from foralls, eliminates empty foralls.
+      go (JTForall refs t) = do
+        refs' <- catMaybes <$> mapM checkRef refs
+        if null refs'
+           then go t
+           else JTForall refs' <$> go t
+      go x = f go x
+
+      checkRef x@(_, ref) = do
+        vars <- tc_vars <$> get
+        case M.lookup ref vars of
+          Just (SVType t) -> return Nothing
+          _ -> return $ Just x
+
+resolveType = resolveTypeGen composOpM
+resolveTypeShallow = resolveTypeGen (const return)
+
+--TODO create proper bounds for records
+integrateLocalType :: JLocalType -> TMonad JType
+integrateLocalType (env,typ) = do
+  (r, frame) <- withLocalScope $ flip evalStateT M.empty $ do
+                                 mapM_ integrateEnv env
+                                 cloneType typ
+  resolveType $ JTForall (frame2VarRefs frame) r
+    where
+      getRef (mbName, ref) = do
+            m <- get
+            case M.lookup ref m of
+              Just newTy -> return newTy
+              Nothing -> do
+                newTy <- (\x -> JTFree (mbName, snd x)) <$> lift newVarRef
+                put $ M.insert ref newTy m
+                return newTy
+
+      integrateEnv (vr,c) = do
+        newTy <- getRef vr
+        case c of
+          (Sub t) -> lift . (newTy <:) =<< cloneType t
+          (Super t) -> lift . (<: newTy) =<< cloneType t
+
+      cloneType (JTFree vr) = getRef vr
+      cloneType x = composOpM cloneType x
+
+lookupEnv :: Ident -> TMonad JType
+lookupEnv ident = resolveType =<< go . tc_env =<< get
+    where go (e:es) = case M.lookup ident e of
+                        Just t -> return t
+                        Nothing -> go es
+          go _ = tyErr0 $ "unable to resolve variable name: " ++ (show $ jsToDoc $ ident)
+
+
+freeVars :: JType -> TMonad (Set Int)
+freeVars t = execWriterT . go =<< resolveType t
+    where go (JTFree (_, ref)) = tell (S.singleton ref)
+          go x = composOpM_ go x
+
+--only works on resolved types
+instantiateScheme :: [VarRef] -> JType -> TMonad JType
+instantiateScheme vrs t = evalStateT (go t) M.empty
+    where
+      schemeVars = S.fromList $ map snd vrs
+      go :: JType -> StateT (Map Int JType) TMonad JType
+      go (JTFree vr@(mbName, ref))
+          | ref `S.member` schemeVars = do
+                       m <- get
+                       case M.lookup ref m of
+                         Just newTy -> return newTy
+                         Nothing -> do
+                           newRef <- (\x -> (mbName, snd x)) <$> lift newVarRef
+                           put $ M.insert ref (JTFree newRef) m
+                           mapM_ (lift . addConstraint newRef <=< mapConstraint go) =<< lift (lookupConstraintsList vr)
+                           return (JTFree newRef)
+      go x = composOpM go x
+
+--only works on resolved types
+instantiateRigidScheme :: [VarRef] -> JType -> TMonad JType
+instantiateRigidScheme vrs t = evalStateT (go t) M.empty
+    where
+      schemeVars = S.fromList $ map snd vrs
+      go :: JType -> StateT (Map Int JType) TMonad JType
+      go (JTFree vr@(mbName, ref))
+          | ref `S.member` schemeVars = do
+                       m <- get
+                       case M.lookup ref m of
+                         Just newTy -> return newTy
+                         Nothing -> do
+                           newRef <- JTRigid vr . S.fromList <$> lift (lookupConstraintsList vr)
+                           put $ M.insert ref newRef m
+                           return newRef
+      go x = composOpM go x
+
+--only works on resolved types
+checkEscapedVars :: [VarRef] -> JType -> TMonad ()
+checkEscapedVars vrs t = go t
+    where
+      vs = S.fromList $ map snd vrs
+      go t@(JTRigid (_,ref) _)
+          | ref `S.member` vs = tyErr1 "Qualified var escapes into environment" t
+          | otherwise = return ()
+      go x = composOpM_ go x
+
+-- Subtyping
+(<:) :: JType -> JType -> TMonad ()
+x <: y = do
+     xt <- resolveTypeShallow x --shallow because subtyping can close
+     yt <- resolveTypeShallow y
+     -- trace ("sub : " ++ show xt ++ ", " ++ show yt) $ return ()
+     if xt == yt
+        then return ()
+        else go xt yt `withContext` (do
+                                      xt <- prettyType x
+                                      yt <- prettyType y
+                                      return $ "When applying subtype constraint: " ++ xt ++ " <: " ++ yt)
+  where
+
+    go _ JTStat = return ()
+    go JTImpossible _ = return ()
+
+    go xt@(JTFree ref) yt@(JTFree ref2) = addConstraint ref  (Sub yt) >>
+                                          addConstraint ref2 (Super xt)
+
+    go (JTFree ref) yt = addConstraint ref (Sub yt)
+    go xt (JTFree ref) = addConstraint ref (Super xt)
+
+    --above or below jtfrees ?
+
+    -- v <: \/ a. t --> v <: t[a:=x], x not in conclusion
+    go xt yt@(JTForall vars t) = do
+           t' <- instantiateRigidScheme vars t
+           go xt t'
+           checkEscapedVars vars =<< resolveType xt
+           --then check that no fresh types appear in xt
+
+    -- \/ a. t <: v --> [t] <: v
+    go (JTForall vars t) yt = do
+           t' <- instantiateScheme vars t
+           go t' yt
+
+    go xt@(JTFunc argsx retx) yt@(JTFunc argsy rety) = do
+           -- TODO: zipWithM_ (<:) (appArgst ++ repeat JTStat) argst -- handle empty args cases
+           when (length argsy < length argsx) $ tyErr2Sub xt yt
+           zipWithM_ (<:) argsy argsx -- functions are contravariant in argument type
+           retx <: rety -- functions are covariant in return type
+    go (JTList xt) (JTList yt) = xt <: yt
+    go (JTMap xt) (JTMap yt) = xt <: yt
+    go (JTRecord xt xm) (JTRecord yt ym)
+        | M.isSubmapOfBy (\_ _ -> True) ym xm = xt <: yt >> intersectionWithM (<:) xm ym >> return () --TODO not right?
+    go xt yt = tyErr2Sub xt yt
+
+x <<:> y = join $ liftA2 (<:) x y
+
+someUpperBound :: [JType] -> TMonad JType
+someUpperBound [] = return JTStat
+someUpperBound xs = do
+  res <- newTyVar
+  b <- (mapM_ (<: res) xs >> return True) `catchError` \e -> return False
+  if b then return res else return JTStat
+
+someLowerBound :: [JType] -> TMonad JType
+someLowerBound [] = return JTImpossible
+someLowerBound xs = do
+  res <- newTyVar
+  mapM_ (res <:) xs
+  return res
+--  b <- (mapM_ (res <:) xs >> return True) `catchError` \e -> return False
+--  if b then return res else return JTImpossible
+
+x =.= y = do
+      x <: y
+      y <: x
+      return x
+
+--todo difft ixing. a[b] --num lookup, a#[b] --string lookup, a.[b] --num literal lookup (i.e. tuple projection)
+
+instance JTypeCheck JExpr where
+    typecheck (ValExpr e) = typecheck e
+    typecheck (SelExpr e (StrI i)) =
+        do et <- typecheck e
+           case et of
+             (JTRecord t m) -> case M.lookup i m of
+                               Just res -> return res
+                               Nothing -> tyErr1 ("Record contains no field named " ++ show i) et -- record extension would go here
+             (JTFree r) -> do
+                            res <- newTyVar
+                            addConstraint r (Sub (JTRecord res (M.singleton i res)))
+                            return res
+             _ -> tyErr1 "Cannot use record selector on this value" et
+    typecheck (IdxExpr e e1) = undefined --this is tricky
+    typecheck (InfixExpr s e e1)
+        | s `elem` ["-","/","*"] = setFixed JTNum >> return JTNum
+        | s == "+" = setFixed JTNum >> return JTNum -- `orElse` setFixed JTStr --TODO: Intersection types
+        | s == "++" = setFixed JTString >> return JTString
+        | s `elem` [">","<"] = setFixed JTNum >> return JTBool
+        | s `elem` ["==","/="] = do
+                            et <- typecheck e
+                            e1t <- typecheck e1
+                            et =.= e1t
+                            return JTBool
+        | s `elem` ["||","&&"] = setFixed JTBool >> return JTBool
+        | otherwise = throwError $ "Unhandled operator: " ++ s
+        where setFixed t = do
+                  typecheck e  <<:> return t
+                  typecheck e1 <<:> return t
+
+    typecheck (PostExpr _ e) = case e of
+                                 (SelExpr _ _) -> go
+                                 (ValExpr (JVar _)) -> go
+                                 (IdxExpr _ _) -> go
+                                 _ -> tyErr1 "Value not compatible with postfix assignment" =<< typecheck e
+        where go = (typecheck e <<:> return JTNum) >> return JTNum
+
+    typecheck (IfExpr e e1 e2) = do
+                            typecheck e <<:> return JTBool
+                            join $ liftA2 (\x y -> someUpperBound [x,y]) (typecheck e1) (typecheck e2)
+
+    typecheck (NewExpr e) = undefined --yipe
+
+    --when we instantiate a scheme, all the elements of the head
+    --that are not in the tail are henceforth unreachable and can be closed
+    --but that's just an optimization
+    typecheck (ApplExpr e appArgse) = do
+                            et <- typecheck e
+                            appArgst <- mapM typecheck appArgse
+                            let go (JTForall vars t) = go =<< instantiateScheme vars t
+                                go (JTFunc argst rett) = do
+                                        zipWithM_ (<:) (appArgst ++ repeat JTStat) argst
+                                        return rett
+                                go (JTFree vr) = do
+                                        ret <- newTyVar
+                                        addConstraint vr (Sub (JTFunc appArgst ret))
+                                        return ret
+                                go x = tyErr1 "Cannot apply value as function" x
+                            go et
+
+
+    typecheck (UnsatExpr _) = undefined --saturate (avoiding creation of existing ids) then typecheck
+    typecheck (AntiExpr s) = fail $ "Antiquoted expression not provided with explicit signature: " ++ show s
+
+    --TODO: if we're typechecking a function, we can assign the types of the args to the given args
+    typecheck (TypeExpr forceType e t)
+              | forceType = integrateLocalType t
+              | otherwise = do
+                            t1 <- integrateLocalType t
+                            typecheck e <<:> return t1
+                            return t1
+
+instance JTypeCheck JVal where
+    typecheck (JVar i) =
+        case i of
+          StrI "true" -> return JTBool
+          StrI "false" -> return JTBool
+          StrI "null"  -> newTyVar
+          StrI _ -> lookupEnv i
+
+    typecheck (JInt _) = return JTNum
+    typecheck (JDouble _) = return JTNum
+    typecheck (JStr _) = return JTString
+    typecheck (JList xs) = typecheck (JHash $ M.fromList $ zip (map show [0..]) xs)
+                           -- fmap JTList . someUpperBound =<< mapM typecheck xs
+    typecheck (JRegEx _) = undefined --regex object
+    typecheck (JHash mp) = do
+      mp' <- T.mapM typecheck mp
+      t <- if M.null mp'
+             then return JTImpossible
+             else someUpperBound $ M.elems mp'
+      return $ JTRecord t mp'
+    typecheck (JFunc args body) = do
+          ((argst',res'), frame) <- withLocalScope $ do
+                                      argst <- mapM newVarDecl args
+                                      res <- typecheck body
+                                      return (argst,res)
+          rt <- resolveType $ JTFunc argst' res'
+          freeVarsInArgs <- S.unions <$> mapM freeVars argst'
+          freeVarsInRes  <- freeVars res'
+          setFrozen $ frame `S.difference` (freeVarsInArgs `S.intersection` freeVarsInRes)
+          tryCloseFrozenVars
+          resolveType $ JTForall (frame2VarRefs frame) rt
+
+    typecheck (UnsatVal _) = undefined --saturate (avoiding creation of existing ids) then typecheck
+
+instance JTypeCheck JStat where
+    typecheck (DeclStat ident Nothing) = newVarDecl ident >> return JTStat
+    typecheck (DeclStat ident (Just t)) = integrateLocalType t >>= addEnv ident >> return JTStat
+    typecheck (ReturnStat e) = typecheck e
+    typecheck (IfStat e s s1) = do
+                            typecheck e <<:> return JTBool
+                            join $ liftA2 (\x y -> someUpperBound [x,y]) (typecheck s) (typecheck s1)
+    typecheck (WhileStat e s) = do
+                            typecheck e <<:> return JTBool
+                            typecheck s
+    typecheck (ForInStat _ _ _ _) = undefined -- yipe!
+    typecheck (SwitchStat e xs d) = undefined -- check e, unify e with firsts, check seconds, take glb of seconds
+                                    --oh, hey, add typecase to language!?
+    typecheck (TryStat _ _ _ _) = undefined -- should be easy
+    typecheck (BlockStat xs) = do
+                            ts <- mapM typecheckWithBlock xs
+                            someUpperBound $ stripStat ts
+        where stripStat (JTStat:ts) = stripStat ts
+              stripStat (t:ts) = t : stripStat ts
+              stripStat t = t
+    typecheck (ApplStat args body) = typecheck (ApplExpr args body) >> return JTStat
+    typecheck (PostStat s e) = typecheck (PostExpr s e) >> return JTStat
+    typecheck (AssignStat e e1) = do
+      typecheck e1 <<:> typecheck e
+      return JTStat
+    typecheck (UnsatBlock _) = undefined --oyvey
+    typecheck (AntiStat _) = undefined --oyvey
+    typecheck BreakStat = return JTStat
+    typecheck (ForeignStat i t) = integrateLocalType t >>= addEnv i >> return JTStat
+
+typecheckWithBlock stat = typecheck stat `withContext` (return $ "In statement: " ++ renderStyle (style {mode = OneLineMode}) (renderJs stat))
diff --git a/Language/Javascript/JMacro/Typed.hs b/Language/Javascript/JMacro/Typed.hs
deleted file mode 100644
--- a/Language/Javascript/JMacro/Typed.hs
+++ /dev/null
@@ -1,1349 +0,0 @@
-{-# LANGUAGE QuasiQuotes, FlexibleInstances #-}
-module Language.Javascript.JMacro.Typed where
-
-import Prelude hiding (tail, init, head, last, minimum, maximum, foldr1, foldl1, (!!), read)
-
-import Language.Javascript.JMacro.Base
-import Language.Javascript.JMacro.QQ
-import Control.Monad
-import Control.Monad.State
-import Control.Monad.Error
-import Control.Applicative
-import Data.List (intercalate, deleteFirstsBy, find)
-import Data.Function(on)
-import qualified Data.Map as M
-import Data.Map(Map)
-import Data.Maybe(fromMaybe)
-import qualified Data.Set as S
-import Data.Set(Set)
-import Text.PrettyPrint.HughesPJ
-import Debug.Trace
-
-
---todo: collect errors
---pretty types, bump down variable nums
---infer missing vs. assert missing
---type parser
---intersection types
---lists, new/this, extensible records
---flag to automatically introduce new things into environment
---seperate resAtoms function
-
-{--------------------------------------------------------------------
-  Main Interface
---------------------------------------------------------------------}
-
-runTypecheck :: JTypeCheck a => a -> IO ()
-runTypecheck x =  either putStrLn print $ evalState (runErrorT go) tcStateEmpty
-    where go = do
-            res <- typecheck x
-            showenv <- do
-                 (env:topenv:_) <- tc_env <$> get
-                 r@(JTRec i) <- newRec
-                 putRec i (M.toList env)
-                 r'@(JTRec i') <- newRec
-                 putRec i' (M.toList topenv)
---                 killSats
-                 s <- showType r
-                 s' <- prettyType' r'
-                 pres <- showType res
-                 return (pres,s,s')
-            return showenv
-
-{--------------------------------------------------------------------
-  Types
---------------------------------------------------------------------}
-
-data JType = JTNum
-           | JTStr
-           | JTBool
-           | JTRec Int
-           | JTFunc [JType] JType
-           | JTList (Maybe Int) (Maybe JType) --can be multityped, monotyped, or neither
-                                              --jtint is an index into a record
-           | JTStat
-           | JTSat Int
-           | BotOf JType
-           | JTVar Int deriving (Show, Eq)
-
-data JConstr = Sub JType | Super JType deriving Show
-
---canextend needs scoping, to deal with inner lambdas. oyvey. things can only be extended in the scope that they are introduced in. this scoping should be introduced in a scopedRecs thang
-data TCState = TCS {tc_env :: [Map Ident JType],
-                    tc_vars :: Map Int JType,
-                    tc_constrs :: Map Int [JConstr],
-                    tc_recs :: Map Int [(Ident, JType)],
-                    tc_scopedSat :: [Set Int],
-                    tc_varCt :: Int,
-                    tc_strictnull :: Bool,
-                    tc_canextend :: Bool,
-                    tc_debug :: Bool,
-                    tc_expandFree :: Bool} deriving Show
-
-tcStateEmpty :: TCState
-tcStateEmpty = TCS [M.empty,M.empty] M.empty M.empty M.empty [S.empty] 0 True True True True
-
-
-type JMonad a = ErrorT String (State TCState) a
-
-orElse :: JMonad a -> JMonad a -> JMonad a
-x `orElse` y = do
-  st <- get
-  x `catchError` \e1 -> do
-       put st
-       y `catchError` \e2 -> do
-          throwError $ e1 ++ ",\n" ++ e2
-
-{--------------------------------------------------------------------
-  Env utilities
---------------------------------------------------------------------}
-
---fix to maybe do it, or insert top level
-lookupEnvErr :: Ident -> JMonad JType
-lookupEnvErr i@(StrI s) = do
-  ans <- msum . map (M.lookup i) . tc_env <$> get
-  case ans of
-    Just x -> return x
-    Nothing -> do
-             b <- tc_expandFree <$> get
-             if b
-                then do
-                  ns <- newTopSat
-                  addTopEnv i ns
-                  return ns
-                else throwError $ "Variable not in scope: " ++ s
-
---puts idents in scope, as constrained free variables
-withLocalScope :: [Ident] -> JMonad a -> JMonad a
-withLocalScope args act = do
-  env <- tc_env <$> get
-  sats <- tc_scopedSat <$> get
-  modify (\tcs -> tcs {tc_scopedSat = S.empty : sats, tc_env = M.empty : env})
-  mapM (addNewSat) args
-  res <- act
-  (_:restSats) <- tc_scopedSat <$> get
-  (_:restEnv) <- tc_env <$> get
-  modify (\tcs -> tcs {tc_env = restEnv, tc_scopedSat = restSats})
-  return res
-
---puts idents in scope, as normal free variables
-withLocalScope' :: [Ident] -> JMonad a -> JMonad a
-withLocalScope' args act = do
-  env <- tc_env <$> get
-  modify (\tcs -> tcs {tc_env = M.empty : env})
-  mapM (addNewVar) args
-  res <- act
-  (_:restEnv) <- tc_env <$> get
-  modify (\tcs -> tcs {tc_env = restEnv})
-  return res
-
-inConditional :: JMonad a -> JMonad a
-inConditional act = do
-  oldCE <- tc_canextend <$> get
-  modify (\tcs -> tcs {tc_canextend = False})
-  res <- act
-  modify (\tcs -> tcs {tc_canextend = oldCE})
-  return res
-
-addEnv :: Ident -> JType -> JMonad ()
-addEnv i t = do
-  (env:envs) <- tc_env <$> get
-  modify (\tcs -> tcs {tc_env = M.insert i t env : envs})
-
-addTopEnv :: Ident -> JType -> JMonad ()
-addTopEnv i t = do
-  (env:envs) <- reverse . tc_env <$> get
-  modify (\tcs -> tcs {tc_env = reverse $ M.insert i t env : envs})
-
-newV :: JMonad Int
-newV = do
-  x <- tc_varCt <$> get
-  modify (\tcs -> tcs {tc_varCt = x + 1})
-  return x
-
-newVar :: JMonad JType
-newVar = JTVar <$> newV
-
-newSat :: JMonad JType
-newSat = do
-  x <- newV
-  (sat:sats) <- tc_scopedSat <$> get
-  modify (\tcs -> tcs {tc_scopedSat = S.insert x sat : sats})
-  return (JTSat x)
-
-addNewSat :: Ident -> JMonad ()
-addNewSat i = addEnv i =<< newSat
-
-addNewVar :: Ident -> JMonad ()
-addNewVar i = addEnv i =<< newVar
-
-newTopSat :: JMonad JType
-newTopSat = do
-  x <- newV
-  (sat:sats) <- reverse . tc_scopedSat <$> get
-  modify (\tcs -> tcs {tc_scopedSat = reverse $ S.insert x sat : sats})
-  return (JTSat x)
-
-killSats :: JMonad ()
-killSats = modify (\tcs -> tcs {tc_scopedSat = [S.empty]})
-
-newSatAtScope :: [Int] -> JMonad JType
-newSatAtScope is = do
-  x <- newV
-  let go (s:ss) = if any (flip S.member s) is
-                  then S.insert x s : ss
-                  else s : go ss
-      go [] = []
-  modify (\tcs -> tcs {tc_scopedSat = reverse $ go $ reverse (tc_scopedSat tcs)})
---  trace ("nsas: " ++ show is ++ ", " ++ show x) $ return ()
-  return (JTSat x)
-
-satInScope :: Int -> JMonad Bool
-satInScope i = any (S.member i) . tc_scopedSat <$> get
-
-incScope :: Int -> Int -> JMonad ()
-incScope i ni = do --move i up to scope of ni
-  let go (s:ss) = if S.member ni s && not (S.member i s)
-                  then S.insert i s : ss
-                  else s : go ss
-      go [] = []
-  modify (\tcs -> tcs {tc_scopedSat = reverse $ go $ reverse (tc_scopedSat tcs)})
-
-
-bumpScope :: Int -> JType -> JMonad ()
-bumpScope i x@(JTVar _) = do
-  xt <- resolveType x
-  case xt of
-    (JTVar _) -> return ()
-    _ -> bumpScope i xt
-
---bump constraints?
-bumpScope i (JTSat i') = incScope i' i
-
-bumpScope i (JTFunc args ret) = do
-  mapM (bumpScope i) args
-  bumpScope i ret
-
-bumpScope i(JTRec i') = mapM_ go =<< getRec i'
-  where go (_,v) = bumpScope i v
-bumpScope _ _ = return ()
-
-
-{--------------------------------------------------------------------
-  Record utilities
---------------------------------------------------------------------}
-
-getRec :: Int -> JMonad [(Ident, JType)]
-getRec i = fromMaybe [] . (M.lookup i) . tc_recs <$> get
-
-putRec :: Int -> [(Ident, JType)] -> JMonad ()
-putRec i xs = do
-  recs <- tc_recs <$> get
-  modify (\tcs -> tcs {tc_recs = M.insert i xs recs})
-
-recLookup :: Ident -> JType -> JMonad (Maybe JType)
-recLookup v (JTRec i) = maybe Nothing (lookup v) . M.lookup i . tc_recs <$> get
-recLookup _ _ = return $ Nothing
-
-newRec :: JMonad JType
-newRec = do
-  x <- tc_varCt <$> get
-  modify (\tcs -> tcs {tc_varCt = x + 1})
-  return (JTRec x)
-
-{--------------------------------------------------------------------
-  Constraint utilities
---------------------------------------------------------------------}
-
-unzipConstrs :: [JConstr] -> ([JType],[JType])
-unzipConstrs = foldr go ([],[])
-            where
-              go (Sub l)   ~(ls, rs) = (l:ls, rs)
-              go (Super r) ~(ls, rs) = (ls, r:rs)
-
-zipConstrs :: [JType] -> [JType] -> [JConstr]
-zipConstrs subs supers = map Sub subs ++ map Super supers
-
-lookupConstraints :: Int -> JMonad [JConstr]
-lookupConstraints i = fromMaybe [] . M.lookup i . tc_constrs <$> get
-
---move simplification away from here, delay to last possible moment
-addConstraint :: Int -> JConstr -> JMonad ()
-addConstraint i c = do
-  cs <- lookupConstraints i
-  constrs <- tc_constrs <$> get
-  modify (\tcs -> tcs {tc_constrs = M.insert i (c:cs) constrs})
-
-
-{--------------------------------------------------------------------
-  Type utilities
---------------------------------------------------------------------}
-
-chkNoNull :: [JType] -> JMonad ()
-chkNoNull xs = do
-    strictnull <- tc_strictnull <$> get
-    if strictnull
-       then mapM_ (chkNull <=< resolveType) xs
-       else return ()
-  where chkNull x@(JTVar _) = tyErr1 "Attempt to return a (potentially) null variable" x
-        chkNull _ = return ()
-
-showType :: JType -> JMonad String
-showType (JTVar (-1)) = return ""
-showType x@(JTVar _) = do
-  xt <- resolveType x
-  case xt of
-    (JTVar i') -> return $ "t"++show i'
-    _ -> showType xt
-showType (JTSat i) = do
-    cs <- lookupConstraints i
-    case cs of
-      [] -> return $ "ct" ++ show i
-      _ -> do
-        cst <- mapM go cs
-        return $ "ct" ++ show i ++ " <= [" ++ intercalate ", " cst ++ "]"
-  where go (Sub x) = do
-             str <- showType x
-             return ("<: " ++ str)
-        go (Super x) = do
-             str <- showType x
-             return (">: " ++ str)
-
-
-showType JTNum = return "Num"
-showType JTStr = return "String"
-showType JTBool = return "Bool"
-showType (JTRec i) = do
-  rs <- getRec i
-  strs <- mapM go rs
-  return $ "{" ++ intercalate ", " strs ++ "...}"
-    where go (StrI s, t) = do
-                           st <- showType t
-                           return (s ++ ": " ++ st)
-showType (JTFunc args res) = do
-  strs <- mapM showType args
-  rest <- showType res
-  if length strs == -1 --fixme
-     then return $ concat strs ++ " -> " ++  rest
-     else return $ "((" ++ intercalate ", " strs ++ ") -> " ++ rest++")"
-showType JTStat = return $ "()"
-
-showType (JTList _ (Just mono)) = do
-  m <- showType mono
-  return $ "[" ++ m ++ "]"
-
-showType (JTList (Just multi) _) = do
-  showType (JTRec multi)
-
-showType (JTList Nothing Nothing) = error "trying to show bad list"
-
-prettyType :: JType -> JMonad String
-prettyType x = showType x -- =<< resC False x
-
-prettyType' :: JType -> JMonad String
-prettyType' x = showType =<< resC False x
-
-resolveType :: JType -> JMonad JType
-resolveType (JTSat i) = return $ JTSat i
-resolveType (JTVar i) = do
-  vars <- tc_vars <$> get
-  case M.lookup i vars of
-    Just t -> do
-      rt <- resolveType t
-      when (t /= rt) $ do
-                modify (\tcs -> tcs {tc_vars = M.insert i rt vars})
-      return rt
-    _ -> return (JTVar i)
-resolveType r@(JTRec i) = do
-  (is, ts) <- unzip <$> getRec i
-  ts' <-  mapM resolveType ts
-  putRec i (zip is ts')
-  return r
-
-resolveType (JTFunc argst rett) = do
-  argst' <- mapM resolveType argst
-  rett' <- resolveType rett
-  return (JTFunc argst' rett')
-resolveType x = return x
-
-resolveState :: JMonad ()
-resolveState = do
-  envs <- tc_env <$> get
-  envs' <- forM envs $ \env ->
-                      let (is,ts) = unzip $ M.toList env
-                      in  M.fromList . zip is <$> mapM (resC False <=< resolveType) ts
-  modify (\tcs -> tcs {tc_env = envs'})
-
-{--------------------------------------------------------------------
-  Trace/Error utilities
---------------------------------------------------------------------}
-
-ifDbg :: JMonad () -> JMonad ()
-ifDbg x = flip when x . tc_debug =<< get
-
-traceSats :: JMonad ()
-traceSats = ifDbg $ do
-              ss <- tc_scopedSat <$> get
-              trace ("scoped sats: " ++ show ss) $ return ()
-
-traceVars :: JMonad ()
-traceVars = ifDbg $ do
-  resolveState
-  vars <- tc_vars <$> get
-  trace (show vars) $ return ()
-
-traceConstrs:: JMonad ()
-traceConstrs = ifDbg $ do
-  resolveState
-  cs <- tc_constrs <$> get
-  trace (show cs) $ return ()
-
-tyErr1 :: String -> JType -> JMonad a
-tyErr1 s t = do
-  st <- prettyType t
-  throwError $ s ++ ": " ++ st
-
-tyErr2 :: String -> JType -> JType -> JMonad a
-tyErr2 s t t' = do
-  st <- prettyType t
-  st' <- prettyType t'
-  throwError $ s ++ ". Expected: " ++ st ++ ", Inferred: " ++ st'
-
-tyErr2l :: String -> [JType] -> [JType] -> JMonad a
-tyErr2l s t t' = do
-  sts <- mapM showType t
-  sts' <- mapM showType t'
-  throwError $ s ++ ". Expected: (" ++ intercalate ", " sts ++
-                 "), Inferred: (" ++ intercalate "," sts' ++")"
-
-traceTy :: String -> JType -> JMonad ()
-traceTy s x = ifDbg $ do
-    xt <- showType x
-    trace (s ++ ": " ++ show xt) $ return ()
-
-traceTys :: String -> JType -> JType -> JMonad ()
-traceTys s x y = ifDbg $ do
-       xt <- showType x
-       yt <- showType y
-       trace (s ++": " ++ xt ++ ", " ++ yt) $ return ()
-
-{--------------------------------------------------------------------
-  Subtyping
---------------------------------------------------------------------}
-
---subtype {} {x:a} fails
---subtype {x:a} {} succeeds with {}
--- x is a subtype of y
---subtype enforces subtype relation
-(<:) :: JType -> JType -> JMonad ()
-x <: y = do
-  xr <- resolveType x
-  yr <- resolveType y
-  if xr == yr
-     then return ()
-     else traceTys "subtyping" xr yr >> subtype xr yr
-
-subtype :: JType -> JType -> JMonad ()
-subtype x@(JTSat i) y@(JTSat i') = do
-  addConstraint i (Sub y)
-  bumpScope i y
-
---assigning a free variable to a fixed type
---is incoherent, as it implies usage of a null variable
-subtype x@(JTVar _) y = do
-  x' <- resolveType x
-  case x' of
-    JTVar _ -> tyErr1 "Cannot subtype a free variable in" y
-    _ -> x' <: y
-
---assigning to a free variable fixes it
-subtype x y@(JTVar _) = do
-  y' <- resolveType y
-  case y' of
-    JTVar _ -> do
-            y' =.= x
-    _ -> x <: y'
-
-subtype x (JTSat i') = do
-  cs <- lookupConstraints i'
-  mapM_ go cs
-  addConstraint i' (Super x)
-      where go (Sub c) = x <: c
-            go (Super c) = c <: x
-
-subtype (JTSat i) y = do
-  cs <- lookupConstraints i
-  mapM_ go cs
-  addConstraint i (Sub y)
-      where go (Sub c) = c <: y
-            go (Super c) = y <: c
-
---lookup ys in xs
-subtype x@(JTRec i) y@(JTRec i') = do
-  yl <- getRec i'
-  xl <- getRec i
-  let go [] = return ()
-      go ((ident@(StrI s),v):ls) = do
-            case lookup ident xl of
-              Just t -> do
-                        t <: v
-                        go ls
-              Nothing -> tyErr2 ("Couldn't subtype, missing property " ++ s) x y
-
-  go yl
-
-subtype x@(JTFunc argsx retx) y@(JTFunc argsy rety) = do
- when (length argsy < length argsx) $ tyErr2 "Couldn't match" x y
- zipWithM_ (<:) argsy argsx -- functions are contravariant in argument type
- retx <: rety -- functions are covariant in return type
-
---List case
-subtype x y
-    | x == y = return ()
-    | otherwise = tyErr2 "Couldn't subtype" x y
-
-
-{--------------------------------------------------------------------
-  Unification
---------------------------------------------------------------------}
-
---Unification should be very limited, and really only occur with
---free variables or atoms. Everything else is constraints.
-
---deal with constraints!?
-occursCheck :: Int -> JType -> JMonad ()
-occursCheck i typ = go typ >>= \b -> if b
-                  then do
-                    xt <- showType (JTVar i)
-                    yt <- showType typ
-                    throwError $ "Could not construct infinite type when unifying " ++ xt ++" and " ++ yt
-                  else return ()
-    where go t@(JTVar _) = resolveType t >>= \rt -> case rt of
-                                                      (JTVar i') -> return (i==i')
-                                                      _ -> go rt
-          go (JTRec i') = or <$> (mapM (go . snd) =<< getRec i')
-          go (JTFunc args ret) = or <$> mapM go (ret:args)
-          go _ = return False
-          --list case
-
---unify, but fail if first argument is free
-(<=.=) :: JType -> JType -> JMonad ()
-x <=.= y = do
-    strictnull <- tc_strictnull <$> get
-    xr <- resolveType x
-    if strictnull
-        then case xr of
-               (JTVar _) -> tyErr1 "Attempt to use null variable as type" y
-               _ -> return ()
-        else return ()
-    case xr of
-      (JTSat _) -> xr <: y
-      _ -> do
-        yr <- resolveType y
-        case yr of
-          (JTSat _) -> yr <: xr
-          _ -> xr =.= yr
-
-(=.=) :: JType -> JType -> JMonad ()
-x =.= y = do
-  xr <- resolveType x
-  yr <- resolveType y
-  if (xr == yr)
-     then return ()
-     else traceTys "unifying" xr yr >> unify xr yr
-
-unify (JTVar i) t' = do
-  occursCheck i t'
-  case t' of
-    (JTVar i') -> do
-            newt <- newVar
-            vars <- tc_vars <$> get
-            modify (\tcs -> tcs {tc_vars = M.insert i' newt $
-                                           M.insert i  newt $
-                                           vars})
-    _ -> do
-      vars <- tc_vars <$> get
-      modify (\tcs -> tcs {tc_vars = M.insert i t' vars})
-
-unify t t'@(JTVar _)  =  t' =.= t
-
---force actual unification with free vars?
-{-
-unify :: JType -> JType -> JMonad ()
-unify (JTSat _) (JTSat _) = throwError "unification of two constrained type variables is unimplemented"
-
-unify (JTSat i) t' = do
-  cs <- lookupConstraints i
-  mapM_ go cs
-  let (subs,supers) = unzipConstrs cs
-  luball subs
-  glball supers
-  addConstraint i (Sub t')
-  b <- satInScope i
-  when (not b) $ addConstraint i (Super t')
-      where go (Sub x) = t' <: x
-            go (Super x) = x <: t'
-
-unify y x@(JTSat _) = unify x y
-
-unify (JTRec i) (JTRec i') = do
-  xl <- getRec i
-  yl <- getRec i'
-
-  --find every value in x in y, and unify each
-  let go ((l,v):lvs) = case find ((==l) . fst) yl of
-                         Nothing -> go lvs
-                         Just (_,v') -> v =.= v'
-      go _ = return ()
-
-  go xl
-
-  let xld = deleteFirstsBy ((==) `on` fst) xl yl --xs not in ys
-      yld = deleteFirstsBy ((==) `on` fst) yl xl --ys not in xs
-
-  putRec i  (xl++yld)
-  putRec i' (yl++xld)
-  return ()
-
-unify x@(JTFunc argsx retx) y@(JTFunc argsy rety) = do
- when (length argsx /= length argsy) $ tyErr2 "Couldn't match functions" x y
- zipWithM_ (=.=) argsx argsy
- retx =.= rety
--}
-unify t t' = do
-  rt  <- resolveType t
-  rt' <- resolveType t'
-  if rt == rt'
-     then return ()
-     else tyErr2 "Type error" t t'
-
-
-{--------------------------------------------------------------------
-  Clone -- i.e. schema instantiation
---------------------------------------------------------------------}
-type JMonadClone a = StateT [(Int,JType)] (ErrorT String (State TCState)) a
-
-addSub :: (Int,JType) -> JMonadClone ()
-addSub x = do
-  st <- get
-  put (x:st)
-
-findSub :: Int -> JMonadClone (Maybe JType)
-findSub i = do
-  sub <- lookup i <$> get
-  case sub of
-    Just x -> do
-              newsub <- case x of
-                          (JTVar i') -> if i' /= i then findSub i' else return $ Just x
-                          (JTRec i') -> if i' /= i then findSub i' else return $ Just x
-                          (JTSat i') -> if i' /= i then findSub i' else return $ Just x
-                          _ -> return $ Just x
-              case newsub of
-                Just ans -> return $ Just ans
-                Nothing -> return $ Just x
-    _ -> return Nothing
-
-traceSubs :: JMonadClone ()
-traceSubs = do
-  st <- get
-  trace (show st) $ return ()
-
-traceC :: JConstr -> JMonadClone ()
-traceC (Sub x) = lift $ traceTy "Sub" x
-traceC (Super x) = lift $ traceTy "Super" x
-
-clone :: JType -> JMonad JType
-clone t = evalStateT (clone'' t) []
-
-cloneMany :: [JType] -> JMonad [JType]
-cloneMany ts = evalStateT (mapM clone'' ts) []
-
---clone just replaces free variables
-clone'' :: JType -> JMonadClone JType
-clone'' x = do
-  lift $ traceTy "Cloning" x
-  c <- clone' x
-  lift $ traceTy "Clone Result" c
-  return c
-
-clone' :: JType -> JMonadClone JType
-clone' x@(JTVar _) = do
-  xt <- lift $ resolveType x
-  case xt of
-    (JTVar i) -> do
-            mbsub <- findSub i
-            case mbsub of
-              Just sub -> return sub
-              _ -> do
-                   nv <- lift $ newVar
-                   addSub (i,nv)
-                   return $ nv
-    _ -> clone' xt
-
-clone' (JTSat i) = do
-    mbsub <- findSub i
-    b <- lift $ satInScope i
-    case (mbsub,b) of
-      (Just sub,_) -> return sub
-      (_,False) -> do
-        cs <- lift $ lookupConstraints i
-        let (subs,supers) = unzipConstrs cs
-        subs' <- mapM clone' subs
-        supers' <- mapM clone' supers
-        ns@(JTSat i') <- lift $ newSatAtScope [i]
-        lift $ mapM (addConstraint i') $ zipConstrs subs' supers'
-        addSub (i,ns)
-        return ns
-      _ -> do
-        cs <- lift $ lookupConstraints i
-        let (subs,supers) = unzipConstrs cs
-        subs' <- mapM clone' subs
-        supers' <- mapM clone' supers
-        constrs <- lift $ tc_constrs <$> get
-        lift $ modify (\tcs -> tcs {tc_constrs = M.insert i (zipConstrs subs' supers') constrs})
-        addSub (i,JTSat i)
-        return (JTSat i)
-
-clone' (JTFunc args ret) = do
-  args' <- mapM clone' args
-  ret' <- clone' ret
-  return (JTFunc args' ret')
-
-clone' (JTRec i) = do
-    mbsub <- findSub i
-    case mbsub of
-      Just sub -> return sub
-      _ -> do
-        rl <- lift $ getRec i
-        rl' <- mapM go rl
-        r'@(JTRec i') <- lift $ newRec
-        lift $ putRec i' rl'
-        return r'
-  where go (i',v) = do
-             v' <- clone' v
-             return (i',v')
-
-clone' (JTList mbmulti mbmono) = do
-  mbmulti' <- maybe (return Nothing) (fmap Just . cloneRec) mbmulti
-  mbmono'  <- maybe (return Nothing) (fmap Just . clone') mbmono
-  return $ JTList mbmulti' mbmono'
-         where cloneRec x = do
-                 (JTRec i) <- clone' (JTRec x)
-                 return i
-
-clone' x = return x
-
-substitute :: JType -> JMonadClone JType
-substitute x@(JTVar _) = do
-  xt <- lift $ resolveType x
-  case xt of
-    (JTVar i) -> do
-            mbsub <- findSub i
-            case mbsub of
-              Just sub -> return sub
-              _ -> return xt
-    _ -> substitute xt
-
-substitute (JTSat i) = do
-    mbsub <- findSub i
-    b <- lift $ satInScope i
-    case (mbsub,b) of
-      (Just sub,_) -> return sub
-      (_,False) -> do
-        cs <- lift $ lookupConstraints i
-        let (subs,supers) = unzipConstrs cs
-        subs' <- mapM substitute subs
-        supers' <- mapM substitute supers
-        ns@(JTSat i') <- lift $ newSatAtScope [i]
-        lift $ mapM (addConstraint i') $ zipConstrs subs' supers'
-        addSub (i,ns)
-        return ns
-      _ -> do
-        cs <- lift $ lookupConstraints i
-        let (subs,supers) = unzipConstrs cs
-        subs' <- mapM substitute subs
-        supers' <- mapM substitute supers
-        constrs <- lift $ tc_constrs <$> get
-        lift $ modify (\tcs -> tcs {tc_constrs = M.insert i (zipConstrs subs' supers') constrs})
-        return (JTSat i)
-
-substitute (JTFunc args ret) = do
-  args' <- mapM substitute args
-  ret' <- substitute ret
-  return (JTFunc args' ret')
-
-substitute (JTRec i) = do
-    mbsub <- findSub i
-    case mbsub of
-      Just sub -> return sub
-      _ -> do
-        rl <- lift $ getRec i
-        rl' <- mapM go rl
-        r'@(JTRec i') <- lift $ newRec
-        lift $ putRec i' rl'
-        return r'
-  where go (i',v) = do
-          v' <- substitute v
-          return (i',v')
-substitute x = return x
-
-
-{--------------------------------------------------------------------
-  Constraint Resolution
---------------------------------------------------------------------}
-
-resC :: Bool -> JType -> JMonad JType
-resC inApp x = flip evalStateT [] $ do
-  lift $ traceTy "resC" x
-  c <- resC' inApp False x
-  lift $ traceTy "resC Ans" c
-  return c
-
-resC' :: Bool -> Bool -> JType -> JMonadClone JType
-resC' inApp contra x@(JTVar _) = do
-  xt <- lift $ resolveType x
-  case xt of
-    (JTVar i) -> return (JTVar i)
-    _ -> resC' inApp contra xt
-
-resC' inApp contra (JTFunc args ret) = do
-  args' <- mapM (resC' inApp True) args --mapM (resC' (not contra)) args
-  ret'  <- resC' False False ret
-  return (JTFunc args' ret')
-
-resC' inApp contra r@(JTRec i) = do
-  rl  <- lift $ getRec i
-  rl' <- mapM go rl
-  lift $ putRec i rl'
-  return r
-      where go (i',v) = do
-              v' <- resC' inApp contra v
-              return (i',v')
-
---in app we substitute, otherwise we keep as constrained
-resC' inApp contra x@(JTSat i) = do
-    mbsub <- findSub i
-    b <- lift $ satInScope i
-    case (mbsub,b) of
-      (Just sub, _) -> return sub
-      (_, False) -> do
-        JTSat (i') <- substitute (JTSat i)
-        cs <- lift (lookupConstraints i')
-        cs' <- simplifyCs cs
-        mapM traceC cs'
-        ans <- resCs cs'
-        --keep supertype, subtype constraints distinct
-        ans' <- case (contra && not inApp, ans) of
-          (True,(JTRec _)) -> trace "wao" $do
-                      ns@(JTSat i'') <- lift $ newSat --newSatAtScope [i]
-                      lift $ addConstraint i'' (Sub ans)
-                      addSub (i,ns)
-                      return ns
-          (True,(JTFunc _ _ )) -> do
-                      ns@(JTSat i'') <- lift $ newSat --newSatAtScope [i]
-                      lift $ addConstraint i'' (Sub ans)
-                      addSub (i,ns)
-                      return ns
-          _ -> return ans
-        addSub (i,ans')
-        lift $ traceTy "hai" ans'
-        return ans'
-      _ -> do
-        cs <- lift (lookupConstraints i)
-        cs' <- simplifyCs cs
-        if any isAtom cs'
-          then do
-              ans <- resCs cs'
-              addSub (i,ans)
-              return ans
-          else return x {- do
-              ns@(JTSat i') <- lift $ newSat
-              mapM (addConstraint i') cs'
-              addSub (i,ns)
-              return ns-}
-    where
-      resCs cs = do
-        let (subs,supers) = unzipConstrs cs
-        subs' <- mapM (resC' inApp contra) subs
-        supers' <- mapM (resC' inApp contra) supers
-        lubsubs   <- lift $ resolveType =<< luball subs'
-        glbsupers <- lift $ resolveType =<< glball supers'
-        case (length subs', length supers') of
-          (0,0) -> return lubsubs
-          (0,_) -> return glbsupers
-          (_,0) -> return lubsubs
-          _     -> lift $ glbsupers \/ lubsubs
-      isAtom (Sub JTNum) = True
-      isAtom (Super JTNum) = True
-      isAtom (Sub JTStr) = True
-      isAtom (Super JTStr) = True
-      isAtom _ = False
-      --isatom should go deeper into sats
-
-resC' inApp contra (JTList mbmulti mbmono) = do
-  mbmulti' <- maybe (return Nothing) (fmap Just . resRec) mbmulti
-  mbmono'  <- maybe (return Nothing) (fmap Just . (resC' inApp contra)) mbmono
-  return (JTList mbmulti' mbmono')
-         where resRec x = do
-                 (JTRec i) <- resC' inApp contra (JTRec x)
-                 return i
-
-resC' _ _ x = return x
-
-getBot (JTRec _) = return $ JTRec (-1)
-getBot (JTFunc _ ret) = do
-  ret' <- getBot ret
-  return $ JTFunc [] ret'
-getBot x@(JTVar _) = do
-  rx <- resolveType x
-  case rx of
-    (JTVar _) -> return $ BotOf rx
-    _ -> getBot rx
-getBot x@(JTList mbmulti mbmono) = do
-  mbmono' <- maybe (return Nothing) (\x -> Just <$> getBot x) mbmono
-  return $ JTList (fmap (const (negate 1)) mbmulti) mbmono --only bot of multi if multi, only bot of mono if mono!!!! TODO
-getBot x = return x
-
-simplifyCs :: [JConstr] -> JMonadClone [JConstr]
-simplifyCs cs = concat <$> mapM simplifyC cs
-
-simplifyC :: JConstr -> JMonadClone [JConstr]
-simplifyC (Sub c) = case c of
-                      JTSat i -> do
-                             b <- lift $ satInScope i
-                             if b
-                               then return [Sub c]
-                               else do
-                                   cs <- lift $ lookupConstraints i
-                                   (subs, supers) <- unzipConstrs <$> simplifyCs cs
-                                   supers' <- lift $ map Sub <$> mapM getBot supers
-                                   return $ map Sub subs ++ supers'
-                      _ -> return [Sub c]
-
-simplifyC (Super c) = case c of
-                      JTSat i -> do
-                             b <- lift $ satInScope i
-                             if b
-                               then return [Super c]
-                               else do
-                                   cs <- lift $ lookupConstraints i
-                                   (subs, supers) <- unzipConstrs <$> simplifyCs cs
-                                   subs' <- lift $ map Sub <$> mapM getBot subs
-                                   return $ map Super supers ++ subs'
-                      _ -> return [Super c]
-
-{--------------------------------------------------------------------
-  Least upper bound
---------------------------------------------------------------------}
-
---{} \/ {a} = {a}
-(\/) :: JType -> JType -> JMonad JType
-x \/ y = do
-  xr <- resolveType x
-  yr <- resolveType y
-  if xr == yr
-     then return xr
-     else do
-       traceTys "lub" xr yr
-       ans <- lub xr yr
-       traceTy "lub ans" ans
-       return ans
-
-lub :: JType -> JType -> JMonad JType
-
-lub x@(JTSat i) y@(JTSat i') = do
-  ns@(JTSat i'') <- newSatAtScope [i, i']
-  addConstraint i'' (Sub y)
-  addConstraint i'' (Sub x)
-  return ns
-
---check if value satisfies constraint then proceed with constraint
-lub (JTSat i) y = do
-  cs <- lookupConstraints i
-  mapM_ go cs
-  ns@(JTSat i') <- newSatAtScope [i]
-  mapM (addConstraint i') (Sub y : cs)
-  return ns
-      where go (Sub c) = y <: c
-            go (Super c) = c <: y
-
-lub x y@(JTSat _) = y \/ x
-
-lub x@(JTVar _) y = do
-  xt <- resolveType x
-  case xt of
-    (JTVar _) ->  do
-            ns@(JTSat i'') <- newSat
-            addConstraint i'' (Sub y)
---            addConstraint i'' (Sub x)
-            x =.= ns -- ?
-            return ns
-    _ -> xt \/ y
-
-lub x y@(JTVar _) = y \/ x
-
-lub (JTFunc args ret) (JTFunc args' ret') = do
-  args'' <- zipWithM (/\) args args'
-  ret'' <- ret \/ ret'
-  return $ JTFunc args'' ret''
-
-lub (JTRec i) (JTRec i') = do
-  xl <- getRec i
-  yl <- getRec i'
-  --find every value in x in y, and return lub of each
-  let go ((l,v):lvs) = case find ((==l) . fst) yl of
-                         Nothing -> go lvs
-                         Just (_,v') -> do
-                                    newv <- v \/ v'
-                                    ((l,newv) :) <$> go lvs
-      go _ = return []
-  xlyl <- go xl
-
-  --then add every value of x not in y and every value of y not in x
-  let xld = deleteFirstsBy ((==) `on` fst) xl yl --xs not in ys
-      yld = deleteFirstsBy ((==) `on` fst) yl xl --ys not in xs
-
-  r'@(JTRec i'') <- newRec
-  putRec i'' $ xlyl ++ xld ++ yld
-  return r'
-
-lub (JTList mbmulti mbmono) (JTList mbmulti' mbmono') = do
-  mbmulti'' <- case (mbmulti, mbmulti') of
-                 (Just multi, Just multi') -> do
-                      (JTRec i) <- (JTRec multi) \/ (JTRec multi')
-                      return $ Just i
-                 _ -> return Nothing
-  mbmono'' <- case (mbmono, mbmono') of
-                (Just mono, Just mono') -> Just <$> mono \/ mono'
-                _ -> return Nothing
-  return $ JTList mbmulti'' mbmono''
-
-lub x y
-  | x == y = return x
-  | otherwise = do
-        tyErr2 "No Least Upper Bound Exists" x y
-
-luball :: [JType] -> JMonad JType
-luball (h:xs) = do
-  foldM (\x y -> x \/ y) h xs
-luball [] = newVar
-
-
-{--------------------------------------------------------------------
- Greatest Lower bound
---------------------------------------------------------------------}
-
-(/\) :: JType -> JType -> JMonad JType
-x /\ y = do
-  xr <- resolveType x
-  yr <- resolveType y
-  if xr == yr
-     then return xr
-     else do
-       traceTys "glb" xr yr
-       ans <- glb xr yr
-       traceTy "glb ans" ans
-       return ans
-
-glb :: JType -> JType -> JMonad JType
-glb (JTSat i) (JTSat i') = do
-  ns <- newSatAtScope [i, i']
-  addConstraint i (Super ns)
-  addConstraint i' (Super ns)
-  return ns
-
---glb of a free variable and anything is a subtype of the free var and the other thing
-glb x@(JTVar _) y = do
-  xt <- resolveType x
-  case xt of
-    (JTVar _) -> do
-            ns@(JTSat i) <- newSatAtScope [-1] --always right?
---            addConstraint i (Super x)
-            addConstraint i (Super y)
-            x =.= ns -- ?
-            return ns
-    _ -> x /\ y
-
-glb x y@(JTVar _) = y /\ x
-
-glb x@(JTSat i) y = do
-  ns@(JTSat i') <- newSatAtScope [i]
-  addConstraint i' (Super y)
-  addConstraint i' (Super x)
-  return ns
-
-glb x y@(JTSat _) = y /\ x
-
-glb (JTFunc args ret) (JTFunc args' ret') = do
-  args'' <- zipWithM (\/) args args'
-  ret'' <- ret /\ ret'
-  return $ JTFunc args'' ret''
-
-glb (JTRec i) (JTRec i') = do
-  xl <- getRec i
-  yl <- getRec i'
-    --find every value in x in y, and return glb of each
-  let go ((l,v):lvs) = case find ((==l) . fst) yl of
-                         Nothing -> go lvs
-                         Just (_,v') -> do
-                                    newv <- err2may (v /\ v')
-                                    case newv of
-                                      Just nv -> ((l,nv) :) <$> go lvs
-                                      Nothing -> go lvs
-      go _ = return []
-  r'@(JTRec i'') <- newRec
-  putRec i'' =<< go xl
-  return r'
-           where err2may v = fmap Just v `orElse` return Nothing
-
-glb (JTList mbmulti mbmono) (JTList mbmulti' mbmono') = do
-  mbmulti'' <- case (mbmulti, mbmulti') of
-                 (Just multi, Just multi') -> do
-                      (JTRec i) <- (JTRec multi) /\ (JTRec multi')
-                      return $ Just i
-                 _ -> return Nothing
-  mbmono'' <- case (mbmono, mbmono') of
-                (Just mono, Just mono') -> Just <$> mono /\ mono'
-                _ -> return Nothing
-  return $ JTList mbmulti'' mbmono''
-
-
-glb x y
-  | x == y = return x
-  | otherwise = tyErr2 "No Greatest Lower Bound Exists" x y
-
-glball :: [JType] -> JMonad JType
-glball (h:xs) = do
-  foldM (\x y -> x /\ y) h xs
-glball [] = newVar
-
-{--------------------------------------------------------------------
-  Typecheck
---------------------------------------------------------------------}
-
-class JTypeCheck a where
-    typecheck :: a -> JMonad JType
-
-instance JTypeCheck JStat where
-    typecheck (DeclStat i) = addNewVar i >> return JTStat
-    typecheck (ReturnStat e) = typecheck e
-    typecheck (BlockStat xs) = typecheck xs
-    typecheck (AssignStat x y) = do
-                            xt <- typecheckLhs x
-                            yt <- typecheck y
-                            yt <: xt
-                            return JTStat
-
-    typecheck (IfStat e s s') = do
-      (<=.= JTBool) =<< typecheck e
-      if (s' == BlockStat [])
-        then inConditional $ typecheck s
-        else inConditional $ do
-          --can we allow assignments that happen in both, or is this way too hard?
-          st <- typecheck s
-          st' <- typecheck s'
-          chkNoNull [st,st']
-          st /\ st'
-    typecheck (WhileStat e s) = do
-      (<=.= JTBool) =<< typecheck e
-      inConditional $ typecheck s
-
-    --for in statements iterate over names
-    typecheck (ForInStat False i e s) = withLocalScope' [i] $ do
-      (JTStr =.=) =<< lookupEnvErr i
-      et <- resolveType =<< typecheck e
-      case et of
-          --list case
-          JTRec _ -> return ()
-          _ -> tyErr1 "Attempt to use 'for in' construct with improper type" et
-      inConditional $ typecheck s
-
-    --for each in statements iterate over property values
-    typecheck (ForInStat True ident e s) = withLocalScope' [ident] $ do
-      et <- resolveType =<< typecheck e
-      case et of
-        --list case
-        JTRec i -> do
-                --el <- map snd . init <$> rec2list et
-                el <- map snd <$> getRec i
-                case el of
-                  [] -> return ()
-                  es -> do
-                       e' <- glball es
-                       (e' =.=) =<< lookupEnvErr ident
-        _ -> tyErr1 "Attempt to use 'for each in' construct with improper type" et
-      inConditional $ typecheck s
-    typecheck (ApplStat e args) = typecheck (ApplExpr e args) >> return JTStat
-    typecheck (PostStat s e) = typecheck (PostExpr s e) >> return JTStat
-    typecheck BreakStat = return JTStat
-    --Switch
-    --Unsat $ Anti -- anti can take signature!?
-
----add special cases in selectors for lists, etc!
-
-typecheckLhs :: JExpr -> JMonad JType
-typecheckLhs (SelExpr e1 ident@(StrI s)) = do
-  e1t <- typecheck e1
-  case e1t of
-    JTRec i -> do
-             newt <- recLookup ident e1t
-             canextend <- tc_canextend <$> get
-             case newt of
-               Just t -> return t
-               Nothing -> if canextend
-                           then do
-                             v <- newVar
-                             rs <- getRec i
-                             putRec i $ (ident,v):rs
-                             return v
-                           else tyErr1 "Attempt to extend record in conditional code" e1t
-    JTSat i -> do
-             ns <- newSatAtScope [i]
-             nr@(JTRec i') <- newRec
-             putRec i' [(ident,ns)]
-             addConstraint i (Sub nr)
-             return ns
-    _ -> tyErr1 ("No property " ++ s ++ " in type") e1t
-
-typecheckLhs x = typecheck x
-
-
-instance JTypeCheck JExpr where
-    typecheck (ValExpr v) = typecheck v
-    typecheck (SelExpr e1 ident@(StrI s)) = do
-                            e1t <- typecheck e1
-                            newt <- recLookup ident e1t
-                            case (newt, e1t) of
-                              (Just t, _) -> return t
-                              (Nothing, JTSat i) -> do
-                                   ns <- newSatAtScope [i]
-                                   nr@(JTRec i') <- newRec
-                                   putRec i' [(ident,ns)]
-                                   addConstraint i (Sub nr)
-                                   return ns
-                              (Nothing, _) -> tyErr1 ("No property " ++ s ++ " in type") e1t
-
-    --NewExpr -- this is really a special appl
-    --Unsat & Anti
-    typecheck (InfixExpr s e1 e2)
-        | s `elem` ["-","/","*"] = setFixed JTNum
-        | s == "+" = setFixed JTNum `orElse` setFixed JTStr --TODO: Intersection types
-        | s `elem` [">","<","==","/="] = setFixed JTNum >> return JTBool
-        | s `elem` ["||","&&"] = setFixed JTBool
-        | otherwise = throwError $ "Unhandled operator: " ++ s
-      where setFixed t = do
-              (<=.=) t =<< typecheck e1
-              (<=.=) t =<< typecheck e2
-              return t
-
-    --check that e is either a selexpr or a var or an idxexpr
-    typecheck (PostExpr _ e) = case e of
-                                 (SelExpr _ _) -> go
-                                 (ValExpr (JVar _)) -> go
-                                 (IdxExpr _ _) -> go
-                                 _ -> tyErr1 "Value not compatible with postfix assignment" =<< typecheck e
-        where go = ((<=.= JTNum) =<< typecheck e) >> return JTNum
-
-    typecheck (IfExpr e e1 e2) = do
-                            (<=.= JTBool) =<< typecheck e
-                            e1t <- typecheck e1
-                            e2t <- typecheck e2
-                            e1t /\ e2t
-
-    typecheck (ApplExpr e args) = do
-                            et <- resolveType =<< typecheck e
-                            argst <- mapM (resolveType <=< typecheck) args
-                            appFun et argst
-    typecheck (IdxExpr e1 e2) = do
-                            e1t <- resolveType =<< typecheck e1
-                            e2t <- resolveType =<< typecheck e2
-                            case e1t of
-                              (JTList _ (Just t)) -> return t
-                              (JTList (Just r) _)  -> case e2 of
-                                        (ValExpr (JStr i)) -> do
-                                          newt <- recLookup (StrI i) (JTRec r)
-                                          case newt of
-                                            Just t -> return t
-                                            Nothing -> tyErr1 ("No property " ++ i ++ " in type") e1t
-                                        (ValExpr (JInt i)) -> do
-                                          newt <- recLookup (StrI $ show i) (JTRec r)
-                                          case newt of
-                                            Just t -> return t
-                                            Nothing -> tyErr1 ("No property " ++ show i ++ " in type") e1t
-                                        _ -> tyErr1 "Cannot index into hash/tuple with runtime expression" e1t
-                              (JTList _ _) -> tyErr1 "List/Hash with no inhabited types" e1t
-                              (JTSat i) -> do
-                                      ns <- newSatAtScope [i]
-                                      mbrec <- case e2 of
-                                         (ValExpr (JStr i)) -> do
-                                            nr@(JTRec i') <- newRec
-                                            putRec i' [(StrI i,ns)]
-                                            return $ Just i'
-                                         (ValExpr (JInt i)) -> do
-                                            nr@(JTRec i') <- newRec
-                                            putRec i' [(StrI $ show i,ns)]
-                                            return $ Just i'
-                                         _ -> return Nothing
-                                      addConstraint i (Sub $ JTList mbrec (Just ns))
-                                      return ns
-                              _ -> tyErr1 "Attempting to index into something of type" e1t
-
-appFun :: JType -> [JType] -> JMonad JType
-appFun(JTFunc args ret) appArgs = do
-    when (length args > length appArgs) $ tyErr2l "Mismatched argument lengths" args appArgs
-    appArgs' <- cloneMany appArgs
-    (JTFunc args' ret') <- clone (JTFunc args ret)
-    zipWithM (<:) appArgs' args'
-    (JTFunc args'' ret'') <- withLocalScope [] $ resC True $ JTFunc args' ret'
---    zipWithM (=.=) args'' appArgs'
-    return ret''
---    withLocalScope [] $ resC True ret''
-
-appFun (JTSat i) args' = do
-  s  <- newSatAtScope [i]
-  mapM (bumpScope i) args'
-  addConstraint i (Sub $ JTFunc args' s)
-  return s
-
-appFun x _ = tyErr1 "Attempting to apply as a function something of type"  x
-
-instance JTypeCheck JVal where
-    typecheck (JVar i) = case i of
-                           StrI "true" -> return JTBool
-                           StrI "false" -> return JTBool
-                           StrI "null"  -> newVar
-                           StrI _ -> resolveType =<< lookupEnvErr i
-    typecheck (JInt _) = return JTNum
-    typecheck (JDouble _) = return JTNum
-    typecheck (JStr _) = return JTStr
-    typecheck (JFunc args stat) =
-                           withLocalScope args ( do
-                             argst <- mapM (typecheck . JVar) args
-                             rett <- typecheck stat
-                             resC False $ JTFunc argst rett)
-    typecheck (JHash m) = do
-            let (is, es) = unzip $ M.toList m
-            ets <- mapM typecheck es
-            let initialrec
-                    | null is = []
-                    | otherwise =  zip (map StrI is) ets
-            r@(JTRec i) <- newRec
-            putRec i initialrec
-            return r
-    typecheck (JList es) = do
-            (JTRec i) <- typecheck $ JHash $ M.fromList (zip (map show [1..]) es)
-            es' <- mapM typecheck es
-            e'' <- (Just <$> glball es') `orElse` return Nothing
-            return $ JTList (Just i) e''
-    --List
-
-instance JTypeCheck [JStat] where
-    typecheck [] = return JTStat
-    typecheck stats = do
-      ts <- filter (/=JTStat) <$> (mapM resolveType =<< mapM typecheckAnnotated stats)
-      case ts of
-        [] -> return JTStat
-        _ -> chkNoNull ts >> glball ts
-
-typecheckAnnotated :: (JMacro a, JsToDoc a, JTypeCheck a) => a -> JMonad JType
-typecheckAnnotated stat = typecheck stat `catchError` \ e -> throwError $ e ++ "\nIn statement:\n" ++ renderStyle (style {mode = OneLineMode}) (renderJs stat)
diff --git a/Language/Javascript/JMacro/Types.hs b/Language/Javascript/JMacro/Types.hs
new file mode 100644
--- /dev/null
+++ b/Language/Javascript/JMacro/Types.hs
@@ -0,0 +1,154 @@
+{-# Language StandaloneDeriving, DeriveDataTypeable, FlexibleContexts, UndecidableInstances, FlexibleInstances #-}
+module Language.Javascript.JMacro.Types (
+  JType(..), Constraint(..), JLocalType, VarRef, anyType, parseType, runTypeParser
+  ) where
+
+import Control.Applicative hiding ((<|>))
+import Data.Char
+
+import Data.Maybe(fromMaybe)
+
+import Text.ParserCombinators.Parsec
+import Text.Parsec.Prim hiding (runParser, try)
+import Text.ParserCombinators.Parsec.Language(emptyDef)
+import qualified Text.ParserCombinators.Parsec.Token as P
+
+import qualified Data.Map as M
+import Data.Map (Map)
+import Data.Set (Set)
+import Data.Generics
+
+type VarRef = (Maybe String, Int)
+
+-- sum types for list/record, map/record
+
+data JType = JTNum
+           | JTString
+           | JTBool
+           | JTStat
+           | JTFunc [JType] (JType)
+           | JTList JType
+           | JTMap  JType
+           | JTRecord JType (Map String JType)
+           | JTRigid VarRef (Set Constraint)
+           | JTImpossible
+           | JTFree VarRef
+           | JTForall [VarRef] JType
+             deriving (Eq, Ord, Read, Show, Typeable, Data)
+
+data Constraint = Sub JType
+                | Super JType
+                -- | Choice Constraint Constraint
+                -- | GLB (Set JType)
+                -- | LUB (Set JType)
+                  deriving (Eq, Ord, Read, Show, Typeable, Data)
+
+type JLocalType = ([(VarRef,Constraint)], JType)
+
+type TypeParserState = (Int, Map String Int)
+
+typLang :: P.LanguageDef TypeParserState
+typLang = emptyDef {
+           P.reservedNames = ["()","->"],
+           P.reservedOpNames = ["()","->","::"],
+           P.identLetter = alphaNum <|> oneOf "_$",
+           P.identStart  = letter <|> oneOf "_$"
+          }
+
+lexer = P.makeTokenParser typLang
+
+whiteSpace= P.whiteSpace lexer
+symbol    = P.symbol lexer
+parens    = P.parens lexer
+braces    = P.braces lexer
+brackets  = P.brackets lexer
+dot       = P.dot lexer
+colon     = P.colon lexer
+semi      = P.semi lexer
+identifier= P.identifier lexer
+reserved  = P.reserved lexer
+reservedOp= P.reservedOp lexer
+commaSep1 = P.commaSep1 lexer
+commaSep  = P.commaSep  lexer
+
+lexeme    = P.lexeme lexer
+
+parseType :: String -> Either ParseError JType
+parseType s = runParser anyType (0,M.empty) "" s
+
+parseConstrainedType s = runParser constrainedType (0,M.empty) "" s
+
+runTypeParser = withLocalState (0,M.empty) (try (parens constrainedType) <|> constrainedType) -- anyType
+
+withLocalState :: (Functor m, Monad m) => st -> ParsecT s st m a -> ParsecT s st' m a
+withLocalState initState subParser = mkPT $
+    \(State input pos otherState) -> fixState otherState <$> runParsecT subParser (State input pos initState)
+      where
+        fixState s res = (fmap . fmap) go res
+            where go (Ok a (State input pos _localState) pe) = Ok a (State input pos s) pe
+                  go (Error e) = (Error e)
+
+
+type TypeParser a = CharParser TypeParserState a
+
+constrainedType :: TypeParser JLocalType
+constrainedType = do
+  c <- try (Just <$> (constraintHead <* reservedOp "=>")) <|> return Nothing
+  t <- anyType
+  return (fromMaybe [] c, t)
+
+--do we need to read supertype constraints, i.e. subtype constraints which have the freevar on the right??
+constraintHead :: TypeParser [(VarRef,Constraint)]
+constraintHead = parens go <|> go
+    where go = commaSep1 constraint
+          constraint = do
+            r <- freeVarRef =<< identifier
+            c <- (reservedOp "<:" >> (return Sub)) <|>
+                 (reservedOp ":>" >> (return Super))
+            t <- anyType
+            return $ (r, c t)
+
+anyType :: TypeParser JType
+anyType = try (parens anyType) <|> funOrAtomType <|> listType <|> recordType
+
+funOrAtomType :: TypeParser JType
+funOrAtomType = do
+  r <- anyNestedType `sepBy1` (lexeme (string "->"))
+  return $ case r of
+    [x] -> x
+    (x:xs) -> JTFunc (init r) (last r)
+    _ -> error "funOrAtomType"
+
+listType :: TypeParser JType
+listType = JTList <$> brackets anyType
+
+anyNestedType :: TypeParser JType
+anyNestedType = nullType <|> parens anyType <|> atomicType <|> listType <|> recordType
+
+nullType = reservedOp "()" >> return JTStat
+
+atomicType :: TypeParser JType
+atomicType = do
+  a <- identifier
+  case a of
+    "Num" -> return JTNum
+    "String" -> return JTString
+    "Bool" -> return JTBool
+    (x:xs) | isUpper x -> fail $ "Unknown type: " ++ a
+           | otherwise -> JTFree <$> freeVarRef a
+    _ -> error "typeAtom"
+
+recordType :: TypeParser JType
+recordType = braces $ JTRecord JTImpossible . M.fromList <$> commaSep namePair
+    where namePair = do
+            n <- identifier
+            reservedOp "::"
+            t <- anyType
+            return (n, t)
+
+freeVarRef :: String -> TypeParser VarRef
+freeVarRef v = do
+  (i,m) <- getState
+  (\x -> (Just v, x)) <$> maybe (setState (i+1,M.insert v i m) >> return i)
+                                 return
+                                 (M.lookup v m)
diff --git a/jmacro.cabal b/jmacro.cabal
--- a/jmacro.cabal
+++ b/jmacro.cabal
@@ -1,5 +1,5 @@
 name:                jmacro
-version:             0.3.2
+version:             0.4.1
 synopsis:            QuasiQuotation library for programmatic generation of Javascript code.
 description:         Javascript syntax, functional syntax, hygienic names, compile-time guarantees of syntactic correctness, limited typechecking.
 category:            Language
@@ -7,25 +7,24 @@
 license-file:        LICENSE
 author:              Gershom Bazerman
 maintainer:          gershomb@gmail.com
-Tested-With:         GHC == 6.10.3
+Tested-With:         GHC == 6.12.3
 Build-Type:          Simple
 Cabal-Version:       >= 1.6
 
 
 library
-  build-depends:     base >= 4, base < 5, containers, pretty, safe >= 0.2, parsec >= 2.1, template-haskell >= 2.3, mtl, haskell-src-exts, haskell-src-exts-qq, bytestring >= 0.9, syb, pcre-light, json
+  build-depends:     base >= 4, base < 5, containers, pretty, safe >= 0.2, parsec > 3.0, template-haskell >= 2.3, mtl > 1.1 , haskell-src-exts, haskell-src-meta, bytestring >= 0.9, syb, pcre-light, json
 
   exposed-modules:   Language.Javascript.JMacro
                      Language.Javascript.JMacro.Util
-                     Language.Javascript.JMacro.Typed
+                     Language.Javascript.JMacro.TypeCheck
+                     Language.Javascript.JMacro.Types
                      Language.Javascript.JMacro.Prelude
                      Language.Javascript.JMacro.Rpc
   other-modules:     Language.Javascript.JMacro.Base
                      Language.Javascript.JMacro.QQ
                      Language.Javascript.JMacro.ParseTH
   ghc-options:       -Wall
-  if impl(ghc >= 6.8)
-    ghc-options:     -fwarn-tabs
 
 executable jmacro
   build-depends: parseargs