Add kind equalities to GHC.
[ghc.git] / compiler / types / Unify.hs
index 87681e0..0c2469a 100644 (file)
@@ -1,23 +1,23 @@
 -- (c) The University of Glasgow 2006
 
-{-# LANGUAGE CPP, DeriveFunctor #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveFunctor #-}
 
 module Unify (
-        -- Matching of types:
-        --      the "tc" prefix indicates that matching always
-        --      respects newtypes (rather than looking through them)
-        tcMatchTy, tcUnifyTyWithTFs, tcMatchTys, tcMatchTyX, tcMatchTysX,
-        ruleMatchTyX, tcMatchPreds,
-
-        MatchEnv(..), matchList,
+        tcMatchTy, tcMatchTys, tcMatchTyX, tcMatchTysX, tcUnifyTyWithTFs,
+        ruleMatchTyX,
 
         typesCantMatch,
 
         -- Side-effect free unification
-        tcUnifyTy, tcUnifyTys, BindFlag(..),
-
-        UnifyResultM(..), UnifyResult, tcUnifyTysFG
+        tcUnifyTy, tcUnifyTys,
+        tcUnifyTysFG,
+        BindFlag(..),
+        UnifyResult, UnifyResultM(..),
 
+        -- Matching a type against a lifted type (coercion)
+        liftCoMatch
    ) where
 
 #include "HsVersions.h"
@@ -26,27 +26,27 @@ import Var
 import VarEnv
 import VarSet
 import Kind
-import Type
+import Type hiding ( getTvSubstEnv )
+import Coercion hiding ( getCvSubstEnv )
 import TyCon
-import TypeRep
-import Util ( filterByList )
+import TyCoRep hiding ( getTvSubstEnv, getCvSubstEnv )
+import Util
+import Pair
 import Outputable
-import FastString (sLit)
 
-import Control.Monad (liftM, foldM, ap)
+import Control.Monad
+#if __GLASGOW_HASKELL__ > 710
+import qualified Control.Monad.Fail as MonadFail
+#endif
 #if __GLASGOW_HASKELL__ < 709
-import Control.Applicative (Applicative(..))
+import Data.Traversable ( traverse )
 #endif
+import Control.Applicative hiding ( empty )
+import qualified Control.Applicative
 
 {-
-************************************************************************
-*                                                                      *
-                Matching
-*                                                                      *
-************************************************************************
 
-
-Matching is much tricker than you might think.
+Unification is much tricker than you might think.
 
 1. The substitution we generate binds the *template type variables*
    which are given to us explicitly.
@@ -66,191 +66,93 @@ Matching is much tricker than you might think.
    where x is the template type variable.  Then we do not want to
    bind x to a/b!  This is a kind of occurs check.
    The necessary locals accumulate in the RnEnv2.
--}
 
-data MatchEnv
-  = ME  { me_tmpls :: VarSet    -- Template variables
-        , me_env   :: RnEnv2    -- Renaming envt for nested foralls
-        }                       --   In-scope set includes template variables
-    -- Nota Bene: MatchEnv isn't specific to Types.  It is used
-    --            for matching terms and coercions as well as types
-
-tcMatchTy :: TyVarSet           -- Template tyvars
-          -> Type               -- Template
-          -> Type               -- Target
-          -> Maybe TvSubst      -- One-shot; in principle the template
-                                -- variables could be free in the target
-tcMatchTy tmpls ty1 ty2
-  = tcMatchTyX tmpls init_subst ty1 ty2
-  where
-    init_subst = mkTvSubst in_scope emptyTvSubstEnv
-    in_scope   = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
-        -- We're assuming that all the interesting
-        -- tyvars in ty1 are in tmpls
+Note [Kind coercions in Unify]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We wish to match/unify while ignoring casts. But, we can't just ignore
+them completely, or we'll end up with ill-kinded substitutions. For example,
+say we're matching `a` with `ty |> co`. If we just drop the cast, we'll
+return [a |-> ty], but `a` and `ty` might have different kinds. We can't
+just match/unify their kinds, either, because this might gratuitously
+fail. After all, `co` is the witness that the kinds are the same -- they
+may look nothing alike.
+
+So, we pass a kind coercion to the match/unify worker. This coercion witnesses
+the equality between the substed kind of the left-hand type and the substed
+kind of the right-hand type. To get this coercion, we first have to match/unify
+the kinds before looking at the types. Happily, we need look only one level
+up, as all kinds are guaranteed to have kind *.
+
+We thought, at one point, that this was all unnecessary: why should casts
+be in types in the first place? But they do. In
+dependent/should_compile/KindEqualities2, we see, for example
+the constraint Num (Int |> (blah ; sym blah)).
+We naturally want to find a dictionary for that constraint, which
+requires dealing with coercions in this manner.
 
-tcMatchTys :: TyVarSet          -- Template tyvars
-           -> [Type]            -- Template
-           -> [Type]            -- Target
-           -> Maybe TvSubst     -- One-shot; in principle the template
-                                -- variables could be free in the target
+-}
+
+-- | @tcMatchTy tys t1 t2@ produces a substitution (over a subset of
+-- the variables @tys@) @s@ such that @s(t1)@ equals @t2@.
+-- The returned substitution might
+-- bind coercion variables, if the variable is an argument to a GADT
+-- constructor.
+tcMatchTy :: TyCoVarSet -> Type -> Type -> Maybe TCvSubst
+tcMatchTy tmpls ty1 ty2 = tcMatchTys tmpls [ty1] [ty2]
+
+-- | This is similar to 'tcMatchTy', but extends a substitution
+tcMatchTyX :: TyCoVarSet          -- ^ Template tyvars
+           -> TCvSubst            -- ^ Substitution to extend
+           -> Type                -- ^ Template
+           -> Type                -- ^ Target
+           -> Maybe TCvSubst
+tcMatchTyX tmpls subst ty1 ty2 = tcMatchTysX tmpls subst [ty1] [ty2]
+
+-- | Like 'tcMatchTy' but over a list of types.
+tcMatchTys :: TyCoVarSet     -- ^ Template tyvars
+           -> [Type]         -- ^ Template
+           -> [Type]         -- ^ Target
+           -> Maybe TCvSubst -- ^ One-shot; in principle the template
+                             -- variables could be free in the target
 tcMatchTys tmpls tys1 tys2
