diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # kempe
 
+# 0.2.0.12
+
+  * Typechecker is 𝜖 faster
+  
 # 0.2.0.11
 
   * Fix bug in typechecker
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright Vanessa McHale (c) 2020-2021
+Copyright Vanessa McHale (c) 2020-2022
 
 Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
 
diff --git a/docs/manual.pdf b/docs/manual.pdf
Binary files a/docs/manual.pdf and b/docs/manual.pdf differ
diff --git a/kempe.cabal b/kempe.cabal
--- a/kempe.cabal
+++ b/kempe.cabal
@@ -1,9 +1,9 @@
 cabal-version:   3.0
 name:            kempe
-version:         0.2.0.11
+version:         0.2.0.12
 license:         BSD-3-Clause
 license-file:    LICENSE
-copyright:       Copyright: (c) 2020-2021 Vanessa McHale
+copyright:       Copyright: (c) 2020-2022 Vanessa McHale
 maintainer:      vamchale@gmail.com
 author:          Vanessa McHale
 synopsis:        Kempe compiler
@@ -128,20 +128,6 @@
 
     if !flag(cross)
         build-tool-depends: alex:alex, happy:happy
-
-    if impl(ghc >=8.0)
-        ghc-options:
-            -Wincomplete-uni-patterns -Wincomplete-record-updates
-            -Wredundant-constraints -Widentities
-
-    if impl(ghc >=8.4)
-        ghc-options: -Wmissing-export-lists
-
-    if impl(ghc >=8.2)
-        ghc-options: -Wcpp-undef
-
-    if impl(ghc >=8.10)
-        ghc-options: -Wunused-packages
 
 executable kc
     main-is:          Main.hs
diff --git a/run/Main.hs b/run/Main.hs
--- a/run/Main.hs
+++ b/run/Main.hs
@@ -123,9 +123,9 @@
 commandP :: Parser Command
 commandP = hsubparser
     (command "typecheck" (info tcP (progDesc "Type-check module contents"))
-    <> command "lint" (info lintP (progDesc "Lint a file")))
+    <> command "lint" (info lintP (progDesc "Lint a file"))
+    <> command "cdecl" (info cdeclP (progDesc "Generate C headers for exported Kempe code")))
     <|> hsubparser (command "fmt" (info fmtP (progDesc "Pretty-print a Kempe file")) <> internal)
-    <|> hsubparser (command "cdecl" (info cdeclP (progDesc "Generate C headers for exported Kempe code")))
     <|> compileP
     where
         tcP = TypeCheck <$> kmpFile
diff --git a/src/Kempe/AST.hs b/src/Kempe/AST.hs
--- a/src/Kempe/AST.hs
+++ b/src/Kempe/AST.hs
@@ -59,7 +59,7 @@
     pretty (ConsAnn tSz b ty) = braces ("tySz" <+> colon <+> pretty tSz <+> "tag" <+> colon <+> pretty b <+> "type" <+> colon <+> pretty ty)
 
 voidStackType :: StackType a -> StackType ()
-voidStackType (StackType vars ins outs) = StackType (S.map void vars) (void <$> ins) (void <$> outs)
+voidStackType (StackType ins outs) = StackType (void <$> ins) (void <$> outs)
 
 data Pattern c b = PatternInt b Integer
                  | PatternCons { patternKind :: c, patternName :: TyName c } -- a constructed pattern
@@ -273,4 +273,4 @@
 
 -- | Used in "Kempe.Monomorphize" for patterns
 flipStackType :: StackType () -> StackType ()
-flipStackType (StackType vars is os) = StackType vars os is
+flipStackType (StackType is os) = StackType os is
diff --git a/src/Kempe/AST/Size.hs b/src/Kempe/AST/Size.hs
--- a/src/Kempe/AST/Size.hs
+++ b/src/Kempe/AST/Size.hs
@@ -24,7 +24,6 @@
 import           Data.Int        (Int64)
 import qualified Data.IntMap     as IM
 import           Data.Monoid     (Sum (..))
-import qualified Data.Set        as S
 import           GHC.Generics    (Generic)
 import           Kempe.Name
 import           Kempe.Unique
@@ -36,8 +35,7 @@
                | TyApp a (KempeTy a) (KempeTy a) -- type applied to another, e.g. Just Int
                deriving (Generic, NFData, Functor, Eq, Ord) -- questionable eq instance but eh
 
