Commit 33dcb810 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Simplify the API for tcInstTyVars, and make it more consistent with other similar functions

parent fd46acf1
......@@ -596,7 +596,7 @@ liftTcM = id
newVar :: Kind -> TR TcType
newVar = liftTcM . newFlexiTyVarTy
instTyVars :: [TyVar] -> TR ([TcTyVar], [TcType], TvSubst)
instTyVars :: [TyVar] -> TR (TvSubst, [TcTyVar])
-- Instantiate fresh mutable type variables from some TyVars
-- This function preserves the print-name, which helps error messages
instTyVars = liftTcM . tcInstTyVars
......@@ -613,7 +613,7 @@ type RttiInstantiation = [(TcTyVar, TyVar)]
-- mapping from new (instantiated) -to- old (skolem) type variables
instScheme :: QuantifiedType -> TR (TcType, RttiInstantiation)
instScheme (tvs, ty)
= liftTcM $ do { (tvs', _, subst) <- tcInstTyVars tvs
= liftTcM $ do { (subst, tvs') <- tcInstTyVars tvs
; let rtti_inst = [(tv',tv) | (tv',tv) <- tvs' `zip` tvs]
; return (substTy subst ty, rtti_inst) }
......@@ -950,7 +950,7 @@ getDataConArgTys dc con_app_ty
= do { let UnaryRep rep_con_app_ty = repType con_app_ty
; traceTR (text "getDataConArgTys 1" <+> (ppr con_app_ty $$ ppr rep_con_app_ty
$$ ppr (tcSplitTyConApp_maybe rep_con_app_ty)))
; (_, _, subst) <- instTyVars (univ_tvs ++ ex_tvs)
; (subst, _) <- instTyVars (univ_tvs ++ ex_tvs)
; addConstraint rep_con_app_ty (substTy subst (dataConOrigResTy dc))
-- See Note [Constructor arg types]
; let con_arg_tys = substTys subst (dataConRepArgTys dc)
......@@ -1183,8 +1183,8 @@ congruenceNewtypes lhs rhs = go lhs rhs >>= \rhs' -> return (lhs,rhs')
| otherwise = do
traceTR (text "(Upgrade) upgraded " <> ppr ty <>
text " in presence of newtype evidence " <> ppr new_tycon)
(_, vars, _) <- instTyVars (tyConTyVars new_tycon)
let ty' = mkTyConApp new_tycon vars
(_, vars) <- instTyVars (tyConTyVars new_tycon)
let ty' = mkTyConApp new_tycon (mkTyVarTys vars)
UnaryRep rep_ty = repType ty'
_ <- liftTcM (unifyType ty rep_ty)
-- assumes that reptype doesn't ^^^^ touch tyconApp args
......
......@@ -168,9 +168,14 @@ deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
deeplyInstantiate orig ty
| Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
= do { (_, tys, subst) <- tcInstTyVars tvs
= do { (subst, tvs') <- tcInstTyVars tvs
; ids1 <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
; wrap1 <- instCall orig tys (substTheta subst theta)
; let theta' = substTheta subst theta
; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
; traceTc "Instantiating (deply)" (vcat [ ppr ty
, text "with" <+> ppr tvs'
, text "args:" <+> ppr ids1
, text "theta:" <+> ppr theta' ])
; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
; return (mkWpLams ids1
<.> wrap2
......
......@@ -698,7 +698,7 @@ tcExpr (RecordUpd record_expr rbinds _ _ _) res_ty
mk_inst_ty :: TvSubst -> (TKVar, TcType) -> TcM (TvSubst, TcType)
-- Deals with instantiation of kind variables
-- c.f. TcMType.tcInstTyVarsX
-- c.f. TcMType.tcInstTyVars
mk_inst_ty subst (tv, result_inst_ty)
| is_fixed_tv tv -- Same as result type
= return (extendTvSubst subst tv result_inst_ty, result_inst_ty)
......@@ -706,7 +706,8 @@ tcExpr (RecordUpd record_expr rbinds _ _ _) res_ty
= do { new_ty <- newFlexiTyVarTy (TcType.substTy subst (tyVarKind tv))
; return (extendTvSubst subst tv new_ty, new_ty) }
; (_, result_inst_tys, result_subst) <- tcInstTyVars con1_tvs
; (result_subst, con1_tvs') <- tcInstTyVars con1_tvs
; let result_inst_tys = mkTyVarTys con1_tvs'
; (scrut_subst, scrut_inst_tys) <- mapAccumLM mk_inst_ty emptyTvSubst
(con1_tvs `zip` result_inst_tys)
......@@ -734,7 +735,7 @@ tcExpr (RecordUpd record_expr rbinds _ _ _) res_ty
-- Phew!
; return $ mkHsWrapCo co_res $
RecordUpd (mkLHsWrap scrut_co record_expr') rbinds'
relevant_cons scrut_inst_tys result_inst_tys }
relevant_cons scrut_inst_tys result_inst_tys }
where
upd_fld_names = hsRecFields rbinds
......@@ -1111,11 +1112,12 @@ instantiateOuter orig id
= return (HsVar id, tau)
| otherwise
= do { (_, tys, subst) <- tcInstTyVars tvs
; doStupidChecks id tys
; let theta' = substTheta subst theta
; traceTc "Instantiating" (ppr id <+> text "with" <+> (ppr tys $$ ppr theta'))
; wrap <- instCall orig tys theta'
= do { (subst, tvs') <- tcInstTyVars tvs
; let tys' = mkTyVarTys tvs'
theta' = substTheta subst theta
; doStupidChecks id tys'
; traceTc "Instantiating" (ppr id <+> text "with" <+> (ppr tys' $$ ppr theta'))
; wrap <- instCall orig tys' theta'
; return (mkHsWrap wrap (HsVar id), TcType.substTy subst tau) }
where
(tvs, theta, tau) = tcSplitSigmaTy (idType id)
......
......@@ -437,22 +437,16 @@ newPolyFlexiTyVarTy :: TcM TcType
newPolyFlexiTyVarTy = do { tv <- newMetaTyVar PolyTv liftedTypeKind
; return (TyVarTy tv) }
tcInstTyVars :: [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
tcInstTyVars :: [TKVar] -> TcM (TvSubst, [TcTyVar])
-- Instantiate with META type variables
-- Note that this works for a sequence of kind and type
-- variables. Eg [ (k:BOX), (a:k->k) ]
-- Gives [ (k7:BOX), (a8:k7->k7) ]
tcInstTyVars tyvars = tcInstTyVarsX emptyTvSubst tyvars
tcInstTyVars tyvars = mapAccumLM tcInstTyVarX emptyTvSubst tyvars
-- emptyTvSubst has an empty in-scope set, but that's fine here
-- Since the tyvars are freshly made, they cannot possibly be
-- captured by any existing for-alls.
tcInstTyVarsX :: TvSubst -> [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
-- The "X" part is because of extending the substitution
tcInstTyVarsX subst tyvars =
do { (subst', tyvars') <- mapAccumLM tcInstTyVarX subst tyvars
; return (tyvars', mkTyVarTys tyvars', subst') }
tcInstTyVarX :: TvSubst -> TKVar -> TcM (TvSubst, TcTyVar)
-- Make a new unification variable tyvar whose Name and Kind come from
-- an existing TyVar. We substitute kind variables in the kind.
......
......@@ -787,7 +787,7 @@ tcPatSynPat :: PatEnv -> Located Name -> PatSyn
tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
= do { let (univ_tvs, ex_tvs, prov_theta, req_theta, arg_tys, ty) = patSynSig pat_syn
; (univ_tvs', inst_tys, subst) <- tcInstTyVars univ_tvs
; (subst, univ_tvs') <- tcInstTyVars univ_tvs
; checkExistentials ex_tvs penv
; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
......@@ -817,7 +817,7 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
LamPat mc -> PatSkol (PatSynCon pat_syn) mc
LetPat {} -> UnkSkol -- Doesn't matter
; req_wrap <- instCall PatOrigin inst_tys req_theta'
; req_wrap <- instCall PatOrigin (mkTyVarTys univ_tvs') req_theta'
; traceTc "instCall" (ppr req_wrap)
; traceTc "checkConstraints {" Outputable.empty
......@@ -848,10 +848,10 @@ matchExpectedPatTy inner_match pat_ty
-- that is the other way round to matchExpectedPatTy
| otherwise
= do { (_, tys, subst) <- tcInstTyVars tvs
; wrap1 <- instCall PatOrigin tys (substTheta subst theta)
= do { (subst, tvs') <- tcInstTyVars tvs
; wrap1 <- instCall PatOrigin (mkTyVarTys tvs') (substTheta subst theta)
; (wrap2, arg_tys) <- matchExpectedPatTy inner_match (TcType.substTy subst tau)
; return (wrap2 <.> wrap1 , arg_tys) }
; return (wrap2 <.> wrap1, arg_tys) }
where
(tvs, theta, tau) = tcSplitSigmaTy pat_ty
......@@ -868,7 +868,7 @@ matchExpectedConTy data_tc pat_ty
| Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc
-- Comments refer to Note [Matching constructor patterns]
-- co_tc :: forall a. T [a] ~ T7 a
= do { (_, tys, subst) <- tcInstTyVars (tyConTyVars data_tc)
= do { (subst, tvs') <- tcInstTyVars (tyConTyVars data_tc)
-- tys = [ty1,ty2]
; traceTc "matchExpectedConTy" (vcat [ppr data_tc,
......@@ -877,10 +877,11 @@ matchExpectedConTy data_tc pat_ty
; co1 <- unifyType (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty
-- co1 : T (ty1,ty2) ~ pat_ty
; let co2 = mkTcUnbranchedAxInstCo Nominal co_tc tys
; let tys' = mkTyVarTys tvs'
co2 = mkTcUnbranchedAxInstCo Nominal co_tc tys'
-- co2 : T (ty1,ty2) ~ T7 ty1 ty2
; return (mkTcSymCo co2 `mkTcTransCo` co1, tys) }
; return (mkTcSymCo co2 `mkTcTransCo` co1, tys') }
| otherwise
= matchExpectedTyConApp data_tc pat_ty
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment