diff --git a/gcl/gcl.cabal b/gcl/gcl.cabal
index ed7907bd..af1152cb 100644
--- a/gcl/gcl.cabal
+++ b/gcl/gcl.cabal
@@ -30,6 +30,7 @@ library
       GCL.Range
       GCL.Substitution
       GCL.Type
+      GCL.Type2.Common
       GCL.Type2.Infer
       GCL.Type2.MiniAst
       GCL.Type2.RSE
diff --git a/gcl/src/GCL/Type2/Common.hs b/gcl/src/GCL/Type2/Common.hs
new file mode 100644
index 00000000..0084417c
--- /dev/null
+++ b/gcl/src/GCL/Type2/Common.hs
@@ -0,0 +1,15 @@
+module GCL.Type2.Common where
+
+import Data.Map (Map)
+import qualified Syntax.Abstract.Types as A
+import Syntax.Common.Types (Name)
+
+type TyVar = Name
+
+type TmVar = Name
+
+data Scheme
+  = Forall [TyVar] A.Type -- ∀α₁, ..., αₙ. t
+  deriving (Eq, Show)
+
+type Env = Map TmVar Scheme
diff --git a/gcl/src/GCL/Type2/Infer.hs b/gcl/src/GCL/Type2/Infer.hs
index c562826e..8a31378f 100644
--- a/gcl/src/GCL/Type2/Infer.hs
+++ b/gcl/src/GCL/Type2/Infer.hs
@@ -18,6 +18,7 @@ import qualified Data.Text as Text
 import Debug.Trace
 import GCL.Range (MaybeRanged (maybeRangeOf), Range)
 import GCL.Type (TypeError (..))
+import GCL.Type2.Common (Env, Scheme (..), TyVar)
 import GCL.Type2.RSE
 import qualified Hack
 import Pretty
@@ -30,16 +31,6 @@ newtype Inference = Inference
   { _counter :: Int
   }
 
