From 79a8b87c0bd61d56b4cf45bd584c9174aab48e61 Mon Sep 17 00:00:00 2001 From: simonpj Date: Tue, 21 Dec 2004 12:23:03 +0000 Subject: [PATCH] [project @ 2004-12-21 12:22:22 by simonpj] --------------------------------- Improve handling of lexically scoped type variables --------------------------------- If we have f :: T a -> a f (x :: T b) = ... then the lexically scoped variable 'b' should refer to the rigid type variable 'a', without any intervening wobbliness. Previously the in-scope type variables were always mutable TyVars, which were instantatiated to point to the type they were bound to; but since the advent of GADTs the intervening mutable type variable is a bad thing. Hence * In the type environment, ATyVar now carries a type * The call to refineTyVars in tc_pat on SigPatIn finds the types by matching * Then tcExtendTyVarEnv3 extends the type envt appropriately Rater a lot of huff and puff, but it's quite natural for ATyVar to contain a type. Various other small nomenclature changes along the way. --- ghc/compiler/coreSyn/Subst.lhs | 10 +++--- ghc/compiler/specialise/Rules.lhs | 4 +-- ghc/compiler/typecheck/Inst.lhs | 4 +-- ghc/compiler/typecheck/TcEnv.lhs | 37 +++++++++++---------- ghc/compiler/typecheck/TcExpr.lhs | 25 +++----------- ghc/compiler/typecheck/TcHsType.lhs | 4 +-- ghc/compiler/typecheck/TcPat.lhs | 59 +++++++++++++++++++++++++++++----- ghc/compiler/typecheck/TcRnTypes.lhs | 13 ++++++-- ghc/compiler/typecheck/TcSplice.lhs | 4 +-- ghc/compiler/typecheck/TcType.lhs | 4 +-- ghc/compiler/typecheck/TcUnify.lhs | 3 ++ ghc/compiler/types/FunDeps.lhs | 8 ++--- ghc/compiler/types/InstEnv.lhs | 8 ++--- ghc/compiler/types/Type.lhs | 23 +++++++------ ghc/compiler/types/Unify.lhs | 46 +++++++++++++------------- 15 files changed, 147 insertions(+), 105 deletions(-) diff --git a/ghc/compiler/coreSyn/Subst.lhs b/ghc/compiler/coreSyn/Subst.lhs index 8a7d9dd..859c1d4 100644 --- a/ghc/compiler/coreSyn/Subst.lhs +++ b/ghc/compiler/coreSyn/Subst.lhs @@ -40,7 +40,7 @@ import CoreUtils ( exprIsTrivial ) import qualified Type ( substTy ) import Type ( Type, tyVarsOfType, mkTyVarTy, - TvSubstEnv, TvSubst(..), substTyVar ) + TvSubstEnv, TvSubst(..), substTyVarBndr ) import VarSet import VarEnv import Var ( setVarUnique, isId, mustHaveLocalBinding ) @@ -431,7 +431,7 @@ simplLetId subst@(Subst in_scope env tvs) old_id -- Extend the substitution if the unique has changed, -- or there's some useful occurrence information - -- See the notes with substTyVar for the delSubstEnv + -- See the notes with substTyVarBndr for the delSubstEnv occ_info = occInfo old_info new_env | new_id /= old_id || isFragileOcc occ_info = extendVarEnv env old_id (DoneId new_id occ_info) @@ -473,9 +473,9 @@ substRecBndrs subst bndrs \begin{code} subst_tv :: Subst -> TyVar -> (Subst, TyVar) --- Unpackage and re-package for substTyVar +-- Unpackage and re-package for substTyVarBndr subst_tv (Subst in_scope id_env tv_env) tv - = case substTyVar (TvSubst in_scope tv_env) tv of + = case substTyVarBndr (TvSubst in_scope tv_env) tv of (TvSubst in_scope' tv_env', tv') -> (Subst in_scope' id_env tv_env', tv') @@ -510,7 +510,7 @@ subst_id keep_fragile rec_subst subst@(Subst in_scope env tvs) old_id new_id = maybeModifyIdInfo (substIdInfo keep_fragile rec_subst) id2 -- Extend the substitution if the unique has changed - -- See the notes with substTyVar for the delSubstEnv + -- See the notes with substTyVarBndr for the delSubstEnv new_env | new_id /= old_id = extendVarEnv env old_id (DoneId new_id (idOccInfo old_id)) | otherwise diff --git a/ghc/compiler/specialise/Rules.lhs b/ghc/compiler/specialise/Rules.lhs index f344d9a..e09dc22 100644 --- a/ghc/compiler/specialise/Rules.lhs +++ b/ghc/compiler/specialise/Rules.lhs @@ -26,7 +26,7 @@ import Var ( Var ) import VarSet import VarEnv import TcType ( TvSubstEnv ) -import Unify ( matchTyX, MatchEnv(..) ) +import Unify ( tcMatchTyX, MatchEnv(..) ) import BasicTypes ( Activation, CompilerPhase, isActive ) import Outputable @@ -324,7 +324,7 @@ We only want to replace (f T) with f', not (f Int). \begin{code} ------------------------------------------ match_ty menv (tv_subst, id_subst) ty1 ty2 - = do { tv_subst' <- Unify.matchTyX menv tv_subst ty1 ty2 + = do { tv_subst' <- Unify.tcMatchTyX menv tv_subst ty1 ty2 ; return (tv_subst', id_subst) } \end{code} diff --git a/ghc/compiler/typecheck/Inst.lhs b/ghc/compiler/typecheck/Inst.lhs index f30ebcb..2f09895 100644 --- a/ghc/compiler/typecheck/Inst.lhs +++ b/ghc/compiler/typecheck/Inst.lhs @@ -67,7 +67,7 @@ import TcType ( Type, TcType, TcThetaType, TcTyVarSet, TcTyVar, pprPred, pprParendType, pprThetaArrow, pprTheta, pprClassPred ) import Type ( substTy, substTys, substTyWith, substTheta, zipTopTvSubst ) -import Unify ( matchTys ) +import Unify ( tcMatchTys ) import Kind ( isSubKind ) import Packages ( isHomeModule ) import HscTypes ( ExternalPackageState(..) ) @@ -583,7 +583,7 @@ addInst dflags home_ie dfun ; let { tys' = substTys tenv tys ; (matches, _) = lookupInstEnv dflags (pkg_ie, home_ie) cls tys' ; dup_dfuns = [dup_dfun | (_, (_, dup_tys, dup_dfun)) <- matches, - isJust (matchTys (mkVarSet tvs) tys' dup_tys)] } + isJust (tcMatchTys (mkVarSet tvs) tys' dup_tys)] } -- Find memebers of the match list which -- dfun itself matches. If the match is 2-way, it's a duplicate ; case dup_dfuns of diff --git a/ghc/compiler/typecheck/TcEnv.lhs b/ghc/compiler/typecheck/TcEnv.lhs index 3aba65f..50f5c2b 100644 --- a/ghc/compiler/typecheck/TcEnv.lhs +++ b/ghc/compiler/typecheck/TcEnv.lhs @@ -17,7 +17,7 @@ module TcEnv( -- Local environment tcExtendKindEnv, - tcExtendTyVarEnv, tcExtendTyVarEnv2, + tcExtendTyVarEnv, tcExtendTyVarEnv2, tcExtendTyVarEnv3, tcExtendIdEnv, tcExtendIdEnv1, tcExtendIdEnv2, tcLookup, tcLookupLocated, tcLookupLocalIds, tcLookupId, tcLookupTyVar, @@ -49,9 +49,9 @@ import HsSyn ( LRuleDecl, LHsBinds, LSig, pprLHsBinds ) import TcIface ( tcImportDecl ) import TcRnMonad import TcMType ( zonkTcType, zonkTcTyVar, zonkTcTyVarsAndFV ) -import TcType ( Type, TcKind, TcTyVar, TcTyVarSet, +import TcType ( Type, TcKind, TcTyVar, TcTyVarSet, TcType, tyVarsOfType, tyVarsOfTypes, tcSplitDFunTy, mkGenTyConApp, - getDFunTyKey, tcTyConAppTyCon, + getDFunTyKey, tcTyConAppTyCon, tcGetTyVar, mkTyVarTy, tidyOpenType, tidyOpenTyVar, pprTyThingCategory ) import qualified Type ( getTyVar_maybe ) @@ -197,12 +197,12 @@ tcLookup name Nothing -> tcLookupGlobal name `thenM` \ thing -> returnM (AGlobal thing) -tcLookupTyVar :: Name -> TcM Id +tcLookupTyVar :: Name -> TcM TcTyVar tcLookupTyVar name = tcLookup name `thenM` \ thing -> case thing of - ATyVar tv -> returnM tv - other -> pprPanic "tcLookupTyVar" (ppr name) + ATyVar _ ty -> returnM (tcGetTyVar "tcLookupTyVar" ty) + other -> pprPanic "tcLookupTyVar" (ppr name) tcLookupId :: Name -> TcM Id -- Used when we aren't interested in the binding level @@ -248,22 +248,25 @@ tcExtendKindEnv things thing_inside tcExtendTyVarEnv :: [TyVar] -> TcM r -> TcM r tcExtendTyVarEnv tvs thing_inside - = tc_extend_tv_env [(getName tv, ATyVar tv) | tv <- tvs] tvs thing_inside + = tc_extend_tv_env [ATyVar tv (mkTyVarTy tv) | tv <- tvs] thing_inside tcExtendTyVarEnv2 :: [(TyVar,TcTyVar)] -> TcM r -> TcM r tcExtendTyVarEnv2 tv_pairs thing_inside - = tc_extend_tv_env [(getName tv1, ATyVar tv2) | (tv1,tv2) <- tv_pairs] - [tv | (_,tv) <- tv_pairs] - thing_inside + = tc_extend_tv_env [ATyVar tv1 (mkTyVarTy tv2) | (tv1,tv2) <- tv_pairs] thing_inside -tc_extend_tv_env binds tyvars thing_inside +tcExtendTyVarEnv3 :: [(TyVar,TcType)] -> TcM r -> TcM r +tcExtendTyVarEnv3 ty_pairs thing_inside + = tc_extend_tv_env [ATyVar tv1 ty2 | (tv1,ty2) <- ty_pairs] thing_inside + +tc_extend_tv_env binds thing_inside = getLclEnv `thenM` \ env@(TcLclEnv {tcl_env = le, tcl_tyvars = gtvs, tcl_rdr = rdr_env}) -> let - le' = extendNameEnvList le binds - rdr_env' = extendLocalRdrEnv rdr_env (map fst binds) - new_tv_set = mkVarSet tyvars + names = [getName tv | ATyVar tv _ <- binds] + rdr_env' = extendLocalRdrEnv rdr_env names + le' = extendNameEnvList le (names `zip` binds) + new_tv_set = tyVarsOfTypes [ty | ATyVar _ ty <- binds] in -- It's important to add the in-scope tyvars to the global tyvar set -- as well. Consider @@ -343,8 +346,8 @@ find_thing ignore_it tidy_env (ATcId id _ _) in returnM (tidy_env', Just msg) -find_thing ignore_it tidy_env (ATyVar tv) - = zonkTcTyVar tv `thenM` \ tv_ty -> +find_thing ignore_it tidy_env (ATyVar tv ty) + = zonkTcType ty `thenM` \ tv_ty -> if ignore_it tv_ty then returnM (tidy_env, Nothing) else let @@ -606,6 +609,6 @@ wrongThingErr expected thing name ptext SLIT("used as a") <+> text expected) where pp_thing (AGlobal thing) = pprTyThingCategory thing - pp_thing (ATyVar _) = ptext SLIT("Type variable") + pp_thing (ATyVar _ _) = ptext SLIT("Type variable") pp_thing (ATcId _ _ _) = ptext SLIT("Local identifier") \end{code} diff --git a/ghc/compiler/typecheck/TcExpr.lhs b/ghc/compiler/typecheck/TcExpr.lhs index 615a4b0..de6ecff 100644 --- a/ghc/compiler/typecheck/TcExpr.lhs +++ b/ghc/compiler/typecheck/TcExpr.lhs @@ -34,8 +34,8 @@ import TcEnv ( tcLookup, tcLookupId, checkProcLevel, import TcArrows ( tcProc ) import TcMatches ( tcMatchesCase, tcMatchLambda, tcDoStmts, tcThingWithSig, TcMatchCtxt(..) ) import TcHsType ( tcHsSigType, UserTypeCtxt(..) ) -import TcPat ( badFieldCon ) -import TcMType ( tcInstTyVars, tcInstType, newTyFlexiVarTy, zonkTcType, readMetaTyVar ) +import TcPat ( badFieldCon, refineTyVars ) +import TcMType ( tcInstTyVars, tcInstType, newTyFlexiVarTy, zonkTcType ) import TcType ( Type, TcTyVar, TcType, TcSigmaType, TcRhoType, MetaDetails(..), tcSplitFunTys, tcSplitTyConApp, mkTyVarTys, isSigmaTy, mkFunTy, mkTyConApp, tyVarsOfTypes, isLinearPred, @@ -634,7 +634,8 @@ tcApp fun args res_ty Infer _ -> do -- Type check args first, then -- refine result type, then do tcResult { the_app' <- tcArgs fun fun' args expected_arg_tys - ; actual_res_ty' <- refineResultTy fun_tvs actual_res_ty + ; subst <- refineTyVars fun_tvs + ; let actual_res_ty' = substTy subst actual_res_ty ; co_fn <- tcResult fun args res_ty actual_res_ty' ; traceTc (text "tcApp: infer" <+> vcat [ppr fun <+> ppr args, ppr the_app', ppr actual_res_ty, ppr actual_res_ty']) @@ -722,24 +723,6 @@ checkArgsCtxt fun args (Check expected_res_ty) actual_res_ty tidy_env | otherwise = appCtxt fun args in returnM (env2, message) - ----------------- -refineResultTy :: [TcTyVar] -- Newly instantiated meta-tyvars of the function - -> TcType -- Result type, instantiated with those tyvars - -> TcM TcType -- Refined result type --- De-wobblify the result type, by taking account what we learned --- from type-checking the arguments. Just one level of de-wobblification --- though. What a hack! -refineResultTy tvs res_ty - = do { mb_prs <- mapM mk_pr tvs - ; let subst = mkTopTvSubst (catMaybes mb_prs) - ; return (substTy subst res_ty) } - where - mk_pr tv = do { details <- readMetaTyVar tv - ; case details of - Indirect ty -> return (Just (tv,ty)) - other -> return Nothing - } \end{code} diff --git a/ghc/compiler/typecheck/TcHsType.lhs b/ghc/compiler/typecheck/TcHsType.lhs index 21b9b48..e25d0ad 100644 --- a/ghc/compiler/typecheck/TcHsType.lhs +++ b/ghc/compiler/typecheck/TcHsType.lhs @@ -392,7 +392,7 @@ kcTyVar name -- Could be a tyvar or a tycon tcLookup name `thenM` \ thing -> traceTc (text "lk2" <+> ppr name <+> ppr thing) `thenM_` case thing of - ATyVar tv -> returnM (tyVarKind tv) + ATyVar tv _ -> returnM (tyVarKind tv) AThing kind -> returnM kind AGlobal (ATyCon tc) -> returnM (tyConKind tc) other -> wrongThingErr "type" thing name @@ -500,7 +500,7 @@ ds_var_app :: Name -> [Type] -> TcM Type ds_var_app name arg_tys = tcLookup name `thenM` \ thing -> case thing of - ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys) + ATyVar _ ty -> returnM (mkAppTys ty arg_tys) AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys) -- AThing _ -> tcLookupTyCon name `thenM` \ tc -> -- returnM (mkGenTyConApp tc arg_tys) diff --git a/ghc/compiler/typecheck/TcPat.lhs b/ghc/compiler/typecheck/TcPat.lhs index 77de074..2d84f05 100644 --- a/ghc/compiler/typecheck/TcPat.lhs +++ b/ghc/compiler/typecheck/TcPat.lhs @@ -4,7 +4,7 @@ \section[TcPat]{Typechecking patterns} \begin{code} -module TcPat ( tcPat, tcPats, PatCtxt(..), badFieldCon, polyPatSig ) where +module TcPat ( tcPat, tcPats, PatCtxt(..), badFieldCon, polyPatSig, refineTyVars ) where #include "HsVersions.h" @@ -20,18 +20,20 @@ import Inst ( InstOrigin(..), import Id ( Id, idType, mkLocalId ) import Name ( Name ) import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns ) -import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv, +import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv3, tcLookupClass, tcLookupDataCon, tcLookupId ) -import TcMType ( newTyFlexiVarTy, arityErr, tcSkolTyVars ) +import TcMType ( newTyFlexiVarTy, arityErr, tcSkolTyVars, readMetaTyVar ) import TcType ( TcType, TcTyVar, TcSigmaType, TcTauType, zipTopTvSubst, SkolemInfo(PatSkol), isSkolemTyVar, pprSkolemTyVar, + TvSubst, mkTvSubst, substTyVar, substTy, MetaDetails(..), mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy ) +import VarEnv ( mkVarEnv ) -- ugly import Kind ( argTypeKind, liftedTypeKind ) import TcUnify ( tcSubPat, Expected(..), zapExpectedType, zapExpectedTo, zapToListTy, zapToTyConApp ) import TcHsType ( UserTypeCtxt(..), TcSigInfo( sig_tau ), TcSigFun, tcHsPatSigType ) import TysWiredIn ( stringTy, parrTyCon, tupleTyCon ) -import Unify ( MaybeErr(..), tcRefineTys, tcMatchTys ) +import Unify ( MaybeErr(..), gadtRefineTys, gadtMatchTys ) import Type ( substTys, substTheta ) import CmdLineOpts ( opt_IrrefutableTuples ) import TyCon ( TyCon ) @@ -41,6 +43,7 @@ import PrelNames ( eqStringName, eqName, geName, negateName, minusName, integralClassName ) import BasicTypes ( isBoxed ) import SrcLoc ( Located(..), SrcSpan, noLoc, unLoc, getLoc ) +import Maybes ( catMaybes ) import ErrUtils ( Message ) import Outputable import FastString @@ -241,8 +244,13 @@ tc_pat ctxt (SigPatIn pat sig) pat_ty thing_inside = do { -- See Note [Pattern coercions] below (sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig ; tcSubPat sig_ty pat_ty - ; (pat', tvs, res) <- tcExtendTyVarEnv sig_tvs $ - tc_lpat ctxt pat (Check sig_ty) thing_inside + ; subst <- refineTyVars sig_tvs -- See note [Type matching] + ; let tv_binds = [(tv, substTyVar subst tv) | tv <- sig_tvs] + sig_ty' = substTy subst sig_ty + ; (pat', tvs, res) + <- tcExtendTyVarEnv3 tv_binds $ + tc_lpat ctxt pat (Check sig_ty') thing_inside + ; return (SigPatOut pat' sig_ty, tvs, res) } tc_pat ctxt pat@(TypePat ty) pat_ty thing_inside @@ -492,8 +500,8 @@ refineAlt :: PatCtxt -> DataCon -> TcM a -> TcM a refineAlt ctxt con ex_tvs ctxt_tys pat_tys thing_inside = do { old_subst <- getTypeRefinement - ; let refiner | can_i_refine ctxt = tcRefineTys - | otherwise = tcMatchTys + ; let refiner | can_i_refine ctxt = gadtRefineTys + | otherwise = gadtMatchTys ; case refiner ex_tvs old_subst pat_tys ctxt_tys of Failed msg -> failWithTc (inaccessibleAlt msg) Succeeded new_subst -> do { @@ -505,6 +513,41 @@ refineAlt ctxt con ex_tvs ctxt_tys pat_tys thing_inside can_i_refine other_ctxt = False \end{code} +Note [Type matching] +~~~~~~~~~~~~~~~~~~~~ +This little function @refineTyVars@ is a little tricky. Suppose we have a pattern type +signature + f = \(x :: Term a) -> body +Then 'a' should be bound to a wobbly type. But if we have + f :: Term b -> some-type + f = \(x :: Term a) -> body +then 'a' should be bound to the rigid type 'b'. So we want to + * instantiate the type sig with fresh meta tyvars (e.g. \alpha) + * unify with the type coming from the context + * read out whatever information has been gleaned + from that unificaiton (e.g. unifying \alpha with 'b') + * and replace \alpha by 'b' in the type, when typechecking the + pattern inside the type sig (x in this case) +It amounts to combining rigid info from the context and from the sig. + +Exactly the same thing happens for 'smart function application'. + +\begin{code} +refineTyVars :: [TcTyVar] -- Newly instantiated meta-tyvars of the function + -> TcM TvSubst -- Substitution mapping any of the meta-tyvars that + -- has been unifies to what it was instantiated to +-- Just one level of de-wobblification though. What a hack! +refineTyVars tvs + = do { mb_prs <- mapM mk_pr tvs + ; return (mkTvSubst (mkVarEnv (catMaybes mb_prs))) } + where + mk_pr tv = do { details <- readMetaTyVar tv + ; case details of + Indirect ty -> return (Just (tv,ty)) + other -> return Nothing + } +\end{code} + %************************************************************************ %* * Note [Pattern coercions] diff --git a/ghc/compiler/typecheck/TcRnTypes.lhs b/ghc/compiler/typecheck/TcRnTypes.lhs index 3b71b1d..ed1fb86 100644 --- a/ghc/compiler/typecheck/TcRnTypes.lhs +++ b/ghc/compiler/typecheck/TcRnTypes.lhs @@ -48,7 +48,7 @@ import HscTypes ( FixityEnv, GenAvailInfo(..), AvailInfo, availName, IsBootInterface, Deprecations ) import Packages ( PackageId ) -import Type ( Type, TvSubstEnv ) +import Type ( Type, TvSubstEnv, pprParendType ) import TcType ( TcTyVarSet, TcType, TcTauType, TcThetaType, SkolemInfo, TcPredType, TcKind, tcCmpPred, tcCmpType, tcCmpTypes ) import InstEnv ( DFunId, InstEnv ) @@ -386,15 +386,22 @@ topArrowCtxt = ArrCtxt { proc_level = topProcLevel, proc_banned = [] } data TcTyThing = AGlobal TyThing -- Used only in the return type of a lookup + | ATcId TcId ThLevel ProcLevel -- Ids defined in this module; may not be fully zonked - | ATyVar TyVar -- Type variables + + | ATyVar TyVar TcType -- Type variables; tv -> type. It can't just be a TyVar + -- that is mutated to point to the type it is bound to, + -- because that would make it a wobbly type, and we + -- want pattern-bound lexically-scoped type variables to + -- be able to stand for rigid types + | AThing TcKind -- Used temporarily, during kind checking, for the -- tycons and clases in this recursive group instance Outputable TcTyThing where -- Debugging only ppr (AGlobal g) = text "AGlobal" <+> ppr g ppr (ATcId g tl pl) = text "ATcId" <+> ppr g <+> ppr tl <+> ppr pl - ppr (ATyVar t) = text "ATyVar" <+> ppr t + ppr (ATyVar tv ty) = text "ATyVar" <+> ppr tv <+> pprParendType ty ppr (AThing k) = text "AThing" <+> ppr k \end{code} diff --git a/ghc/compiler/typecheck/TcSplice.lhs b/ghc/compiler/typecheck/TcSplice.lhs index 0a7ae7f..b5e13f7 100644 --- a/ghc/compiler/typecheck/TcSplice.lhs +++ b/ghc/compiler/typecheck/TcSplice.lhs @@ -556,8 +556,8 @@ reifyThing (ATcId id _ _) ; fix <- reifyFixity (idName id) ; return (TH.VarI (reifyName id) ty2 Nothing fix) } -reifyThing (ATyVar tv) - = do { ty1 <- zonkTcTyVar tv +reifyThing (ATyVar tv ty) + = do { ty1 <- zonkTcType ty ; ty2 <- reifyType ty1 ; return (TH.TyVarI (reifyName tv) ty2) } diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index 187ac27..93ba131 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -97,7 +97,7 @@ module TcType ( mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst, getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, extendTvSubst, extendTvSubstList, isInScope, - substTy, substTys, substTyWith, substTheta, substTyVar, + substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr, isUnLiftedType, -- Source types are always lifted isUnboxedTupleType, -- Ditto @@ -149,7 +149,7 @@ import Type ( -- Re-exports mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst, getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, extendTvSubst, extendTvSubstList, isInScope, - substTy, substTys, substTyWith, substTheta, substTyVar, + substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr, typeKind, repType, pprKind, pprParendKind, diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index 87b30c6..179a7db 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -383,6 +383,9 @@ tcSubPat :: TcSigmaType -- Pattern type signature -> TcM () -- In patterns we insist on an exact match; hence no CoFn returned -- See Note [Pattern coercions] in TcPat +-- However, we can't call unify directly, because both types might be +-- polymorphic; hence the call to tcSub, followed by a check for +-- the identity coercion tcSubPat sig_ty (Infer hole) = do { sig_ty' <- zonkTcType sig_ty diff --git a/ghc/compiler/types/FunDeps.lhs b/ghc/compiler/types/FunDeps.lhs index 8ec4084..f74663c 100644 --- a/ghc/compiler/types/FunDeps.lhs +++ b/ghc/compiler/types/FunDeps.lhs @@ -16,7 +16,7 @@ module FunDeps ( import Name ( getSrcLoc ) import Var ( Id, TyVar ) import Class ( Class, FunDep, classTvsFds ) -import Unify ( unifyTys, unifyTysX ) +import Unify ( tcUnifyTys, tcUnifyTysX ) import Type ( mkTvSubst, substTy ) import TcType ( Type, ThetaType, PredType(..), tcEqType, predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred ) @@ -302,10 +302,10 @@ checkClsFD qtvs fd clas_tvs tys1 tys2 -- The same function is also used from InstEnv.badFunDeps, when we need -- to *unify*; in which case the qtvs are the variables of both ls1 and ls2. -- However unifying with the qtvs being the left-hand lot *is* just matching, --- so we can call unifyTys in both cases - = case unifyTys qtvs ls1 ls2 of +-- so we can call tcUnifyTys in both cases + = case tcUnifyTys qtvs ls1 ls2 of Nothing -> [] - Just unif | maybeToBool (unifyTysX qtvs unif rs1 rs2) + Just unif | maybeToBool (tcUnifyTysX qtvs unif rs1 rs2) -- 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 diff --git a/ghc/compiler/types/InstEnv.lhs b/ghc/compiler/types/InstEnv.lhs index e7a7d8a..cc1c445 100644 --- a/ghc/compiler/types/InstEnv.lhs +++ b/ghc/compiler/types/InstEnv.lhs @@ -23,7 +23,7 @@ import Type ( TvSubstEnv ) import TcType ( Type, tcTyConAppTyCon, tcIsTyVarTy, tcSplitDFunTy, tyVarsOfTypes, isExistentialTyVar ) -import Unify ( matchTys, unifyTys ) +import Unify ( tcMatchTys, tcUnifyTys ) import FunDeps ( checkClsFD ) import TyCon ( TyCon ) import Outputable @@ -336,7 +336,7 @@ lookup_inst_env env key_cls key_tys key_all_tvs find [] ms us = (ms, us) find (item@(tpl_tyvars, tpl, dfun_id) : rest) ms us - = case matchTys tpl_tyvars tpl key_tys of + = case tcMatchTys tpl_tyvars tpl key_tys of Just subst -> find rest ((subst,item):ms) us Nothing -- Does not match, so next check whether the things unify @@ -347,7 +347,7 @@ lookup_inst_env env key_cls key_tys key_all_tvs ) -- Unification will break badly if the variables overlap -- They shouldn't because we allocate separate uniques for them - case unifyTys (key_vars `unionVarSet` tpl_tyvars) key_tys tpl of + case tcUnifyTys (key_vars `unionVarSet` tpl_tyvars) key_tys tpl of Just _ -> find rest ms (dfun_id:us) Nothing -> find rest ms us @@ -369,7 +369,7 @@ insert_overlapping new_item (item:items) old_beats_new = item `beats` new_item (_, (tvs1, tys1, _)) `beats` (_, (tvs2, tys2, _)) - = isJust (matchTys tvs2 tys2 tys1) -- A beats B if A is more specific than B + = isJust (tcMatchTys tvs2 tys2 tys1) -- A beats B if A is more specific than B -- I.e. if B can be instantiated to match A \end{code} diff --git a/ghc/compiler/types/Type.lhs b/ghc/compiler/types/Type.lhs index d3b87ff..f4f020b 100644 --- a/ghc/compiler/types/Type.lhs +++ b/ghc/compiler/types/Type.lhs @@ -70,7 +70,7 @@ module Type ( extendTvSubst, extendTvSubstList, isInScope, -- Performing substitution on types - substTy, substTys, substTyWith, substTheta, substTyVar, + substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr, deShadowTy, -- Pretty-printing @@ -994,7 +994,7 @@ instance Ord PredType where { compare = tcCmpPred } \begin{code} data TvSubst = TvSubst InScopeSet -- The in-scope type variables - TvSubstEnv -- The substitution itself; guaranteed idempotent + TvSubstEnv -- The substitution itself -- See Note [Apply Once] {- ---------------------------------------------------------- @@ -1138,13 +1138,10 @@ substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys) -- Note that the in_scope set is poked only if we hit a forall -- so it may often never be fully computed -subst_ty subst@(TvSubst in_scope env) ty +subst_ty subst ty = go ty where - go ty@(TyVarTy tv) = case (lookupVarEnv env tv) of - Nothing -> ty - Just ty' -> ty' -- See Note [Apply Once] - + go (TyVarTy tv) = substTyVar subst tv go (TyConApp tc tys) = let args = map go tys in args `seqList` TyConApp tc args @@ -1158,11 +1155,17 @@ subst_ty subst@(TvSubst in_scope env) ty -- The mkAppTy smart constructor is important -- we might be replacing (a Int), represented with App -- by [Int], represented with TyConApp - go (ForAllTy tv ty) = case substTyVar subst tv of + go (ForAllTy tv ty) = case substTyVarBndr subst tv of (subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty) -substTyVar :: TvSubst -> TyVar -> (TvSubst, TyVar) -substTyVar subst@(TvSubst in_scope env) old_var +substTyVar :: TvSubst -> TyVar -> Type +substTyVar (TvSubst in_scope env) tv + = case (lookupVarEnv env tv) of + Nothing -> TyVarTy tv + Just ty' -> ty' -- See Note [Apply Once] + +substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar) +substTyVarBndr subst@(TvSubst in_scope env) old_var | old_var == new_var -- No need to clone -- But we *must* zap any current substitution for the variable. -- For example: diff --git a/ghc/compiler/types/Unify.lhs b/ghc/compiler/types/Unify.lhs index 0143235..004d003 100644 --- a/ghc/compiler/types/Unify.lhs +++ b/ghc/compiler/types/Unify.lhs @@ -1,11 +1,11 @@ \begin{code} module Unify ( -- Matching and unification - matchTys, matchTyX, tcMatchPreds, MatchEnv(..), + tcMatchTys, tcMatchTyX, tcMatchPreds, MatchEnv(..), - unifyTys, unifyTysX, + tcUnifyTys, tcUnifyTysX, - tcRefineTys, tcMatchTys, coreRefineTys, + gadtRefineTys, gadtMatchTys, coreRefineTys, -- Re-export MaybeErr(..) @@ -13,6 +13,7 @@ module Unify ( #include "HsVersions.h" +import Type ( pprParendType ) import Var ( Var, TyVar, tyVarKind ) import VarEnv import VarSet @@ -62,13 +63,13 @@ data MatchEnv , me_env :: RnEnv2 -- Renaming envt for nested foralls } -- In-scope set includes template tyvars -matchTys :: TyVarSet -- Template tyvars +tcMatchTys :: TyVarSet -- Template tyvars -> [Type] -- Template -> [Type] -- Target -> Maybe TvSubstEnv -- One-shot; in principle the template -- variables could be free in the target -matchTys tmpls tys1 tys2 +tcMatchTys tmpls tys1 tys2 = match_tys (ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope_tyvars}) emptyTvSubstEnv tys1 tys2 @@ -87,13 +88,13 @@ tcMatchPreds tmpls ps1 ps2 menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars } in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2) -matchTyX :: MatchEnv +tcMatchTyX :: MatchEnv -> TvSubstEnv -- Substitution to extend -> Type -- Template -> Type -- Target -> Maybe TvSubstEnv -matchTyX menv subst ty1 ty2 = match menv subst ty1 ty2 -- Rename for export +tcMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2 -- Rename for export \end{code} Now the internals of matching @@ -182,51 +183,48 @@ match_pred menv subst p1 p2 = Nothing %************************************************************************ \begin{code} -tcRefineTys, tcMatchTys +gadtRefineTys, gadtMatchTys :: [TyVar] -- Try to unify these -> TvSubstEnv -- Not idempotent -> [Type] -> [Type] -> MaybeErr Message TvSubstEnv -- Not idempotent -- This one is used by the type checker. Neither the input nor result -- substitition is idempotent -tcRefineTys ex_tvs subst tys1 tys2 +gadtRefineTys ex_tvs subst tys1 tys2 = initUM (tryToBind (mkVarSet ex_tvs)) (unify_tys subst tys1 tys2) -tcMatchTys ex_tvs subst tys1 tys2 +gadtMatchTys ex_tvs subst tys1 tys2 = initUM (bindOnly (mkVarSet ex_tvs)) (unify_tys subst tys1 tys2) ---------------------------- coreRefineTys :: [TyVar] -- Try to unify these -> TvSubst -- A full-blown apply-once substitition - -> Type -- A fixed point of the incoming substitution - -> Type + -> Type -- Both types should be a fixed point + -> Type -- of the incoming substitution -> Maybe TvSubstEnv -- In-scope set is unaffected -- Used by Core Lint and the simplifier. Takes a full apply-once substitution. -- The incoming substitution's in-scope set should mention all the variables free -- in the incoming types coreRefineTys ex_tvs subst@(TvSubst in_scope orig_env) ty1 ty2 = maybeErrToMaybe $ initUM (tryToBind (mkVarSet ex_tvs)) $ - do { -- Apply the input substitution; nothing int ty2 - let ty1' = substTy subst ty1 - -- Run the unifier, starting with an empty env - ; extra_env <- unify emptyTvSubstEnv ty1' ty2 + do { -- Run the unifier, starting with an empty env + ; extra_env <- unify emptyTvSubstEnv ty1 ty2 -- Find the fixed point of the resulting non-idempotent - -- substitution, and apply it to the + -- substitution, and apply it to the incoming substitution ; let extra_subst = TvSubst in_scope extra_env_fixpt extra_env_fixpt = mapVarEnv (substTy extra_subst) extra_env orig_env' = mapVarEnv (substTy extra_subst) orig_env ; return (orig_env' `plusVarEnv` extra_env_fixpt) } - ---------------------------- -unifyTys :: TyVarSet -> [Type] -> [Type] -> Maybe TvSubstEnv -unifyTys bind_these tys1 tys2 +tcUnifyTys :: TyVarSet -> [Type] -> [Type] -> Maybe TvSubstEnv +tcUnifyTys bind_these tys1 tys2 = maybeErrToMaybe $ initUM (bindOnly bind_these) $ unify_tys emptyTvSubstEnv tys1 tys2 -unifyTysX :: TyVarSet -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv -unifyTysX bind_these subst tys1 tys2 +tcUnifyTysX :: TyVarSet -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv +tcUnifyTysX bind_these subst tys1 tys2 = maybeErrToMaybe $ initUM (bindOnly bind_these) $ unify_tys subst tys1 tys2 @@ -258,8 +256,10 @@ unify :: TvSubstEnv -- An existing substitution to extend -- nor guarantee that the outgoing one is. That's fixed up by -- the wrappers. +-- Respects newtypes, PredTypes + unify subst ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> pprParendType ty2) $ - unify_ subst ty1 ty2 + unify_ subst ty1 ty2 -- in unify_, any NewTcApps/Preds should be taken at face value unify_ subst (TyVarTy tv1) ty2 = uVar False subst tv1 ty2 -- 1.7.10.4