Simplify API to tcMatchTys

Previously tcMatchTys took a set of "template type variables" to
bind.  But all the calls are top-level, and we always want to
bind all variables in the template.  So I simplified the API
by omitting that argument.

There should be no change in behaviour.

Feel free to merge to 8.0 if it helps in merging other patches

compiler/typecheck/FunDeps.hs

@@ -258,9 +258,9 @@ improveClsFD clas_tvs fd
              length tys_inst == length clas_tvs
             , ppr tys_inst <+> ppr tys_actual )
 
-    case tcMatchTys qtv_set ltys1 ltys2 of
+    case tcMatchTys ltys1 ltys2 of
         Nothing  -> []
-        Just subst | isJust (tcMatchTysX qtv_set subst rtys1 rtys2)
+        Just subst | isJust (tcMatchTysX subst rtys1 rtys2)
                         -- Don't include any equations that already hold.
                         -- Reason: then we know if any actual improvement has happened,
                         --         in which case we need to iterate the solver
@@ -314,7 +314,6 @@ improveClsFD clas_tvs fd
                         --              whose kind mentions that kind variable!
                         --          Trac #6015, #6068
   where
-    qtv_set = mkVarSet qtvs
     (ltys1, rtys1) = instFD fd clas_tvs tys_inst
     (ltys2, rtys2) = instFD fd clas_tvs tys_actual
 

compiler/typecheck/TcErrors.hs

@@ -1891,7 +1891,7 @@ mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
                       ev_var_matches ty = case getClassPredTys_maybe ty of
                          Just (clas', tys')
                            | clas' == clas
-                           , Just _ <- tcMatchTys (tyCoVarsOfTypes tys) tys tys'
+                           , Just _ <- tcMatchTys tys tys'
                            -> True
                            | otherwise
                            -> any ev_var_matches (immSuperClasses clas' tys')

compiler/typecheck/TcSimplify.hs

@@ -1959,8 +1959,7 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
       = return False
 
     the_ty   = mkTyVarTy the_tv
-    tmpl_tvs = tyCoVarsOfType the_ty
-    mb_subst = tcMatchTy tmpl_tvs the_ty default_ty
+    mb_subst = tcMatchTy the_ty default_ty
       -- Make sure the kinds match too; hence this call to tcMatchTy
       -- E.g. suppose the only constraint was (Typeable k (a::k))
       -- With the addition of polykinded defaulting we also want to reject

compiler/typecheck/TcTyClsDecls.hs

@@ -1590,7 +1590,7 @@ rejigConRes tmpl_tvs res_tmpl dc_tvs res_ty
         -- So we return ([a,b,z], [x,y], [a~(x,y),b~z], T [(x,y)] z z)
   | Just subst <- ASSERT( isLiftedTypeKind (typeKind res_ty) )
                   ASSERT( isLiftedTypeKind (typeKind res_tmpl) )
-                  tcMatchTy (mkVarSet tmpl_tvs) res_tmpl res_ty
+                  tcMatchTy res_tmpl res_ty
   = let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tmpl_tvs dc_tvs subst
         raw_ex_tvs = dc_tvs `minusList` univ_tvs
         (arg_subst, substed_ex_tvs)
@@ -1979,28 +1979,26 @@ checkValidTyCon tc
                 -- NB: this check assumes that all the constructors of a given
                 -- data type use the same type variables
         where
-        (tvs1, _, _, res1) = dataConSig con1
-        ts1 = mkVarSet tvs1
+        (_, _, _, res1) = dataConSig con1
         fty1 = dataConFieldType con1 lbl
         lbl = flLabel label
 
         checkOne (_, con2)    -- Do it bothways to ensure they are structurally identical
-            = do { checkFieldCompat lbl con1 con2 ts1 res1 res2 fty1 fty2
-                 ; checkFieldCompat lbl con2 con1 ts2 res2 res1 fty2 fty1 }
+            = do { checkFieldCompat lbl con1 con2 res1 res2 fty1 fty2
+                 ; checkFieldCompat lbl con2 con1 res2 res1 fty2 fty1 }
             where
-                (tvs2, _, _, res2) = dataConSig con2
-                ts2 = mkVarSet tvs2
+                (_, _, _, res2) = dataConSig con2
                 fty2 = dataConFieldType con2 lbl
     check_fields [] = panic "checkValidTyCon/check_fields []"
 
-checkFieldCompat :: FieldLabelString -> DataCon -> DataCon -> TyVarSet
+checkFieldCompat :: FieldLabelString -> DataCon -> DataCon
                  -> Type -> Type -> Type -> Type -> TcM ()
