diff --git a/purescript.cabal b/purescript.cabal
--- a/purescript.cabal
+++ b/purescript.cabal
@@ -1,5 +1,5 @@
 name: purescript
-version: 0.3.5
+version: 0.3.6
 cabal-version: >=1.8
 build-type: Simple
 license: MIT
@@ -17,7 +17,7 @@
 library
     build-depends: base >=4 && <5, cmdtheline -any, containers -any,
                    directory -any, filepath -any, mtl -any, parsec -any, syb -any,
-                   transformers -any, utf8-string -any, pattern-arrows -any
+                   transformers -any, utf8-string -any, pattern-arrows -any, monad-unify -any
     exposed-modules: Data.Generics.Extras
                      Language.PureScript
                      Language.PureScript.Options
@@ -25,7 +25,6 @@
                      Language.PureScript.Kinds
                      Language.PureScript.Names
                      Language.PureScript.Types
-                     Language.PureScript.Unknown
                      Language.PureScript.Values
                      Language.PureScript.Scope
                      Language.PureScript.Sugar
diff --git a/src/Language/PureScript.hs b/src/Language/PureScript.hs
--- a/src/Language/PureScript.hs
+++ b/src/Language/PureScript.hs
@@ -30,6 +30,7 @@
 
 import Data.List (intercalate)
 import Control.Monad (when, forM)
+import Control.Monad.State.Lazy
 import Control.Applicative ((<$>))
 import qualified Data.Map as M
 
@@ -54,7 +55,9 @@
 compile opts ms = do
   sorted <- sortModules ms
   desugared <- desugar sorted
-  (elaborated, env) <- runCheck $ forM desugared $ \(Module moduleName decls) -> Module moduleName <$> typeCheckAll (ModuleName moduleName) decls
+  (elaborated, env) <- runCheck $ forM desugared $ \(Module moduleName decls) -> do
+    modify (\s -> s { checkCurrentModule = Just (ModuleName moduleName) })
+    Module moduleName <$> typeCheckAll (ModuleName moduleName) decls
   regrouped <- createBindingGroupsModule . collapseBindingGroupsModule $ elaborated
   let js = concatMap (flip (moduleToJs opts) env) $ regrouped
   let exts = intercalate "\n" . map (flip moduleToPs env) $ regrouped
diff --git a/src/Language/PureScript/Kinds.hs b/src/Language/PureScript/Kinds.hs
--- a/src/Language/PureScript/Kinds.hs
+++ b/src/Language/PureScript/Kinds.hs
@@ -17,8 +17,9 @@
 module Language.PureScript.Kinds where
 
 import Data.Data
-import Language.PureScript.Unknown
 
+import Control.Monad.Unify (TypedUnknown(..))
+
 -- |
 -- The data type of kinds
 --
@@ -26,7 +27,7 @@
   -- |
   -- Unification variable of type Kind
   --
-  = KUnknown (Unknown Kind)
+  = KUnknown (TypedUnknown Kind)
   -- |
   -- The kind of types
   --
diff --git a/src/Language/PureScript/Pretty/Kinds.hs b/src/Language/PureScript/Pretty/Kinds.hs
--- a/src/Language/PureScript/Pretty/Kinds.hs
+++ b/src/Language/PureScript/Pretty/Kinds.hs
@@ -21,17 +21,17 @@
 
 import Control.Arrow (ArrowPlus(..))
 import Control.PatternArrows
+import Control.Monad.Unify
 
 import Language.PureScript.Kinds
 import Language.PureScript.Pretty.Common
-import Language.PureScript.Unknown
 
 typeLiterals :: Pattern () Kind String
 typeLiterals = mkPattern match
   where
   match Star = Just "*"
   match Bang = Just "!"
-  match (KUnknown (Unknown u)) = Just $ 'u' : show u
+  match (KUnknown (TypedUnknown (Unknown u))) = Just $ 'u' : show u
   match _ = Nothing
 
 matchRow :: Pattern () Kind ((), Kind)
diff --git a/src/Language/PureScript/Pretty/Types.hs b/src/Language/PureScript/Pretty/Types.hs
--- a/src/Language/PureScript/Pretty/Types.hs
+++ b/src/Language/PureScript/Pretty/Types.hs
@@ -23,10 +23,10 @@
 
 import Control.Arrow ((<+>))
 import Control.PatternArrows
+import Control.Monad.Unify
 
 import Language.PureScript.Types
 import Language.PureScript.Pretty.Common
-import Language.PureScript.Unknown
 
 typeLiterals :: Pattern () Type String
 typeLiterals = mkPattern match
@@ -38,7 +38,7 @@
   match (Object row) = Just $ "{ " ++ prettyPrintType row ++ " }"
   match (TypeVar var) = Just var
   match (TypeConstructor ctor) = Just $ show ctor