-type TyVar = Name
-
-type TmVar = Name
-
-data Scheme
-  = Forall [TyVar] A.Type -- ∀α₁, ..., αₙ. t
-  deriving (Show)
-
-type Env = Map TmVar Scheme
-
 instance {-# OVERLAPPING #-} Show Env where
   show e = intercalate "\n" $ map (\(var, scheme) -> s var <> " :: " <> showScheme scheme) (Map.toList e)
     where
@@ -73,7 +64,6 @@ checkDuplicateNames names =
 checkOccurs :: Name -> A.Type -> Bool
 checkOccurs name ty = Set.member name (freeTypeVars ty)
 
--- TODO: maybe `Subst` type class?
 applySubst :: Subst -> A.Type -> A.Type
 applySubst _ ty@A.TBase {} = ty
 applySubst subst (A.TArray interval ty range) =
@@ -112,11 +102,11 @@ applySubstExpr subst (T.Op op ty) = T.Op op (applySubst subst ty)
 applySubstExpr subst (T.Chain chain) = T.Chain (applySubstChain subst chain)
 applySubstExpr subst (T.App e1 e2 range) = T.App (applySubstExpr subst e1) (applySubstExpr subst e2) range
 applySubstExpr subst (T.Lam param ty body range) = T.Lam param (applySubst subst ty) (applySubstExpr subst body) range
-applySubstExpr subst (T.Quant _ _ _ _ _) = undefined
+applySubstExpr subst (T.Quant op args cond expr range) = T.Quant (applySubstExpr subst op) args (applySubstExpr subst cond) (applySubstExpr subst expr) range
 applySubstExpr subst (T.ArrIdx arr index range) = T.ArrIdx (applySubstExpr subst arr) (applySubstExpr subst index) range
 applySubstExpr subst (T.ArrUpd arr index expr range) = T.ArrUpd (applySubstExpr subst arr) (applySubstExpr subst index) (applySubstExpr subst expr) range
 applySubstExpr subst (T.Case expr clauses range) = T.Case (applySubstExpr subst expr) (map (applySubstClause subst) clauses) range
-applySubstExpr subst (T.Subst _ _) = undefined
+applySubstExpr subst (T.Subst _ _) = undefined -- XXX: what is this?
 applySubstExpr subst (T.EHole text range ty holeNumber) = T.EHole text range (applySubst subst ty) holeNumber
 
 applySubstChain :: Subst -> T.Chain -> T.Chain
@@ -183,25 +173,28 @@ freeTypeVarsScheme (Forall tvs ty) =
 
 unify :: A.Type -> A.Type -> Maybe Range -> Result Subst
 unify (A.TBase t1 _) (A.TBase t2 _) _ | t1 == t2 = return mempty
-unify (A.TArray _i1 t1 _) (A.TArray _i2 t2 _) l = unify t1 t2 l
-unify (A.TArray _i t1 _) (A.TApp (A.TApp (A.TOp (Arrow _)) i _) t2 _) l = do
-  s1 <- unify i typeInt l
-  s2 <- unify t1 t2 l
+unify (A.TArray _i1 t1 _) (A.TArray _i2 t2 _) r = unify t1 t2 r
+unify (A.TArray _i t1 _) (A.TApp (A.TApp (A.TOp (Arrow _)) i _) t2 _) r = do
+  s1 <- unify i typeInt r
+  s2 <- unify t1 t2 r
   return (s2 <> s1)
-unify (A.TOp op1) (A.TOp op2) _ | op1 == op2 = return mempty
-unify (A.TData n1 l1) (A.TData n2 l2) _ = undefined
-unify (A.TApp a1 a2 _) (A.TApp b1 b2 _) l = do
-  s1 <- unify a1 b1 l
-  s2 <- unify (applySubst s1 a2) (applySubst s1 b2) l
+unify (A.TOp (Arrow _)) (A.TOp (Arrow _)) _ = return mempty
+unify t1@(A.TData n1 _) t2@(A.TData n2 _) r =
+  if n1 == n2
+    then return mempty
+    else throwError $ UnifyFailed t1 t2 r
+unify (A.TApp a1 a2 _) (A.TApp b1 b2 _) r = do
+  s1 <- unify a1 b1 r
+  s2 <- unify (applySubst s1 a2) (applySubst s1 b2) r
   return $ s2 <> s1
-unify (A.TVar name _) ty l = unifyVar name ty l
-unify ty (A.TVar name _) l = unifyVar name ty l
+unify (A.TVar name _) ty r = unifyVar name ty r
+unify ty (A.TVar name _) r = unifyVar name ty r
 unify A.TType A.TType _ = return mempty
-unify t1 t2 l =
+unify t1 t2 r =
   trace
     (show (pretty t1) <> " != " <> show (pretty t2))
     throwError
-    $ UnifyFailed t1 t2 l
+    $ UnifyFailed t1 t2 r
 
 unifyVar :: Name -> A.Type -> Maybe Range -> Result Subst
 unifyVar name ty range
@@ -211,11 +204,6 @@ unifyVar name ty range
       let subst = Map.singleton name ty
        in return subst
 
--- (-->) :: a -> b -> (a --> b)
---
-
--- * -> *
-
 typeToKind :: A.Type -> RSE Env Inference A.Type
 typeToKind A.TBase {} = return A.TType
 typeToKind A.TArray {} = return $ A.TType `typeToType` A.TType
@@ -227,35 +215,24 @@ typeToKind (A.TData name _) = do
   case Map.lookup name env of
     Just (Forall _ k) -> return k
     Nothing -> throwError $ NotInScope name
-typeToKind (A.TVar name _) = do
-  env <- ask
-  case Map.lookup name env of
-    -- BUG: this probably wrong
-    Just (Forall tyParams _) -> return $ foldr (\_ acc -> A.TType `typeToType` acc) A.TType tyParams -- XXX: is this correct?
-    Nothing -> throwError $ NotInScope name
-typeToKind A.TMetaVar {} = undefined
+typeToKind (A.TVar _ _) = do
+  return A.TType
+typeToKind (A.TMetaVar name range) = typeToKind (A.TVar name range) -- XXX: hack
 typeToKind A.TType = return A.TType
 typeToKind (A.TApp t1 t2 _) = do
   t1Kind <- typeToKind t1
-  -- BUG: this is wrong, didn't even check k2
+  t2Kind <- typeToKind t2
   case t1Kind of
     (A.TApp (A.TApp (A.TOp (Arrow _)) k1 _) k2 _) -> do
-      _ <- lift $ unify t2 k1 (maybeRangeOf t2)
+      _ <- lift $ unify t2Kind k1 (maybeRangeOf t2)
       return k2
-    (A.TApp A.TType _ range) -> throwError $ PatternArityMismatch 2 1 range
-    -- \* *
-    (A.TApp _ (A.TApp _ _ _) range) -> throwError $ PatternArityMismatch 1 2 range -- (* -> *) (* -> *)
+    A.TType -> do
+      -- \* *
+      throwError $ UnifyFailed A.TType t2Kind (maybeRangeOf t1)
     ty' -> do
       traceM $ show ty'
       error "unknown kind"
 
--- typeToKind (TApp f x) = do
---  (k1 -> k2) <- typeToKind f
---  typeToKind x == k1
---  return k2
-
--- (* -> * -> *) (* -> *)
-
 -- we keep `T.Expr` to prevent repeating calculate the same expression
 infer :: A.Expr -> RSE Env Inference (Subst, A.Type, T.Expr)
 infer (A.Lit lit range) = inferLit lit range
diff --git a/gcl/src/GCL/Type2/ToTyped.hs b/gcl/src/GCL/Type2/ToTyped.hs
index 45a8d16d..f43c771a 100644
--- a/gcl/src/GCL/Type2/ToTyped.hs
+++ b/gcl/src/GCL/Type2/ToTyped.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
 
@@ -14,30 +13,30 @@ import qualified Data.Map as Map
 import Debug.Trace
 import GCL.Range (MaybeRanged (maybeRangeOf), Range)
 import GCL.Type (TypeError (..))
+import GCL.Type2.Common (Env, Scheme (..))
 import GCL.Type2.Infer
 import GCL.Type2.RSE
 import qualified Hack
 import Pretty
 import qualified Syntax.Abstract.Types as A
-import Syntax.Common.Types (Name (Name))
+import Syntax.Common.Types (Name)
 import qualified Syntax.Typed.Types as T
 
--- TODO: check valid type
--- prevent
--- `con A : Int Int`
-collectDeclToEnv :: A.Declaration -> Result Env
+collectDeclToEnv :: A.Declaration -> RSE Env Inference Env
 collectDeclToEnv (A.ConstDecl names ty _ _) = do
-  checkDuplicateNames names
+  lift $ checkDuplicateNames names
+  _ <- typeToKind ty
   return $ Map.fromList $ map (\name -> (name, Forall [] ty)) names
 collectDeclToEnv (A.VarDecl names ty _ _) = do
-  checkDuplicateNames names
+  lift $ checkDuplicateNames names
+  _ <- typeToKind ty
   return $ Map.fromList $ map (\name -> (name, Forall [] ty)) names
 
 type DefnMap = Map A.Definition Scheme
 
 -- XXX: is checking duplicate definition required here?
 collectDefnToEnv :: A.Definition -> RSE Env Inference Env
-collectDefnToEnv (A.TypeDefn name args ctors _loc) = do
+collectDefnToEnv (A.TypeDefn name args ctors _range) = do
   let nameTy = A.TData name (maybeRangeOf name)
 
   let kind = foldr (\_ acc -> A.TType `typeToType` acc) A.TType args
@@ -60,29 +59,29 @@ collectDefnToEnv (A.TypeDefn name args ctors _loc) = do
           (Map.member ctorName env')
           (throwError $ DuplicatedIdentifiers [ctorName])
 
-        let vars = extractMetaVars ctorArgs
-        let diff = filter (`notElem` args) (nub vars)
+        let (tvs, ctorTy) = extractMetaVars nameTy ctorArgs
+        let diff = filter (`notElem` args) (nub tvs)
 
         case diff of
-          [] -> return $ Map.insert ctorName (Forall args (foldr (typeToType . toTVar) nameTy vars)) env'
+          [] -> return $ Map.insert ctorName (Forall args ctorTy) env'
           (x : _) -> throwError $ NotInScope x
     )
     kindEnv
     ctors
   where
-    extractMetaVars =
-      map
-        ( \case
-            (A.TMetaVar n _) -> n
-            _ -> error "impossible"
+    extractMetaVars baseTy =
+      foldr
+        ( \argType (ftvs, argTypes) ->
+            case argType of
+              (A.TMetaVar n _) -> (n : ftvs, A.TVar n (maybeRangeOf n) `typeToType` argTypes)
+              ty -> (ftvs, ty `typeToType` argTypes)
         )
-
-    toTVar v = A.TVar v (maybeRangeOf v)
+        ([], baseTy)
 collectDefnToEnv (A.FuncDefnSig name ty _ _) = do
   env <- ask
   case Map.lookup name env of
     Nothing -> return $ Map.singleton name (Forall [] ty)
-    Just _ -> undefined
+    Just _ -> throwError $ DuplicatedIdentifiers [name]
 collectDefnToEnv (A.FuncDefn name body) = do
   (_, ty, _) <- infer body
   return $ Map.singleton name (Forall [] ty)
@@ -91,7 +90,7 @@ class ToTyped a t | a -> t where
   toTyped :: a -> RSE Env Inference t
 
 instance ToTyped A.Program T.Program where
-  toTyped (A.Program defns decls exprs stmts loc) = do
+  toTyped (A.Program defns decls exprs stmts range) = do
     traceM $ "defns: " <> show (pretty defns)
     traceM $ "decls: " <> show (pretty decls)
     traceM $ "exprs: " <> show (pretty exprs)
@@ -100,7 +99,7 @@ instance ToTyped A.Program T.Program where
     declEnv <-
       foldM
         ( \env' decl -> do
-            declEnv' <- lift $ collectDeclToEnv decl
+            declEnv' <- collectDeclToEnv decl
             let dups = declEnv' `Map.intersection` env'
             unless
               (null dups)
@@ -112,10 +111,8 @@ instance ToTyped A.Program T.Program where
     defnEnv <-
       foldM
         ( \env' defn -> do
-            -- traceM $ Hack.sshow defn
             -- NOTE: definitions have to be in order
             defnEnv <- local (const env') (collectDefnToEnv defn)
-            -- traceM $ show defnEnv
             return $ defnEnv <> env'
         )
         declEnv
@@ -133,56 +130,69 @@ instance ToTyped A.Program T.Program where
     typedDecls <-
       mapM
         ( \decl -> do
-            -- traceM $ show decl
             local (const newEnv) (toTyped decl)
         )
         decls
     typedExprs <- local (const newEnv) (mapM toTyped exprs)
     typedStmts <- local (const newEnv) (mapM toTyped stmts)
-    return $ T.Program typedDefns typedDecls typedExprs typedStmts loc
+    return $ T.Program typedDefns typedDecls typedExprs typedStmts range
 
 instance ToTyped A.Definition T.Definition where
-  toTyped (A.TypeDefn name args ctors loc) = return $ T.TypeDefn name args (map toTypedTypeDefnCtor ctors) loc
-  toTyped (A.FuncDefnSig name ty prop loc) = undefined
+  toTyped (A.TypeDefn name args ctors range) = return $ T.TypeDefn name args (map toTypedTypeDefnCtor ctors) range
+  toTyped (A.FuncDefnSig name ty prop range) = toTypedFuncDefnSig name ty prop range
   toTyped (A.FuncDefn name body) = T.FuncDefn name <$> toTyped body
 
 toTypedTypeDefnCtor :: A.TypeDefnCtor -> T.TypeDefnCtor
 toTypedTypeDefnCtor (A.TypeDefnCtor name args) = T.TypeDefnCtor name args
 
+-- FIXME: prop is not needed, remove in the future
+toTypedFuncDefnSig :: Name -> A.Type -> Maybe A.Expr -> Maybe Range -> RSE Env Inference T.Definition
+toTypedFuncDefnSig name ty prop range = do
+  tyKind <- typeToKind ty
+
+  when
+    (tyKind /= A.TType)
+    (throwError $ UnifyFailed tyKind A.TType range)
+
+  return (T.FuncDefnSig' name tyKind range)
+
 instance ToTyped A.Declaration T.Declaration where
-  toTyped (A.ConstDecl names ty prop loc) = do
+  toTyped (A.ConstDecl names ty prop range) = do
     -- TODO: some kind stuff
     case prop of
       Just p -> do
         p' <- toTyped p
-        return $ T.ConstDecl names ty (Just p') loc
+        return $ T.ConstDecl names ty (Just p') range
       Nothing ->
-        return $ T.ConstDecl names ty Nothing loc
-  toTyped (A.VarDecl names ty prop loc) = do
+        return $ T.ConstDecl names ty Nothing range
+  toTyped (A.VarDecl names ty prop range) = do
     -- TODO: some kind stuff
     case prop of
       Just p -> do
         p' <- toTyped p
-        return $ T.VarDecl names ty (Just p') loc
+        return $ T.VarDecl names ty (Just p') range
       Nothing ->
-        return $ T.VarDecl names ty Nothing loc
+        return $ T.VarDecl names ty Nothing range
 
 instance ToTyped A.Stmt T.Stmt where
-  toTyped (A.Skip loc) = return (T.Skip loc)
-  toTyped (A.Abort loc) = return (T.Abort loc)
-  toTyped (A.Assign names exprs loc) = toTypedAssign names exprs loc
-  toTyped (A.AAssign arr index expr loc) = toTypedAAssign arr index expr loc
-  toTyped (A.Assert expr loc) = toTypedAssert expr loc
-  toTyped (A.LoopInvariant e1 e2 loc) = toTypedLoopInvariant e1 e2 loc
-  toTyped (A.Do gds loc) = toTypedDo gds loc
-  toTyped (A.If gds loc) = toTypedIf gds loc
-  toTyped (A.Spec text range) = undefined
+  toTyped (A.Skip range) = return (T.Skip range)
+  toTyped (A.Abort range) = return (T.Abort range)
+  toTyped (A.Assign names exprs range) = toTypedAssign names exprs range
+  toTyped (A.AAssign arr index expr range) = toTypedAAssign arr index expr range
+  toTyped (A.Assert expr range) = toTypedAssert expr range
+  toTyped (A.LoopInvariant e1 e2 range) = toTypedLoopInvariant e1 e2 range
+  toTyped (A.Do gds range) = toTypedDo gds range
+  toTyped (A.If gds range) = toTypedIf gds range
+  toTyped (A.Spec text range) = T.Spec' text range <$> ask
   toTyped (A.Proof t1 t2 range) = return (T.Proof t1 t2 range)
-  -- the rest exprs are all ints
-  toTyped _stmt = trace (show _stmt) undefined
+  toTyped (A.Alloc var exprs range) = toTypedAlloc var exprs range
+  toTyped (A.HLookup name expr range) = toTypedHLookup name expr range
+  toTyped (A.HMutate left right range) = toTypedHMutate left right range
+  toTyped (A.Dispose expr range) = toTypedDispose expr range
+  toTyped A.Block {} = undefined
 
 toTypedAssign :: [Name] -> [A.Expr] -> Maybe Range -> RSE Env Inference T.Stmt
-toTypedAssign names exprs loc
+toTypedAssign names exprs range
   | length names > length exprs = throwError $ RedundantNames (drop (length exprs) names)
   | length names < length exprs = throwError $ RedundantExprs (drop (length names) exprs)
   | otherwise = do
@@ -200,10 +210,10 @@ toTypedAssign names exprs loc
               toTyped expr
           )
           assignments
-      return $ T.Assign names typedExprs loc
+      return $ T.Assign names typedExprs range
 
 toTypedAAssign :: A.Expr -> A.Expr -> A.Expr -> Maybe Range -> RSE Env Inference T.Stmt
-toTypedAAssign arr index expr loc = do
+toTypedAAssign arr index expr range = do
   ftv <- freshTVar
   (sa, typedArr) <- typeCheck arr (typeInt `typeToType` ftv)
   (si, typedIndex) <- local (applySubstEnv sa) (typeCheck index typeInt)
@@ -215,18 +225,18 @@ toTypedAAssign arr index expr loc = do
           (applySubstExpr resultSubst typedArr)
           (applySubstExpr resultSubst typedIndex)
           (applySubstExpr resultSubst typedExpr)
-          loc
+          range
 
   return resultStmt
 
 toTypedAssert :: A.Expr -> Maybe Range -> RSE Env Inference T.Stmt
-toTypedAssert expr loc = do
+toTypedAssert expr range = do
   (s1, exprTy, typedExpr) <- infer expr
   s2 <- lift $ unify exprTy typeBool (maybeRangeOf expr)
-  return (T.Assert (applySubstExpr (s2 <> s1) typedExpr) loc)
+  return (T.Assert (applySubstExpr (s2 <> s1) typedExpr) range)
 
 toTypedLoopInvariant :: A.Expr -> A.Expr -> Maybe Range -> RSE Env Inference T.Stmt
-toTypedLoopInvariant e1 e2 loc = do
+toTypedLoopInvariant e1 e2 range = do
   (e1Subst, typedE1) <- typeCheck e1 typeBool
   (e2Subst, typedE2) <- local (applySubstEnv e1Subst) (typeCheck e2 typeInt)
   let resultSubst = e2Subst <> e1Subst
@@ -234,26 +244,68 @@ toTypedLoopInvariant e1 e2 loc = do
         T.LoopInvariant
           (applySubstExpr resultSubst typedE1)
           (applySubstExpr resultSubst typedE2)
-          loc
+          range
 
   return resultStmt
 
 toTypedDo :: [A.GdCmd] -> Maybe Range -> RSE Env Inference T.Stmt
-toTypedDo gds loc = do
+toTypedDo gds range = do
   typedGds <- mapM toTyped gds
-  return (T.Do typedGds loc)
+  return (T.Do typedGds range)
 
 toTypedIf :: [A.GdCmd] -> Maybe Range -> RSE Env Inference T.Stmt
-toTypedIf gds loc = do
+toTypedIf gds range = do
   typedGds <- mapM toTyped gds
-  return (T.If typedGds loc)
+  return (T.If typedGds range)
+
+toTypedAlloc :: Name -> [A.Expr] -> Maybe Range -> RSE Env Inference T.Stmt
+toTypedAlloc var exprs range = do
+  env <- ask
+  ty <- case Map.lookup var env of
+    Just scheme -> instantiate scheme
+    Nothing -> throwError $ NotInScope var
+
+  s <- lift $ unify ty typeInt range
+  (resultSubst, typedExprs) <-
+    foldM
+      ( \(s', typedExprs') expr -> do
+          (exprSubst, typedExpr) <- local (applySubstEnv s') (typeCheck expr typeInt)
+          return (exprSubst <> s', typedExpr : typedExprs')
+      )
+      (s, [])
+      exprs
+
+  return (T.Alloc var (map (applySubstExpr resultSubst) typedExprs) range)
+
+toTypedHLookup :: Name -> A.Expr -> Maybe Range -> RSE Env Inference T.Stmt
+toTypedHLookup name expr range = do
+  env <- ask
+  ty <- case Map.lookup name env of
+    Just scheme -> instantiate scheme
+    Nothing -> throwError $ NotInScope name
+
+  s1 <- lift $ unify ty typeInt (maybeRangeOf name)
+  (s2, typedExpr) <- local (applySubstEnv s1) (typeCheck expr typeInt)
+
+  return $ T.HLookup name (applySubstExpr (s2 <> s1) typedExpr) range
+
+toTypedHMutate :: A.Expr -> A.Expr -> Maybe Range -> RSE Env Inference T.Stmt
+toTypedHMutate left right range = do
+  (s1, typedLeft) <- typeCheck left typeInt
+  (s2, typedRight) <- local (applySubstEnv s1) (typeCheck right typeInt)
+  return $ T.HMutate (applySubstExpr (s2 <> s1) typedLeft) (applySubstExpr (s2 <> s1) typedRight) range
+
+toTypedDispose :: A.Expr -> Maybe Range -> RSE Env Inference T.Stmt
+toTypedDispose expr range = do
+  (s, typedExpr) <- typeCheck expr typeInt
+  return $ T.Dispose (applySubstExpr s typedExpr) range
 
 instance ToTyped A.GdCmd T.GdCmd where
-  toTyped (A.GdCmd expr stmts loc) = do
+  toTyped (A.GdCmd expr stmts range) = do
     (exprSubst, typedExpr) <- typeCheck expr typeBool
     typedStmts <- mapM toTyped stmts
 
-    return (T.GdCmd (applySubstExpr exprSubst typedExpr) typedStmts loc)
+    return (T.GdCmd (applySubstExpr exprSubst typedExpr) typedStmts range)
 
 instance ToTyped A.Expr T.Expr where
   toTyped expr = do
@@ -263,10 +315,7 @@ instance ToTyped A.Expr T.Expr where
     -- so it is probably really inefficient to do so when
     -- there is likely a few tyvars needed to be substituted
     let typed' = applySubstExpr subst typed
-    -- traceM $ show (pretty typed')
-    -- traceM $ show (pretty ty)
-    -- traceM $ show subst
-    -- traceM $ "\n" <> Hack.sshow typed <> "\n"
+
     return typed'
 
 runToTyped :: (ToTyped a t) => a -> Env -> Either TypeError t
diff --git a/gcl/src/Pretty/Typed.hs b/gcl/src/Pretty/Typed.hs
index a66fb7de..ad1bd52c 100644
--- a/gcl/src/Pretty/Typed.hs
+++ b/gcl/src/Pretty/Typed.hs
@@ -57,6 +57,7 @@ instance Pretty Definition where
   pretty (FuncDefnSig name typ Nothing _) = pretty name <> ": " -- <> pretty typ
   pretty (FuncDefnSig name typ (Just prop) _) =
     pretty name <> ": " <> {- pretty typ <> -} "{ " <> pretty prop <> " }"
+  pretty (FuncDefnSig' name typ range) = pretty name <> ": " -- <> pretty typ
   pretty (FuncDefn name expr) = pretty name <+> " = " <+> pretty expr
 
 instance Pretty TypeDefnCtor where
@@ -85,6 +86,7 @@ instance Pretty Stmt where
   pretty (If gdCmds _) =
     "if" <> line <> vsep (map (\x -> " |" <+> pretty x <> line) gdCmds) <> "fi"
   pretty (Spec content _ _) = "[!" <> pretty content <> "!]"
+  pretty (Spec' content _ _) = "[!" <> pretty content <> "!]"
   pretty (Proof anchor contents _) =
     -- "{-" <> vsep (map (\x -> pretty x <> line) anchors) <> "-}"
     "{- #" <> pretty anchor <> line <> pretty contents <> line <> "-}"
diff --git a/gcl/src/Server/Hover.hs b/gcl/src/Server/Hover.hs
index b0c557a6..11a64be0 100644
--- a/gcl/src/Server/Hover.hs
+++ b/gcl/src/Server/Hover.hs
@@ -73,6 +73,7 @@ unkind (Typed.TMetaVar name _ loc) = UnTyped.TMetaVar name loc
 instance Collect Typed.Definition where
   collect (Typed.TypeDefn _ _ ctors _) = foldMap collect ctors
   collect (Typed.FuncDefnSig name kinded prop _) = annotateType name (unkind kinded) <> collect kinded <> maybe mempty collect prop
+  collect (Typed.FuncDefnSig' name kinded _) = annotateType name kinded -- XXX: this is probably incomplete?
   collect (Typed.FuncDefn _name expr) = collect expr
 
 instance Collect Typed.TypeDefnCtor where
@@ -109,6 +110,7 @@ instance Collect Typed.Stmt where -- TODO: Display hover info for names.
   collect (Typed.Do gdCmds _) = foldMap collect gdCmds
   collect (Typed.If gdCmds _) = foldMap collect gdCmds
   collect Typed.Spec {} = mempty
+  collect Typed.Spec' {} = mempty
   collect Typed.Proof {} = mempty
   collect (Typed.Alloc _name exprs _) = foldMap collect exprs
   collect (Typed.HLookup _name expr _) = collect expr
diff --git a/gcl/src/Server/Load.hs b/gcl/src/Server/Load.hs
index f926a4cd..3508030d 100644
--- a/gcl/src/Server/Load.hs
+++ b/gcl/src/Server/Load.hs
@@ -15,6 +15,7 @@ import qualified Data.Text as Text
 import Error (Error (..))
 import GCL.Range (Range)
 import qualified GCL.Type as TypeChecking
+import GCL.Type2.ToTyped
 import qualified GCL.WP as WP
 import Server.GoToDefn (collectLocationLinks)
 import Server.Highlighting (collectHighlighting)
@@ -53,7 +54,8 @@ load filePath = do
         -- parse source into concrete syntax
         concrete <- ExceptT $ parse filePath source
         abstract <- ExceptT $ reportHolesOrToAbstract concrete filePath
-        elaborated <- ExceptT $ elaborate abstract
+        elaborated <- ExceptT $ elaborate2 abstract
+        -- elaborated <- ExceptT $ elaborate abstract
         ExceptT $ case WP.sweep elaborated of
           Left err -> do
             logText "  sweep error\n"
@@ -171,3 +173,15 @@ load filePath = do
         Right typedProgram -> do
           logText "  program elaborated\n"
           return $ Right typedProgram
+
+    elaborate2 :: A.Program -> ServerM (Either () T.Program)
+    elaborate2 abstract = do
+      logText "  [WARN] running experimental new typechecker, things might break"
+      case runToTyped abstract mempty of
+        Left e -> do
+          logText "  elaborate error\n"
+          onError $ TypeError e
+          return $ Left ()
+        Right typedProgram -> do
+          logText "  program elaborated\n"
+          return $ Right typedProgram
diff --git a/gcl/src/Syntax/Abstract/Types.hs b/gcl/src/Syntax/Abstract/Types.hs
index 4bba3645..bebe76ed 100644
--- a/gcl/src/Syntax/Abstract/Types.hs
+++ b/gcl/src/Syntax/Abstract/Types.hs
@@ -127,16 +127,28 @@ data Type
   | TType -- "*"
   deriving (Show, Generic)
 
+-- NOTE: i don't want to deal with template haskell right now
+-- but i want to catch incomplete patterns when i add new variants in
 instance Eq Type where
   TBase base1 _ == TBase base2 _ = base1 == base2
+  TBase {} == _ = False
   TArray int1 ty1 _ == TArray int2 ty2 _ = int1 == int2 && ty1 == ty2
+  TArray {} == _ = False
   TTuple i1 == TTuple i2 = i1 == i2
+  TTuple {} == _ = False
+  TFunc {} == _ = False
   TOp op1 == TOp op2 = op1 == op2
+  TOp {} == _ = False
   TData name1 _ == TData name2 _ = name1 == name2
-  TApp left1 right1 _ == TApp left2 right2 _ = left1 == right1 && left2 == right2
+  TData {} == _ = False
+  TApp left1 right1 _ == TApp left2 right2 _ = left1 == left2 && right1 == right2
+  TApp {} == _ = False
   TVar name1 _ == TVar name2 _ = name1 == name2
+  TVar {} == _ = False
   TMetaVar name1 _ == TMetaVar name2 _ = name1 == name2
-  _ == _ = False
+  TMetaVar {} == _ = False
+  TType == TType = True
+  TType == _ = False
 
 --------------------------------------------------------------------------------
 
diff --git a/gcl/src/Syntax/Typed/Instances/Free.hs b/gcl/src/Syntax/Typed/Instances/Free.hs
index 5de9c6ae..ddac4510 100644
--- a/gcl/src/Syntax/Typed/Instances/Free.hs
+++ b/gcl/src/Syntax/Typed/Instances/Free.hs
@@ -58,6 +58,7 @@ instance Free Stmt where
   freeVars (Do gdcmds _) = Set.unions (map freeVars gdcmds)
   freeVars (If gdcmds _) = Set.unions (map freeVars gdcmds)
   freeVars (Spec _ _ _) = mempty
+  freeVars (Spec' _ _ _) = mempty
   freeVars (Proof _ _ _) = mempty
   freeVars (Alloc x es _) =
     Set.singleton x <> Set.unions (map freeVars es)
diff --git a/gcl/src/Syntax/Typed/Instances/Located.hs b/gcl/src/Syntax/Typed/Instances/Located.hs
index 2503bc6f..df22df36 100644
--- a/gcl/src/Syntax/Typed/Instances/Located.hs
+++ b/gcl/src/Syntax/Typed/Instances/Located.hs
@@ -15,6 +15,7 @@ instance MaybeRanged Declaration where
 instance MaybeRanged Definition where
   maybeRangeOf (TypeDefn _ _ _ r) = r
   maybeRangeOf (FuncDefnSig _ _ _ r) = r
+  maybeRangeOf (FuncDefnSig' _ _ r) = r
   maybeRangeOf (FuncDefn l r) = maybeRangeOf l <---> maybeRangeOf r
 
 instance MaybeRanged TypeDefnCtor where
@@ -30,6 +31,7 @@ instance MaybeRanged Stmt where
   maybeRangeOf (Do _ l) = l
   maybeRangeOf (If _ l) = l
   maybeRangeOf (Spec _ r _) = Just r
+  maybeRangeOf (Spec' _ r _) = Just r
   maybeRangeOf (Proof _ _ r) = Just r
   maybeRangeOf (Alloc _ _ l) = l
   maybeRangeOf (HLookup _ _ l) = l
diff --git a/gcl/src/Syntax/Typed/Types.hs b/gcl/src/Syntax/Typed/Types.hs
index 100c89eb..b143d8f9 100644
--- a/gcl/src/Syntax/Typed/Types.hs
+++ b/gcl/src/Syntax/Typed/Types.hs
@@ -3,6 +3,7 @@ module Syntax.Typed.Types where
 import Data.Text (Text)
 import GCL.Common (Index, TypeInfo)
 import GCL.Range (Range)
+import GCL.Type2.Common (Env)
 import Syntax.Abstract.Types (Interval, Kind, Lit (..), Pattern, TBase (..), Type (..))
 import Syntax.Common.Types (Name, Op, TypeOp)
 
@@ -18,6 +19,7 @@ data Program
 data Definition
   = TypeDefn Name [Name] [TypeDefnCtor] (Maybe Range)
   | FuncDefnSig Name KindedType (Maybe Expr) (Maybe Range)
+  | FuncDefnSig' Name Type (Maybe Range)
   | FuncDefn Name Expr
   deriving (Eq, Show)
 
@@ -39,6 +41,7 @@ data Stmt
   | Do [GdCmd] (Maybe Range)
   | If [GdCmd] (Maybe Range)
   | Spec Text Range [(Index, TypeInfo)]
+  | Spec' Text Range Env
   | Proof Text Text Range
   | Alloc Name [Expr] (Maybe Range) --  p := new (e1,e2,..,en)
   | HLookup Name Expr (Maybe Range) --  x := *e