-  = tcMatchTysX tmpls init_subst tys1 tys2
-  where
-    init_subst = mkTvSubst in_scope emptyTvSubstEnv
-    in_scope   = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
-
-tcMatchTyX :: TyVarSet          -- Template tyvars
-           -> TvSubst           -- Substitution to extend
-           -> Type              -- Template
-           -> Type              -- Target
-           -> Maybe TvSubst
-tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
-  = case match menv subst_env ty1 ty2 of
-        Just subst_env' -> Just (TvSubst in_scope subst_env')
-        Nothing         -> Nothing
-  where
-    menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
-
-tcMatchTysX :: TyVarSet          -- Template tyvars
-            -> TvSubst           -- Substitution to extend
-            -> [Type]            -- Template
-            -> [Type]            -- Target
-            -> Maybe TvSubst     -- One-shot; in principle the template
-                                 -- variables could be free in the target
-tcMatchTysX tmpls (TvSubst in_scope subst_env) tys1 tys2
-  = case match_tys menv subst_env tys1 tys2 of
-        Just subst_env' -> Just (TvSubst in_scope subst_env')
-        Nothing         -> Nothing
-  where
-    menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
-
-tcMatchPreds
-        :: [TyVar]                      -- Bind these
-        -> [PredType] -> [PredType]
-        -> Maybe TvSubstEnv
-tcMatchPreds tmpls ps1 ps2
-  = matchList (match menv) emptyTvSubstEnv ps1 ps2
-  where
-    menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
-    in_scope_tyvars = mkInScopeSet (tyVarsOfTypes ps1 `unionVarSet` tyVarsOfTypes ps2)
-
--- This one is called from the expression matcher, which already has a MatchEnv in hand
-ruleMatchTyX :: MatchEnv
-         -> TvSubstEnv          -- Substitution to extend
-         -> Type                -- Template
-         -> Type                -- Target
-         -> Maybe TvSubstEnv
-
-ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2      -- Rename for export
-
--- Now the internals of matching
-
--- | Workhorse matching function.  Our goal is to find a substitution
--- on all of the template variables (specified by @me_tmpls menv@) such
--- that @ty1@ and @ty2@ unify.  This substitution is accumulated in @subst@.
--- If a variable is not a template variable, we don't attempt to find a
--- substitution for it; it must match exactly on both sides.  Furthermore,
--- only @ty1@ can have template variables.
---
--- This function handles binders, see 'RnEnv2' for more details on
--- how that works.
-match :: MatchEnv       -- For the most part this is pushed downwards
-      -> TvSubstEnv     -- Substitution so far:
-                        --   Domain is subset of template tyvars
-                        --   Free vars of range is subset of
-                        --      in-scope set of the RnEnv2
-      -> Type -> Type   -- Template and target respectively
-      -> Maybe TvSubstEnv
-
-match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
-                         | Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
-
-match menv subst (TyVarTy tv1) ty2
-  | Just ty1' <- lookupVarEnv subst tv1'        -- tv1' is already bound
-  = if eqTypeX (nukeRnEnvL rn_env) ty1' ty2
-        -- ty1 has no locally-bound variables, hence nukeRnEnvL
-    then Just subst
-    else Nothing        -- ty2 doesn't match
-
-  | tv1' `elemVarSet` me_tmpls menv
-  = if any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
-    then Nothing        -- Occurs check
-                        -- ezyang: Is this really an occurs check?  It seems
-                        -- to just reject matching \x. A against \x. x (maintaining
-                        -- the invariant that the free vars of the range of @subst@
-                        -- are a subset of the in-scope set in @me_env menv@.)
-    else do { subst1 <- match_kind menv subst (tyVarKind tv1) (typeKind ty2)
-                        -- Note [Matching kinds]
-            ; return (extendVarEnv subst1 tv1' ty2) }
-
-   | otherwise  -- tv1 is not a template tyvar
-   = case ty2 of
-        TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
-        _                                       -> Nothing
+  = tcMatchTysX tmpls (mkEmptyTCvSubst in_scope) tys1 tys2
   where
-    rn_env = me_env menv
-    tv1' = rnOccL rn_env tv1
-
-match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2)
-  = do { subst' <- match_kind menv subst (tyVarKind tv1) (tyVarKind tv2)
-       ; match menv' subst' ty1 ty2 }
-  where         -- Use the magic of rnBndr2 to go under the binders
-    menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
-
-match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2)
-  | tc1 == tc2 = match_tys menv subst tys1 tys2
-match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
-  = do { subst' <- match menv subst ty1a ty2a
-       ; match menv subst' ty1b ty2b }
-match menv subst (AppTy ty1a ty1b) ty2
-  | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
-        -- 'repSplit' used because the tcView stuff is done above
-  = do { subst' <- match menv subst ty1a ty2a
-       ; match menv subst' ty1b ty2b }
-
-match _ subst (LitTy x) (LitTy y) | x == y  = return subst
-
-match _ _ _ _
-  = Nothing
-
-
-
---------------
-match_kind :: MatchEnv -> TvSubstEnv -> Kind -> Kind -> Maybe TvSubstEnv
--- Match the kind of the template tyvar with the kind of Type
--- Note [Matching kinds]
-match_kind menv subst k1 k2
-  | k2 `isSubKind` k1
-  = return subst
-
-  | otherwise
-  = match menv subst k1 k2
-
--- Note [Matching kinds]
--- ~~~~~~~~~~~~~~~~~~~~~
--- For ordinary type variables, we don't want (m a) to match (n b)
--- if say (a::*) and (b::*->*).  This is just a yes/no issue.
---
--- For coercion kinds matters are more complicated.  If we have a
--- coercion template variable co::a~[b], where a,b are presumably also
--- template type variables, then we must match co's kind against the
--- kind of the actual argument, so as to give bindings to a,b.
---
--- In fact I have no example in mind that *requires* this kind-matching
--- to instantiate template type variables, but it seems like the right
--- thing to do.  C.f. Note [Matching variable types] in Rules.hs
-
---------------
-match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
-match_tys menv subst tys1 tys2 = matchList (match menv) subst tys1 tys2
-
---------------
-matchList :: (env -> a -> b -> Maybe env)
-           -> env -> [a] -> [b] -> Maybe env
-matchList _  subst []     []     = Just subst
-matchList fn subst (a:as) (b:bs) = do { subst' <- fn subst a b
-                                      ; matchList fn subst' as bs }
-matchList _  _     _      _      = Nothing
+    in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfTypes tys2)
+        -- We're assuming that all the interesting
+        -- tyvars in tys1 are in tmpls
+
+-- | Like 'tcMatchTys', but extending a substitution
+tcMatchTysX :: TyCoVarSet     -- ^ Template tyvars
+            -> TCvSubst       -- ^ Substitution to extend
+            -> [Type]         -- ^ Template
+            -> [Type]         -- ^ Target
+            -> Maybe TCvSubst -- ^ One-shot substitution
+tcMatchTysX tmpls (TCvSubst in_scope tv_env cv_env) tys1 tys2
+-- See Note [Kind coercions in Unify]
+  = case tc_unify_tys (matchBindFun tmpls) False False
+                      (mkRnEnv2 in_scope) tv_env cv_env tys1 tys2 of
+      Unifiable (tv_env', cv_env')
+        -> Just $ TCvSubst in_scope tv_env' cv_env'
+      _ -> Nothing
+
+-- | This one is called from the expression matcher,
+-- which already has a MatchEnv in hand
+ruleMatchTyX
+  :: TyCoVarSet          -- ^ template variables
+  -> RnEnv2
+  -> TvSubstEnv          -- ^ type substitution to extend
+  -> Type                -- ^ Template
+  -> Type                -- ^ Target
+  -> Maybe TvSubstEnv
+ruleMatchTyX tmpl_tvs rn_env tenv tmpl target
+-- See Note [Kind coercions in Unify]
+  = case tc_unify_tys (matchBindFun tmpl_tvs) False False rn_env
+                      tenv emptyCvSubstEnv [tmpl] [target] of
+      Unifiable (tenv', _) -> Just tenv'
+      _                    -> Nothing
+
+matchBindFun :: TyCoVarSet -> TyVar -> BindFlag
+matchBindFun tvs tv = if tv `elemVarSet` tvs then BindMe else Skolem
 
 {-
 ************************************************************************
@@ -293,7 +195,7 @@ suffices.
 -- apart, even after arbitrary type function evaluation and substitution?
 typesCantMatch :: [(Type,Type)] -> Bool
 -- See Note [Pruning dead case alternatives]
-typesCantMatch prs = any (\(s,t) -> cant_match s t) prs
+typesCantMatch prs = any (uncurry cant_match) prs
   where
     cant_match :: Type -> Type -> Bool
     cant_match t1 t2 = case tcUnifyTysFG (const BindMe) [t1] [t2] of
@@ -386,83 +288,51 @@ usages won't notice this design choice.
 -}
 
 tcUnifyTy :: Type -> Type       -- All tyvars are bindable
-          -> Maybe TvSubst      -- A regular one-shot (idempotent) substitution
+          -> Maybe TCvSubst
+                       -- A regular one-shot (idempotent) substitution
 -- Simple unification of two types; all type variables are bindable
-tcUnifyTy ty1 ty2
-  = case initUM (const BindMe) (unify ty1 ty2) of
-      Unifiable subst -> Just subst
-      _other          -> Nothing
+tcUnifyTy t1 t2 = tcUnifyTys (const BindMe) [t1] [t2]
 
 -- | Unify two types, treating type family applications as possibly unifying
 -- with anything and looking through injective type family applications.
-tcUnifyTyWithTFs :: Bool -> Type -> Type -> Maybe TvSubst
--- This algorithm is a direct implementation of the "Algorithm U" presented in
--- the paper "Injective type families for Haskell", Figures 2 and 3.  Equation
--- numbers in the comments refer to equations from the paper.
-tcUnifyTyWithTFs twoWay t1 t2 = niFixTvSubst `fmap` go t1 t2 emptyTvSubstEnv
-    where
-      go :: Type -> Type -> TvSubstEnv -> Maybe TvSubstEnv
-      -- look through type synonyms
-      go t1 t2 theta | Just t1' <- tcView t1 = go t1' t2  theta
-      go t1 t2 theta | Just t2' <- tcView t2 = go t1  t2' theta
-      -- proper unification
-      go (TyVarTy tv) t2 theta
-          -- Equation (1)
-          | Just t1' <- lookupVarEnv theta tv
-          = go t1' t2 theta
-          | otherwise = let t2' = Type.substTy (niFixTvSubst theta) t2
-                        in if tv `elemVarEnv` tyVarsOfType t2'
-                           -- Equation (2)
-                           then Just theta
-                           -- Equation (3)
-                           else Just $ extendVarEnv theta tv t2'
-      -- Equation (4)
-      go t1 t2@(TyVarTy _) theta | twoWay = go t2 t1 theta
-      -- Equation (5)
-      go (AppTy s1 s2) ty theta | Just(t1, t2) <- splitAppTy_maybe ty =
-          go s1 t1 theta >>= go s2 t2
-      go ty (AppTy s1 s2) theta | Just(t1, t2) <- splitAppTy_maybe ty =
-          go s1 t1 theta >>= go s2 t2
-
-      go (TyConApp tc1 tys1) (TyConApp tc2 tys2) theta
-        -- Equation (6)
-        | isAlgTyCon tc1 && isAlgTyCon tc2 && tc1 == tc2
-        = let tys = zip tys1 tys2
-          in foldM (\theta' (t1,t2) -> go t1 t2 theta') theta tys
-
-        -- Equation (7)
-        | isTypeFamilyTyCon tc1 && isTypeFamilyTyCon tc2 && tc1 == tc2
-        , Injective inj <- familyTyConInjectivityInfo tc1
-        = let tys1' = filterByList inj tys1
-              tys2' = filterByList inj tys2
-              injTys = zip tys1' tys2'
-          in foldM (\theta' (t1,t2) -> go t1 t2 theta') theta injTys
-
-        -- Equations (8)
-        | isTypeFamilyTyCon tc1
-        = Just theta
-
-        -- Equations (9)
-        | isTypeFamilyTyCon tc2, twoWay
-        = Just theta
-
-      -- Equation (10)
-      go _ _ _ = Nothing
+tcUnifyTyWithTFs :: Bool  -- ^ True <=> do two-way unification;
+                          --   False <=> do one-way matching.
+                          --   See end of sec 5.2 from the paper
+                 -> Type -> Type -> Maybe TCvSubst
+-- This algorithm is an implementation of the "Algorithm U" presented in
+-- the paper "Injective type families for Haskell", Figures 2 and 3.
+-- The code is incorporated with the standard unifier for convenience, but
+-- its operation should match the specification in the paper.
+tcUnifyTyWithTFs twoWay t1 t2
+  = case tc_unify_tys (const BindMe) twoWay True
+                       rn_env emptyTvSubstEnv emptyCvSubstEnv
+                       [t1] [t2] of
+      Unifiable  (subst, _) -> Just $ niFixTCvSubst subst
+      MaybeApart (subst, _) -> Just $ niFixTCvSubst subst
+      -- we want to *succeed* in questionable cases. This is a
+      -- pre-unification algorithm.
+      SurelyApart      -> Nothing
+  where
+    rn_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [t1, t2]
 
 -----------------
-tcUnifyTys :: (TyVar -> BindFlag)
+tcUnifyTys :: (TyCoVar -> BindFlag)
            -> [Type] -> [Type]
-           -> Maybe TvSubst     -- A regular one-shot (idempotent) substitution
+           -> Maybe TCvSubst
+                                -- ^ A regular one-shot (idempotent) substitution
+                                -- that unifies the erased types. See comments
+                                -- for 'tcUnifyTysFG'
+
 -- The two types may have common type variables, and indeed do so in the
 -- second call to tcUnifyTys in FunDeps.checkClsFD
 tcUnifyTys bind_fn tys1 tys2
   = case tcUnifyTysFG bind_fn tys1 tys2 of
-      Unifiable subst -> Just subst
-      _               -> Nothing
+      Unifiable result -> Just result
+      _                -> Nothing
 
 -- This type does double-duty. It is used in the UM (unifier monad) and to
 -- return the final result. See Note [Fine-grained unification]
-type UnifyResult = UnifyResultM TvSubst
+type UnifyResult = UnifyResultM TCvSubst
 data UnifyResultM a = Unifiable a        -- the subst that unifies the types
                     | MaybeApart a       -- the subst has as much as we know
                                          -- it must be part of an most general unifier
@@ -470,17 +340,71 @@ data UnifyResultM a = Unifiable a        -- the subst that unifies the types
                     | SurelyApart
                     deriving Functor
 
--- See Note [Fine-grained unification]
+instance Applicative UnifyResultM where
+  pure  = Unifiable
+  (<*>) = ap
+
+instance Monad UnifyResultM where
+  return = pure
+
+  SurelyApart  >>= _ = SurelyApart
+  MaybeApart x >>= f = case f x of
+                         Unifiable y -> MaybeApart y
+                         other       -> other
+  Unifiable x  >>= f = f x
+
+instance Alternative UnifyResultM where
+  empty = SurelyApart
+
+  a@(Unifiable {})  <|> _                 = a
+  _                 <|> b@(Unifiable {})  = b
+  a@(MaybeApart {}) <|> _                 = a
+  _                 <|> b@(MaybeApart {}) = b
+  SurelyApart       <|> SurelyApart       = SurelyApart
+
+instance MonadPlus UnifyResultM where
+  mzero = Control.Applicative.empty
+  mplus = (<|>)
+
+-- | @tcUnifyTysFG bind_tv tys1 tys2@ attepts to find a substitution @s@ (whose
+-- domain elements all respond 'BindMe' to @bind_tv@) such that
+-- @s(tys1)@ and that of @s(tys2)@ are equal, as witnessed by the returned
+-- Coercions.
 tcUnifyTysFG :: (TyVar -> BindFlag)
              -> [Type] -> [Type]
              -> UnifyResult
 tcUnifyTysFG bind_fn tys1 tys2
-  = initUM bind_fn (unify_tys tys1 tys2)
+  = do { (env, _) <- tc_unify_tys bind_fn True False env
+                                  emptyTvSubstEnv emptyCvSubstEnv
+                                  tys1 tys2
+       ; return $ niFixTCvSubst env }
+  where
+    vars = tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2
+    env  = mkRnEnv2 $ mkInScopeSet vars
+
+-- | This function is actually the one to call the unifier -- a little
+-- too general for outside clients, though.
+tc_unify_tys :: (TyVar -> BindFlag)
+             -> Bool        -- ^ True <=> unify; False <=> match
+             -> Bool        -- ^ True <=> doing an injectivity check
+             -> RnEnv2
+             -> TvSubstEnv  -- ^ substitution to extend
+             -> CvSubstEnv
+             -> [Type] -> [Type]
+             -> UnifyResultM (TvSubstEnv, CvSubstEnv)
+tc_unify_tys bind_fn unif inj_check rn_env tv_env cv_env tys1 tys2
+  = initUM bind_fn unif inj_check rn_env tv_env cv_env $
+    do { unify_tys kis1 kis2
+       ; unify_tys tys1 tys2
+       ; (,) <$> getTvSubstEnv <*> getCvSubstEnv }
+  where
+    kis1 = map typeKind tys1
+    kis2 = map typeKind tys2
 
 instance Outputable a => Outputable (UnifyResultM a) where
-  ppr SurelyApart    = ptext (sLit "SurelyApart")
-  ppr (Unifiable x)  = ptext (sLit "Unifiable") <+> ppr x
-  ppr (MaybeApart x) = ptext (sLit "MaybeApart") <+> ppr x
+  ppr SurelyApart    = text "SurelyApart"
+  ppr (Unifiable x)  = text "Unifiable" <+> ppr x
+  ppr (MaybeApart x) = text "MaybeApart" <+> ppr x
 
 {-
 ************************************************************************
@@ -491,7 +415,7 @@ instance Outputable a => Outputable (UnifyResultM a) where
 
 Note [Non-idempotent substitution]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-During unification we use a TvSubstEnv that is
+During unification we use a TvSubstEnv/CvSubstEnv pair that is
   (a) non-idempotent
   (b) loop-free; ie repeatedly applying it yields a fixed point
 
@@ -517,41 +441,48 @@ This is the reason for extending env with [f:k -> f:*], in the
 definition of env' in niFixTvSubst
 -}
 
-niFixTvSubst :: TvSubstEnv -> TvSubst
+niFixTCvSubst :: TvSubstEnv -> TCvSubst
 -- Find the idempotent fixed point of the non-idempotent substitution
 -- See Note [Finding the substitution fixpoint]
 -- ToDo: use laziness instead of iteration?
-niFixTvSubst env = f env
+niFixTCvSubst tenv = f tenv
   where
-    f env | not_fixpoint = f (mapVarEnv (substTy subst') env)
-          | otherwise    = subst
+    f tenv
+        | not_fixpoint = f (mapVarEnv (substTy subst') tenv)
+        | otherwise    = subst
         where
-          not_fixpoint  = foldVarSet ((||) . in_domain) False all_range_tvs
-          in_domain tv  = tv `elemVarEnv` env
+          not_fixpoint  = foldVarSet ((||) . in_domain) False range_tvs
+          in_domain tv  = tv `elemVarEnv` tenv
 
-          range_tvs     = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet env
-          all_range_tvs = closeOverKinds range_tvs
-          subst         = mkTvSubst (mkInScopeSet all_range_tvs) env
+          range_tvs     = foldVarEnv (unionVarSet . tyCoVarsOfType) emptyVarSet tenv
+          subst         = mkTCvSubst (mkInScopeSet range_tvs)
+                                     (tenv, emptyCvSubstEnv)
 
              -- env' extends env by replacing any free type with
              -- that same tyvar with a substituted kind
              -- See note [Finding the substitution fixpoint]
-          env'          = extendVarEnvList env [ (rtv, mkTyVarTy $ setTyVarKind rtv $
-                                                       substTy subst $ tyVarKind rtv)
-                                               | rtv <- varSetElems range_tvs
-                                               , not (in_domain rtv) ]
-          subst'        = mkTvSubst (mkInScopeSet all_range_tvs) env'
-
-niSubstTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
+          tenv'         = extendVarEnvList tenv [ (rtv, mkTyVarTy $
+                                                        setTyVarKind rtv $
+                                                        substTy subst $
+                                                        tyVarKind rtv)
+                                                | rtv <- varSetElems range_tvs
+                                                , not (in_domain rtv) ]
+          subst'        = mkTCvSubst (mkInScopeSet range_tvs)
+                                     (tenv', emptyCvSubstEnv)
+
+niSubstTvSet :: TvSubstEnv -> TyCoVarSet -> TyCoVarSet
 -- Apply the non-idempotent substitution to a set of type variables,
 -- remembering that the substitution isn't necessarily idempotent
 -- This is used in the occurs check, before extending the substitution
-niSubstTvSet subst tvs
+niSubstTvSet tsubst tvs
   = foldVarSet (unionVarSet . get) emptyVarSet tvs
   where
-    get tv = case lookupVarEnv subst tv of
-               Nothing -> unitVarSet tv
-               Just ty -> niSubstTvSet subst (tyVarsOfType ty)
+    get tv
+      | Just ty <- lookupVarEnv tsubst tv
+      = niSubstTvSet tsubst (tyCoVarsOfType ty)
+
+      | otherwise
+      = unitVarSet tv
 
 {-
 ************************************************************************
@@ -559,25 +490,184 @@ niSubstTvSet subst tvs
                 The workhorse
 *                                                                      *
 ************************************************************************
+
+Note [Specification of unification]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The algorithm implemented here is rather delicate, and we depend on it
+to uphold certain properties. This is a summary of these required
+properties. Any reference to "flattening" refers to the flattening
+algorithm in FamInstEnv (See Note [Flattening] in FamInstEnv), not
+the flattening algorithm in the solver.
+
+Notation:
+ θ,φ    substitutions
+ ξ    type-function-free types
+ τ,σ  other types
+ τ♭   type τ, flattened
+
+ ≡    eqType
+
+(U1) Soundness.
+If (unify τ₁ τ₂) = Unifiable θ, then θ(τ₁) ≡ θ(τ₂). θ is a most general
+unifier for τ₁ and τ₂.
+
+(U2) Completeness.
+If (unify ξ₁ ξ₂) = SurelyApart,
+then there exists no substitution θ such that θ(ξ₁) ≡ θ(ξ₂).
+
+These two properties are stated as Property 11 in the "Closed Type Families"
+paper (POPL'14). Below, this paper is called [CTF].
+
+(U3) Apartness under substitution.
+If (unify ξ τ♭) = SurelyApart, then (unify ξ θ(τ)♭) = SurelyApart, for
+any θ. (Property 12 from [CTF])
+
+(U4) Apart types do not unify.
+If (unify ξ τ♭) = SurelyApart, then there exists no θ such that
+θ(ξ) = θ(τ). (Property 13 from [CTF])
+
+THEOREM. Completeness w.r.t ~
+If (unify τ₁♭ τ₂♭) = SurelyApart, then there exists no proof that (τ₁ ~ τ₂).
+
+PROOF. See appendix of [CTF].
+
+
+The unification algorithm is used for type family injectivity, as described
+in the "Injective Type Families" paper (Haskell'15), called [ITF]. When run
+in this mode, it has the following properties.
+
+(I1) If (unify σ τ) = SurelyApart, then σ and τ are not unifiable, even
+after arbitrary type family reductions. Note that σ and τ are not flattened
+here.
+
+(I2) If (unify σ τ) = MaybeApart θ, and if some
+φ exists such that φ(σ) ~ φ(τ), then φ extends θ.
+
+
+Furthermore, the RULES matching algorithm requires this property,
+but only when using this algorithm for matching:
+
+(M1) If (match σ τ) succeeds with θ, then all matchable tyvars in σ
+are bound in θ.
+
+Property M1 means that we must extend the substitution with, say
+(a ↦ a) when appropriate during matching.
+See also Note [Self-substitution when matching].
+
+(M2) Completeness of matching.
+If θ(σ) = τ, then (match σ τ) = Unifiable φ, where θ is an extension of φ.
+
+Sadly, property M2 and I2 conflict. Consider
+
+type family F1 a b where
+  F1 Int    Bool   = Char
+  F1 Double String = Char
+
+Consider now two matching problems:
+
+P1. match (F1 a Bool) (F1 Int Bool)
+P2. match (F1 a Bool) (F1 Double String)
+
+In case P1, we must find (a ↦ Int) to satisfy M2.
+In case P2, we must /not/ find (a ↦ Double), in order to satisfy I2. (Note
+that the correct mapping for I2 is (a ↦ Int). There is no way to discover
+this, but we musn't map a to anything else!)
+
+We thus must parameterize the algorithm over whether it's being used
+for an injectivity check (refrain from looking at non-injective arguments
+to type families) or not (do indeed look at those arguments).
+
+(It's all a question of whether or not to include equation (7) from Fig. 2
+of [ITF].)
+
+This extra parameter is a bit fiddly, perhaps, but seemingly less so than
+having two separate, almost-identical algorithms.
+
+Note [Self-substitution when matching]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+What should happen when we're *matching* (not unifying) a1 with a1? We
+should get a substitution [a1 |-> a1]. A successful match should map all
+the template variables (except ones that disappear when expanding synonyms).
+But when unifying, we don't want to do this, because we'll then fall into
+a loop.
+
+This arrangement affects the code in three places:
+ - If we're matching a refined template variable, don't recur. Instead, just
+   check for equality. That is, if we know [a |-> Maybe a] and are matching
+   (a ~? Maybe Int), we want to just fail.
+
+ - Skip the occurs check when matching. This comes up in two places, because
+   matching against variables is handled separately from matching against
+   full-on types.
+
+Note that this arrangement was provoked by a real failure, where the same
+unique ended up in the template as in the target. (It was a rule firing when
+compiling Data.List.NonEmpty.)
+
+Note [Matching coercion variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this:
+
+   type family F a
+
+   data G a where
+     MkG :: F a ~ Bool => G a
+
+   type family Foo (x :: G a) :: F a
+   type instance Foo MkG = False
+
+We would like that to be accepted. For that to work, we need to introduce
+a coercion variable on the left an then use it on the right. Accordingly,
+at use sites of Foo, we need to be able to use matching to figure out the
+value for the coercion. (See the desugared version:
+
+   axFoo :: [a :: *, c :: F a ~ Bool]. Foo (MkG c) = False |> (sym c)
+
+) We never want this action to happen during *unification* though, when
+all bets are off.
+
 -}
 
-unify :: Type -> Type -> UM ()
+-- See Note [Specification of unification]
+unify_ty :: Type -> Type -> Coercion   -- Types to be unified and a co
+                                       -- between their kinds
+                                       -- See Note [Kind coercions in Unify]
+         -> UM ()
 -- Respects newtypes, PredTypes
 
--- in unify, any NewTcApps/Preds should be taken at face value
-unify (TyVarTy tv1) ty2  = uVar tv1 ty2
-unify ty1 (TyVarTy tv2)  = uVar tv2 ty1
+unify_ty ty1 ty2 kco
+  | Just ty1' <- coreView ty1 = unify_ty ty1' ty2 kco
+  | Just ty2' <- coreView ty2 = unify_ty ty1 ty2' kco
+  | CastTy ty1' co <- ty1     = unify_ty ty1' ty2 (co `mkTransCo` kco)
+  | CastTy ty2' co <- ty2     = unify_ty ty1 ty2' (kco `mkTransCo` mkSymCo co)
 
-unify ty1 ty2 | Just ty1' <- tcView ty1 = unify ty1' ty2
-unify ty1 ty2 | Just ty2' <- tcView ty2 = unify ty1 ty2'
+unify_ty (TyVarTy tv1) ty2 kco = uVar tv1 ty2 kco
+unify_ty ty1 (TyVarTy tv2) kco
+  = do { unif <- amIUnifying
+       ; if unif
+         then umSwapRn $ uVar tv2 ty1 (mkSymCo kco)
+         else surelyApart }  -- non-tv on left; tv on right: can't match.
 
-unify ty1 ty2
+unify_ty ty1 ty2 _kco
   | Just (tc1, tys1) <- splitTyConApp_maybe ty1
   , Just (tc2, tys2) <- splitTyConApp_maybe ty2
-  = if tc1 == tc2
+  = if tc1 == tc2 || (isStarKind ty1 && isStarKind ty2)
     then if isInjectiveTyCon tc1 Nominal
          then unify_tys tys1 tys2
-         else don'tBeSoSure $ unify_tys tys1 tys2
+         else do { let inj | isTypeFamilyTyCon tc1
+                           = case familyTyConInjectivityInfo tc1 of
+                               NotInjective -> repeat False
+                               Injective bs -> bs
+                           | otherwise
+                           = repeat False
+
+                       (inj_tys1, noninj_tys1) = partitionByList inj tys1
+                       (inj_tys2, noninj_tys2) = partitionByList inj tys2
+
+                 ; unify_tys inj_tys1 inj_tys2
+                 ; inj_tf <- checkingInjectivity
+                 ; unless inj_tf $ -- See (end of) Note [Specification of unification]
+                   don'tBeSoSure $ unify_tys noninj_tys1 noninj_tys2 }
     else -- tc1 /= tc2
          if isGenerativeTyCon tc1 Nominal && isGenerativeTyCon tc2 Nominal
          then surelyApart
@@ -585,109 +675,168 @@ unify ty1 ty2
 
         -- Applications need a bit of care!
         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
-        -- NB: we've already dealt with type variables and Notes,
+        -- NB: we've already dealt with type variables,
         -- so if one type is an App the other one jolly well better be too
-unify (AppTy ty1a ty1b) ty2
-  | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
-  = do  { unify ty1a ty2a
-        ; unify ty1b ty2b }
-
-unify ty1 (AppTy ty2a ty2b)
-  | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
-  = do  { unify ty1a ty2a
-        ; unify ty1b ty2b }
-
-unify (LitTy x) (LitTy y) | x == y = return ()
-
-unify _ _ = surelyApart
-        -- ForAlls??
+unify_ty (AppTy ty1a ty1b) ty2 _kco
+  | Just (ty2a, ty2b) <- tcRepSplitAppTy_maybe ty2
+  = unify_ty_app ty1a ty1b ty2a ty2b
+
+unify_ty ty1 (AppTy ty2a ty2b) _kco
+  | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
+  = unify_ty_app ty1a ty1b ty2a ty2b
+
+unify_ty (LitTy x) (LitTy y) _kco | x == y = return ()
+
+unify_ty (ForAllTy (Named tv1 _) ty1) (ForAllTy (Named tv2 _) ty2) kco
+  = do { unify_ty (tyVarKind tv1) (tyVarKind tv2) (mkNomReflCo liftedTypeKind)
+       ; umRnBndr2 tv1 tv2 $ unify_ty ty1 ty2 kco }
+
+-- See Note [Matching coercion variables]
+unify_ty (CoercionTy co1) (CoercionTy co2) kco
+  = do { unif <- amIUnifying
+       ; c_subst <- getCvSubstEnv
+       ; case co1 of
+           CoVarCo cv
+             |  not unif
+             ,  not (cv `elemVarEnv` c_subst)
+             -> do { b <- tvBindFlagL cv
+                   ; if b == BindMe
+                       then do { checkRnEnvRCo co2
+                               ; let [_, _, co_l, co_r] = decomposeCo 4 kco
+                                  -- cv :: t1 ~ t2
+                                  -- co2 :: s1 ~ s2
+                                  -- co_l :: t1 ~ s1
+                                  -- co_r :: t2 ~ s2
+                               ; extendCvEnv cv (co_l `mkTransCo`
+                                                 co2 `mkTransCo`
+                                                 mkSymCo co_r) }
+                       else return () }
+           _ -> return () }
+
+unify_ty ty1 _ _
+  | Just (tc1, _) <- splitTyConApp_maybe ty1
+  , not (isGenerativeTyCon tc1 Nominal)
+  = maybeApart
+
+unify_ty _ ty2 _
+  | Just (tc2, _) <- splitTyConApp_maybe ty2
+  , not (isGenerativeTyCon tc2 Nominal)
+  = do { unif <- amIUnifying
+       ; if unif then maybeApart else surelyApart }
+
+unify_ty _ _ _ = surelyApart
+
+unify_ty_app :: Type -> Type -> Type -> Type -> UM ()
+unify_ty_app ty1a ty1b ty2a ty2b
+  = do { -- TODO (RAE): Remove this exponential behavior.
+         let ki1a = typeKind ty1a
+             ki2a = typeKind ty2a
+       ; unify_ty ki1a ki2a (mkNomReflCo liftedTypeKind)
+       ; let kind_co = mkNomReflCo ki1a
+       ; unify_ty ty1a ty2a kind_co
+       ; unify_ty ty1b ty2b (mkNthCo 0 kind_co) }
 
-------------------------------
 unify_tys :: [Type] -> [Type] -> UM ()
 unify_tys orig_xs orig_ys
   = go orig_xs orig_ys
   where
     go []     []     = return ()
-    go (x:xs) (y:ys) = do { unify x y
-                          ; go xs ys }
+    go (x:xs) (y:ys)
+      = do { unify_ty x y (mkNomReflCo $ typeKind x)
+           ; go xs ys }
     go _ _ = maybeApart  -- See Note [Lists of different lengths are MaybeApart]
 
 ---------------------------------
-uVar :: TyVar           -- Type variable to be unified
-     -> Type            -- with this type
+uVar :: TyVar           -- Variable to be unified
+     -> Type            -- with this Type
+     -> Coercion        -- :: kind tv ~N kind ty
      -> UM ()
 
-uVar tv1 ty
- = do { subst <- umGetTvSubstEnv
-         -- Check to see whether tv1 is refined by the substitution
+uVar tv1 ty kco
+ = do { -- Check to see whether tv1 is refined by the substitution
+        subst <- getTvSubstEnv
       ; case (lookupVarEnv subst tv1) of
-          Just ty' -> unify ty' ty     -- Yes, call back into unify'
-          Nothing  -> uUnrefined subst tv1 ty ty }  -- No, continue
-
-uUnrefined :: TvSubstEnv          -- environment to extend (from the UM monad)
-           -> TyVar               -- Type variable to be unified
-           -> Type                -- with this type
-           -> Type                -- (version w/ expanded synonyms)
+          Just ty' -> do { unif <- amIUnifying
+                         ; if unif
+                           then unify_ty ty' ty kco   -- Yes, call back into unify
+                           else -- when *matching*, we don't want to just recur here.
+                                -- this is because the range of the subst is the target
+                                -- type, not the template type. So, just check for
+                                -- normal type equality.
+                                guard (ty' `eqType` ty) }
+          Nothing  -> uUnrefined tv1 ty ty kco } -- No, continue
+
+uUnrefined :: TyVar             -- variable to be unified
+           -> Type              -- with this Type
+           -> Type              -- (version w/ expanded synonyms)
+           -> Coercion          -- :: kind tv ~N kind ty
            -> UM ()
 
 -- We know that tv1 isn't refined
 
-uUnrefined subst tv1 ty2 ty2'
-  | Just ty2'' <- tcView ty2'
-  = uUnrefined subst tv1 ty2 ty2''      -- Unwrap synonyms
+uUnrefined tv1 ty2 ty2' kco
+  | Just ty2'' <- coreView ty2'
+  = uUnrefined tv1 ty2 ty2'' kco    -- Unwrap synonyms
                 -- This is essential, in case we have
                 --      type Foo a = a
                 -- and then unify a ~ Foo a
 
-uUnrefined subst tv1 ty2 (TyVarTy tv2)
-  | tv1 == tv2          -- Same type variable
-  = return ()
-
-    -- Check to see whether tv2 is refined
-  | Just ty' <- lookupVarEnv subst tv2
-  = uUnrefined subst tv1 ty' ty'
-
-  | otherwise
-
-  = do {   -- So both are unrefined; unify the kinds
-       ; unify (tyVarKind tv1) (tyVarKind tv2)
+  | TyVarTy tv2 <- ty2'
+  = do { tv1' <- umRnOccL tv1
+       ; tv2' <- umRnOccR tv2
+       ; unif <- amIUnifying
+           -- See Note [Self-substitution when matching]
+       ; when (tv1' /= tv2' || not unif) $ do
+       { subst <- getTvSubstEnv
+          -- Check to see whether tv2 is refined
+       ; case lookupVarEnv subst tv2 of
+         {  Just ty' | unif -> uUnrefined tv1 ty' ty' kco
+         ;  _               -> do
+       {   -- So both are unrefined
 
            -- And then bind one or the other,
            -- depending on which is bindable
-           -- NB: unlike TcUnify we do not have an elaborate sub-kinding
-           --     story.  That is relevant only during type inference, and
-           --     (I very much hope) is not relevant here.
-       ; b1 <- tvBindFlag tv1
-       ; b2 <- tvBindFlag tv2
-       ; let ty1 = TyVarTy tv1
+       ; b1 <- tvBindFlagL tv1
+       ; b2 <- tvBindFlagR tv2
+       ; let ty1 = mkTyVarTy tv1
        ; case (b1, b2) of
-           (Skolem, Skolem) -> maybeApart -- See Note [Unification with skolems]
-           (BindMe, _)      -> extendSubst tv1 ty2
-           (_, BindMe)      -> extendSubst tv2 ty1 }
-
-uUnrefined subst tv1 ty2 ty2'   -- ty2 is not a type variable
-  | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2')
-  = maybeApart                          -- Occurs check
-                                        -- See Note [Fine-grained unification]
-  | otherwise
-  = do { unify k1 k2
-       -- Note [Kinds Containing Only Literals]
-       ; bindTv tv1 ty2 }        -- Bind tyvar to the synonym if poss
-  where
-    k1 = tyVarKind tv1
-    k2 = typeKind ty2'
+           (BindMe, _)        -> do { checkRnEnvR ty2 -- make sure ty2 is not a local
+                                    ; extendTvEnv tv1 (ty2 `mkCastTy` mkSymCo kco) }
+           (_, BindMe) | unif -> do { checkRnEnvL ty1 -- ditto for ty1
+                                    ; extendTvEnv tv2 (ty1 `mkCastTy` kco) }
+
+           _ | tv1' == tv2' -> return ()
+             -- How could this happen? If we're only matching and if
+             -- we're comparing forall-bound variables.
+
+           _ -> maybeApart -- See Note [Unification with skolems]
+  }}}}
+
+uUnrefined tv1 ty2 ty2' kco -- ty2 is not a type variable
+  = do { occurs <- elemNiSubstSet tv1 (tyCoVarsOfType ty2')
+       ; unif   <- amIUnifying
+       ; if unif && occurs  -- See Note [Self-substitution when matching]
+         then maybeApart       -- Occurs check, see Note [Fine-grained unification]
+         else do bindTv tv1 (ty2 `mkCastTy` mkSymCo kco) }
+            -- Bind tyvar to the synonym if poss
+
+elemNiSubstSet :: TyVar -> TyCoVarSet -> UM Bool
+elemNiSubstSet v set
+  = do { tsubst <- getTvSubstEnv
+       ; return $ v `elemVarSet` niSubstTvSet tsubst set }
 
 bindTv :: TyVar -> Type -> UM ()
-bindTv tv ty      -- ty is not a type variable
-  = do  { b <- tvBindFlag tv
+bindTv tv ty    -- ty is not a variable
+  = do  { checkRnEnvR ty -- make sure ty mentions no local variables
+        ; b <- tvBindFlagL tv
         ; case b of
             Skolem -> maybeApart  -- See Note [Unification with skolems]
-            BindMe -> extendSubst tv ty
+            BindMe -> extendTvEnv tv ty
         }
 
 {-
-************************************************************************
-*                                                                      *
+%************************************************************************
+%*                                                                      *
                 Binding decisions
 *                                                                      *
 ************************************************************************
@@ -698,6 +847,7 @@ data BindFlag
 
   | Skolem      -- This type variable is a skolem constant
                 -- Don't bind it; it only matches itself
+  deriving Eq
 
 {-
 ************************************************************************
@@ -707,51 +857,336 @@ data BindFlag
 ************************************************************************
 -}
 
-newtype UM a = UM { unUM :: (TyVar -> BindFlag)
-                         -> TvSubstEnv
-                         -> UnifyResultM (a, TvSubstEnv) }
+data UMEnv = UMEnv { um_bind_fun :: TyVar -> BindFlag
+                       -- the user-supplied BindFlag function
+                   , um_unif     :: Bool   -- unification (True) or matching?
+                   , um_inj_tf   :: Bool   -- checking for injectivity?
+                             -- See (end of) Note [Specification of unification]
+                   , um_rn_env   :: RnEnv2 }
+
+data UMState = UMState
+                   { um_tv_env   :: TvSubstEnv
+                   , um_cv_env   :: CvSubstEnv }
+
+newtype UM a = UM { unUM :: UMEnv -> UMState
+                         -> UnifyResultM (UMState, a) }
 
 instance Functor UM where
       fmap = liftM
 
 instance Applicative UM where
-      pure a = UM (\_tvs subst  -> Unifiable (a, subst))
-      (<*>) = ap
+      pure a = UM (\_ s -> pure (s, a))
+      (<*>)  = ap
 
 instance Monad UM where
   return   = pure
-  fail _   = UM (\_tvs _subst -> SurelyApart) -- failed pattern match
-  m >>= k  = UM (\tvs  subst  -> case unUM m tvs subst of
-                           Unifiable (v, subst') -> unUM (k v) tvs subst'
-                           MaybeApart (v, subst') ->
-                             case unUM (k v) tvs subst' of
-                               Unifiable (v', subst'') -> MaybeApart (v', subst'')
-                               other                   -> other
-                           SurelyApart -> SurelyApart)
-
--- returns an idempotent substitution
-initUM :: (TyVar -> BindFlag) -> UM () -> UnifyResult
-initUM badtvs um = fmap (niFixTvSubst . snd) $ unUM um badtvs emptyTvSubstEnv
-
-tvBindFlag :: TyVar -> UM BindFlag
-tvBindFlag tv = UM (\tv_fn subst -> Unifiable (tv_fn tv, subst))
-
--- | Extend the TvSubstEnv in the UM monad
-extendSubst :: TyVar -> Type -> UM ()
-extendSubst tv ty = UM (\_tv_fn subst -> Unifiable ((), extendVarEnv subst tv ty))
-
--- | Retrive the TvSubstEnv from the UM monad
-umGetTvSubstEnv :: UM TvSubstEnv
-umGetTvSubstEnv = UM $ \_tv_fn subst -> Unifiable (subst, subst)
+  fail _   = UM (\_ _ -> SurelyApart) -- failed pattern match
+  m >>= k  = UM (\env state ->
+                  do { (state', v) <- unUM m env state
+                     ; unUM (k v) env state' })
+
+instance Alternative UM where
+  empty     = UM (\_ _ -> mzero)
+  m1 <|> m2 = UM (\env state ->
+                  unUM m1 env state <|>
+                  unUM m2 env state)
+
+  -- need this instance because of a use of 'guard' above
+instance MonadPlus UM where
+  mzero = Control.Applicative.empty
+  mplus = (<|>)
+
+#if __GLASGOW_HASKELL__ > 710
+instance MonadFail.MonadFail UM where
+    fail _   = UM (\_tvs _subst -> SurelyApart) -- failed pattern match
+#endif
+
+initUM :: (TyVar -> BindFlag)
+       -> Bool        -- True <=> unify; False <=> match
+       -> Bool        -- True <=> doing an injectivity check
+       -> RnEnv2
+       -> TvSubstEnv  -- subst to extend
+       -> CvSubstEnv
+       -> UM a -> UnifyResultM a
+initUM badtvs unif inj_tf rn_env subst_env cv_subst_env um
+  = case unUM um env state of
+      Unifiable (_, subst)  -> Unifiable subst
+      MaybeApart (_, subst) -> MaybeApart subst
+      SurelyApart           -> SurelyApart
+  where
+    env = UMEnv { um_bind_fun = badtvs
+                , um_unif     = unif
+                , um_inj_tf   = inj_tf
+                , um_rn_env   = rn_env }
+    state = UMState { um_tv_env = subst_env
+                    , um_cv_env = cv_subst_env }
+
+tvBindFlagL :: TyVar -> UM BindFlag
+tvBindFlagL tv = UM $ \env state ->
+  Unifiable (state, if inRnEnvL (um_rn_env env) tv
+                    then Skolem
+                    else um_bind_fun env tv)
+
+tvBindFlagR :: TyVar -> UM BindFlag
+tvBindFlagR tv = UM $ \env state ->
+  Unifiable (state, if inRnEnvR (um_rn_env env) tv
+                    then Skolem
+                    else um_bind_fun env tv)
+
+getTvSubstEnv :: UM TvSubstEnv
+getTvSubstEnv = UM $ \_ state -> Unifiable (state, um_tv_env state)
+
+getCvSubstEnv :: UM CvSubstEnv
+getCvSubstEnv = UM $ \_ state -> Unifiable (state, um_cv_env state)
+
+extendTvEnv :: TyVar -> Type -> UM ()
+extendTvEnv tv ty = UM $ \_ state ->
+  Unifiable (state { um_tv_env = extendVarEnv (um_tv_env state) tv ty }, ())
+
+extendCvEnv :: CoVar -> Coercion -> UM ()
+extendCvEnv cv co = UM $ \_ state ->
+  Unifiable (state { um_cv_env = extendVarEnv (um_cv_env state) cv co }, ())
+
+umRnBndr2 :: TyCoVar -> TyCoVar -> UM a -> UM a
+umRnBndr2 v1 v2 thing = UM $ \env state ->
+  let rn_env' = rnBndr2 (um_rn_env env) v1 v2 in
+  unUM thing (env { um_rn_env = rn_env' }) state
+
+checkRnEnv :: (RnEnv2 -> Var -> Bool) -> VarSet -> UM ()
+checkRnEnv inRnEnv varset = UM $ \env state ->
+  if any (inRnEnv (um_rn_env env)) (varSetElems varset)
+  then MaybeApart (state, ())
+  else Unifiable (state, ())
 
 -- | Converts any SurelyApart to a MaybeApart
 don'tBeSoSure :: UM () -> UM ()
-don'tBeSoSure um = UM $ \tv_fn subst -> case unUM um tv_fn subst of
-  SurelyApart -> MaybeApart ((), subst)
-  other       -> other
+don'tBeSoSure um = UM $ \env state ->
+  case unUM um env state of
+    SurelyApart -> MaybeApart (state, ())
+    other       -> other
+
+checkRnEnvR :: Type -> UM ()
+checkRnEnvR ty = checkRnEnv inRnEnvR (tyCoVarsOfType ty)
+
+checkRnEnvL :: Type -> UM ()
+checkRnEnvL ty = checkRnEnv inRnEnvL (tyCoVarsOfType ty)
+
+checkRnEnvRCo :: Coercion -> UM ()
+checkRnEnvRCo co = checkRnEnv inRnEnvR (tyCoVarsOfCo co)
+
+umRnOccL :: TyVar -> UM TyVar
+umRnOccL v = UM $ \env state ->
+  Unifiable (state, rnOccL (um_rn_env env) v)
+
+umRnOccR :: TyVar -> UM TyVar
+umRnOccR v = UM $ \env state ->
+  Unifiable (state, rnOccR (um_rn_env env) v)
+
+umSwapRn :: UM a -> UM a
+umSwapRn thing = UM $ \env state ->
+  let rn_env' = rnSwap (um_rn_env env) in
+  unUM thing (env { um_rn_env = rn_env' }) state
+
+amIUnifying :: UM Bool
+amIUnifying = UM $ \env state -> Unifiable (state, um_unif env)
+
+checkingInjectivity :: UM Bool
+checkingInjectivity = UM $ \env state -> Unifiable (state, um_inj_tf env)
 
 maybeApart :: UM ()
-maybeApart = UM (\_tv_fn subst -> MaybeApart ((), subst))
+maybeApart = UM (\_ state -> MaybeApart (state, ()))
 
 surelyApart :: UM a
-surelyApart = UM (\_tv_fn _subst -> SurelyApart)
+surelyApart = UM (\_ _ -> SurelyApart)
+
+{-
+%************************************************************************
+%*                                                                      *
+            Matching a (lifted) type against a coercion
+%*                                                                      *
+%************************************************************************
+
+This section defines essentially an inverse to liftCoSubst. It is defined
+here to avoid a dependency from Coercion on this module.
+
+-}
+
+data MatchEnv = ME { me_tmpls :: TyVarSet
+                   , me_env   :: RnEnv2 }
+
+-- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'.  In particular, if
+--   @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@,
+--   where @==@ there means that the result of tyCoSubst has the same
+--   type as the original co; but may be different under the hood.
+--   That is, it matches a type against a coercion of the same
+--   "shape", and returns a lifting substitution which could have been
+--   used to produce the given coercion from the given type.
+--   Note that this function is incomplete -- it might return Nothing
+--   when there does indeed exist a possible lifting context.
+--
+-- This function is incomplete in that it doesn't respect the equality
+-- in `eqType`. That is, it's possible that this will succeed for t1 and
+-- fail for t2, even when t1 `eqType` t2. That's because it depends on
+-- there being a very similar structure between the type and the coercion.
+-- This incompleteness shouldn't be all that surprising, especially because
+-- it depends on the structure of the coercion, which is a silly thing to do.
+--
+-- The lifting context produced doesn't have to be exacting in the roles
+-- of the mappings. This is because any use of the lifting context will
+-- also require a desired role. Thus, this algorithm prefers mapping to
+-- nominal coercions where it can do so.
+liftCoMatch :: TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
+liftCoMatch tmpls ty co
+  = do { cenv1 <- ty_co_match menv emptyVarEnv ki ki_co ki_ki_co ki_ki_co
+       ; cenv2 <- ty_co_match menv cenv1       ty co
+                              (mkNomReflCo co_lkind) (mkNomReflCo co_rkind)
+       ; return (LC (mkEmptyTCvSubst in_scope) cenv2) }
+  where
+    menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
+    in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
+    -- Like tcMatchTy, assume all the interesting variables
+    -- in ty are in tmpls
+
+    ki       = typeKind ty
+    ki_co    = promoteCoercion co
+    ki_ki_co = mkNomReflCo liftedTypeKind
+
+    Pair co_lkind co_rkind = coercionKind ki_co
+
+-- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
+ty_co_match :: MatchEnv   -- ^ ambient helpful info
+            -> LiftCoEnv  -- ^ incoming subst
+            -> Type       -- ^ ty, type to match
+            -> Coercion   -- ^ co, coercion to match against
+            -> Coercion   -- ^ :: kind of L type of substed ty ~N L kind of co
+            -> Coercion   -- ^ :: kind of R type of substed ty ~N R kind of co
+            -> Maybe LiftCoEnv
+ty_co_match menv subst ty co lkco rkco
+  | Just ty' <- coreViewOneStarKind ty = ty_co_match menv subst ty' co lkco rkco
+
+  -- handle Refl case:
+  | tyCoVarsOfType ty `isNotInDomainOf` subst
+  , Just (ty', _) <- isReflCo_maybe co
+  , ty `eqType` ty'
+  = Just subst
+
+  where
+    isNotInDomainOf :: VarSet -> VarEnv a -> Bool
+    isNotInDomainOf set env
+      = noneSet (\v -> elemVarEnv v env) set
+
+    noneSet :: (Var -> Bool) -> VarSet -> Bool
+    noneSet f = foldVarSet (\v rest -> rest && (not $ f v)) True
+
+ty_co_match menv subst ty co lkco rkco
+  | CastTy ty' co' <- ty
+  = ty_co_match menv subst ty' co (co' `mkTransCo` lkco) (co' `mkTransCo` rkco)
+
+  | CoherenceCo co1 co2 <- co
+  = ty_co_match menv subst ty co1 (lkco `mkTransCo` mkSymCo co2) rkco
+
+  | SymCo co' <- co
+  = swapLiftCoEnv <$> ty_co_match menv (swapLiftCoEnv subst) ty co' rkco lkco
+
+  -- Match a type variable against a non-refl coercion
+ty_co_match menv subst (TyVarTy tv1) co lkco rkco
+  | Just co1' <- lookupVarEnv subst tv1' -- tv1' is already bound to co1
+  = if eqCoercionX (nukeRnEnvL rn_env) co1' co
+    then Just subst
+    else Nothing       -- no match since tv1 matches two different coercions
+
+  | tv1' `elemVarSet` me_tmpls menv           -- tv1' is a template var
+  = if any (inRnEnvR rn_env) (tyCoVarsOfCoList co)
+    then Nothing      -- occurs check failed
+    else Just $ extendVarEnv subst tv1' $
+                castCoercionKind co (mkSymCo lkco) (mkSymCo rkco)
+
+  | otherwise
+  = Nothing
+
+  where
+    rn_env = me_env menv
+    tv1' = rnOccL rn_env tv1
+
+  -- just look through SubCo's. We don't really care about roles here.
+ty_co_match menv subst ty (SubCo co) lkco rkco
+  = ty_co_match menv subst ty co lkco rkco
+
+ty_co_match menv subst (AppTy ty1a ty1b) co _lkco _rkco
+  | Just (co2, arg2) <- splitAppCo_maybe co     -- c.f. Unify.match on AppTy
+  = ty_co_match_app menv subst ty1a ty1b co2 arg2
+ty_co_match menv subst ty1 (AppCo co2 arg2) _lkco _rkco
+  | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
+       -- yes, the one from Type, not TcType; this is for coercion optimization
+  = ty_co_match_app menv subst ty1a ty1b co2 arg2
+
+ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos) _lkco _rkco
+  = ty_co_match_tc menv subst tc1 tys tc2 cos
+ty_co_match menv subst (ForAllTy (Anon ty1) ty2) (TyConAppCo _ tc cos) _lkco _rkco
+  = ty_co_match_tc menv subst funTyCon [ty1, ty2] tc cos
+
+ty_co_match menv subst (ForAllTy (Named tv1 _) ty1)
+                       (ForAllCo tv2 kind_co2 co2)
+                       lkco rkco
+  = do { subst1 <- ty_co_match menv subst (tyVarKind tv1) kind_co2
+                               ki_ki_co ki_ki_co
+       ; let rn_env0 = me_env menv
+             rn_env1 = rnBndr2 rn_env0 tv1 tv2
+             menv'   = menv { me_env = rn_env1 }
+       ; ty_co_match menv' subst1 ty1 co2 lkco rkco }
+  where
+    ki_ki_co = mkNomReflCo liftedTypeKind
+
+ty_co_match _ subst (CoercionTy {}) _ _ _
+  = Just subst -- don't inspect coercions
+
+ty_co_match menv subst ty co lkco rkco
+  | Just co' <- pushRefl co = ty_co_match menv subst ty co' lkco rkco
+  | otherwise               = Nothing
+
+ty_co_match_tc :: MatchEnv -> LiftCoEnv
+               -> TyCon -> [Type]
+               -> TyCon -> [Coercion]
+               -> Maybe LiftCoEnv
+ty_co_match_tc menv subst tc1 tys1 tc2 cos2
+  = do { guard (tc1 == tc2)
+       ; ty_co_match_args menv subst tys1 cos2 lkcos rkcos }
+  where
+    Pair lkcos rkcos
+      = traverse (fmap mkNomReflCo . coercionKind) cos2
+
+ty_co_match_app :: MatchEnv -> LiftCoEnv
+                -> Type -> Type -> Coercion -> Coercion
+                -> Maybe LiftCoEnv
+ty_co_match_app menv subst ty1a ty1b co2a co2b
+  = do { -- TODO (RAE): Remove this exponential behavior.
+         subst1 <- ty_co_match menv subst  ki1a ki2a ki_ki_co ki_ki_co
+       ; let Pair lkco rkco = mkNomReflCo <$> coercionKind ki2a
+       ; subst2 <- ty_co_match menv subst1 ty1a co2a lkco rkco
+       ; ty_co_match menv subst2 ty1b co2b (mkNthCo 0 lkco) (mkNthCo 0 rkco) }
+  where
+    ki1a = typeKind ty1a
+    ki2a = promoteCoercion co2a
+    ki_ki_co = mkNomReflCo liftedTypeKind
+
+ty_co_match_args :: MatchEnv -> LiftCoEnv -> [Type]
+                 -> [Coercion] -> [Coercion] -> [Coercion]
+                 -> Maybe LiftCoEnv
+ty_co_match_args _    subst []       []         _ _ = Just subst
+ty_co_match_args menv subst (ty:tys) (arg:args) (lkco:lkcos) (rkco:rkcos)
+  = do { subst' <- ty_co_match menv subst ty arg lkco rkco
+       ; ty_co_match_args menv subst' tys args lkcos rkcos }
+ty_co_match_args _    _     _        _          _ _ = Nothing
+
+pushRefl :: Coercion -> Maybe Coercion
+pushRefl (Refl Nominal (AppTy ty1 ty2))
+  = Just (AppCo (Refl Nominal ty1) (mkNomReflCo ty2))
+pushRefl (Refl r (ForAllTy (Anon ty1) ty2))
+  = Just (TyConAppCo r funTyCon [mkReflCo r ty1, mkReflCo r ty2])
+pushRefl (Refl r (TyConApp tc tys))
+  = Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
+pushRefl (Refl r (ForAllTy (Named tv _) ty))
+  = Just (mkHomoForAllCos_NoRefl [tv] (Refl r ty))
+    -- NB: NoRefl variant. Otherwise, we get a loop!
+pushRefl (Refl r (CastTy ty co))  = Just (castCoercionKind (Refl r ty) co co)
+pushRefl _                        = Nothing