X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=23c3381581a2dd4a62b1b1e9597bf8e335e7f161;hb=ef47b5c2f44fce638b623c9cf5bb2f7f62ba619d;hp=fa129d3927fd04c2a6beb0372160927c648cca42;hpb=0065d5ab628975892cea1ec7303f968c3338cbe1;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index fa129d3..23c3381 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -23,8 +23,12 @@ module TcMType ( newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, -------------------------------- + -- Creating new coercion variables + newCoVars, + + -------------------------------- -- Instantiation - tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar, + tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, tcInstSigTyVars, zonkSigTyVar, tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, tcSkolSigType, tcSkolSigTyVars, @@ -58,11 +62,11 @@ import TypeRep ( Type(..), PredType(..), -- Friend; can see representation import TcType ( TcType, TcThetaType, TcTauType, TcPredType, TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), MetaDetails(..), SkolemInfo(..), BoxInfo(..), - BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType, - UserTypeCtxt(..), - isMetaTyVar, isSigTyVar, metaTvRef, + BoxyTyVar, BoxyType, UserTypeCtxt(..), kindVarRef, + mkKindVar, isMetaTyVar, isSigTyVar, metaTvRef, tcCmpPred, isClassPred, tcGetTyVar, - tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, + tcSplitPhiTy, tcSplitPredTy_maybe, + tcSplitAppTy_maybe, tcValidInstHeadTy, tcSplitForAllTys, tcIsTyVarTy, tcSplitSigmaTy, isUnLiftedType, isIPPred, @@ -71,21 +75,23 @@ import TcType ( TcType, TcThetaType, TcTauType, TcPredType, tyVarsOfPred, getClassPredTys_maybe, tyVarsOfType, tyVarsOfTypes, tcView, pprPred, pprTheta, pprClassPred ) -import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar, - isLiftedTypeKind, isArgTypeKind, isOpenTypeKind, +import Type ( Kind, KindVar, + isLiftedTypeKind, isSubArgTypeKind, isSubOpenTypeKind, liftedTypeKind, defaultKind ) import Type ( TvSubst, zipTopTvSubst, substTy ) +import Coercion ( mkCoKind ) import Class ( Class, classArity, className ) import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon, tyConArity, tyConName ) import Var ( TyVar, tyVarKind, tyVarName, isTcTyVar, - mkTyVar, mkTcTyVar, tcTyVarDetails ) + mkTyVar, mkTcTyVar, tcTyVarDetails, + CoVar, mkCoVar ) -- Assertions #ifdef DEBUG import TcType ( isFlexi, isBoxyTyVar, isImmutableTyVar ) -import Kind ( isSubKind ) +import Type ( isSubKind ) #endif -- others: @@ -96,10 +102,12 @@ import VarSet import DynFlags ( dopt, DynFlag(..) ) import Util ( nOfThem, isSingleton, notNull ) import ListSetOps ( removeDups ) +import UniqSupply ( uniqsFromSupply ) import Outputable import Control.Monad ( when ) import Data.List ( (\\) ) + \end{code} @@ -140,10 +148,17 @@ tcInstType inst_tyvars ty %************************************************************************ \begin{code} +newCoVars :: [(TcType,TcType)] -> TcM [CoVar] +newCoVars spec + = do { us <- newUniqueSupply + ; return [ mkCoVar (mkSysTvName uniq FSLIT("co")) + (mkCoKind ty1 ty2) + | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] } + newKindVar :: TcM TcKind newKindVar = do { uniq <- newUnique - ; ref <- newMutVar Nothing - ; return (KindVar (mkKindVar uniq ref)) } + ; ref <- newMutVar Flexi + ; return (mkTyVarTy (mkKindVar uniq ref)) } newKindVars :: Int -> TcM [TcKind] newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ()) @@ -201,9 +216,13 @@ newMetaTyVar box_info kind ; ref <- newMutVar Flexi ; ; let name = mkSysTvName uniq fs fs = case box_info of - BoxTv -> FSLIT("bx") + BoxTv -> FSLIT("t") TauTv -> FSLIT("t") SigTv _ -> FSLIT("a") + -- We give BoxTv and TauTv the same string, because + -- otherwise we get user-visible differences in error + -- messages, which are confusing. If you want to see + -- the box_info of each tyvar, use -dppr-debug ; return (mkTcTyVar name kind (MetaTv box_info ref)) } instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar @@ -327,12 +346,6 @@ readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv ) tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar -- Instantiate with a BOXY type variable tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar - -tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType) --- tcInstType instantiates the outer-level for-alls of a TcType with --- fresh BOXY type variables, splits off the dictionary part, --- and returns the pieces. -tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty \end{code} @@ -445,6 +458,10 @@ zonkTcPredType (ClassP c ts) zonkTcPredType (IParam n t) = zonkTcType t `thenM` \ new_t -> returnM (IParam n new_t) +zonkTcPredType (EqPred t1 t2) + = zonkTcType t1 `thenM` \ new_t1 -> + zonkTcType t2 `thenM` \ new_t2 -> + returnM (EqPred new_t1 new_t2) \end{code} ------------------- These ...ToType, ...ToKind versions @@ -569,10 +586,13 @@ zonkType unbound_var_fn ty go ty `thenM` \ ty' -> returnM (ForAllTy tyvar ty') - go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' -> - returnM (ClassP c tys') - go_pred (IParam n ty) = go ty `thenM` \ ty' -> - returnM (IParam n ty') + go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' -> + returnM (ClassP c tys') + go_pred (IParam n ty) = go ty `thenM` \ ty' -> + returnM (IParam n ty') + go_pred (EqPred ty1 ty2) = go ty1 `thenM` \ ty1' -> + go ty2 `thenM` \ ty2' -> + returnM (EqPred ty1' ty2') zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable -> TcTyVar -> TcM TcType @@ -596,35 +616,20 @@ zonk_tc_tyvar unbound_var_fn tyvar %************************************************************************ \begin{code} -readKindVar :: KindVar -> TcM (Maybe TcKind) +readKindVar :: KindVar -> TcM (MetaDetails) writeKindVar :: KindVar -> TcKind -> TcM () readKindVar kv = readMutVar (kindVarRef kv) -writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val) +writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val) ------------- zonkTcKind :: TcKind -> TcM TcKind -zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1 - ; k2' <- zonkTcKind k2 - ; returnM (FunKind k1' k2') } -zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv - ; case mb_kind of - Nothing -> returnM k - Just k -> zonkTcKind k } -zonkTcKind other_kind = returnM other_kind +zonkTcKind k = zonkTcType k ------------- zonkTcKindToKind :: TcKind -> TcM Kind -zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1 - ; k2' <- zonkTcKindToKind k2 - ; returnM (FunKind k1' k2') } - -zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv - ; case mb_kind of - Nothing -> return liftedTypeKind - Just k -> zonkTcKindToKind k } - -zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to * -zonkTcKindToKind other_kind = returnM other_kind +-- When zonking a TcKind to a kind, we need to instantiate kind variables, +-- Haskell specifies that * is to be used, so we follow that. +zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k \end{code} %************************************************************************ @@ -689,11 +694,11 @@ checkValidType ctxt ty kind_ok = case ctxt of TySynCtxt _ -> True -- Any kind will do - ResSigCtxt -> isOpenTypeKind actual_kind - ExprSigCtxt -> isOpenTypeKind actual_kind + ResSigCtxt -> isSubOpenTypeKind actual_kind + ExprSigCtxt -> isSubOpenTypeKind actual_kind GenPatCtxt -> isLiftedTypeKind actual_kind ForSigCtxt _ -> isLiftedTypeKind actual_kind - other -> isArgTypeKind actual_kind + other -> isSubArgTypeKind actual_kind ubx_tup | not gla_exts = UT_NotOk | otherwise = case ctxt of @@ -731,14 +736,16 @@ check_poly_type (Rank 0) ubx_tup ty = check_tau_type (Rank 0) ubx_tup ty check_poly_type rank ubx_tup ty - = let - (tvs, theta, tau) = tcSplitSigmaTy ty - in - check_valid_theta SigmaCtxt theta `thenM_` - check_tau_type (decRank rank) ubx_tup tau `thenM_` - checkFreeness tvs theta `thenM_` - checkAmbiguity tvs theta (tyVarsOfType tau) - + | null tvs && null theta + = check_tau_type rank ubx_tup ty + | otherwise + = do { check_valid_theta SigmaCtxt theta + ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow + ; checkFreeness tvs theta + ; checkAmbiguity tvs theta (tyVarsOfType tau) } + where + (tvs, theta, tau) = tcSplitSigmaTy ty + ---------------------------------------- check_arg_type :: Type -> TcM () -- The sort of type that can instantiate a type variable, @@ -777,12 +784,12 @@ check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty -- The Right Thing would be to fix the way that SPECIALISE instance pragmas -- are handled, but the quick thing is just to permit PredTys here. check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags -> - check_source_ty dflags TypeCtxt sty + check_pred_ty dflags TypeCtxt sty check_tau_type rank ubx_tup (TyVarTy _) = returnM () check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty) - = check_poly_type rank UT_NotOk arg_ty `thenM_` - check_poly_type rank UT_Ok res_ty + = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_` + check_poly_type rank UT_Ok res_ty check_tau_type rank ubx_tup (AppTy ty1 ty2) = check_arg_type ty1 `thenM_` check_arg_type ty2 @@ -889,12 +896,12 @@ check_valid_theta ctxt [] check_valid_theta ctxt theta = getDOpts `thenM` \ dflags -> warnTc (notNull dups) (dupPredWarn dups) `thenM_` - mappM_ (check_source_ty dflags ctxt) theta + mappM_ (check_pred_ty dflags ctxt) theta where (_,dups) = removeDups tcCmpPred theta ------------------------- -check_source_ty dflags ctxt pred@(ClassP cls tys) +check_pred_ty dflags ctxt pred@(ClassP cls tys) = -- Class predicates are valid in all contexts checkTc (arity == n_tys) arity_err `thenM_` @@ -910,7 +917,7 @@ check_source_ty dflags ctxt pred@(ClassP cls tys) arity_err = arityErr "Class" class_name arity n_tys how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this")) -check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty +check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty -- Implicit parameters only allows in type -- signatures; not in instance decls, superclasses etc -- The reason for not allowing implicit params in instances is a bit subtle @@ -921,7 +928,7 @@ check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty -- instance decl would show up two uses of ?x. -- Catch-all -check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty) +check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty) ------------------------- check_class_pred_tys dflags ctxt tys @@ -1025,7 +1032,7 @@ checkThetaCtxt ctxt theta = vcat [ptext SLIT("In the context:") <+> pprTheta theta, ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ] -badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty +badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"), nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)] dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups) @@ -1185,6 +1192,7 @@ fvTypes tys = concat (map fvType tys) fvPred :: PredType -> [TyVar] fvPred (ClassP _ tys') = fvTypes tys' fvPred (IParam _ ty) = fvType ty +fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2 -- Size of a type: the number of variables and constructors sizeType :: Type -> Int @@ -1203,4 +1211,5 @@ sizeTypes xs = sum (map sizeType xs) sizePred :: PredType -> Int sizePred (ClassP _ tys') = sizeTypes tys' sizePred (IParam _ ty) = sizeType ty +sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 \end{code}