From 1add6282808b5ae98e72ef7034634036c9b91b04 Mon Sep 17 00:00:00 2001 From: Manuel M T Chakravarty Date: Wed, 1 Oct 2008 05:32:43 +0000 Subject: [PATCH] Make sure to zonk the kind of coercion variables MERGE TO 6.10 --- compiler/basicTypes/Var.lhs | 15 ++++----------- compiler/typecheck/Inst.lhs | 2 +- compiler/typecheck/TcHsSyn.lhs | 16 ++++++++++++++-- compiler/typecheck/TcMType.lhs | 27 ++++++++++++++++++++++----- compiler/typecheck/TcPat.lhs | 11 +++-------- compiler/typecheck/TcSimplify.lhs | 25 +++++++++++++------------ 6 files changed, 57 insertions(+), 39 deletions(-) diff --git a/compiler/basicTypes/Var.lhs b/compiler/basicTypes/Var.lhs index eec6c80..ee09c3e 100644 --- a/compiler/basicTypes/Var.lhs +++ b/compiler/basicTypes/Var.lhs @@ -288,7 +288,7 @@ mkTcTyVar name kind details %************************************************************************ \begin{code} -type CoVar = Var -- A coercion variable is simply a type +type CoVar = TyVar -- A coercion variable is simply a type -- variable of kind @ty1 :=: ty2@. Hence its -- 'varType' is always @PredTy (EqPred t1 t2)@ @@ -310,16 +310,9 @@ mkCoVar name kind = ASSERT( isCoercionKind kind ) } mkWildCoVar :: Kind -> TyVar --- ^ Create a type variable that is never referred to, so its unique doesn't matter -mkWildCoVar kind - = ASSERT( isCoercionKind kind ) - TyVar { varName = mkSysTvName wild_uniq (fsLit "co_wild"), - realUnique = _ILIT(1), - varType = kind, - isCoercionVar = True } - where - wild_uniq = mkBuiltinUnique 1 - +-- ^ Create a type variable that is never referred to, so its unique doesn't +-- matter +mkWildCoVar = mkCoVar (mkSysTvName (mkBuiltinUnique 1) (fsLit "co_wild")) \end{code} %************************************************************************ diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index c009ebe..5ad0bed 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -287,7 +287,7 @@ newDictBndr :: InstLoc -> TcPredType -> TcM Inst newDictBndr inst_loc pred@(EqPred ty1 ty2) = do { uniq <- newUnique ; let name = mkPredName uniq inst_loc pred - co = mkGivenCo $ TyVarTy (Var.mkCoVar name (PredTy pred)) + co = mkGivenCo $ TyVarTy (Var.mkCoVar name (PredTy pred)) ; return (EqInst {tci_name = name, tci_loc = inst_loc, tci_left = ty1, diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs index fe9c808..7e15770 100644 --- a/compiler/typecheck/TcHsSyn.lhs +++ b/compiler/typecheck/TcHsSyn.lhs @@ -251,11 +251,22 @@ zonkDictBndrs :: ZonkEnv -> [Var] -> TcM [Var] zonkDictBndrs env ids = mappM (zonkDictBndr env) ids zonkDictBndr :: ZonkEnv -> Var -> TcM Var -zonkDictBndr env var | isTyVar var = return var +zonkDictBndr env var | isTyVar var = zonkTyVarBndr env var | otherwise = zonkIdBndr env var zonkTopBndrs :: [TcId] -> TcM [Id] zonkTopBndrs ids = zonkIdBndrs emptyZonkEnv ids + +-- Zonk the kind of a non-TC tyvar in case it is a coercion variable (their +-- kind contains types). +-- +zonkTyVarBndr :: ZonkEnv -> TyVar -> TcM TyVar +zonkTyVarBndr env tv + | isCoVar tv + = do { kind <- zonkTcTypeToType env (tyVarKind tv) + ; return $ setTyVarKind tv kind + } + | otherwise = return tv \end{code} @@ -607,7 +618,8 @@ 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 ) - return (env, WpTyLam tv) + do { tv' <- zonkTyVarBndr env tv + ; return (env, WpTyLam tv') } zonkCoFn env (WpApp v) | isTcTyVar v = do { co <- zonkTcTyVar v ; return (env, WpTyApp co) } diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 02de940..543c61c 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -763,8 +763,11 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- -- We leave skolem TyVars alone; they are immutable. zonkQuantifiedTyVar tv - | ASSERT( isTcTyVar tv ) - isSkolemTyVar tv = return tv + | ASSERT2( isTcTyVar tv, ppr tv ) + isSkolemTyVar tv + = do { kind <- zonkTcType (tyVarKind tv) + ; return $ setTyVarKind tv kind + } -- It might be a skolem type variable, -- for example from a user type signature @@ -896,12 +899,14 @@ zonkType unbound_var_fn ty -- The two interesting cases! go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar - | otherwise = return (TyVarTy tyvar) + | otherwise = liftM TyVarTy $ + zonkTyVar unbound_var_fn tyvar -- Ordinary (non Tc) tyvars occur inside quantified types go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do ty' <- go ty - return (ForAllTy tyvar ty') + tyvar' <- zonkTyVar unbound_var_fn tyvar + return (ForAllTy tyvar' ty') go_pred (ClassP c tys) = do tys' <- mapM go tys return (ClassP c tys') @@ -911,7 +916,7 @@ zonkType unbound_var_fn ty ty2' <- go ty2 return (EqPred ty1' ty2') -zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable +zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var -> TcTyVar -> TcM TcType zonk_tc_tyvar unbound_var_fn tyvar | not (isMetaTyVar tyvar) -- Skolems @@ -922,6 +927,18 @@ zonk_tc_tyvar unbound_var_fn tyvar ; case cts of Flexi -> unbound_var_fn tyvar -- Unbound meta type variable Indirect ty -> zonkType unbound_var_fn ty } + +-- Zonk the kind of a non-TC tyvar in case it is a coercion variable (their +-- kind contains types). +-- +zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var + -> TyVar -> TcM TyVar +zonkTyVar unbound_var_fn tv + | isCoVar tv + = do { kind <- zonkType unbound_var_fn (tyVarKind tv) + ; return $ setTyVarKind tv kind + } + | otherwise = return tv \end{code} diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index 2e86583..2a2409e 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -617,10 +617,6 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside where uwScrut = unwrapFamInstScrutinee tycon ctxt_res_tys res_pat - ; traceTc $ case sym_coi of - IdCo -> text "sym_coi:IdCo" - ACo co -> text "sym_coi: ACoI" <+> ppr co - -- Add the stupid theta ; addDataConStupidTheta data_con ctxt_res_tys @@ -655,7 +651,7 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside -- ex_tvs was non-null. -- ; unless (null theta') $ -- FIXME: AT THE MOMENT WE CHEAT! We only perform the rigidity test - -- if we explicit or implicit (by a GADT def) have equality + -- if we explicitly or implicitly (by a GADT def) have equality -- constraints. ; let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec] theta' = substTheta tenv (eq_preds ++ full_theta) @@ -665,8 +661,8 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside pstate' | no_equalities = pstate | otherwise = pstate { pat_eqs = True } - ; unless no_equalities (checkTc (isRigidTy pat_ty) - (nonRigidMatch data_con)) + ; unless no_equalities $ + checkTc (isRigidTy pat_ty) (nonRigidMatch data_con) ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $ tcConArgs data_con arg_tys' arg_pats pstate' thing_inside @@ -719,7 +715,6 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside | otherwise = pat - tcConArgs :: DataCon -> [TcSigmaType] -> Checker (HsConPatDetails Name) (HsConPatDetails Id) diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index a274cab..113de25 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -2211,7 +2211,8 @@ Note that reduceImplication env orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc, tci_tyvars = tvs, - tci_given = extra_givens, tci_wanted = wanteds }) + tci_given = extra_givens, tci_wanted = wanteds + }) = do { -- Solve the sub-problem ; let try_me _ = ReduceMe -- Note [Freeness and implications] env' = env { red_givens = extra_givens ++ red_givens env @@ -2225,13 +2226,6 @@ reduceImplication env [ ppr (red_givens env), ppr extra_givens, ppr wanteds]) ; (irreds, binds) <- checkLoop env' wanteds - ; let (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens - -- SLPJ Sept 07: I think this is bogus; currently - -- there are no Eqinsts in extra_givens - dict_ids = map instToId extra_dict_givens - - -- Note [Reducing implication constraints] - -- Tom -- update note, put somewhere! ; traceTc (text "reduceImplication result" <+> vcat [ppr irreds, ppr binds]) @@ -2251,8 +2245,6 @@ reduceImplication env -- we may have instantiated a cotv -- => must make a new implication constraint! - ; traceTc $ text "reduceImplication condition" <+> ppr backOff - -- Progress is no longer measered by the number of bindings ; if backOff then -- No progress -- If there are any irreds, we back off and do nothing @@ -2271,13 +2263,22 @@ reduceImplication env -- equations depending on whether we solve -- dictionary constraints or equational constraints - eq_tyvars = varSetElems $ tyVarsOfTypes $ map eqInstType extra_eq_givens + (extra_eq_givens, extra_dict_givens) + = partition isEqInst extra_givens + -- SLPJ Sept 07: I think this is bogus; currently + -- there are no Eqinsts in extra_givens + dict_ids = map instToId extra_dict_givens + + -- Note [Reducing implication constraints] + -- Tom -- update note, put somewhere! + ; let eq_tyvars = varSetElems $ tyVarsOfTypes $ + map eqInstType extra_eq_givens -- SLPJ Sept07: this looks Utterly Wrong to me, but I think -- that current extra_givens has no EqInsts, so -- it makes no difference co = wrap_inline -- Note [Always inline implication constraints] <.> mkWpTyLams tvs - <.> mkWpLams eq_tyvars + <.> mkWpTyLams eq_tyvars <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind) wrap_inline | null dict_ids = idHsWrapper -- 1.7.10.4