-data StackType b = StackType { quantify :: S.Set (Name b)
-                             , inTypes  :: [KempeTy b]
+data StackType b = StackType { inTypes  :: [KempeTy b]
                              , outTypes :: [KempeTy b]
                              } deriving (Generic, NFData, Eq, Ord)
 
@@ -65,7 +63,7 @@
     pretty (TyApp _ ty ty') = parens (pretty ty <+> pretty ty')
 
 instance Pretty (StackType a) where
-    pretty (StackType _ ins outs) = sep (fmap pretty ins) <+> "--" <+> sep (fmap pretty outs)
+    pretty (StackType ins outs) = sep (fmap pretty ins) <+> "--" <+> sep (fmap pretty outs)
 
 data ABI = Cabi
          | Kabi
diff --git a/src/Kempe/CGen.hs b/src/Kempe/CGen.hs
--- a/src/Kempe/CGen.hs
+++ b/src/Kempe/CGen.hs
@@ -10,21 +10,21 @@
 cGen = mapMaybe cDecl
 
 cDecl :: KempeDecl a c (StackType ()) -> Maybe CFunc
-cDecl ExtFnDecl{}                                        = Nothing
-cDecl TyDecl{}                                           = Nothing
-cDecl FunDecl{}                                          = Nothing
-cDecl (Export _ Cabi (Name n _ (StackType _ [] [])))     = Just (CFunc n [CVoid] CVoid)
-cDecl (Export _ Cabi (Name n _ (StackType _ [] [o])))    = Just (CFunc n [CVoid] (kempeTyToCType o))
-cDecl (Export _ Cabi (Name n _ (StackType _ ins [])))    = Just (CFunc n (kempeTyToCType <$> ins) CVoid)
-cDecl (Export _ Cabi (Name n _ (StackType _ ins [o])))   = Just (CFunc n (kempeTyToCType <$> ins) (kempeTyToCType o))
-cDecl (Export _ Cabi _)                                  = error "Multiple return not suppported :("
-cDecl (Export _ ArmAbi (Name n _ (StackType _ [] [])))   = Just (CFunc n [CVoidPtr] CVoid)
-cDecl (Export _ ArmAbi (Name n _ (StackType _ [] [o])))  = Just (CFunc n [CVoidPtr] (kempeTyToCType o))
-cDecl (Export _ ArmAbi (Name n _ (StackType _ ins [])))  = Just (CFunc n (CVoidPtr : fmap kempeTyToCType ins) CVoid)
-cDecl (Export _ ArmAbi (Name n _ (StackType _ ins [o]))) = Just (CFunc n (CVoidPtr : fmap kempeTyToCType ins) (kempeTyToCType o))
-cDecl (Export _ ArmAbi _)                                = error "Multiple return not suppported :("
-cDecl (Export _ Hooked (Name n _ _))                     = Just (CFunc n [CVoidPtr] CVoid)
-cDecl (Export _ Kabi _)                                  = error "You probably don't want to do this."
+cDecl ExtFnDecl{}                                      = Nothing
+cDecl TyDecl{}                                         = Nothing
+cDecl FunDecl{}                                        = Nothing
+cDecl (Export _ Cabi (Name n _ (StackType [] [])))     = Just (CFunc n [CVoid] CVoid)
+cDecl (Export _ Cabi (Name n _ (StackType [] [o])))    = Just (CFunc n [CVoid] (kempeTyToCType o))
+cDecl (Export _ Cabi (Name n _ (StackType ins [])))    = Just (CFunc n (kempeTyToCType <$> ins) CVoid)
+cDecl (Export _ Cabi (Name n _ (StackType ins [o])))   = Just (CFunc n (kempeTyToCType <$> ins) (kempeTyToCType o))
+cDecl (Export _ Cabi _)                                = error "Multiple return not suppported :("
+cDecl (Export _ ArmAbi (Name n _ (StackType [] [])))   = Just (CFunc n [CVoidPtr] CVoid)
+cDecl (Export _ ArmAbi (Name n _ (StackType [] [o])))  = Just (CFunc n [CVoidPtr] (kempeTyToCType o))
+cDecl (Export _ ArmAbi (Name n _ (StackType ins [])))  = Just (CFunc n (CVoidPtr : fmap kempeTyToCType ins) CVoid)
+cDecl (Export _ ArmAbi (Name n _ (StackType ins [o]))) = Just (CFunc n (CVoidPtr : fmap kempeTyToCType ins) (kempeTyToCType o))
+cDecl (Export _ ArmAbi _)                              = error "Multiple return not suppported :("
+cDecl (Export _ Hooked (Name n _ _))                   = Just (CFunc n [CVoidPtr] CVoid)
+cDecl (Export _ Kabi _)                                = error "You probably don't want to do this."
 
 kempeTyToCType :: KempeTy a -> CType
 kempeTyToCType (TyBuiltin _ TyInt)  = CInt
diff --git a/src/Kempe/File.hs b/src/Kempe/File.hs
--- a/src/Kempe/File.hs
+++ b/src/Kempe/File.hs
@@ -22,7 +22,6 @@
 import           Data.Bifunctor            (bimap)
 import           Data.Functor              (void)
 import           Data.Semigroup            ((<>))
-import qualified Data.Set                  as S
 import           Data.Tuple.Ext            (fst3)
 import           Data.Typeable             (Typeable)
 import           Kempe.AST
@@ -80,7 +79,7 @@
     (i, m) <- parseProcess fp
     (mMono, _) <- yeetIO $ monomorphize i m
     putDoc $ prettyTypedModule (fmap (bimap fromMonoConsAnn fromMono) mMono)
-    where fromMono (is, os) = StackType S.empty is os
+    where fromMono (is, os) = StackType is os
           fromMonoConsAnn (ConsAnn _ _ ty) = fromMono ty
 
 dumpIR :: Typeable a => Int -> Declarations a c b -> Doc ann
diff --git a/src/Kempe/IR/Type.hs b/src/Kempe/IR/Type.hs
--- a/src/Kempe/IR/Type.hs
+++ b/src/Kempe/IR/Type.hs
@@ -13,17 +13,16 @@
                      , WriteSt (..)
                      ) where
 