-checkFieldCompat fld con1 con2 tvs1 res1 res2 fty1 fty2
+checkFieldCompat fld con1 con2 res1 res2 fty1 fty2
   = do  { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
         ; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
   where
-    mb_subst1 = tcMatchTy tvs1 res1 res2
-    mb_subst2 = tcMatchTyX tvs1 (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
+    mb_subst1 = tcMatchTy res1 res2
+    mb_subst2 = tcMatchTyX (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
 
 -------------------------------
 -- | Check for ill-scoped telescopes in a tycon.
@@ -2051,8 +2049,7 @@ checkValidDataCon dflags existential_ok tc con
               , ppr orig_res_ty <+> dcolon <+> ppr (typeKind orig_res_ty)])
 
 
-        ; checkTc (isJust (tcMatchTy (mkVarSet tc_tvs)
-                                     res_ty_tmpl
+        ; checkTc (isJust (tcMatchTy res_ty_tmpl
                                      orig_res_ty))
                   (badDataConTyCon con res_ty_tmpl orig_res_ty)
             -- Note that checkTc aborts if it finds an error. This is

compiler/typecheck/TcValidity.hs

@@ -1280,12 +1280,10 @@ checkConsistentFamInst (Just (clas, mini_env)) fam_tc at_tvs at_tys
        ; discardResult $ foldrM check_arg emptyTCvSubst $
                          tyConTyVars fam_tc `zip` at_tys }
   where
-    at_tv_set = mkVarSet at_tvs
-
     check_arg :: (TyVar, Type) -> TCvSubst -> TcM TCvSubst
     check_arg (fam_tc_tv, at_ty) subst
       | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
-      = case tcMatchTyX at_tv_set subst at_ty inst_ty of
+      = case tcMatchTyX subst at_ty inst_ty of
            Just subst | all_distinct subst -> return subst
            _ -> failWithTc $ wrongATArgErr at_ty inst_ty
                 -- No need to instantiate here, because the axiom

compiler/types/FamInstEnv.hs

@@ -425,11 +425,9 @@ identicalFamInstHead (FamInst { fi_axiom = ax1 }) (FamInst { fi_axiom = ax2 })
     brs2 = coAxiomBranches ax2
 
     identical_branch br1 br2
-      =  isJust (tcMatchTys tvs1 lhs1 lhs2)
-      && isJust (tcMatchTys tvs2 lhs2 lhs1)
+      =  isJust (tcMatchTys lhs1 lhs2)
+      && isJust (tcMatchTys lhs2 lhs1)
       where
-        tvs1 = mkVarSet (coAxBranchTyVars br1)
-        tvs2 = mkVarSet (coAxBranchTyVars br2)
         lhs1 = coAxBranchLHS br1
         lhs2 = coAxBranchLHS br2
 
@@ -726,7 +724,7 @@ lookupFamInstEnv
 lookupFamInstEnv
    = lookup_fam_inst_env match
    where
-     match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
+     match _ _ tpl_tys tys = tcMatchTys tpl_tys tys
 
 lookupFamInstEnvConflicts
     :: FamInstEnvs
@@ -1014,8 +1012,8 @@ isDominatedBy branch branches
   = or $ map match branches
     where
       lhs = coAxBranchLHS branch
-      match (CoAxBranch { cab_tvs = tvs, cab_lhs = tys })
-        = isJust $ tcMatchTys (mkVarSet tvs) tys lhs
+      match (CoAxBranch { cab_lhs = tys })
+        = isJust $ tcMatchTys tys lhs
 
 {-
 ************************************************************************
@@ -1105,7 +1103,7 @@ findBranch branches target_tys
                             map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
             -- See Note [Flattening] below
             flattened_target = flattenTys in_scope target_tys
-        in case tcMatchTys (mkVarSet (tpl_tvs ++ tpl_cvs)) tpl_lhs target_tys of
+        in case tcMatchTys tpl_lhs target_tys of
         Just subst -- matching worked. now, check for apartness.
           |  apartnessCheck flattened_target branch
           -> -- matching worked & we're apart from all incompatible branches.

compiler/types/InstEnv.hs

@@ -414,12 +414,12 @@ identicalClsInstHead :: ClsInst -> ClsInst -> Bool
 -- e.g.  both are   Eq [(a,b)]
 -- Used for overriding in GHCi
 -- Obviously should be insenstive to alpha-renaming
-identicalClsInstHead (ClsInst { is_cls_nm = cls_nm1, is_tcs = rough1, is_tvs = tvs1, is_tys = tys1 })
-                     (ClsInst { is_cls_nm = cls_nm2, is_tcs = rough2, is_tvs = tvs2, is_tys = tys2 })
+identicalClsInstHead (ClsInst { is_cls_nm = cls_nm1, is_tcs = rough1, is_tys = tys1 })
+                     (ClsInst { is_cls_nm = cls_nm2, is_tcs = rough2, is_tys = tys2 })
   =  cls_nm1 == cls_nm2
   && not (instanceCantMatch rough1 rough2)  -- Fast check for no match, uses the "rough match" fields
-  && isJust (tcMatchTys (mkVarSet tvs1) tys1 tys2)
-  && isJust (tcMatchTys (mkVarSet tvs2) tys2 tys1)
+  && isJust (tcMatchTys tys1 tys2)
+  && isJust (tcMatchTys tys2 tys1)
 
 {-
 ************************************************************************
@@ -711,7 +711,7 @@ lookupInstEnv' ie vis_mods cls tys
       | instanceCantMatch rough_tcs mb_tcs
       = find ms us rest
 
-      | Just subst <- tcMatchTys tpl_tv_set tpl_tys tys
+      | Just subst <- tcMatchTys tpl_tys tys
       = find ((item, map (lookupTyVar subst) tpl_tvs) : ms) us rest
 
         -- Does not match, so next check whether the things unify
@@ -848,8 +848,7 @@ insert_overlapping new_item (old_item : old_items)
     -- `instB` can be instantiated to match `instA`
     -- or the two are equal
     (instA,_) `more_specific_than` (instB,_)
-      = isJust (tcMatchTys (mkVarSet (is_tvs instB))
-               (is_tys instB) (is_tys instA))
+      = isJust (tcMatchTys (is_tys instB) (is_tys instA))
 
     (instA, _) `can_override` (instB, _)
        =  hasOverlappingFlag  (overlapMode (is_flag instA))

compiler/types/Unify.hs

@@ -92,44 +92,45 @@ requires dealing with coercions in this manner.
 
 -}
 
--- | @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]
+-- | @tcMatchTy t1 t2@ produces a substitution (over fvs(t1))
+-- @s@ such that @s(t1)@ equals @t2@.
+-- The returned substitution might bind coercion variables,
+-- if the variable is an argument to a GADT constructor.
+--
+-- We don't pass in a set of "template variables" to be bound
+-- by the match, because tcMatchTy (and similar functions) are
+-- always used on top-level types, so we can bind any of the
+-- free variables of the LHS.
+tcMatchTy :: Type -> Type -> Maybe TCvSubst
+tcMatchTy ty1 ty2 = tcMatchTys [ty1] [ty2]
 
 -- | This is similar to 'tcMatchTy', but extends a substitution
-tcMatchTyX :: TyCoVarSet          -- ^ Template tyvars
-           -> TCvSubst            -- ^ Substitution to extend
+tcMatchTyX :: TCvSubst            -- ^ Substitution to extend
            -> Type                -- ^ Template
            -> Type                -- ^ Target
            -> Maybe TCvSubst
-tcMatchTyX tmpls subst ty1 ty2 = tcMatchTysX tmpls subst [ty1] [ty2]
+tcMatchTyX subst ty1 ty2 = tcMatchTysX subst [ty1] [ty2]
 
 -- | Like 'tcMatchTy' but over a list of types.
-tcMatchTys :: TyCoVarSet     -- ^ Template tyvars
-           -> [Type]         -- ^ Template
+tcMatchTys :: [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 (mkEmptyTCvSubst in_scope) tys1 tys2
+tcMatchTys tys1 tys2
+  = tcMatchTysX (mkEmptyTCvSubst in_scope) tys1 tys2
   where
-    in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfTypes tys2)
-        -- We're assuming that all the interesting
-        -- tyvars in tys1 are in tmpls
+    in_scope = mkInScopeSet (tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2)
 
 -- | Like 'tcMatchTys', but extending a substitution
-tcMatchTysX :: TyCoVarSet     -- ^ Template tyvars
-            -> TCvSubst       -- ^ Substitution to extend
+tcMatchTysX :: TCvSubst       -- ^ Substitution to extend
             -> [Type]         -- ^ Template
             -> [Type]         -- ^ Target
             -> Maybe TCvSubst -- ^ One-shot substitution
-tcMatchTysX tmpls (TCvSubst in_scope tv_env cv_env) tys1 tys2
+tcMatchTysX (TCvSubst in_scope tv_env cv_env) tys1 tys2
 -- See Note [Kind coercions in Unify]
-  = case tc_unify_tys (matchBindFun tmpls) False False
+  = case tc_unify_tys (const BindMe)
+                      False  -- Matching, not unifying
+                      False  -- Not an injectivity check
                       (mkRnEnv2 in_scope) tv_env cv_env tys1 tys2 of
       Unifiable (tv_env', cv_env')
         -> Just $ TCvSubst in_scope tv_env' cv_env'