diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # kempe
 
+# 0.2.0.11
+
+  * Fix bug in typechecker
+
 ## 0.2.0.10
 
   * Fix bug in typechecking against inferred signatures.
diff --git a/kempe.cabal b/kempe.cabal
--- a/kempe.cabal
+++ b/kempe.cabal
@@ -1,6 +1,6 @@
 cabal-version:   3.0
 name:            kempe
-version:         0.2.0.10
+version:         0.2.0.11
 license:         BSD-3-Clause
 license-file:    LICENSE
 copyright:       Copyright: (c) 2020-2021 Vanessa McHale
diff --git a/src/Kempe/TyAssign.hs b/src/Kempe/TyAssign.hs
--- a/src/Kempe/TyAssign.hs
+++ b/src/Kempe/TyAssign.hs
@@ -406,14 +406,12 @@
 -- TODO: do we want strict or lazy?
 type EqState a = State (Vars a)
 
--- FIXME: this is too simple-minded.
--- a -- a b
--- checks against
--- dup
--- because it results in the constraint a = b...
+-- need to check stack types are less general up to "alpha-equivalence"
+-- (implicit forall with every new var! in a stack type)
 --
--- NEED to check stack types are equivalent up to "alpha-equivalence"
--- (implicit binding with every space/new var!)
+-- Basically the inferred type has to check against the type in the signature.
+-- Which I'm not sure this does; it should be better-founded with an
+-- explanation of why it works (I'm not sure it works)
 lessGeneral :: StackType a -- ^ Inferred type
             -> StackType a -- ^ Type from signature
             -> Bool
@@ -434,9 +432,6 @@
           lessGeneralAtom :: KempeTy a -> KempeTy a -> EqState a Bool
           lessGeneralAtom TyBuiltin{} TyVar{}                   = pure True
           lessGeneralAtom TyApp{} TyVar{}                       = pure True
-          -- FIXME: Type a_13 (Maybe_1 a_10) -- a_12 is not as general as type a_9 (Maybe_1 a_9) -- a_9
-          --
-          -- FIXME Type a_38 b_39 a_40 -- b_39 b_42 a_41 is not as general as type a_35 b_36 c_37 -- c_37 b_36 a_35
           lessGeneralAtom (TyApp _ ty ty') (TyApp _ ty'' ty''') = (||) <$> lessGeneralAtom ty ty'' <*> lessGeneralAtom ty' ty''' -- lazy pattern match?
           lessGeneralAtom _ _                                   = pure False
           lessGenerals :: [KempeTy a] -> [KempeTy a] -> EqState a Bool
@@ -578,7 +573,7 @@
 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) -> TyApp l (substConstraints tys ty0) (substConstraints tys ty1)
+        Just (TyApp l ty0 ty1) -> let tys' = IM.delete k tys in TyApp l (substConstraints tys' ty0) (substConstraints tys' ty1) -- FIXME: cyclic?
         Just ty'               -> ty'
         Nothing                -> ty
 substConstraints tys (TyApp l ty ty')                   =