-import           Control.DeepSeq            (NFData)
-import           Control.Monad.State.Strict (State)
-import qualified Data.ByteString            as BS
-import qualified Data.ByteString.Lazy       as BSL
-import           Data.Int                   (Int64, Int8)
-import           Data.Semigroup             ((<>))
-import           Data.Text.Encoding         (decodeUtf8)
-import           Data.Word                  (Word8)
-import           GHC.Generics               (Generic)
+import           Control.DeepSeq      (NFData)
+import qualified Data.ByteString      as BS
+import qualified Data.ByteString.Lazy as BSL
+import           Data.Int             (Int64, Int8)
+import           Data.Semigroup       ((<>))
+import           Data.Text.Encoding   (decodeUtf8)
+import           Data.Word            (Word8)
+import           GHC.Generics         (Generic)
 import           Kempe.AST.Size
-import           Prettyprinter              (Doc, Pretty (pretty), braces, brackets, colon, hardline, parens, (<+>))
+import           Prettyprinter        (Doc, Pretty (pretty), braces, brackets, colon, hardline, parens, (<+>))
 import           Prettyprinter.Ext
 
 data WriteSt = WriteSt { wlabels :: [Label]
diff --git a/src/Kempe/Monomorphize.hs b/src/Kempe/Monomorphize.hs
--- a/src/Kempe/Monomorphize.hs
+++ b/src/Kempe/Monomorphize.hs
@@ -79,8 +79,8 @@
         <$ modifying maxStateLens (+1)
 
 tryMono :: MonadError (Error ()) m => StackType () -> m MonoStackType
-tryMono (StackType _ is os) | S.null (freeVars (is ++ os)) = pure (is, os)
-                            | otherwise = throwError $ MonoFailed ()
+tryMono (StackType is os) | S.null (freeVars (is ++ os)) = pure (is, os)
+                          | otherwise = throwError $ MonoFailed ()
 
 -- | A 'ModuleMap' is a map which retrives the 'KempeDecl' associated with
 -- a given 'Name'
@@ -238,7 +238,7 @@
 
 specializeDecl :: KempeDecl () (StackType ()) (StackType ()) -> StackType () -> MonoM (KempeDecl () (StackType ()) (StackType ()))
 specializeDecl (FunDecl _ n _ _ as) sty = do
-    (Name t u newStackType@(StackType _ is os)) <- renamed n =<< tryMono sty
+    (Name t u newStackType@(StackType is os)) <- renamed n =<< tryMono sty
     pure $ FunDecl newStackType (Name t u newStackType) is os as
 specializeDecl (ExtFnDecl l n tys tys' b) _ = pure $ ExtFnDecl l n tys tys' b
 specializeDecl (Export l abi n) _           = pure $ Export l abi n
@@ -249,7 +249,7 @@
 renamedCons (Name t i _) sty@(is, os) fAnn = do
     let t' = t <> squishMonoStackType sty
     (Name _ j _) <- freshName t' sty
-    let newStackType = StackType S.empty is os
+    let newStackType = StackType is os
         ann = fAnn sty
     modifying consEnvLens (M.insert (i, newStackType) (j, ann))
     pure (Name t' j newStackType)
@@ -259,7 +259,7 @@
 renamed (Name t i _) sty@(is, os) = do
     let t' = t <> squishMonoStackType sty
     (Name _ j _) <- freshName t' sty
-    let newStackType = StackType S.empty is os
+    let newStackType = StackType is os
     modifying fnEnvLens (M.insert (i, newStackType) j)
     pure (Name t' j newStackType)
 
diff --git a/src/Kempe/TyAssign.hs b/src/Kempe/TyAssign.hs
--- a/src/Kempe/TyAssign.hs
+++ b/src/Kempe/TyAssign.hs
@@ -57,7 +57,7 @@
 prettyDumpBinds b = vsep (prettyBind <$> IM.toList b)
 
 emptyStackType :: StackType a
-emptyStackType = StackType mempty [] []
+emptyStackType = StackType [] []
 
 maxULens :: Lens' (TyState a) Int
 maxULens f s = fmap (\x -> s { maxU = x }) (f (maxU s))
@@ -104,8 +104,8 @@
 
 -- | Perform substitutions before handing off to 'unifyMatch'
 unifyPrep :: UnifyMap
-           -> [(KempeTy (), KempeTy ())]
-           -> Either (Error ()) (IM.IntMap (KempeTy ()))
+          -> [(KempeTy (), KempeTy ())]
+          -> Either (Error ()) (IM.IntMap (KempeTy ()))
 unifyPrep _ [] = Right mempty
 unifyPrep um ((ty, ty'):tys) =
     let ty'' = inContext um ty
@@ -129,10 +129,10 @@
 unifyMatch _ ((ty@TyApp{}, ty'@TyBuiltin{}):_)                               = Left (UnificationFailed () ty ty')
 unifyMatch um ((TyVar _ (Name _ (Unique k) _), ty@TyApp{}):tys)              = IM.insert k ty <$> unifyPrep (IM.insert k ty um) tys
 unifyMatch um ((ty@TyApp{}, TyVar  _ (Name _ (Unique k) _)):tys)             = IM.insert k ty <$> unifyPrep (IM.insert k ty um) tys
-unifyMatch um ((TyApp _ ty ty', TyApp _ ty'' ty'''):tys)                     = unifyMatch um ((ty, ty'') : (ty', ty''') : tys) -- TODO:  do we need unifyPrep here?
+unifyMatch um ((TyApp _ ty ty', TyApp _ ty'' ty'''):tys)                     = unifyPrep um ((ty, ty'') : (ty', ty''') : tys)
 unifyMatch _ ((ty@TyApp{}, ty'@TyNamed{}):_)                                 = Left (UnificationFailed () (void ty) (void ty'))
 unifyMatch um ((TyVar _ n@(Name _ (Unique k) _), ty@(TyVar _ n')):tys)
-    | n == n' = unifyMatch um tys -- a type variable is always equal to itself, don't bother inserting this!
+    | n == n' = unifyPrep um tys -- a type variable is always equal to itself, don't bother inserting this!
     | otherwise = IM.insert k ty <$> unifyPrep (IM.insert k ty um) tys
 
 unify :: [(KempeTy (), KempeTy ())] -> Either (Error ()) (IM.IntMap (KempeTy ()))
@@ -153,14 +153,14 @@
 typeOfBuiltin :: BuiltinFn -> TypeM () (StackType ())
 typeOfBuiltin Drop = do
     aN <- dummyName "a"
-    pure $ StackType (S.singleton aN) [TyVar () aN] []
+    pure $ StackType [TyVar () aN] []
 typeOfBuiltin Swap = do
     aN <- dummyName "a"
     bN <- dummyName "b"
-    pure $ StackType (S.fromList [aN, bN]) [TyVar () aN, TyVar () bN] [TyVar () bN, TyVar () aN]
+    pure $ StackType [TyVar () aN, TyVar () bN] [TyVar () bN, TyVar () aN]
 typeOfBuiltin Dup = do
     aN <- dummyName "a"
-    pure $ StackType (S.singleton aN) [TyVar () aN] [TyVar () aN, TyVar () aN]
+    pure $ StackType [TyVar () aN] [TyVar () aN, TyVar () aN]
 typeOfBuiltin IntEq      = pure intRel
 typeOfBuiltin IntLeq     = pure intRel
 typeOfBuiltin IntLt      = pure intRel
@@ -186,26 +186,26 @@
 typeOfBuiltin And        = pure boolOp
 typeOfBuiltin Or         = pure boolOp
 typeOfBuiltin Xor        = pure boolOp
-typeOfBuiltin IntNeg     = pure $ StackType S.empty [TyBuiltin () TyInt] [TyBuiltin () TyInt]
-typeOfBuiltin Popcount   = pure $ StackType S.empty [TyBuiltin () TyWord] [TyBuiltin () TyInt]
+typeOfBuiltin IntNeg     = pure $ StackType [TyBuiltin () TyInt] [TyBuiltin () TyInt]
+typeOfBuiltin Popcount   = pure $ StackType [TyBuiltin () TyWord] [TyBuiltin () TyInt]
 
 boolOp :: StackType ()
-boolOp = StackType S.empty [TyBuiltin () TyBool, TyBuiltin () TyBool] [TyBuiltin () TyBool]
+boolOp = StackType [TyBuiltin () TyBool, TyBuiltin () TyBool] [TyBuiltin () TyBool]
 
 intRel :: StackType ()
-intRel = StackType S.empty [TyBuiltin () TyInt, TyBuiltin () TyInt] [TyBuiltin () TyBool]
+intRel = StackType [TyBuiltin () TyInt, TyBuiltin () TyInt] [TyBuiltin () TyBool]
 
 intBinOp :: StackType ()
-intBinOp = StackType S.empty [TyBuiltin () TyInt, TyBuiltin () TyInt] [TyBuiltin () TyInt]
+intBinOp = StackType [TyBuiltin () TyInt, TyBuiltin () TyInt] [TyBuiltin () TyInt]
 
 intShift :: StackType ()
-intShift = StackType S.empty [TyBuiltin () TyInt, TyBuiltin () TyInt] [TyBuiltin () TyInt]
+intShift = StackType [TyBuiltin () TyInt, TyBuiltin () TyInt] [TyBuiltin () TyInt]
 
 wordBinOp :: StackType ()
-wordBinOp = StackType S.empty [TyBuiltin () TyWord, TyBuiltin () TyWord] [TyBuiltin () TyWord]
+wordBinOp = StackType [TyBuiltin () TyWord, TyBuiltin () TyWord] [TyBuiltin () TyWord]
 
 wordShift :: StackType ()
-wordShift = StackType S.empty [TyBuiltin () TyWord, TyBuiltin () TyWord] [TyBuiltin () TyWord]
+wordShift = StackType [TyBuiltin () TyWord, TyBuiltin () TyWord] [TyBuiltin () TyWord]
 
 tyLookup :: Name a -> TypeM a (StackType a)
 tyLookup n@(Name _ (Unique i) l) = do
@@ -223,9 +223,9 @@
 
 -- expandType 1
 dipify :: StackType () -> TypeM () (StackType ())
-dipify (StackType fvrs is os) = do
+dipify (StackType is os) = do
     n <- dummyName "a"
-    pure $ StackType (S.insert n fvrs) (is ++ [TyVar () n]) (os ++ [TyVar () n])
+    pure $ StackType (is ++ [TyVar () n]) (os ++ [TyVar () n])
 
 tyLeaf :: (Pattern b a, [Atom b a]) -> TypeM () (StackType ())
 tyLeaf (p, as) = do
@@ -241,18 +241,18 @@
 
 tyAtom :: Atom b a -> TypeM () (StackType ())
 tyAtom (AtBuiltin _ b) = typeOfBuiltin b
-tyAtom BoolLit{}       = pure $ StackType mempty [] [TyBuiltin () TyBool]
-tyAtom IntLit{}        = pure $ StackType mempty [] [TyBuiltin () TyInt]
-tyAtom Int8Lit{}       = pure $ StackType mempty [] [TyBuiltin () TyInt8 ]
-tyAtom WordLit{}       = pure $ StackType mempty [] [TyBuiltin () TyWord]
+tyAtom BoolLit{}       = pure $ StackType [] [TyBuiltin () TyBool]
+tyAtom IntLit{}        = pure $ StackType [] [TyBuiltin () TyInt]
+tyAtom Int8Lit{}       = pure $ StackType [] [TyBuiltin () TyInt8 ]
+tyAtom WordLit{}       = pure $ StackType [] [TyBuiltin () TyWord]
 tyAtom (AtName _ n)    = renameStack =<< tyLookup (void n)
 tyAtom (Dip _ as)      = dipify =<< tyAtoms as
 tyAtom (AtCons _ tn)   = renameStack =<< consLookup (void tn)
 tyAtom (If _ as as')   = do
     tys <- tyAtoms as
     tys' <- tyAtoms as'
-    (StackType vars ins out) <- mergeStackTypes tys tys'
-    pure $ StackType vars (ins ++ [TyBuiltin () TyBool]) out
+    (StackType ins out) <- mergeStackTypes tys tys'
+    pure $ StackType (ins ++ [TyBuiltin () TyBool]) out
 tyAtom (Case _ ls) = do
     tyLs <- traverse tyLeaf ls
     -- TODO: one-pass fold?
@@ -261,16 +261,16 @@
 assignAtom :: Atom b a -> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
 assignAtom (AtBuiltin _ b) = do { ty <- typeOfBuiltin b ; pure (ty, AtBuiltin ty b) }
 assignAtom (BoolLit _ b)   =
-    let sTy = StackType mempty [] [TyBuiltin () TyBool]
+    let sTy = StackType [] [TyBuiltin () TyBool]
         in pure (sTy, BoolLit sTy b)
 assignAtom (IntLit _ i)    =
-    let sTy = StackType mempty [] [TyBuiltin () TyInt]
+    let sTy = StackType [] [TyBuiltin () TyInt]
         in pure (sTy, IntLit sTy i)
 assignAtom (Int8Lit _ i)    =
-    let sTy = StackType mempty [] [TyBuiltin () TyInt8]
+    let sTy = StackType [] [TyBuiltin () TyInt8]
         in pure (sTy, Int8Lit sTy i)
 assignAtom (WordLit _ u)    =
-    let sTy = StackType mempty [] [TyBuiltin () TyWord]
+    let sTy = StackType [] [TyBuiltin () TyWord]
         in pure (sTy, WordLit sTy u)
 assignAtom (AtName _ n) = do
     sTy <- renameStack =<< tyLookup (void n)
@@ -282,8 +282,8 @@
 assignAtom (If _ as0 as1) = do
     (as0', tys) <- assignAtoms as0
     (as1', tys') <- assignAtoms as1
-    (StackType vars ins out) <- mergeStackTypes tys tys'
-    let resType = StackType vars (ins ++ [TyBuiltin () TyBool]) out
+    (StackType ins out) <- mergeStackTypes tys tys'
+    let resType = StackType (ins ++ [TyBuiltin () TyBool]) out
     pure (resType, If resType as0' as1')
 assignAtom (Case _ ls) = do
     lRes <- traverse assignCase ls
@@ -318,10 +318,10 @@
 tyInsertLeaf :: Name b -- ^ type being declared
              -> S.Set (Name b) -> (TyName a, [KempeTy b]) -> TypeM () ()
 tyInsertLeaf n@(Name _ (Unique k) _) vars (Name _ (Unique i) _, ins) | S.null vars =
-    modifying constructorTypesLens (IM.insert i (voidStackType $ StackType vars ins [TyNamed undefined n])) *>
+    modifying constructorTypesLens (IM.insert i (voidStackType $ StackType ins [TyNamed undefined n])) *>
     modifying kindEnvLens (IM.insert k Star)
                                                | otherwise =
-    let ty = voidStackType $ StackType vars ins [app (TyNamed undefined n) (S.toList vars)] in
+    let ty = voidStackType $ StackType ins [app (TyNamed undefined n) (S.toList vars)] in
     modifying constructorTypesLens (IM.insert i ty) *>
     modifying kindEnvLens (IM.insert k (mkHKT $ S.size vars))
 
@@ -330,12 +330,12 @@
              -> (TyName a, [KempeTy b])
              -> TypeM () (TyName (StackType ()), [KempeTy ()])
 assignTyLeaf n@(Name _ (Unique k) _) vars (tn@(Name _ (Unique i) _), ins) | S.null vars =
-    let ty = voidStackType $ StackType vars ins [TyNamed undefined n] in
+    let ty = voidStackType $ StackType ins [TyNamed undefined n] in
     modifying constructorTypesLens (IM.insert i ty) *>
     modifying kindEnvLens (IM.insert k Star) $>
     (tn $> ty, fmap void ins)
                                                | otherwise =
-    let ty = voidStackType $ StackType vars ins [app (TyNamed undefined n) (S.toList vars)] in
+    let ty = voidStackType $ StackType ins [app (TyNamed undefined n) (S.toList vars)] in
     modifying constructorTypesLens (IM.insert i ty) *>
     modifying kindEnvLens (IM.insert k (mkHKT $ S.size vars)) $>
     (tn $> ty, fmap void ins)
@@ -365,7 +365,7 @@
 assignDecl (TyDecl _ tn ns ls) = TyDecl () (void tn) (void <$> ns) <$> traverse (assignTyLeaf tn (S.fromList ns)) ls
 assignDecl (FunDecl _ n ins os a) = do
     traverse_ kindOf (void <$> ins ++ os)
-    sig <- renameStack $ voidStackType $ StackType (freeVars (ins ++ os)) ins os
+    sig <- renameStack $ voidStackType $ StackType ins os
     (as, inferred) <- assignAtoms a
     reconcile <- mergeStackTypes sig inferred
     when (inferred `lessGeneral` sig) $
@@ -375,10 +375,10 @@
     traverse_ kindOf (void <$> ins ++ os)
     unless (length os <= 1) $
         throwError $ InvalidCImport () (void n)
-    let sig = voidStackType $ StackType S.empty ins os
+    let sig = voidStackType $ StackType ins os
     pure $ ExtFnDecl sig (n $> sig) (void <$> ins) (void <$> os) cn
 assignDecl (Export _ abi n) = do
-    ty@(StackType _ _ os) <- tyLookup (void n)
+    ty@(StackType _ os) <- tyLookup (void n)
     unless (abi == Kabi || length os <= 1) $
         throwError $ InvalidCExport () (void n)
     Export ty abi <$> assignName n
@@ -390,14 +390,14 @@
 tyHeader :: KempeDecl a c b -> TypeM () ()
 tyHeader Export{} = pure ()
 tyHeader (FunDecl _ (Name _ (Unique i) _) ins out _) = do
-    let sig = voidStackType $ StackType (freeVars (ins ++ out)) ins out
+    let sig = voidStackType $ StackType ins out
     modifying tyEnvLens (IM.insert i sig)
 tyHeader (ExtFnDecl _ n@(Name _ (Unique i) _) ins os _) = do
     unless (length os <= 1) $
         throwError $ InvalidCImport () (void n)
     unless (null $ freeVars (ins ++ os)) $
         throwError $ TyVarExt () (void n)
-    let sig = voidStackType $ StackType S.empty ins os -- no free variables allowed in c functions
+    let sig = voidStackType $ StackType ins os -- no free variables allowed in c functions
     modifying tyEnvLens (IM.insert i sig)
 tyHeader TyDecl{} = pure ()
 
@@ -415,7 +415,7 @@
 lessGeneral :: StackType a -- ^ Inferred type
             -> StackType a -- ^ Type from signature
             -> Bool
-lessGeneral (StackType _ is os) (StackType _ is' os') =
+lessGeneral (StackType is os) (StackType is' os') =
     flip evalState mempty $
         if il > il' || ol > ol'
             then (||) <$> lessGenerals trimIs is' <*> lessGenerals trimOs os'
@@ -451,7 +451,7 @@
 tyInsert (TyDecl _ tn ns ls) = traverse_ (tyInsertLeaf tn (S.fromList ns)) ls
 tyInsert (FunDecl _ _ ins out as) = do
     traverse_ kindOf (void <$> ins ++ out) -- FIXME: this gives sketchy results?
-    sig <- renameStack $ voidStackType $ StackType (freeVars (ins ++ out)) ins out
+    sig <- renameStack $ voidStackType $ StackType ins out
     inferred <- tyAtoms as
     _ <- mergeStackTypes sig inferred
     when (inferred `lessGeneral` sig) $
@@ -508,21 +508,21 @@
 
 -- freshen the names in a stack so there aren't overlaps in quanitified variables
 renameStack :: StackType a -> TypeM a (StackType a)
-renameStack (StackType qs ins outs) = do
-    newQs <- traverse withName (S.toList qs)
-    let (newNames, localRenames) = unzip newQs
+renameStack (StackType ins outs) = do
+    newQs <- traverse withName (S.toList $ freeVars ins <> freeVars outs)
+    let (_, localRenames) = unzip newQs
         newBinds = thread localRenames
     withTyState newBinds $
-        StackType (S.fromList newNames) <$> traverse renameIn ins <*> traverse renameIn outs
+        StackType <$> traverse renameIn ins <*> traverse renameIn outs
 
 mergeStackTypes :: StackType () -> StackType () -> TypeM () (StackType ())
-mergeStackTypes st0@(StackType _ i0 o0) st1@(StackType _ i1 o1) = do
+mergeStackTypes st0@(StackType i0 o0) st1@(StackType i1 o1) = do
     let li0 = length i0
         li1 = length i1
         toExpand = max (abs (li0 - li1)) (abs (length o0 - length o1))
 
-    (StackType q ins os) <- (if li0 < li1 then expandType toExpand else pure) st0
-    (StackType q' ins' os') <- (if li1 < li0 then expandType toExpand else pure) st1
+    (StackType ins os) <- (if li0 < li1 then expandType toExpand else pure) st0
+    (StackType ins' os') <- (if li1 < li0 then expandType toExpand else pure) st1
 
     when ((length ins /= length ins') || (length os /= length os')) $
         throwError $ MismatchedLengths () st0 st1
@@ -530,27 +530,27 @@
     zipWithM_ pushConstraint ins ins'
     zipWithM_ pushConstraint os os'
 
-    pure $ StackType (q <> q') ins os
+    pure $ StackType ins os
 
 tyPattern :: Pattern b a -> TypeM () (StackType ())
 tyPattern PatternWildcard{} = do
     aN <- dummyName "a"
-    pure $ StackType (S.singleton aN) [TyVar () aN] []
-tyPattern PatternInt{} = pure $ StackType S.empty [TyBuiltin () TyInt] []
-tyPattern PatternBool{} = pure $ StackType S.empty [TyBuiltin () TyBool] []
+    pure $ StackType [TyVar () aN] []
+tyPattern PatternInt{} = pure $ StackType [TyBuiltin () TyInt] []
+tyPattern PatternBool{} = pure $ StackType [TyBuiltin () TyBool] []
 tyPattern (PatternCons _ tn) = renameStack . flipStackType =<< consLookup (void tn)
 
 assignPattern :: Pattern b a -> TypeM () (StackType (), Pattern (StackType ()) (StackType ()))
 assignPattern (PatternInt _ i) =
-    let sTy = StackType S.empty [TyBuiltin () TyInt] []
+    let sTy = StackType [TyBuiltin () TyInt] []
         in pure (sTy, PatternInt sTy i)
 assignPattern (PatternBool _ i) =
-    let sTy = StackType S.empty [TyBuiltin () TyBool] []
+    let sTy = StackType [TyBuiltin () TyBool] []
         in pure (sTy, PatternBool sTy i)
 assignPattern (PatternCons _ tn) = do { ty <- renameStack . flipStackType =<< consLookup (void tn) ; pure (ty, PatternCons ty (tn $> ty)) }
 assignPattern PatternWildcard{} = do
     aN <- dummyName "a"
-    let resType = StackType (S.singleton aN) [TyVar () aN] []
+    let resType = StackType [TyVar () aN] []
     pure (resType, PatternWildcard resType)
 
 mergeMany :: NonEmpty (StackType ()) -> TypeM () (StackType ())
@@ -562,10 +562,10 @@
     modifying constraintsLens (S.insert (ty, ty'))
 
 expandType :: Int -> StackType () -> TypeM () (StackType ())
-expandType n (StackType q i o) = do
+expandType n (StackType i o) = do
     newVars <- replicateM n (dummyName "a")
     let newTy = TyVar () <$> newVars
-    pure $ StackType (q <> S.fromList newVars) (newTy ++ i) (newTy ++ o)
+    pure $ StackType (newTy ++ i) (newTy ++ o)
 
 substConstraints :: IM.IntMap (KempeTy a) -> KempeTy a -> KempeTy a
 substConstraints _ ty@TyNamed{}                         = ty
@@ -573,33 +573,33 @@
 substConstraints tys ty@(TyVar _ (Name _ (Unique k) _)) =
     case IM.lookup k tys of
         Just ty'@TyVar{}       -> substConstraints (IM.delete k tys) ty' -- TODO: this is to prevent cyclic lookups: is it right?
-        Just (TyApp l ty0 ty1) -> let tys' = IM.delete k tys in TyApp l (substConstraints tys' ty0) (substConstraints tys' ty1) -- FIXME: cyclic?
+        Just (TyApp l ty0 ty1) -> let tys' = IM.delete k tys in TyApp l (substConstraints tys' ty0) (substConstraints tys' ty1)
         Just ty'               -> ty'
         Nothing                -> ty
 substConstraints tys (TyApp l ty ty')                   =
     TyApp l (substConstraints tys ty) (substConstraints tys ty')
 
 substConstraintsStack :: IM.IntMap (KempeTy a) -> StackType a -> StackType a
-substConstraintsStack tys (StackType _ is os) = {-# SCC "substConstraintsStack" #-}
+substConstraintsStack tys (StackType is os) = {-# SCC "substConstraintsStack" #-}
     let is' = substConstraints tys <$> is
         os' = substConstraints tys <$> os
-        in StackType (freeVars (is' ++ os')) is' os'
+        in StackType is' os'
 
 -- do renaming before this
 -- | Given @x@ and @y@, return the 'StackType' of @x y@
 catTypes :: StackType () -- ^ @x@
          -> StackType () -- ^ @y@
          -> TypeM () (StackType ())
-catTypes st0@(StackType _ _ osX) (StackType q1 insY osY) = do
+catTypes st0@(StackType _ osX) (StackType insY osY) = do
     let lY = length insY
         lDiff = lY - length osX
 
     -- all of the "ins" of y have to come from x, so we expand x as needed
-    (StackType q0 insX osX') <- if lDiff > 0
+    (StackType insX osX') <- if lDiff > 0
         then expandType lDiff st0
         else pure st0
 
     -- zip the last (length insY) of osX' with insY
     zipWithM_ pushConstraint (drop (length osX' - lY) osX') insY -- TODO splitAt
 
-    pure $ StackType (q0 <> q1) insX (take (length osX' - lY) osX' ++ osY)
+    pure $ StackType insX (take (length osX' - lY) osX' ++ osY)