content: -- (c) The University of Glasgow 2006
  
  {-# LANGUAGE CPP #-}
  
  module Eta.Types.Unify (
          -- Matching of types:
          --      the "tc" prefix indicates that matching always
          --      respects newtypes (rather than looking through them)
          tcMatchTy, tcMatchTys, tcMatchTyX,
          ruleMatchTyX, tcMatchPreds,
  
          MatchEnv(..), matchList,
  
          typesCantMatch,
  
          -- Side-effect free unification
          tcUnifyTy, tcUnifyTys, BindFlag(..),
  
          UnifyResultM(..), UnifyResult, tcUnifyTysFG
  
     ) where
  
  #include "HsVersions.h"
  
  import Eta.BasicTypes.Var
  import Eta.BasicTypes.VarEnv
  import Eta.BasicTypes.VarSet
  import Eta.Types.Kind
  import Eta.Types.Type
  import Eta.Types.TyCon
  import Eta.Types.TypeRep
  import Eta.Utils.Util
  
  import Control.Monad (liftM, ap)
  #if __GLASGOW_HASKELL__ < 709
  import Control.Applicative (Applicative(..))
  #endif
  
  {-
  ************************************************************************
  *                                                                      *
                  Matching
  *                                                                      *
  ************************************************************************
  
  
  Matching is much tricker than you might think.
  
  1. The substitution we generate binds the *template type variables*
     which are given to us explicitly.
  
  2. We want to match in the presence of foralls;
          e.g     (forall a. t1) ~ (forall b. t2)
  
     That is what the RnEnv2 is for; it does the alpha-renaming
     that makes it as if a and b were the same variable.
     Initialising the RnEnv2, so that it can generate a fresh
     binder when necessary, entails knowing the free variables of
     both types.
  
  3. We must be careful not to bind a template type variable to a
     locally bound variable.  E.g.
          (forall a. x) ~ (forall b. b)
     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
    = case match menv emptyTvSubstEnv 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 }
      in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
          -- We're assuming that all the interesting
          -- tyvars in ty1 are in tmpls
  
  tcMatchTys :: TyVarSet          -- Template tyvars
             -> [Type]            -- Template
             -> [Type]            -- Target
             -> Maybe TvSubst     -- One-shot; in principle the template
                                  -- variables could be free in the target
  
  tcMatchTys tmpls tys1 tys2
    = case match_tys menv emptyTvSubstEnv 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 }
      in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
          -- We're assuming that all the interesting
          -- tyvars in tys1 are in tmpls
  
  -- This is similar, but extends a substitution
  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}
  
  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) (tyVarsOfTypeList 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
    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.lhs
  
  --------------
  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
  
  {-
  ************************************************************************
  *                                                                      *
                  GADTs
  *                                                                      *
  ************************************************************************
  
  Note [Pruning dead case alternatives]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Consider        data T a where
                     T1 :: T Int
                     T2 :: T a
  
                  newtype X = MkX Int
                  newtype Y = MkY Char
  
                  type family F a
                  type instance F Bool = Int
  
  Now consider    case x of { T1 -> e1; T2 -> e2 }
  
  The question before the house is this: if I know something about the type
  of x, can I prune away the T1 alternative?
  
  Suppose x::T Char.  It's impossible to construct a (T Char) using T1,
          Answer = YES we can prune the T1 branch (clearly)
  
  Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
  to 'Bool', in which case x::T Int, so
          ANSWER = NO (clearly)
  
  Suppose x::T X.  Then *in Haskell* it's impossible to construct a (non-bottom)
  value of type (T X) using T1.  But *in FC* it's quite possible.  The newtype
  gives a coercion
          CoX :: X ~ Int
  So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
  of type (T X) constructed with T1.  Hence
          ANSWER = NO we can't prune the T1 branch (surprisingly)
  
  Furthermore, this can even happen; see Trac #1251.  GHC's newtype-deriving
  mechanism uses a cast, just as above, to move from one dictionary to another,
  in effect giving the programmer access to CoX.
  
  Finally, suppose x::T Y.  Then *even in FC* we can't construct a
  non-bottom value of type (T Y) using T1.  That's because we can get
  from Y to Char, but not to Int.
  
  
  Here's a related question.      data Eq a b where EQ :: Eq a a
  Consider
          case x of { EQ -> ... }
  
  Suppose x::Eq Int Char.  Is the alternative dead?  Clearly yes.
  
  What about x::Eq Int a, in a context where we have evidence that a~Char.
  Then again the alternative is dead.
  
  
                          Summary
  
  We are really doing a test for unsatisfiability of the type
  constraints implied by the match. And that is clearly, in general, a
  hard thing to do.
  
  However, since we are simply dropping dead code, a conservative test
  suffices.  There is a continuum of tests, ranging from easy to hard, that
  drop more and more dead code.
  
  For now we implement a very simple test: type variables match
  anything, type functions (incl newtypes) match anything, and only
  distinct data types fail to match.  We can elaborate later.
  -}
  
  typesCantMatch :: [(Type,Type)] -> Bool
  typesCantMatch prs = any (\(s,t) -> cant_match s t) prs
    where
      cant_match :: Type -> Type -> Bool
      cant_match t1 t2
          | Just t1' <- coreView t1 = cant_match t1' t2
          | Just t2' <- coreView t2 = cant_match t1 t2'
  
      cant_match (FunTy a1 r1) (FunTy a2 r2)
          = cant_match a1 a2 || cant_match r1 r2
  
      cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
          | isDistinctTyCon tc1 && isDistinctTyCon tc2
          = tc1 /= tc2 || typesCantMatch (zipEqual "typesCantMatch" tys1 tys2)
  
      cant_match (FunTy {}) (TyConApp tc _) = isDistinctTyCon tc
      cant_match (TyConApp tc _) (FunTy {}) = isDistinctTyCon tc
          -- tc can't be FunTyCon by invariant
  
      cant_match (AppTy f1 a1) ty2
          | Just (f2, a2) <- repSplitAppTy_maybe ty2
          = cant_match f1 f2 || cant_match a1 a2
      cant_match ty1 (AppTy f2 a2)
          | Just (f1, a1) <- repSplitAppTy_maybe ty1
          = cant_match f1 f2 || cant_match a1 a2
  
      cant_match (LitTy x) (LitTy y) = x /= y
  
      cant_match _ _ = False      -- Safe!
  
  -- Things we could add;
  --      foralls
  --      look through newtypes
  --      take account of tyvar bindings (EQ example above)
  
  {-
  ************************************************************************
  *                                                                      *
               Unification
  *                                                                      *
  ************************************************************************
  
  Note [Fine-grained unification]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Do the types (x, x) and ([y], y) unify? The answer is seemingly "no" --
  no substitution to finite types makes these match. But, a substitution to
  *infinite* types can unify these two types: [x |-> [[[...]]], y |-> [[[...]]] ].
  Why do we care? Consider these two type family instances:
  
  type instance F x x   = Int
  type instance F [y] y = Bool
  
  If we also have
  
  type instance Looper = [Looper]
  
  then the instances potentially overlap. The solution is to use unification
  over infinite terms. This is possible (see [1] for lots of gory details), but
  a full algorithm is a little more power than we need. Instead, we make a
  conservative approximation and just omit the occurs check.
  
  [1]: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
  
  tcUnifyTys considers an occurs-check problem as the same as general unification
  failure.
  
  tcUnifyTysFG ("fine-grained") returns one of three results: success, occurs-check
  failure ("MaybeApart"), or general failure ("SurelyApart").
  
  See also Trac #8162.
  
  It's worth noting that unification in the presence of infinite types is not
  complete. This means that, sometimes, a closed type family does not reduce
  when it should. See test case indexed-types/should_fail/Overlap15 for an
  example.
  
  Note [The substitution in MaybeApart]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  The constructor MaybeApart carries data with it, typically a TvSubstEnv. Why?
  Because consider unifying these:
  
  (a, a, Int) ~ (b, [b], Bool)
  
  If we go left-to-right, we start with [a |-> b]. Then, on the middle terms, we
  apply the subst we have so far and discover that we need [b |-> [b]]. Because
  this fails the occurs check, we say that the types are MaybeApart (see above
  Note [Fine-grained unification]). But, we can't stop there! Because if we
  continue, we discover that Int is SurelyApart from Bool, and therefore the
  types are apart. This has practical consequences for the ability for closed
  type family applications to reduce. See test case
  indexed-types/should_compile/Overlap14.
  
  Note [Unifying with skolems]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  If we discover that two types unify if and only if a skolem variable is
  substituted, we can't properly unify the types. But, that skolem variable
  may later be instantiated with a unifyable type. So, we return maybeApart
  in these cases.
  
  Note [Lists of different lengths are MaybeApart]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  It is unusual to call tcUnifyTys or tcUnifyTysFG with lists of different
  lengths. The place where we know this can happen is from compatibleBranches in
  FamInstEnv, when checking data family instances. Data family instances may be
  eta-reduced; see Note [Eta reduction for data family axioms] in TcInstDcls.
  
  We wish to say that
  
    D :: * -> * -> *
    axDF1 :: D Int ~ DFInst1
    axDF2 :: D Int Bool ~ DFInst2
  
  overlap. If we conclude that lists of different lengths are SurelyApart, then
  it will look like these do *not* overlap, causing disaster. See Trac #9371.
  
  In usages of tcUnifyTys outside of family instances, we always use tcUnifyTys,
  which can't tell the difference between MaybeApart and SurelyApart, so those
  usages won't notice this design choice.
  -}
  
  tcUnifyTy :: Type -> Type       -- All tyvars are bindable
            -> Maybe TvSubst      -- A regular one-shot (idempotent) substitution
  -- Simple unification of two types; all type variables are bindable
  tcUnifyTy ty1 ty2
    = case initUM (const BindMe) (unify emptyTvSubstEnv ty1 ty2) of
        Unifiable subst_env -> Just (niFixTvSubst subst_env)
        _other              -> Nothing
  
  -----------------
  tcUnifyTys :: (TyVar -> BindFlag)
             -> [Type] -> [Type]
             -> Maybe TvSubst     -- A regular one-shot (idempotent) substitution
  -- 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
  
  -- 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
  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
                                           -- See Note [The substitution in MaybeApart]
                      | SurelyApart
  
  -- See Note [Fine-grained unification]
  tcUnifyTysFG :: (TyVar -> BindFlag)
               -> [Type] -> [Type]
               -> UnifyResult
  tcUnifyTysFG bind_fn tys1 tys2
    = initUM bind_fn $
      do { subst <- unifyList emptyTvSubstEnv tys1 tys2
  
          -- Find the fixed point of the resulting non-idempotent substitution
          ; return (niFixTvSubst subst) }
  
  {-
  ************************************************************************
  *                                                                      *
                  Non-idempotent substitution
  *                                                                      *
  ************************************************************************
  
  Note [Non-idempotent substitution]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  During unification we use a TvSubstEnv that is
    (a) non-idempotent
    (b) loop-free; ie repeatedly applying it yields a fixed point
  
  Note [Finding the substitution fixpoint]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Finding the fixpoint of a non-idempotent substitution arising from a
  unification is harder than it looks, because of kinds.  Consider
     T k (H k (f:k)) ~ T * (g:*)
  If we unify, we get the substitution
     [ k -> *
     , g -> H k (f:k) ]
  To make it idempotent we don't want to get just
     [ k -> *
     , g -> H * (f:k) ]
  We also want to substitute inside f's kind, to get
     [ k -> *
     , g -> H k (f:*) ]
  If we don't do this, we may apply the substitition to something,
  and get an ill-formed type, i.e. one where typeKind will fail.
  This happened, for example, in Trac #9106.
  
  This is the reason for extending env with [f:k -> f:*], in the
  definition of env' in niFixTvSubst
  -}
  
  niFixTvSubst :: TvSubstEnv -> TvSubst
  -- 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
    where
      f env | not_fixpoint = f (mapVarEnv (substTy subst') env)
            | otherwise    = subst
          where
            not_fixpoint  = foldVarSet ((||) . in_domain) False all_range_tvs
            in_domain tv  = tv `elemVarEnv` env
  
            range_tvs     = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet env
            all_range_tvs = closeOverKinds range_tvs
            subst         = mkTvSubst (mkInScopeSet all_range_tvs) env
  
               -- 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
  -- 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
    = foldVarSet (unionVarSet . get) emptyVarSet tvs
    where
      get tv = case lookupVarEnv subst tv of
                 Nothing -> unitVarSet tv
                 Just ty -> niSubstTvSet subst (tyVarsOfType ty)
  
  {-
  ************************************************************************
  *                                                                      *
                  The workhorse
  *                                                                      *
  ************************************************************************
  -}
  
  unify :: TvSubstEnv     -- An existing substitution to extend
        -> Type -> Type   -- Types to be unified, and witness of their equality
        -> UM TvSubstEnv          -- Just the extended substitution,
                                  -- Nothing if unification failed
  -- We do not require the incoming substitution to be idempotent,
  -- nor guarantee that the outgoing one is.  That's fixed up by
  -- the wrappers.
  
  -- Respects newtypes, PredTypes
  
  -- in unify, any NewTcApps/Preds should be taken at face value
  unify subst (TyVarTy tv1) ty2  = uVar subst tv1 ty2
  unify subst ty1 (TyVarTy tv2)  = uVar subst tv2 ty1
  
  unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
  unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
  
  unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2)
    | tyc1 == tyc2
    = unify_tys subst tys1 tys2
  
  unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
    = do  { subst' <- unify subst ty1a ty2a
          ; unify subst' ty1b ty2b }
  
          -- 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,
          -- so if one type is an App the other one jolly well better be too
  unify subst (AppTy ty1a ty1b) ty2
    | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
    = do  { subst' <- unify subst ty1a ty2a
          ; unify subst' ty1b ty2b }
  
  unify subst ty1 (AppTy ty2a ty2b)
    | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
    = do  { subst' <- unify subst ty1a ty2a
          ; unify subst' ty1b ty2b }
  
  unify subst (LitTy x) (LitTy y) | x == y = return subst
  
  unify _ _ _ = surelyApart
          -- ForAlls??
  
  ------------------------------
  unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
  unify_tys subst xs ys = unifyList subst xs ys
  
  unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
  unifyList subst orig_xs orig_ys
    = go subst orig_xs orig_ys
    where
      go subst []     []     = return subst
      go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
                                  ; go subst' xs ys }
      go subst _ _ = maybeApart subst  -- See Note [Lists of different lengths are MaybeApart]
  
  ---------------------------------
  uVar :: TvSubstEnv      -- An existing substitution to extend
       -> TyVar           -- Type variable to be unified
       -> Type            -- with this type
       -> UM TvSubstEnv
  
  uVar subst tv1 ty
   = -- Check to see whether tv1 is refined by the substitution
     case (lookupVarEnv subst tv1) of
       Just ty' -> unify subst ty' ty     -- Yes, call back into unify'
       Nothing  -> uUnrefined subst       -- No, continue
                              tv1 ty ty
  
  uUnrefined :: TvSubstEnv          -- An existing substitution to extend
             -> TyVar               -- Type variable to be unified
             -> Type                -- with this type
             -> Type                -- (version w/ expanded synonyms)
             -> UM TvSubstEnv
  
  -- We know that tv1 isn't refined
  
  uUnrefined subst tv1 ty2 ty2'
    | Just ty2'' <- tcView ty2'
    = uUnrefined subst tv1 ty2 ty2''      -- 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 subst
  
      -- 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
         ; subst' <- unify subst (tyVarKind tv1) (tyVarKind tv2)
  
             -- 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
         ; case (b1, b2) of
             (Skolem, Skolem) -> maybeApart subst' -- See Note [Unification with skolems]
             (BindMe, _)      -> return (extendVarEnv subst' tv1 ty2)
             (_, BindMe)      -> return (extendVarEnv subst' tv2 ty1) }
  
  uUnrefined subst tv1 ty2 ty2'   -- ty2 is not a type variable
    | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2')
    = maybeApart subst                    -- Occurs check
                                          -- See Note [Fine-grained unification]
    | otherwise
    = do { subst' <- unify subst k1 k2
         -- Note [Kinds Containing Only Literals]
         ; bindTv subst' tv1 ty2 }        -- Bind tyvar to the synonym if poss
    where
      k1 = tyVarKind tv1
      k2 = typeKind ty2'
  
  bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
  bindTv subst tv ty      -- ty is not a type variable
    = do  { b <- tvBindFlag tv
          ; case b of
              Skolem -> maybeApart subst -- See Note [Unification with skolems]
              BindMe -> return $ extendVarEnv subst tv ty
          }
  
  {-
  ************************************************************************
  *                                                                      *
                  Binding decisions
  *                                                                      *
  ************************************************************************
  -}
  
  data BindFlag
    = BindMe      -- A regular type variable
  
    | Skolem      -- This type variable is a skolem constant
                  -- Don't bind it; it only matches itself
  
  {-
  ************************************************************************
  *                                                                      *
                  Unification monad
  *                                                                      *
  ************************************************************************
  -}
  
  newtype UM a = UM { unUM :: (TyVar -> BindFlag)
                           -> UnifyResultM a }
  
  instance Functor UM where
        fmap = liftM
  
  instance Applicative UM where
        pure = return
        (<*>) = ap
  
  instance Monad UM where
    return a = UM (\_tvs -> Unifiable a)
    fail _   = UM (\_tvs -> SurelyApart) -- failed pattern match
    m >>= k  = UM (\tvs -> case unUM m tvs of
                             Unifiable v -> unUM (k v) tvs
                             MaybeApart v ->
                               case unUM (k v) tvs of
                                 Unifiable v' -> MaybeApart v'
                                 other        -> other
                             SurelyApart -> SurelyApart)
  
  initUM :: (TyVar -> BindFlag) -> UM a -> UnifyResultM a
  initUM badtvs um = unUM um badtvs
  
  tvBindFlag :: TyVar -> UM BindFlag
  tvBindFlag tv = UM (\tv_fn -> Unifiable (tv_fn tv))
  
  maybeApart :: TvSubstEnv -> UM TvSubstEnv
  maybeApart subst = UM (\_tv_fn -> MaybeApart subst)
  
  surelyApart :: UM a
  surelyApart = UM (\_tv_fn -> SurelyApart)
  