X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=02eba6dde5b89afb41b53732a3062df783ae0406;hb=25bff7fe1a22edbafa188af8d844c67057fa5eb8;hp=a81270e6c763c3286ef2aaded784c3cb6adb1b79;hpb=c1e6031c54cda2c6f9fc107eb6cb04ab490f1fef;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index a81270e..02eba6d 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -28,14 +28,13 @@ module TcMType ( newWantedCoVar, writeWantedCoVar, readWantedCoVar, newIP, newDict, newSelfDict, isSelfDict, - newWantedEvVar, newWantedEvVars, - newKindConstraint, + newWantedEvVar, newWantedEvVars, newTcEvBinds, addTcEvBind, -------------------------------- -- Instantiation tcInstTyVar, tcInstTyVars, tcInstSigTyVars, - tcInstType, tcInstSigType, + tcInstType, tcInstSigType, instMetaTyVar, tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType, tcSkolSigType, tcSkolSigTyVars, @@ -51,7 +50,7 @@ module TcMType ( -------------------------------- -- Zonking zonkType, mkZonkTcTyVar, zonkTcPredType, - zonkTcTypeCarefully, + zonkTcTypeCarefully, skolemiseUnboundMetaTyVar, zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar, zonkQuantifiedTyVar, zonkQuantifiedTyVars, zonkTcType, zonkTcTypes, zonkTcThetaType, @@ -135,17 +134,6 @@ newWantedEvVars theta = mapM newWantedEvVar theta newWantedCoVar :: TcType -> TcType -> TcM CoVar newWantedCoVar ty1 ty2 = newCoVar ty1 ty2 --- We used to create a mutable co-var -{- --- A wanted coercion variable is a MetaTyVar --- that can be filled in with its binding - = do { uniq <- newUnique - ; ref <- newMutVar Flexi - ; let name = mkSysTvName uniq (fsLit "c") - kind = mkPredTy (EqPred ty1 ty2) - ; return (mkTcTyVar name kind (MetaTv TauTv ref)) } --} - -------------- newEvVar :: TcPredType -> TcM EvVar -- Creates new *rigid* variables for predicates @@ -175,15 +163,6 @@ newName occ ; return (mkInternalName uniq occ loc) } ----------------- -newKindConstraint :: Type -> Kind -> TcM (CoVar, Type) --- Create a new wanted CoVar that constrains the type --- to have the specified kind -newKindConstraint ty kind - = do { ty_k <- newFlexiTyVarTy kind - ; co_var <- newWantedCoVar ty ty_k - ; return (co_var, ty_k) } - ------------------ newSelfDict :: Class -> [TcType] -> TcM DictId -- Make a dictionary for "self". It behaves just like a normal DictId -- except that it responds True to isSelfDict @@ -300,11 +279,12 @@ tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv) newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar -- Make a new meta tyvar out of thin air newMetaTyVar meta_info kind - = do { uniq <- newUnique + = do { uniq <- newMetaUnique ; ref <- newMutVar Flexi ; let name = mkSysTvName uniq fs fs = case meta_info of TauTv -> fsLit "t" + TcsTv -> fsLit "u" SigTv _ -> fsLit "a" ; return (mkTcTyVar name kind (MetaTv meta_info ref)) } @@ -312,7 +292,7 @@ instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar -- Make a new meta tyvar whose Name and Kind -- come from an existing TyVar instMetaTyVar meta_info tyvar - = do { uniq <- newUnique + = do { uniq <- newMetaUnique ; ref <- newMutVar Flexi ; let name = setNameUnique (tyVarName tyvar) uniq kind = tyVarKind tyvar @@ -469,7 +449,7 @@ tcGetGlobalTyVars :: TcM TcTyVarSet tcGetGlobalTyVars = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv ; gbl_tvs <- readMutVar gtv_var - ; gbl_tvs' <- zonkTcTyVarsAndFV (varSetElems gbl_tvs) + ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs ; writeMutVar gtv_var gbl_tvs' ; return gbl_tvs' } \end{code} @@ -480,8 +460,8 @@ tcGetGlobalTyVars zonkTcTyVars :: [TcTyVar] -> TcM [TcType] zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars -zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet -zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar tyvars +zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet +zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars) ----------------- Types @@ -500,9 +480,9 @@ zonkTcTypeCarefully ty SkolemTv {} -> return (TyVarTy tv) FlatSkol ty -> zonkType (zonk_tv env_tvs) ty MetaTv _ ref -> do { cts <- readMutVar ref - ; case cts of - Flexi -> return (TyVarTy tv) - Indirect ty -> zonkType (zonk_tv env_tvs) ty } + ; case cts of + Flexi -> return (TyVarTy tv) + Indirect ty -> zonkType (zonk_tv env_tvs) ty } zonkTcType :: TcType -> TcM TcType -- Simply look through all Flexis @@ -516,9 +496,9 @@ zonkTcTyVar tv SkolemTv {} -> return (TyVarTy tv) FlatSkol ty -> zonkTcType ty MetaTv _ ref -> do { cts <- readMutVar ref - ; case cts of - Flexi -> return (TyVarTy tv) - Indirect ty -> zonkTcType ty } + ; case cts of + Flexi -> return (TyVarTy tv) + Indirect ty -> zonkTcType ty } zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType -- Zonk, and simultaneously apply a non-necessarily-idempotent substitution @@ -526,12 +506,12 @@ zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty where zonk_tv tv = case tcTyVarDetails tv of - SkolemTv {} -> return (TyVarTy tv) - FlatSkol ty -> zonkType zonk_tv ty - MetaTv _ ref -> do { cts <- readMutVar ref - ; case cts of - Flexi -> zonk_flexi tv - Indirect ty -> zonkType zonk_tv ty } + SkolemTv {} -> return (TyVarTy tv) + FlatSkol ty -> zonkType zonk_tv ty + MetaTv _ ref -> do { cts <- readMutVar ref + ; case cts of + Flexi -> zonk_flexi tv + Indirect ty -> zonkType zonk_tv ty } zonk_flexi tv = case lookupTyVar subst tv of Just ty -> zonkType zonk_tv ty @@ -557,8 +537,6 @@ zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar] zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar --- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it. --- -- The quantified type variables often include meta type variables -- we want to freeze them into ordinary type variables, and -- default their kind (e.g. from OpenTypeKind to TypeKind) @@ -569,45 +547,49 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- -- We leave skolem TyVars alone; they are immutable. zonkQuantifiedTyVar tv - | ASSERT2( isTcTyVar tv, ppr tv ) - isSkolemTyVar tv - = do { kind <- zonkTcType (tyVarKind tv) - ; return $ setTyVarKind tv kind - } + = ASSERT2( isTcTyVar tv, ppr tv ) + case tcTyVarDetails tv of + FlatSkol {} -> pprPanic "zonkQuantifiedTyVar" (ppr tv) + SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv) + ; return $ setTyVarKind tv kind } -- It might be a skolem type variable, -- for example from a user type signature - | otherwise -- It's a meta-type-variable - = do { details <- readMetaTyVar tv - - -- Create the new, frozen, skolem type variable - -- We zonk to a skolem, not to a regular TcVar - -- See Note [Zonking to Skolem] + MetaTv _ _ref -> +#ifdef DEBUG + -- [Sept 04] Check for non-empty. + -- See note [Silly Type Synonym] + (readMutVar _ref >>= \cts -> + case cts of + Flexi -> return () + Indirect ty -> WARN( True, ppr tv $$ ppr ty ) + return ()) >> +#endif + skolemiseUnboundMetaTyVar UnkSkol tv + +skolemiseUnboundMetaTyVar :: SkolemInfo -> TcTyVar -> TcM TyVar +-- We have a Meta tyvar with a ref-cell inside it +-- Skolemise it, including giving it a new Name, so that +-- we are totally out of Meta-tyvar-land +-- We create a skolem TyVar, not a regular TyVar +-- See Note [Zonking to Skolem] +skolemiseUnboundMetaTyVar skol_info tv + = ASSERT2( isMetaTyVar tv, ppr tv ) + do { uniq <- newUnique -- Remove it from TcMetaTyVar unique land ; let final_kind = defaultKind (tyVarKind tv) - final_tv = mkSkolTyVar (tyVarName tv) final_kind UnkSkol - - -- Bind the meta tyvar to the new tyvar - ; case details of - Indirect ty -> WARN( True, ppr tv $$ ppr ty ) - return () - -- [Sept 04] I don't think this should happen - -- See note [Silly Type Synonym] - - Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv) - - -- Return the new tyvar + final_name = setNameUnique (tyVarName tv) uniq + final_tv = mkSkolTyVar final_name final_kind skol_info + ; writeMetaTyVar tv (mkTyVarTy final_tv) ; return final_tv } \end{code} \begin{code} zonkImplication :: Implication -> TcM Implication -zonkImplication implic@(Implic { ic_env_tvs = env_tvs, ic_given = given +zonkImplication implic@(Implic { ic_given = given , ic_wanted = wanted }) - = do { env_tvs' <- zonkTcTyVarsAndFV (varSetElems env_tvs) - ; given' <- mapM zonkEvVar given + = do { given' <- mapM zonkEvVar given ; wanted' <- mapBagM zonkWanted wanted - ; return (implic { ic_env_tvs = env_tvs', ic_given = given' - , ic_wanted = wanted' }) } + ; return (implic { ic_given = given', ic_wanted = wanted' }) } zonkEvVar :: EvVar -> TcM EvVar zonkEvVar var = do { ty' <- zonkTcType (varType var) @@ -702,10 +684,8 @@ simplifier knows how to deal with. -- For tyvars bound at a for-all, zonkType zonks them to an immutable -- type variable and zonks the kind too -zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables - -- see zonkTcType, and zonkTcTypeToType - -> TcType - -> TcM Type +zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars + -> TcType -> TcM Type zonkType zonk_tc_tyvar ty = go ty where @@ -745,17 +725,17 @@ zonkType zonk_tc_tyvar ty ty2' <- go ty2 return (EqPred ty1' ty2') -mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var +mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var -> TcTyVar -> TcM TcType mkZonkTcTyVar unbound_var_fn tyvar = ASSERT( isTcTyVar tyvar ) case tcTyVarDetails tyvar of - SkolemTv {} -> return (TyVarTy tyvar) - FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty - MetaTv _ ref -> do { cts <- readMutVar ref - ; case cts of - Flexi -> unbound_var_fn tyvar - Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty } + SkolemTv {} -> return (TyVarTy tyvar) + FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty + MetaTv _ ref -> do { cts <- readMutVar ref + ; case cts of + Flexi -> unbound_var_fn tyvar + Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty } -- Zonk the kind of a non-TC tyvar in case it is a coercion variable -- (their kind contains types). @@ -1155,10 +1135,12 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys) how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this")) -check_pred_ty dflags _ pred@(EqPred ty1 ty2) +check_pred_ty dflags ctxt pred@(EqPred ty1 ty2) = do { -- Equational constraints are valid in all contexts if type -- families are permitted ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred) + ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True) + (eqSuperClassErr pred) -- Check the form of the argument types ; checkValidMonoType ty1 @@ -1315,11 +1297,16 @@ checkThetaCtxt ctxt theta = vcat [ptext (sLit "In the context:") <+> pprTheta theta, ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ] +eqSuperClassErr :: PredType -> SDoc +eqSuperClassErr pred + = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:")) + 2 (ppr pred) + badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc -badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty -eqPredTyErr sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty - $$ - parens (ptext (sLit "Use -XTypeFamilies to permit this")) +badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPred pred +eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPred pred + $$ + parens (ptext (sLit "Use -XTypeFamilies to permit this")) predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"), nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)] dupPredWarn :: [[PredType]] -> SDoc @@ -1632,14 +1619,12 @@ sizeTypes xs = sum (map sizeType xs) -- Size of a predicate -- --- Equalities are a special case. The equality itself doesn't contribute to the --- size and as we do not count class predicates, we have to start with one less. --- This is easy to see considering that, given --- class C a b | a -> b --- type family F a --- constraints (C a b) and (F a ~ b) are equivalent in size. +-- We are considering whether *class* constraints terminate +-- Once we get into an implicit parameter or equality we +-- can't get back to a class constraint, so it's safe +-- to say "size 0". See Trac #4200. sizePred :: PredType -> Int sizePred (ClassP _ tys') = sizeTypes tys' -sizePred (IParam _ ty) = sizeType ty -sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 - 1 +sizePred (IParam {}) = 0 +sizePred (EqPred {}) = 0 \end{code}