From 3787d9878e4d62829a555f01b2a4c5866f24f303 Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Mon, 7 Jan 2008 14:23:06 +0000 Subject: [PATCH] Make the treatment of equalities more uniform This patch (which is part of the fix for Trac #2018) makes coercion variables be handled more uniformly. Generally, they are treated like dictionaries in the type checker, not like type variables, but in a couple of places we were treating them like type variables. Also when zonking we should use zonkDictBndr not zonkIdBndr. --- compiler/hsSyn/HsBinds.lhs | 4 ++-- compiler/hsSyn/HsPat.lhs | 7 ++++--- compiler/typecheck/TcHsSyn.lhs | 4 ++-- compiler/typecheck/TcMType.lhs | 1 + compiler/typecheck/TcSimplify.lhs | 2 +- compiler/typecheck/TcTyFuns.lhs | 2 +- compiler/typecheck/TcType.lhs | 4 +--- compiler/typecheck/TcUnify.lhs | 2 +- compiler/types/FamInstEnv.lhs | 2 +- compiler/types/TypeRep.lhs | 37 ++++++++++++++++++++++--------------- 10 files changed, 36 insertions(+), 29 deletions(-) diff --git a/compiler/hsSyn/HsBinds.lhs b/compiler/hsSyn/HsBinds.lhs index 2fa2959..90442df 100644 --- a/compiler/hsSyn/HsBinds.lhs +++ b/compiler/hsSyn/HsBinds.lhs @@ -343,8 +343,8 @@ data HsWrapper | WpApp Var -- [] d the 'd' is a type-class dictionary | WpTyApp Type -- [] t the 't' is a type or corecion - | WpLam Id -- \d. [] the 'd' is a type-class dictionary - | WpTyLam TyVar -- \a. [] the 'a' is a type or coercion variable + | WpLam Var -- \d. [] the 'd' is a type-class dictionary or coercion variable + | WpTyLam TyVar -- \a. [] the 'a' is a type variable (not coercion var) | WpInline -- inline_me [] Wrap inline around the thing -- Non-empty bindings, so that the identity coercion diff --git a/compiler/hsSyn/HsPat.lhs b/compiler/hsSyn/HsPat.lhs index a524ab8..87f4717 100644 --- a/compiler/hsSyn/HsPat.lhs +++ b/compiler/hsSyn/HsPat.lhs @@ -97,9 +97,10 @@ data Pat id | ConPatOut { pat_con :: Located DataCon, - pat_tvs :: [TyVar], -- Existentially bound type variables - -- including any bound coercion variables - pat_dicts :: [id], -- Ditto dictionaries + pat_tvs :: [TyVar], -- Existentially bound type variables (tyvars only) + pat_dicts :: [id], -- Ditto *coercion variables* and *dictionaries* + -- One reason for putting coercion variable here, I think, + -- is to ensure their kinds are zonked pat_binds :: DictBinds id, -- Bindings involving those dictionaries pat_args :: HsConPatDetails id, pat_ty :: Type -- The type of the pattern diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs index ff5c942..bd3cb8c 100644 --- a/compiler/typecheck/TcHsSyn.lhs +++ b/compiler/typecheck/TcHsSyn.lhs @@ -550,7 +550,7 @@ zonkCoFn env (WpCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1 ; return (env2, WpCompose c1' c2') } zonkCoFn env (WpCo co) = do { co' <- zonkTcTypeToType env co ; return (env, WpCo co') } -zonkCoFn env (WpLam id) = do { id' <- zonkIdBndr env id +zonkCoFn env (WpLam id) = do { id' <- zonkDictBndr env id ; let env1 = extendZonkEnv1 env id' ; return (env1, WpLam id') } zonkCoFn env (WpTyLam tv) = ASSERT( isImmutableTyVar tv ) @@ -776,7 +776,7 @@ zonk_pat env (TuplePat pats boxed ty) zonk_pat env p@(ConPatOut { pat_ty = ty, pat_dicts = dicts, pat_binds = binds, pat_args = args }) = ASSERT( all isImmutableTyVar (pat_tvs p) ) do { new_ty <- zonkTcTypeToType env ty - ; new_dicts <- zonkIdBndrs env dicts + ; new_dicts <- zonkDictBndrs env dicts ; let env1 = extendZonkEnv env new_dicts ; (env2, new_binds) <- zonkRecMonoBinds env1 binds ; (env', new_args) <- zonkConStuff env2 args diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index f1f9082..f7cbb2c 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -104,6 +104,7 @@ import Data.List ( (\\) ) tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables -> TcType -- Type to instantiate -> TcM ([TcTyVar], TcThetaType, TcType) -- Result + -- (type vars (excl coercion vars), preds (incl equalities), rho) tcInstType inst_tyvars ty = case tcSplitForAllTys ty of ([], rho) -> let -- There may be overloading despite no type variables; diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 433266e..be9d70d 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -2207,7 +2207,7 @@ reduceImplication env -- it makes no difference co = wrap_inline -- Note [Always inline implication constraints] <.> mkWpTyLams tvs - <.> mkWpTyLams eq_tyvars + <.> mkWpLams eq_tyvars <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind) wrap_inline | null dict_ids = idHsWrapper diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index ca3c4a8..706fe2f 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -233,7 +233,7 @@ tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1) } tcGenericNormaliseFamInst fun (NoteTy note ty1) = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1 - ; return (mkNoteTyCoI note coi, NoteTy note nty1) + ; return (coi, NoteTy note nty1) } tcGenericNormaliseFamInst fun ty@(TyVarTy tv) | isTcTyVar tv diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs index 625f855..165018d 100644 --- a/compiler/typecheck/TcType.lhs +++ b/compiler/typecheck/TcType.lhs @@ -670,9 +670,7 @@ tcSplitPhiTy ty = split ty ty [] split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs split orig_ty (ForAllTy tv ty) ts - | isCoVar tv = split ty ty (eq_pred:ts) - where - PredTy eq_pred = tyVarKind tv + | isCoVar tv = split ty ty (coVarPred tv : ts) split orig_ty (FunTy arg res) ts | Just p <- tcSplitPredTy_maybe arg = split res res (p:ts) split orig_ty ty ts = (reverse ts, orig_ty) diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 0893850..1acef7c 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -924,7 +924,7 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall -- list of "free vars" for the signature check. ; loc <- getInstLoc (SigOrigin skol_info) - ; dicts <- newDictBndrs loc theta' + ; dicts <- newDictBndrs loc theta' -- Includes equalities ; inst_binds <- tcSimplifyCheck loc tvs' dicts lie ; checkSigTyVarsWrt free_tvs tvs' diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs index a9e1548..12df25d 100644 --- a/compiler/types/FamInstEnv.lhs +++ b/compiler/types/FamInstEnv.lhs @@ -437,7 +437,7 @@ normaliseType env ty@(ForAllTy tyvar ty1) in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1) normaliseType env ty@(NoteTy note ty1) = let (coi,nty1) = normaliseType env ty1 - in (mkNoteTyCoI note coi,NoteTy note nty1) + in (coi,NoteTy note nty1) normaliseType env ty@(TyVarTy _) = (IdCo,ty) normaliseType env (PredTy predty) diff --git a/compiler/types/TypeRep.lhs b/compiler/types/TypeRep.lhs index c694dc8..69ee419 100644 --- a/compiler/types/TypeRep.lhs +++ b/compiler/types/TypeRep.lhs @@ -31,6 +31,7 @@ module TypeRep ( argTypeKind, ubxTupleKind, isLiftedTypeKindCon, isLiftedTypeKind, mkArrowKind, mkArrowKinds, isCoercionKind, + coVarPred, -- Kind constructors... liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon, @@ -412,6 +413,13 @@ isCoercionKind :: Kind -> Bool isCoercionKind (NoteTy _ k) = isCoercionKind k isCoercionKind (PredTy (EqPred {})) = True isCoercionKind other = False + +coVarPred :: CoVar -> PredType +coVarPred tv + = ASSERT( isCoVar tv ) + case tyVarKind tv of + PredTy eq -> eq -- There shouldn't even be a NoteTy in the way + other -> pprPanic "coVarPred" (ppr tv $$ ppr other) \end{code} @@ -484,7 +492,7 @@ pprParendKind = pprParendType ppr_type :: Prec -> Type -> SDoc ppr_type p (TyVarTy tv) = ppr tv ppr_type p (PredTy pred) = ifPprDebug (ptext SLIT("")) <> (ppr pred) -ppr_type p (NoteTy other ty2) = ppr_type p ty2 +ppr_type p (NoteTy other ty2) = ifPprDebug (ptext SLIT("")) <> ppr_type p ty2 ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $ @@ -504,28 +512,27 @@ ppr_type p (FunTy ty1 ty2) ppr_forall_type :: Prec -> Type -> SDoc ppr_forall_type p ty = maybeParen p FunPrec $ - sep [pprForAll tvs, pprThetaArrow (ctxt1 ++ ctxt2), pprType tau] + sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau] where - (tvs, ctxt1, rho) = split1 [] [] ty - (ctxt2, tau) = split2 [] rho + (tvs, rho) = split1 [] ty + (ctxt, tau) = split2 [] rho -- We need to be extra careful here as equality constraints will occur as -- type variables with an equality kind. So, while collecting quantified -- variables, we separate the coercion variables out and turn them into -- equality predicates. - split1 tvs eqs (ForAllTy tv ty) - | isCoVar tv = split1 tvs (eq:eqs) ty - | otherwise = split1 (tv:tvs) eqs ty - where - PredTy eq = tyVarKind tv - split1 tvs eqs (NoteTy _ ty) = split1 tvs eqs ty - split1 tvs eqs ty = (reverse tvs, reverse eqs, ty) + split1 tvs (ForAllTy tv ty) + | not (isCoVar tv) = split1 (tv:tvs) ty + split1 tvs (NoteTy _ ty) = split1 tvs ty + split1 tvs ty = (reverse tvs, ty) split2 ps (NoteTy _ arg -- Rather a disgusting case - `FunTy` res) = split2 ps (arg `FunTy` res) - split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty - split2 ps (NoteTy _ ty) = split2 ps ty - split2 ps ty = (reverse ps, ty) + `FunTy` res) = split2 ps (arg `FunTy` res) + split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty + split2 ps (ForAllTy tv ty) + | isCoVar tv = split2 (coVarPred tv : ps) ty + split2 ps (NoteTy _ ty) = split2 ps ty + split2 ps ty = (reverse ps, ty) ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc ppr_tc_app p tc [] -- 1.7.10.4