-  match (TUnknown (Unknown u)) = Just $ 'u' : show u
+  match (TUnknown (TypedUnknown (Unknown u))) = Just $ 'u' : show u
   match (Skolem s) = Just $ 's' : show s
   match (ConstrainedType deps ty) = Just $ "(" ++ intercalate "," (map (\(pn, ty') -> show pn ++ " (" ++ prettyPrintType ty' ++ ")") deps) ++ ") => " ++ prettyPrintType ty
   match (SaturatedTypeSynonym name args) = Just $ show name ++ "<" ++ intercalate "," (map prettyPrintType args) ++ ">"
@@ -57,7 +57,7 @@
   nameAndTypeToPs name ty = name ++ " :: " ++ prettyPrintType ty
   tailToPs :: Type -> String
   tailToPs REmpty = ""
-  tailToPs (TUnknown (Unknown u)) = " | u" ++ show u
+  tailToPs (TUnknown (TypedUnknown (Unknown u))) = " | u" ++ show u
   tailToPs (TypeVar var) = " | " ++ var
   tailToPs (Skolem s) = " | s" ++ show s
   tailToPs _ = error "Invalid row tail"
diff --git a/src/Language/PureScript/TypeChecker/Kinds.hs b/src/Language/PureScript/TypeChecker/Kinds.hs
--- a/src/Language/PureScript/TypeChecker/Kinds.hs
+++ b/src/Language/PureScript/TypeChecker/Kinds.hs
@@ -15,6 +15,7 @@
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 {-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 
 module Language.PureScript.TypeChecker.Kinds (
     kindOf,
@@ -27,48 +28,42 @@
 import Language.PureScript.Names
 import Language.PureScript.TypeChecker.Monad
 import Language.PureScript.Pretty
-import Language.PureScript.Unknown
 
 import Control.Monad.State
 import Control.Monad.Error
 import Control.Monad.Reader
+import Control.Monad.Unify
 
 import Control.Applicative
 
 import qualified Data.Map as M
 
-instance Unifiable Kind where
+instance Unifiable Check Kind where
   unknown = KUnknown
   isUnknown (KUnknown u) = Just u
   isUnknown _ = Nothing
-  KUnknown u1 ~~ KUnknown u2 | u1 == u2 = return ()
-  KUnknown u ~~ k = replace u k
-  k ~~ KUnknown u = replace u k
-  Star ~~ Star = return ()
-  Bang ~~ Bang = return ()
-  Row k1 ~~ Row k2 = k1 ~~ k2
-  FunKind k1 k2 ~~ FunKind k3 k4 = do
-    k1 ~~ k3
-    k2 ~~ k4
-  k1 ~~ k2 = throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."
-  apply s (KUnknown u) = runSubstitution s u
-  apply s (FunKind k1 k2) = FunKind (apply s k1) (apply s k2)
-  apply _ k = k
-  unknowns (KUnknown (Unknown u)) = [u]
-  unknowns (FunKind k1 k2) = unknowns k1 ++ unknowns k2
-  unknowns _ = []
+  KUnknown u1 ?= KUnknown u2 | u1 == u2 = return ()
+  KUnknown u ?= k = replace u k
+  k ?= KUnknown u = replace u k
+  Star ?= Star = return ()
+  Bang ?= Bang = return ()
+  Row k1 ?= Row k2 = k1 ?= k2
+  FunKind k1 k2 ?= FunKind k3 k4 = do
+    k1 ?= k3
+    k2 ?= k4
+  k1 ?= k2 = UnifyT . lift . throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."
 
 -- |
 -- Infer the kind of a single type
 --
 kindOf :: ModuleName -> Type -> Check Kind
-kindOf moduleName ty = fmap (\(k, s) -> apply s k) . runSubst (SubstContext moduleName) $ starIfUnknown <$> infer ty
+kindOf moduleName ty = liftUnify $ starIfUnknown <$> infer ty
 
 -- |
 -- Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors
 --
 kindsOf :: ModuleName -> ProperName -> [String] -> [Type] -> Check Kind
-kindsOf moduleName name args ts = fmap (starIfUnknown . (\(k, s) -> apply s k)) . runSubst (SubstContext moduleName) $ do
+kindsOf moduleName name args ts = fmap starIfUnknown . liftUnify $ do
   tyCon <- fresh
   kargs <- replicateM (length args) fresh
   let dict = (name, tyCon) : zip (map ProperName args) kargs
@@ -79,7 +74,7 @@
 -- Simultaneously infer the kinds of several mutually recursive type constructors
 --
 kindsOfAll :: ModuleName -> [(ProperName, [String], Type)] -> [(ProperName, [String], [Type])] -> Check ([Kind], [Kind])
-kindsOfAll moduleName syns tys = fmap tidyUp . runSubst (SubstContext moduleName) $ do
+kindsOfAll moduleName syns tys = fmap tidyUp . liftUnify $ do
   synVars <- replicateM (length syns) fresh
   let dict = zipWith (\(name, _, _) var -> (name, var)) syns synVars
   bindLocalTypeVariables moduleName dict $ do
@@ -98,16 +93,16 @@
           solveTypes [ty] kargs synVar) synVars syns
       return (syn_ks, data_ks)
   where
-  tidyUp ((ks1, ks2), s) = (map starIfUnknown $ apply s ks1, map starIfUnknown $ apply s ks2)
+  tidyUp (ks1, ks2) = (map starIfUnknown ks1, map starIfUnknown ks2)
 
 -- |
 -- Solve the set of kind constraints associated with the data constructors for a type constructor
 --
-solveTypes :: [Type] -> [Kind] -> Kind -> Subst Kind
+solveTypes :: [Type] -> [Kind] -> Kind -> UnifyT Check Kind
 solveTypes ts kargs tyCon = do
   ks <- mapM infer ts
-  tyCon ~~ foldr FunKind Star kargs
-  forM_ ks $ \k -> k ~~ Star
+  tyCon ?= foldr FunKind Star kargs
+  forM_ ks $ \k -> k ?= Star
   return tyCon
 
 -- |
@@ -121,39 +116,39 @@
 -- |
 -- Infer a kind for a type
 --
-infer :: Type -> Subst Kind
+infer :: Type -> UnifyT Check Kind
 infer Number = return Star
 infer String = return Star
 infer Boolean = return Star
 infer Array = return $ FunKind Star Star
 infer (Object row) = do
   k <- infer row
-  k ~~ Row Star
+  k ?= Row Star
   return Star
 infer (Function args ret) = do
   ks <- mapM infer args
   k <- infer ret
-  k ~~ Star
-  forM_ ks (~~ Star)
+  k ?= Star
+  forM_ ks (?= Star)
   return Star
 infer (TypeVar v) = do
-  moduleName <- substCurrentModule <$> ask
-  lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
+  Just moduleName <- checkCurrentModule <$> get
+  UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
 infer (TypeConstructor v) = do
   env <- liftCheck getEnv
-  moduleName <- substCurrentModule `fmap` ask
+  Just moduleName <- checkCurrentModule <$> get
   case M.lookup (qualify moduleName v) (types env) of
-    Nothing -> throwError $ "Unknown type constructor '" ++ show v ++ "'"
+    Nothing -> UnifyT . lift . throwError $ "Unknown type constructor '" ++ show v ++ "'"
     Just (kind, _) -> return kind
 infer (TypeApp t1 t2) = do
   k0 <- fresh
   k1 <- infer t1
   k2 <- infer t2
-  k1 ~~ FunKind k2 k0
+  k1 ?= FunKind k2 k0
   return k0
 infer (ForAll ident ty) = do
   k <- fresh
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   bindLocalTypeVariables moduleName [(ProperName ident, k)] $ infer ty
 infer REmpty = do
   k <- fresh
@@ -161,11 +156,11 @@
 infer (RCons _ ty row) = do
   k1 <- infer ty
   k2 <- infer row
-  k2 ~~ Row k1
+  k2 ?= Row k1
   return $ Row k1
 infer (ConstrainedType deps ty) = do
   mapM_ (infer . snd) deps
   k <- infer ty
-  k ~~ Star
+  k ?= Star
   return Star
 infer _ = error "Invalid argument to infer"
diff --git a/src/Language/PureScript/TypeChecker/Monad.hs b/src/Language/PureScript/TypeChecker/Monad.hs
--- a/src/Language/PureScript/TypeChecker/Monad.hs
+++ b/src/Language/PureScript/TypeChecker/Monad.hs
@@ -22,7 +22,6 @@
 import Language.PureScript.Kinds
 import Language.PureScript.Values
 import Language.PureScript.Names
-import Language.PureScript.Unknown
 import Language.PureScript.Declarations
 
 import Data.Data
@@ -34,6 +33,7 @@
 import Control.Monad.State
 import Control.Monad.Error
 import Control.Monad.Reader
+import Control.Monad.Unify
 import Control.Arrow ((***))
 
 import qualified Data.Map as M
@@ -227,6 +227,10 @@
   -- The next type class dictionary name
   --
   , checkNextDictName :: Int
+  -- |
+  -- The current module
+  --
+  , checkCurrentModule :: Maybe ModuleName
   }
 
 -- |
@@ -258,7 +262,7 @@
 --
 runCheck :: Check a -> Either String (a, Environment)
 runCheck c = do
-  (a, s) <- flip runStateT (CheckState emptyEnvironment 0 0) $ unCheck c
+  (a, s) <- flip runStateT (CheckState emptyEnvironment 0 0 Nothing) $ unCheck c
   return (a, checkEnv s)
 
 -- |
@@ -284,129 +288,23 @@
   return n
 
 -- |
--- A substitution maintains a mapping from unification variables to their values, ensuring that
--- the type of a unification variable matches the type of its value.
---
-newtype Substitution = Substitution { runSubstitution :: forall t. (Unifiable t) => Unknown t -> t }
-
-instance Monoid Substitution where
-  mempty = Substitution unknown
-  s1 `mappend` s2 = Substitution $ \u -> apply s1 (apply s2 (unknown u))
-
--- |
--- State for the substitution monad, which contains the current substitution
---
-data SubstState = SubstState { substSubst :: Substitution }
-
--- |
--- Configuration for the substitution monad, constaining the current module
---
-newtype SubstContext = SubstContext { substCurrentModule :: ModuleName } deriving (Show)
-
--- |
--- The substitution monad, which provides the means to unify values to generate a substitution, in addition to
--- the actions supported by the type checking monad @Check@.
---
-newtype Subst a = Subst { unSubst :: ReaderT SubstContext (StateT SubstState Check) a }
-  deriving (Functor, Monad, Applicative, MonadPlus, MonadReader SubstContext)
-
-instance MonadState CheckState Subst where
-  get = Subst . lift . lift $ get
-  put = Subst . lift . lift . put
-
-deriving instance MonadError String Subst
-
--- |
 -- Lift a computation in the @Check@ monad into the substitution monad.
 --
-liftCheck :: Check a -> Subst a
-liftCheck = Subst . lift . lift
-
--- |
--- Get the current substitution monad state
---
-getSubstState :: Subst SubstState
-getSubstState = Subst . lift $ get
+liftCheck :: Check a -> UnifyT Check a
+liftCheck = UnifyT . lift . lift
 
 -- |
 -- Run a computation in the substitution monad, generating a return value and the final substitution.
 --
-runSubst :: SubstContext -> Subst a -> Check (a, Substitution)
-runSubst context subst = do
-  (a, s) <- flip runStateT (SubstState mempty) . flip runReaderT context . unSubst $ subst
-  return (a, substSubst s)
-
--- |
--- Generate a substitution from a substitution function for a single type
---
-substituteWith :: (Typeable t) => (Unknown t -> t) -> Substitution
-substituteWith f = Substitution $ \u -> fromMaybe (unknown u) $ do
-  u1 <- cast u
-  cast (f u1)
-
--- |
--- Substitute a single unification variable
---
-substituteOne :: (Unifiable t) => Unknown t -> t -> Substitution
-substituteOne u t = substituteWith $ \u1 ->
-  case u1 of
-    u2 | u2 == u -> t
-       | otherwise -> unknown u2
-
--- |
--- Replace a unification variable with the specified value in the current substitution
---
-replace :: (Unifiable t) => Unknown t -> t -> Subst ()
-replace u t' = do
-  sub <- substSubst <$> Subst get
-  let t = apply sub t'
-  occursCheck u t
-  let current = apply sub $ unknown u
-  case isUnknown current of
-    Just u1 | u1 == u -> return ()
-    _ -> current ~~ t
-  Subst . modify $ \s -> s { substSubst = substituteOne u t <> substSubst s }
-
--- |
--- Identifies types which support unification
---
-class (Typeable t, Data t, Show t) => Unifiable t where
-  unknown :: Unknown t -> t
-  (~~) :: t -> t -> Subst ()
-  isUnknown :: t -> Maybe (Unknown t)
-  apply :: Substitution -> t -> t
-  unknowns :: t -> [Int]
-
-instance (Unifiable a) => Unifiable [a] where
-  unknown _ = error "not supported"
-  (~~) = zipWithM_ (~~)
-  isUnknown _ = error "not supported"
-  apply s = map (apply s)
-  unknowns = concatMap unknowns
-
--- |
--- Perform the occurs check, to make sure a unification variable does not occur inside a value
---
-occursCheck :: (Unifiable t) => Unknown s -> t -> Subst ()
-occursCheck (Unknown u) t =
-  case isUnknown t of
-    Nothing -> guardWith "Occurs check fails" (u `notElem` unknowns t)
-    _ -> return ()
-
--- |
--- Generate a fresh untyped unification variable
---
-fresh' :: Subst Int
-fresh' = do
-  n <- checkNextVar <$> get
-  modify $ \s -> s { checkNextVar = succ (checkNextVar s) }
-  return n
-
--- |
--- Generate a fresh unification variable at a specific type
---
-fresh :: (Unifiable t) => Subst t
-fresh = unknown . Unknown <$> fresh'
+liftUnify :: (Data a) => UnifyT Check a -> Check a
+liftUnify unify = do
+  st <- get
+  e <- runUnify (defaultUnifyState { unifyNextVar = checkNextVar st }) unify
+  case e of
+    Left err -> throwError err
+    Right (a, ust) -> do
+      modify $ \st -> st { checkNextVar = unifyNextVar ust }
+      return $ runSubstitution (unifyCurrentSubstitution ust) a
 
 -- |
 -- Replace any unqualified names in a type wit their qualified versionss
diff --git a/src/Language/PureScript/TypeChecker/Types.hs b/src/Language/PureScript/TypeChecker/Types.hs
--- a/src/Language/PureScript/TypeChecker/Types.hs
+++ b/src/Language/PureScript/TypeChecker/Types.hs
@@ -14,7 +14,9 @@
 -----------------------------------------------------------------------------
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# LANGUAGE DeriveDataTypeable, FlexibleContexts #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 
 module Language.PureScript.TypeChecker.Types (
     typesOf
@@ -53,11 +55,11 @@
 import Language.PureScript.TypeChecker.Kinds
 import Language.PureScript.TypeChecker.Synonyms
 import Language.PureScript.Pretty
-import Language.PureScript.Unknown
 
 import Control.Monad.State
 import Control.Monad.Error
 import Control.Monad.Reader
+import Control.Monad.Unify
 
 import Control.Applicative
 import Control.Arrow (Arrow(..))
@@ -65,32 +67,16 @@
 import qualified Data.Map as M
 import Data.Function (on)
 
-instance Unifiable Type where
+instance Unifiable Check Type where
   unknown = TUnknown
   isUnknown (TUnknown u) = Just u
   isUnknown _ = Nothing
-  (~~) = unifyTypes
-  apply s (TUnknown u) = runSubstitution s u
-  apply s (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name $ map (apply s) tys
-  apply s (ForAll idents ty) = ForAll idents $ apply s ty
-  apply s (Object r) = Object (apply s r)
-  apply s (Function args ret) = Function (map (apply s) args) (apply s ret)
-  apply s (TypeApp t1 t2) = TypeApp (apply s t1) (apply s t2)
-  apply s (RCons name ty r) = RCons name (apply s ty) (apply s r)
-  apply _ t = t
-  unknowns (TUnknown (Unknown u)) = [u]
-  unknowns (SaturatedTypeSynonym _ tys) = concatMap unknowns tys
-  unknowns (ForAll _ ty) = unknowns ty
-  unknowns (Object r) = unknowns r
-  unknowns (Function args ret) = concatMap unknowns args ++ unknowns ret
-  unknowns (TypeApp t1 t2) = unknowns t1 ++ unknowns t2
-  unknowns (RCons _ ty r) = unknowns ty ++ unknowns r
-  unknowns _ = []
+  (?=) = unifyTypes
 
 -- |
 -- Unify two types, updating the current substitution
 --
-unifyTypes :: Type -> Type -> Subst ()
+unifyTypes :: Type -> Type -> UnifyT Check ()
 unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 ++ " with type " ++ prettyPrintType t2 ++ ":\n" ++ e) $ do
   unifyTypes' t1 t2
   where
@@ -113,7 +99,7 @@
   unifyTypes' String String = return ()
   unifyTypes' Boolean Boolean = return ()
   unifyTypes' Array Array = return ()
-  unifyTypes' (Object row1) (Object row2) = row1 ~~ row2
+  unifyTypes' (Object row1) (Object row2) = row1 ?= row2
   unifyTypes' (Function args1 ret1) (Function args2 ret2) = do
     guardWith "Function applied to incorrect number of args" $ length args1 == length args2
     zipWithM_ unifyTypes args1 args2
@@ -121,7 +107,7 @@
   unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()
   unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do
     env <- getEnv
-    moduleName <- substCurrentModule `fmap` ask
+    Just moduleName <- checkCurrentModule <$> get
     guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (typeConstructorsAreEqual env moduleName c1 c2)
   unifyTypes' (TypeApp t3 t4) (TypeApp t5 t6) = do
     t3 `unifyTypes` t5
@@ -140,7 +126,7 @@
 -- trailing row unification variable, if appropriate, otherwise leftover labels result in a unification
 -- error.
 --
-unifyRows :: Type -> Type -> Subst ()
+unifyRows :: Type -> Type -> UnifyT Check ()
 unifyRows r1 r2 =
   let
     (s1, r1') = rowToList r1
@@ -149,17 +135,17 @@
     sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
     sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
   in do
-    forM_ int (uncurry (~~))
+    forM_ int (uncurry (?=))
     unifyRows' sd1 r1' sd2 r2'
   where
-  unifyRows' :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Subst ()
+  unifyRows' :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> UnifyT Check ()
   unifyRows' [] (TUnknown u) sd r = replace u (rowFromList (sd, r))
   unifyRows' sd r [] (TUnknown u) = replace u (rowFromList (sd, r))
   unifyRows' ((name, ty):row) r others u@(TUnknown un) = do
     occursCheck un ty
     forM_ row $ \(_, t) -> occursCheck un t
     u' <- fresh
-    u ~~ RCons name ty u'
+    u ?= RCons name ty u'
     unifyRows' row r others u'
   unifyRows' [] REmpty [] REmpty = return ()
   unifyRows' [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = return ()
@@ -178,8 +164,7 @@
 --
 typesOf :: ModuleName -> [(Ident, Value)] -> Check [(Ident, (Value, Type))]
 typesOf moduleName vals = do
-  tys <- fmap (\(tys, s) -> map (\(ident, (val, ty)) -> (ident, (overTypes (apply s) val, apply s ty))) tys)
-         . runSubst (SubstContext moduleName) $ do
+  tys <- liftUnify $ do
     let es = map isTyped vals
         typed = filter (isJust . snd . snd) es
         untyped = filter (isNothing . snd . snd) es
@@ -197,11 +182,11 @@
           return (ident, (val', ty'))
         (ident, (val, Nothing)) -> do
           TypedValue _ val' ty <- bindNames dict $ infer val
-          ty ~~ fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)
+          ty ?= fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)
           return (ident, (val', ty))
       when (moduleName == ModuleName (ProperName "Main") && fst e == Ident "main") $ do
         [eff, a] <- replicateM 2 fresh
-        ty ~~ TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a
+        ty ?= TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a
       escapeCheck val ty
       return triple
   forM_ tys $ skolemEscapeCheck . snd . snd
@@ -279,14 +264,14 @@
 -- |
 -- Ensure unsolved unification variables do not escape
 --
-escapeCheck :: Value -> Type -> Subst ()
+escapeCheck :: Value -> Type -> UnifyT Check ()
 escapeCheck value ty = do
-  subst <- substSubst <$> getSubstState
-  let visibleUnknowns = nub $ unknowns $ apply subst ty
+  subst <- unifyCurrentSubstitution <$> UnifyT get
+  let visibleUnknowns = nub $ unknowns $ runSubstitution subst ty
   let allUnknowns = findAllTypes value
   forM_ allUnknowns $ \t -> do
-    let unsolvedUnknowns = nub . unknowns $ apply subst t
-    guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns
+    let unsolvedUnknowns = nub . unknowns $ runSubstitution subst t
+    guardWith ("Escape check fails" ++ show ( runSubstitution subst ty, runSubstitution subst t)) $ null $ unsolvedUnknowns \\ visibleUnknowns
 
 -- |
 -- Find all type annotations occuring inside a value
@@ -304,7 +289,7 @@
 skolemEscapeCheck ty =
   case something (mkQ Nothing findSkolems) ty of
     Nothing -> return ()
-    Just _ -> throwError $ "Skolem variables cannot escape. Consider adding a type signature." ++ show ty
+    Just _ -> throwError $ "Skolem variables cannot escape. Consider adding a type signature."
   where
     findSkolems (Skolem _) = return ()
     findSkolems _ = mzero
@@ -330,9 +315,9 @@
       toName = (:) 't' . show
       ty' = everywhere (mkT typeToVar) $ ty
       typeToVar :: Type -> Type
-      typeToVar (TUnknown (Unknown u)) = TypeVar (toName u)
+      typeToVar (TUnknown (TypedUnknown (Unknown u))) = TypeVar (toName u)
       typeToVar t = t
-  in mkForAll (sort . map toName $ unks) ty'
+  in mkForAll (sort . map (toName . runUnknown) $ unks) ty'
 
 -- |
 -- Replace named type variables with types
@@ -343,14 +328,14 @@
 -- |
 -- Replace named type variables with new unification variables
 --
-replaceAllVarsWithUnknowns :: Type -> Subst Type
+replaceAllVarsWithUnknowns :: Type -> UnifyT Check Type
 replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns
 replaceAllVarsWithUnknowns ty = return ty
 
 -- |
 -- Replace a single type variable with a new unification variable
 --
-replaceVarWithUnknown :: String -> Type -> Subst Type
+replaceVarWithUnknown :: String -> Type -> UnifyT Check Type
 replaceVarWithUnknown ident ty = do
   tu <- fresh
   return $ replaceTypeVars ident tu $ ty
@@ -359,10 +344,10 @@
 -- Replace fully applied type synonyms with the @SaturatedTypeSynonym@ data constructor, which helps generate
 -- better error messages during unification.
 --
-replaceAllTypeSynonyms :: (Functor m, MonadState CheckState m, MonadReader SubstContext m, MonadError String m) => (D.Data d) => d -> m d
+replaceAllTypeSynonyms :: (Functor m, MonadState CheckState m, MonadError String m) => (D.Data d) => d -> m d
 replaceAllTypeSynonyms d = do
   env <- getEnv
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   let syns = map (\((path, name), (args, _)) -> ((path, name), length args)) . M.toList $ typeSynonyms env
   either throwError return $ saturateAllTypeSynonyms env moduleName syns d
 
@@ -378,10 +363,10 @@
 -- |
 -- Replace a type synonym and its arguments with the aliased type
 --
-expandTypeSynonym :: Qualified ProperName -> [Type] -> Subst Type
+expandTypeSynonym :: Qualified ProperName -> [Type] -> UnifyT Check Type
 expandTypeSynonym name args = do
   env <- getEnv
-  moduleName <- substCurrentModule `fmap` ask
+  Just moduleName <- checkCurrentModule <$> get
   case M.lookup (canonicalizeType moduleName env name) (typeSynonyms env) of
     Just (synArgs, body) -> return $ replaceAllTypeVars (zip synArgs args) body
     Nothing -> error "Type synonym was not defined"
@@ -395,20 +380,20 @@
 -- |
 -- Infer a type for a value, rethrowing any error to provide a more useful error message
 --
-infer :: Value -> Subst Value
+infer :: Value -> UnifyT Check Value
 infer val = rethrow (\e -> "Error inferring type of term " ++ prettyPrintValue val ++ ":\n" ++ e) $ infer' val
 
 -- |
 -- Infer a type for a value
 --
-infer' :: Value -> Subst Value
+infer' :: Value -> UnifyT Check Value
 infer' v@(NumericLiteral _) = return $ TypedValue True v Number
 infer' v@(StringLiteral _) = return $ TypedValue True v String
 infer' v@(BooleanLiteral _) = return $ TypedValue True v Boolean
 infer' (ArrayLiteral vals) = do
   ts <- mapM infer vals
   els <- fresh
-  forM_ ts $ \(TypedValue _ _ t) -> els ~~ TypeApp Array t
+  forM_ ts $ \(TypedValue _ _ t) -> els ?= TypeApp Array t
   return $ TypedValue True (ArrayLiteral ts) els
 infer' (Unary op val) = do
   v <- infer val
@@ -448,7 +433,7 @@
     Just ty -> return $ TypedValue True (Accessor prop typed) ty
 infer' (Abs args ret) = do
   ts <- replicateM (length args) fresh
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   bindLocalVariables moduleName (zip args ts) $ do
     body@(TypedValue _ _ bodyTy) <- infer' ret
     return $ TypedValue True (Abs args body) $ Function ts bodyTy
@@ -458,7 +443,7 @@
   app <- checkFunctionApplication f' ft args ret
   return $ TypedValue True app ret
 infer' (Var var) = do
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   ty <- lookupVariable moduleName var
   ty' <- replaceAllTypeSynonyms ty
   case ty' of
@@ -474,7 +459,7 @@
   return $ TypedValue True (Block ss') ret
 infer' v@(Constructor c) = do
   env <- getEnv
-  moduleName <- substCurrentModule `fmap` ask
+  Just moduleName <- checkCurrentModule <$> get
   case M.lookup (qualify moduleName c) (dataConstructors env) of
     Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
     Just (ty, _) -> do ty' <- replaceAllTypeSynonyms ty
@@ -488,10 +473,10 @@
   cond' <- check cond Boolean
   v2@(TypedValue _ _ t2) <- infer th
   v3@(TypedValue _ _ t3) <- infer el
-  t2 ~~ t3
+  t2 ?= t3
   return $ TypedValue True (IfThenElse cond' v2 v3) t2
 infer' (TypedValue checkType val ty) = do
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   kind <- liftCheck $ kindOf moduleName ty
   guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
   ty' <- replaceAllTypeSynonyms ty
@@ -502,7 +487,7 @@
 -- |
 -- Infer the type of a property inside a record with a given type
 --
-inferProperty :: Type -> String -> Subst (Maybe Type)
+inferProperty :: Type -> String -> UnifyT Check (Maybe Type)
 inferProperty (Object row) prop = do
   let (props, _) = rowToList row
   return $ lookup prop props
@@ -517,22 +502,22 @@
 -- |
 -- Infer the type of a unary operator application
 --
-inferUnary :: UnaryOperator -> Value -> Subst Value
+inferUnary :: UnaryOperator -> Value -> UnifyT Check Value
 inferUnary op (TypedValue _ val valTy) =
   case fromMaybe (error "Invalid operator") $ lookup op unaryOps of
     (valTy', resTy) -> do
-      valTy' ~~ valTy
+      valTy' ?= valTy
       return $ TypedValue True (Unary op val) resTy
 inferUnary _ _ = error "Invalid arguments to inferUnary"
 
 -- |
 -- Check the type of a unary operator application
 --
-checkUnary :: UnaryOperator -> Value -> Type -> Subst Value
+checkUnary :: UnaryOperator -> Value -> Type -> UnifyT Check Value
 checkUnary op val res =
   case fromMaybe (error "Invalid operator") $ lookup op unaryOps of
     (valTy, resTy) -> do
-      res ~~ resTy
+      res ?= resTy
       val' <- check val valTy
       return $ Unary op val'
 
@@ -548,32 +533,32 @@
 -- |
 -- Infer the type of a binary operator application
 --
-inferBinary :: BinaryOperator -> Value -> Value -> Subst Value
+inferBinary :: BinaryOperator -> Value -> Value -> UnifyT Check Value
 inferBinary op left@(TypedValue _ _ leftTy) right@(TypedValue _ _ rightTy) | isEqualityTest op = do
-  leftTy ~~ rightTy
+  leftTy ?= rightTy
   return $ TypedValue True (Binary op left right) Boolean
 inferBinary op left@(TypedValue _ _ leftTy) right@(TypedValue _ _ rightTy) =
   case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
     (valTy, resTy) -> do
-      leftTy ~~ valTy
-      rightTy ~~ valTy
+      leftTy ?= valTy
+      rightTy ?= valTy
       return $ TypedValue True (Binary op left right) resTy
 inferBinary _ _ _ = error "Invalid arguments to inferBinary"
 
 -- |
 -- Check the type of a binary operator application
 --
-checkBinary :: BinaryOperator -> Value -> Value -> Type -> Subst Value
+checkBinary :: BinaryOperator -> Value -> Value -> Type -> UnifyT Check Value
 checkBinary op left right res | isEqualityTest op = do
-  res ~~ Boolean
+  res ?= Boolean
   left'@(TypedValue _ _ t1) <- infer left
   right'@(TypedValue _ _ t2) <- infer right
-  t1 ~~ t2
+  t1 ?= t2
   return $ Binary op left' right'
 checkBinary op left right res =
   case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
     (valTy, resTy) -> do
-      res ~~ resTy
+      res ?= resTy
       left' <- check left valTy
       right' <- check right valTy
       return $ Binary op left' right'
@@ -613,15 +598,15 @@
 -- |
 -- Infer the types of variables brought into scope by a binder
 --
-inferBinder :: Type -> Binder -> Subst (M.Map Ident Type)
+inferBinder :: Type -> Binder -> UnifyT Check (M.Map Ident Type)
 inferBinder _ NullBinder = return M.empty
-inferBinder val (StringBinder _) = val ~~ String >> return M.empty
-inferBinder val (NumberBinder _) = val ~~ Number >> return M.empty
-inferBinder val (BooleanBinder _) = val ~~ Boolean >> return M.empty
+inferBinder val (StringBinder _) = val ?= String >> return M.empty
+inferBinder val (NumberBinder _) = val ?= Number >> return M.empty
+inferBinder val (BooleanBinder _) = val ?= Boolean >> return M.empty
 inferBinder val (VarBinder name) = return $ M.singleton name val
 inferBinder val (NullaryBinder ctor) = do
   env <- getEnv
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   case M.lookup (qualify moduleName ctor) (dataConstructors env) of
     Just (ty, _) -> do
       ty `subsumes` val
@@ -629,7 +614,7 @@
     _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
 inferBinder val (UnaryBinder ctor binder) = do
   env <- getEnv
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   case M.lookup (qualify moduleName ctor) (dataConstructors env) of
     Just (ty, _) -> do
       fn <- replaceAllVarsWithUnknowns ty
@@ -643,11 +628,11 @@
   row <- fresh
   rest <- fresh
   m1 <- inferRowProperties row rest props
-  val ~~ Object row
+  val ?= Object row
   return m1
   where
-  inferRowProperties :: Type -> Type -> [(String, Binder)] -> Subst (M.Map Ident Type)
-  inferRowProperties nrow row [] = nrow ~~ row >> return M.empty
+  inferRowProperties :: Type -> Type -> [(String, Binder)] -> UnifyT Check (M.Map Ident Type)
+  inferRowProperties nrow row [] = nrow ?= row >> return M.empty
   inferRowProperties nrow row ((name, binder):binders) = do
     propTy <- fresh
     m1 <- inferBinder propTy binder
@@ -656,13 +641,13 @@
 inferBinder val (ArrayBinder binders) = do
   el <- fresh
   m1 <- M.unions <$> mapM (inferBinder el) binders
-  val ~~ TypeApp Array el
+  val ?= TypeApp Array el
   return m1
 inferBinder val (ConsBinder headBinder tailBinder) = do
   el <- fresh
   m1 <- inferBinder el headBinder
   m2 <- inferBinder val tailBinder
-  val ~~ TypeApp Array el
+  val ?= TypeApp Array el
   return $ m1 `M.union` m2
 inferBinder val (NamedBinder name binder) = do
   m <- inferBinder val binder
@@ -671,10 +656,10 @@
 -- |
 -- Check the types of the return values in a set of binders in a case statement
 --
-checkBinders :: [Type] -> Type -> [([Binder], Maybe Guard, Value)] -> Subst [([Binder], Maybe Guard, Value)]
+checkBinders :: [Type] -> Type -> [([Binder], Maybe Guard, Value)] -> UnifyT Check [([Binder], Maybe Guard, Value)]
 checkBinders _ _ [] = return []
 checkBinders nvals ret ((binders, grd, val):bs) = do
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   m1 <- M.unions <$> zipWithM inferBinder nvals binders
   r <- bindLocalVariables moduleName (M.toList m1) $ do
     val' <- check val ret
@@ -689,19 +674,19 @@
 -- |
 -- Check that a local variable name is not already used
 --
-assignVariable :: Ident -> Subst ()
+assignVariable :: Ident -> UnifyT Check ()
 assignVariable name = do
   env <- checkEnv <$> get
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   case M.lookup (moduleName, name) (names env) of
-    Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
+    Just _ -> UnifyT . lift . throwError $ "Variable with name " ++ show name ++ " already exists."
     _ -> return ()
 
 -- |
 -- Check the type of the return values of a statement, returning whether or not the statement returns on
 -- all code paths
 --
-checkStatement :: M.Map Ident Type -> Type -> Statement -> Subst (Bool, M.Map Ident Type, Statement)
+checkStatement :: M.Map Ident Type -> Type -> Statement -> UnifyT Check (Bool, M.Map Ident Type, Statement)
 checkStatement mass _ (VariableIntroduction name val) = do
   assignVariable name
   val'@(TypedValue _ _ t) <- infer val
@@ -710,7 +695,7 @@
   val'@(TypedValue _ _ t) <- infer val
   case M.lookup ident mass of
     Nothing -> throwError $ "No local variable with name " ++ show ident
-    Just ty -> do t ~~ ty
+    Just ty -> do t ?= ty
                   return (False, mass, Assignment ident val')
 checkStatement mass ret (While val inner) = do
   val' <- check val Boolean
@@ -720,7 +705,7 @@
   (allCodePathsReturn, ifst') <- checkIfStatement mass ret ifst
   return (allCodePathsReturn, mass, If ifst')
 checkStatement mass ret (For ident start end inner) = do
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   assignVariable ident
   start' <- check start Number
   end' <- check end Number
@@ -733,7 +718,7 @@
 -- |
 -- Check the type of an if-then-else statement
 --
-checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> Subst (Bool, IfStatement)
+checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> UnifyT Check (Bool, IfStatement)
 checkIfStatement mass ret (IfStatement val thens Nothing) = do
   val' <- check val Boolean
   (_, _, thens') <- checkBlock mass ret thens
@@ -747,7 +732,7 @@
 -- |
 -- Check the type of an else statement
 --
-checkElseStatement :: M.Map Ident Type -> Type -> ElseStatement -> Subst (Bool, ElseStatement)
+checkElseStatement :: M.Map Ident Type -> Type -> ElseStatement -> UnifyT Check (Bool, ElseStatement)
 checkElseStatement mass ret (Else elses) = do
   (allCodePathsReturn, _, elses') <- checkBlock mass ret elses
   return (allCodePathsReturn, Else elses')
@@ -756,10 +741,10 @@
 -- |
 -- Check the type of the return value of a block of statements
 --
-checkBlock :: M.Map Ident Type -> Type -> [Statement] -> Subst (Bool, M.Map Ident Type, [Statement])
+checkBlock :: M.Map Ident Type -> Type -> [Statement] -> UnifyT Check (Bool, M.Map Ident Type, [Statement])
 checkBlock mass _ [] = return (False, mass, [])
 checkBlock mass ret (s:ss) = do
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   (b1, mass1, s') <- checkStatement mass ret s
   bindLocalVariables moduleName (M.toList mass1) $ case (b1, ss) of
     (True, []) -> return (True, mass1, [s'])
@@ -771,15 +756,15 @@
 -- |
 -- Skolemize a type variable by replacing its instances with fresh skolem constants
 --
-skolemize :: String -> Type -> Subst Type
+skolemize :: String -> Type -> UnifyT Check Type
 skolemize ident ty = do
-  tsk <- Skolem <$> fresh'
+  tsk <- Skolem . runUnknown <$> fresh'
   return $ replaceTypeVars ident tsk ty
 
 -- |
 -- Check the type of a value, rethrowing errors to provide a better error message
 --
-check :: Value -> Type -> Subst Value
+check :: Value -> Type -> UnifyT Check Value
 check val ty = rethrow errorMessage $ check' val ty
   where
   errorMessage msg =
@@ -793,13 +778,13 @@
 -- |
 -- Check the type of a value
 --
-check' :: Value -> Type -> Subst Value
+check' :: Value -> Type -> UnifyT Check Value
 check' val (ForAll idents ty) = do
   sk <- skolemize idents ty
   check val sk
 check' val (ConstrainedType constraints ty) = do
   env <- getEnv
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   dictNames <- flip mapM constraints $ \(Qualified _ (ProperName className), _) -> do
     n <- liftCheck freshDictionaryName
     return $ Ident $ "__dict_" ++ className ++ "_" ++ show n
@@ -812,7 +797,7 @@
   val'@(TypedValue _ _ ty) <- infer val
   -- Don't unify an unknown with an inferred polytype
   ty' <- replaceAllVarsWithUnknowns ty
-  ty' ~~ u
+  ty' ?= u
   return val'
 check' v@(NumericLiteral _) Number = return v
 check' v@(StringLiteral _) String = return v
@@ -825,7 +810,7 @@
   vals' <- check vals (TypeApp Array ty)
   return $ Indexer index' vals'
 check' (Abs args ret) (Function argTys retTy) = do
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   guardWith "Incorrect number of function arguments" (length args == length argTys)
   ret' <- bindLocalVariables moduleName (zip args argTys) $ check ret retTy
   return $ Abs args ret'
@@ -834,13 +819,13 @@
   app <- checkFunctionApplication f' ft args ret
   return $ app
 check' (Var var) ty = do
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   ty1 <- lookupVariable moduleName var
   repl <- replaceAllTypeSynonyms ty1
   repl `subsumes` ty
   return $ Var var
 check' (TypedValue checkType val ty1) ty2 = do
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   kind <- liftCheck $ kindOf moduleName ty1
   guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
   ty1 `subsumes` ty2
@@ -879,7 +864,7 @@
   return $ Block ss'
 check' (Constructor c) ty = do
   env <- getEnv
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   case M.lookup (qualify moduleName c) (dataConstructors env) of
     Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
     Just (ty1, _) -> do
@@ -896,10 +881,10 @@
 --
 -- The @lax@ parameter controls whether or not every record member has to be provided. For object updates, this is not the case.
 --
-checkProperties :: [(String, Value)] -> Type -> Bool -> Subst [(String, Value)]
+checkProperties :: [(String, Value)] -> Type -> Bool -> UnifyT Check [(String, Value)]
 checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where
   go [] [] REmpty = return []
-  go [] [] u@(TUnknown _) = do u ~~ REmpty
+  go [] [] u@(TUnknown _) = do u ?= REmpty
                                return []
   go [] [] (Skolem _) | lax = return []
   go [] ((p, _): _) _ | lax = return []
@@ -908,7 +893,7 @@
   go ((p,v):ps') [] u@(TUnknown _) = do
     v'@(TypedValue _ _ ty) <- infer v
     rest <- fresh
-    u ~~ RCons p ty rest
+    u ?= RCons p ty rest
     ps'' <- go ps' [] rest
     return $ (p, v') : ps''
   go ((p,v):ps') ts r =
@@ -916,7 +901,7 @@
       Nothing -> do
         v'@(TypedValue _ _ ty) <- infer v
         rest <- fresh
-        r ~~ RCons p ty rest
+        r ?= RCons p ty rest
         ps'' <- go ps' ts rest
         return $ (p, v') : ps''
       Just ty -> do
@@ -928,7 +913,7 @@
 -- |
 -- Check the type of a function application, rethrowing errors to provide a better error message
 --
-checkFunctionApplication :: Value -> Type -> [Value] -> Type -> Subst Value
+checkFunctionApplication :: Value -> Type -> [Value] -> Type -> UnifyT Check Value
 checkFunctionApplication fn fnTy args ret = rethrow errorMessage $ checkFunctionApplication' fn fnTy args ret
   where
   errorMessage msg = "Error applying function of type "
@@ -939,7 +924,7 @@
 -- |
 -- Check the type of a function application
 --
-checkFunctionApplication' :: Value -> Type -> [Value] -> Type -> Subst Value
+checkFunctionApplication' :: Value -> Type -> [Value] -> Type -> UnifyT Check Value
 checkFunctionApplication' fn (Function argTys retTy) args ret = do
   guardWith "Incorrect number of function arguments" (length args == length argTys)
   args' <- zipWithM check args argTys
@@ -951,7 +936,7 @@
 checkFunctionApplication' fn u@(TUnknown _) args ret = do
   args' <- mapM (\arg -> infer arg >>= \(TypedValue _ v t) -> TypedValue True v <$> replaceAllVarsWithUnknowns t) args
   let tys = map (\(TypedValue _ _ t) -> t) args'
-  u ~~ Function tys ret
+  u ?= Function tys ret
   return $ App fn args'
 checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) args ret = do
   ty <- expandTypeSynonym name tyArgs
@@ -959,7 +944,7 @@
 checkFunctionApplication' fn (ConstrainedType constraints fnTy) args ret = do
   env <- getEnv
   dicts <- getTypeClassDictionaries
-  moduleName <- substCurrentModule <$> ask
+  Just moduleName <- checkCurrentModule <$> get
   checkFunctionApplication' (App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy args ret
 checkFunctionApplication' _ fnTy args ret = throwError $ "Applying a function of type "
   ++ prettyPrintType fnTy
@@ -969,7 +954,7 @@
 -- |
 -- Check whether one type subsumes another, rethrowing errors to provide a better error message
 --
-subsumes :: Type -> Type -> Subst ()
+subsumes :: Type -> Type -> UnifyT Check ()
 subsumes ty1 ty2 = rethrow errorMessage $ subsumes' ty1 ty2
   where
   errorMessage msg = "Error checking that type "
@@ -981,12 +966,12 @@
 -- |
 -- Check whether one type subsumes another
 --
-subsumes' :: Type -> Type -> Subst ()
+subsumes' :: Type -> Type -> UnifyT Check ()
 subsumes' (ForAll ident ty1) ty2 = do
   replaced <- replaceVarWithUnknown ident ty1
   replaced `subsumes` ty2
 subsumes' (Function args1 ret1) (Function args2 ret2) = do
   zipWithM_ subsumes args2 args1
   ret1 `subsumes` ret2
-subsumes' ty1 ty2 = ty1 ~~ ty2
+subsumes' ty1 ty2 = ty1 ?= ty2
 
diff --git a/src/Language/PureScript/Types.hs b/src/Language/PureScript/Types.hs
--- a/src/Language/PureScript/Types.hs
+++ b/src/Language/PureScript/Types.hs
@@ -20,8 +20,9 @@
 import Data.Data
 import Data.Generics (mkT, mkQ, everywhereBut)
 
+import Control.Monad.Unify
+
 import Language.PureScript.Names
-import Language.PureScript.Unknown (Unknown(..))
 
 -- |
 -- The type of types
@@ -30,7 +31,7 @@
   -- |
   -- A unification variable of type Type
   --
-  = TUnknown (Unknown Type)
+  = TUnknown (TypedUnknown Type)
   -- |
   -- Javascript numbers
   --
diff --git a/src/Language/PureScript/Unknown.hs b/src/Language/PureScript/Unknown.hs
deleted file mode 100644
--- a/src/Language/PureScript/Unknown.hs
+++ /dev/null
@@ -1,28 +0,0 @@
------------------------------------------------------------------------------
---
--- Module      :  Language.PureScript.Unknown
--- Copyright   :  (c) Phil Freeman 2013
--- License     :  MIT
---
--- Maintainer  :  Phil Freeman <paf31@cantab.net>
--- Stability   :  experimental
--- Portability :
---
--- |
--- Data type for unification variables
---
------------------------------------------------------------------------------
-
-{-# LANGUAGE DeriveDataTypeable #-}
-
-module Language.PureScript.Unknown where
-
-import Data.Data
-
--- |
--- The type of typed unification variables
---
-newtype Unknown t = Unknown { runUnknown :: Int } deriving (Show, Eq, Ord, Data, Typeable)
-
-
-