X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcType.lhs;h=a825d23b04771b65af95af0384aa0ea399571846;hp=c68c10ffa6ed0b980f8979df32549255296a814c;hb=HEAD;hpb=3e0a7b9fbc16e432efa562df027d189fa274943a diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs index c68c10f..a825d23 100644 --- a/compiler/typecheck/TcType.lhs +++ b/compiler/typecheck/TcType.lhs @@ -19,18 +19,17 @@ module TcType ( -------------------------------- -- Types TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, - TcTyVar, TcTyVarSet, TcKind, TcCoVar, + TcCoercion, TcTyVar, TcTyVarSet, TcKind, TcCoVar, -------------------------------- -- MetaDetails UserTypeCtxt(..), pprUserTypeCtxt, - TcTyVarDetails(..), pprTcTyVarDetails, + TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv, MetaDetails(Flexi, Indirect), MetaInfo(..), - SkolemInfo(..), pprSkolTvBinding, pprSkolInfo, isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isSigTyVar, isOverlappableTyVar, isTyConableTyVar, metaTvRef, - isFlexi, isIndirect, isUnkSkol, isRuntimeUnkSkol, + isFlexi, isIndirect, isRuntimeUnkSkol, -------------------------------- -- Builders @@ -51,9 +50,9 @@ module TcType ( --------------------------------- -- Predicates. -- Again, newtypes are opaque - tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX, + eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX, eqKind, - isSigmaTy, isOverloadedTy, isRigidTy, + isSigmaTy, isOverloadedTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy, isIntegerTy, isBoolTy, isUnitTy, isCharTy, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, @@ -62,19 +61,12 @@ module TcType ( --------------------------------- -- Misc type manipulators deNoteType, - tyClsNamesOfType, tyClsNamesOfDFunHead, + orphNamesOfType, orphNamesOfDFunHead, orphNamesOfCo, getDFunTyKey, --------------------------------- -- Predicate types - getClassPredTys_maybe, getClassPredTys, - isClassPred, isTyVarClassPred, isEqPred, - mkClassPred, mkIPPred, tcSplitPredTy_maybe, - mkDictTy, evVarPred, - isPredTy, isDictTy, isDictLikeTy, - tcSplitDFunTy, tcSplitDFunHead, predTyUnique, - isIPPred, - isRefineableTy, isRefineablePred, + mkMinimalBySCs, transSuperClasses, immSuperClasses, -- * Tidying type related things up for printing tidyType, tidyTypes, @@ -82,7 +74,8 @@ module TcType ( tidyTyVarBndr, tidyFreeTyVars, tidyOpenTyVar, tidyOpenTyVars, tidyTopType, tidyPred, - tidyKind, tidySkolemTyVar, + tidyKind, + tidyCo, tidyCos, --------------------------------- -- Foreign import and export @@ -102,32 +95,38 @@ module TcType ( tcSplitIOType_maybe, -- :: Type -> Maybe Type -------------------------------- - -- Rexported from Coercion - typeKind, - - -------------------------------- - -- Rexported from Type - Kind, -- Stuff to do with kinds is insensitive to pre/post Tc + -- Rexported from Kind + Kind, typeKind, unliftedTypeKind, liftedTypeKind, argTypeKind, openTypeKind, mkArrowKind, mkArrowKinds, isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind, isSubArgTypeKind, isSubKind, splitKindFunTys, defaultKind, kindVarRef, mkKindVar, - Type, PredType(..), ThetaType, + -------------------------------- + -- Rexported from Type + Type, Pred(..), PredType, ThetaType, mkForAllTy, mkForAllTys, mkFunTy, mkFunTys, zipFunTys, mkTyConApp, mkAppTy, mkAppTys, applyTy, applyTys, mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys, + getClassPredTys_maybe, getClassPredTys, + isClassPred, isTyVarClassPred, isEqPred, + mkClassPred, mkIPPred, splitPredTy_maybe, + mkDictTy, isPredTy, isDictTy, isDictLikeTy, + tcSplitDFunTy, tcSplitDFunHead, + isIPPred, mkEqPred, + -- Type substitutions TvSubst(..), -- Representation visible to a few friends - TvSubstEnv, emptyTvSubst, substEqSpec, + TvSubstEnv, emptyTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst, unionTvSubst, - getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, lookupTyVar, - extendTvSubst, extendTvSubstList, isInScope, mkTvSubst, zipTyEnv, - substTy, substTys, substTyWith, substTheta, substTyVar, substTyVars, substTyVarBndr, + getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, + Type.lookupTyVar, Type.extendTvSubst, Type.substTyVarBndr, + extendTvSubstList, isInScope, mkTvSubst, zipTyEnv, + Type.substTy, substTys, substTyWith, substTheta, substTyVar, substTyVars, isUnLiftedType, -- Source types are always lifted isUnboxedTupleType, -- Ditto @@ -139,15 +138,15 @@ module TcType ( pprKind, pprParendKind, pprType, pprParendType, pprTypeApp, pprTyThingCategory, - pprPred, pprTheta, pprThetaArrow, pprClassPred + pprPred, pprTheta, pprThetaArrow, pprThetaArrowTy, pprClassPred ) where #include "HsVersions.h" -- friends: +import Kind import TypeRep -import DataCon import Class import Var import ForeignCall @@ -155,11 +154,10 @@ import VarSet import Type import Coercion import TyCon -import HsExpr( HsMatchContext ) -- others: import DynFlags -import Name +import Name hiding (varName) import NameSet import VarEnv import PrelNames @@ -219,6 +217,8 @@ type TcType = Type -- A TcType can have mutable type variables -- a cannot occur inside a MutTyVar in T; that is, -- T is "flattened" before quantifying over a +type TcCoercion = Coercion -- A TcCoercion can contain TcTypes. + -- These types do not have boxy type variables in them type TcPredType = PredType type TcThetaType = ThetaType @@ -265,7 +265,7 @@ the same type variable in both type signatures. But that takes explanation. The alternative (currently implemented) is to have a special kind of skolem constant, SigTv, which can unify with other SigTvs. These are *not* treated -as righd for the purposes of GADTs. And they are used *only* for pattern +as rigid for the purposes of GADTs. And they are used *only* for pattern bindings and mutually recursive function bindings. See the function TcBinds.tcInstSig, and its use_skols parameter. @@ -273,9 +273,15 @@ TcBinds.tcInstSig, and its use_skols parameter. \begin{code} -- A TyVarDetails is inside a TyVar data TcTyVarDetails - = SkolemTv SkolemInfo -- A skolem constant + = SkolemTv -- A skolem + Bool -- True <=> this skolem type variable can be overlapped + -- when looking up instances + -- See Note [Binding when looking up instances] in InstEnv + + | RuntimeUnk -- Stands for an as-yet-unknown type in the GHCi + -- interactive context - | FlatSkol TcType + | FlatSkol TcType -- The "skolem" obtained by flattening during -- constraint simplification @@ -285,67 +291,41 @@ data TcTyVarDetails | MetaTv MetaInfo (IORef MetaDetails) +vanillaSkolemTv, superSkolemTv :: TcTyVarDetails +-- See Note [Binding when looking up instances] in InstEnv +vanillaSkolemTv = SkolemTv False -- Might be instantiated +superSkolemTv = SkolemTv True -- Treat this as a completely distinct type + data MetaDetails = Flexi -- Flexi type variables unify to become Indirects | Indirect TcType -data MetaInfo +instance Outputable MetaDetails where + ppr Flexi = ptext (sLit "Flexi") + ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty + +data MetaInfo = TauTv -- This MetaTv is an ordinary unification variable -- A TauTv is always filled in with a tau-type, which -- never contains any ForAlls - | SigTv Name -- A variant of TauTv, except that it should not be + | SigTv -- A variant of TauTv, except that it should not be -- unified with a type, only with a type variable -- SigTvs are only distinguished to improve error messages -- see Note [Signature skolems] -- The MetaDetails, if filled in, will -- always be another SigTv or a SkolemTv - -- The Name is the name of the function from whose - -- type signature we got this skolem | TcsTv -- A MetaTv allocated by the constraint solver -- Its particular property is that it is always "touchable" -- Nevertheless, the constraint solver has to try to guess -- what type to instantiate it to ----------------------------------- --- SkolemInfo describes a site where --- a) type variables are skolemised --- b) an implication constraint is generated -data SkolemInfo - = SigSkol UserTypeCtxt -- A skolem that is created by instantiating - -- a programmer-supplied type signature - -- Location of the binding site is on the TyVar - - -- The rest are for non-scoped skolems - | ClsSkol Class -- Bound at a class decl - | InstSkol -- Bound at an instance decl - | FamInstSkol -- Bound at a family instance decl - | PatSkol -- An existential type variable bound by a pattern for - DataCon -- a data constructor with an existential type. - (HsMatchContext Name) - -- e.g. data T = forall a. Eq a => MkT a - -- f (MkT x) = ... - -- The pattern MkT x will allocate an existential type - -- variable for 'a'. - - | ArrowSkol -- An arrow form (see TcArrows) - - | IPSkol [IPName Name] -- Binding site of an implicit parameter - - | RuleSkol RuleName -- The LHS of a RULE - | GenSkol TcType -- Bound when doing a subsumption check for ty - - | RuntimeUnkSkol -- a type variable used to represent an unknown - -- runtime type (used in the GHCi debugger) - - | UnkSkol -- Unhelpful info (until I improve it) - ------------------------------------- --- UserTypeCtxt describes the places where a --- programmer-written type signature can occur --- Like SkolemInfo, no location info -data UserTypeCtxt +-- UserTypeCtxt describes the origin of the polymorphic type +-- in the places where we need to an expression has that type + +data UserTypeCtxt = FunSigCtxt Name -- Function type signature -- Also used for types in SPECIALISE pragmas | ExprSigCtxt -- Expression type signature @@ -364,6 +344,10 @@ data UserTypeCtxt | SpecInstCtxt -- SPECIALISE instance pragma | ThBrackCtxt -- Template Haskell type brackets [t| ... |] + | GenSigCtxt -- Higher-rank or impredicative situations + -- e.g. (f e) where f has a higher-rank type + -- We might want to elaborate this + -- Notes re TySynCtxt -- We allow type synonyms that aren't types; e.g. type List = [] -- @@ -409,11 +393,12 @@ kind_var_occ = mkOccName tvName "k" \begin{code} pprTcTyVarDetails :: TcTyVarDetails -> SDoc -- For debugging -pprTcTyVarDetails (SkolemTv _) = ptext (sLit "sk") -pprTcTyVarDetails (FlatSkol {}) = ptext (sLit "fsk") -pprTcTyVarDetails (MetaTv TauTv _) = ptext (sLit "tau") -pprTcTyVarDetails (MetaTv TcsTv _) = ptext (sLit "tcs") -pprTcTyVarDetails (MetaTv (SigTv _) _) = ptext (sLit "sig") +pprTcTyVarDetails (SkolemTv {}) = ptext (sLit "sk") +pprTcTyVarDetails (RuntimeUnk {}) = ptext (sLit "rt") +pprTcTyVarDetails (FlatSkol {}) = ptext (sLit "fsk") +pprTcTyVarDetails (MetaTv TauTv _) = ptext (sLit "tau") +pprTcTyVarDetails (MetaTv TcsTv _) = ptext (sLit "tcs") +pprTcTyVarDetails (MetaTv SigTv _) = ptext (sLit "sig") pprUserTypeCtxt :: UserTypeCtxt -> SDoc pprUserTypeCtxt (FunSigCtxt n) = ptext (sLit "the type signature for") <+> quotes (ppr n) @@ -428,53 +413,7 @@ pprUserTypeCtxt ResSigCtxt = ptext (sLit "a result type signature") pprUserTypeCtxt (ForSigCtxt n) = ptext (sLit "the foreign declaration for") <+> quotes (ppr n) pprUserTypeCtxt DefaultDeclCtxt = ptext (sLit "a type in a `default' declaration") pprUserTypeCtxt SpecInstCtxt = ptext (sLit "a SPECIALISE instance pragma") - -pprSkolTvBinding :: TcTyVar -> SDoc --- Print info about the binding of a skolem tyvar, --- or nothing if we don't have anything useful to say -pprSkolTvBinding tv - = ASSERT ( isTcTyVar tv ) - quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv) - where - ppr_details (SkolemTv info) = ppr_skol info - ppr_details (FlatSkol {}) = ptext (sLit "is a flattening type variable") - ppr_details (MetaTv (SigTv n) _) = ptext (sLit "is bound by the type signature for") - <+> quotes (ppr n) - ppr_details (MetaTv _ _) = ptext (sLit "is a meta type variable") - - ppr_skol UnkSkol = ptext (sLit "is an unknown type variable") -- Unhelpful - ppr_skol RuntimeUnkSkol = ptext (sLit "is an unknown runtime type") - ppr_skol info = sep [ptext (sLit "is a rigid type variable bound by"), - sep [pprSkolInfo info, - nest 2 (ptext (sLit "at") <+> ppr (getSrcLoc tv))]] - -instance Outputable SkolemInfo where - ppr = pprSkolInfo - -pprSkolInfo :: SkolemInfo -> SDoc --- Complete the sentence "is a rigid type variable bound by..." -pprSkolInfo (SigSkol ctxt) = pprUserTypeCtxt ctxt -pprSkolInfo (IPSkol ips) = ptext (sLit "the implicit-parameter bindings for") - <+> pprWithCommas ppr ips -pprSkolInfo (ClsSkol cls) = ptext (sLit "the class declaration for") <+> quotes (ppr cls) -pprSkolInfo InstSkol = ptext (sLit "the instance declaration") -pprSkolInfo FamInstSkol = ptext (sLit "the family instance declaration") -pprSkolInfo (RuleSkol name) = ptext (sLit "the RULE") <+> doubleQuotes (ftext name) -pprSkolInfo ArrowSkol = ptext (sLit "the arrow form") -pprSkolInfo (PatSkol dc _) = sep [ ptext (sLit "a pattern with constructor") - , ppr dc <+> dcolon <+> ppr (dataConUserType dc) ] -pprSkolInfo (GenSkol ty) = sep [ ptext (sLit "the polymorphic type") - , quotes (ppr ty) ] - --- UnkSkol --- For type variables the others are dealt with by pprSkolTvBinding. --- For Insts, these cases should not happen -pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) ptext (sLit "UnkSkol") -pprSkolInfo RuntimeUnkSkol = WARN( True, text "pprSkolInfo: RuntimeUnkSkol" ) ptext (sLit "RuntimeUnkSkol") - -instance Outputable MetaDetails where - ppr Flexi = ptext (sLit "Flexi") - ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty +pprUserTypeCtxt GenSigCtxt = ptext (sLit "a type expected by the context") \end{code} @@ -490,19 +429,22 @@ instance Outputable MetaDetails where -- -- It doesn't change the uniques at all, just the print names. tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar) -tidyTyVarBndr env@(tidy_env, subst) tyvar - = case tidyOccName tidy_env (getOccName name) of - (tidy', occ') -> ((tidy', subst'), tyvar'') +tidyTyVarBndr (tidy_env, subst) tyvar + = case tidyOccName tidy_env occ1 of + (tidy', occ') -> ((tidy', subst'), tyvar') where - subst' = extendVarEnv subst tyvar tyvar'' - tyvar' = setTyVarName tyvar name' - name' = tidyNameOcc name occ' - -- Don't forget to tidy the kind for coercions! - tyvar'' | isCoVar tyvar = setTyVarKind tyvar' kind' - | otherwise = tyvar' - kind' = tidyType env (tyVarKind tyvar) + subst' = extendVarEnv subst tyvar tyvar' + tyvar' = setTyVarName tyvar name' + name' = tidyNameOcc name occ' where name = tyVarName tyvar + occ = getOccName name + -- System Names are for unification variables; + -- when we tidy them we give them a trailing "0" (or 1 etc) + -- so that they don't take precedence for the un-modified name + occ1 | isSystemName name = mkTyVarOcc (occNameString occ ++ "0") + | otherwise = occ + --------------- tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv @@ -578,28 +520,44 @@ tidyTopType :: Type -> Type tidyTopType ty = tidyType emptyTidyEnv ty --------------- -tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar) --- Tidy the type inside a GenSkol, preparatory to printing it -tidySkolemTyVar env tv - = ASSERT( isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv ) ) - (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1) - where - (env1, info1) = case tcTyVarDetails tv of - SkolemTv info -> (env1, SkolemTv info') - where - (env1, info') = tidy_skol_info env info - info -> (env, info) - - tidy_skol_info env (GenSkol ty) = (env1, GenSkol ty1) - where - (env1, ty1) = tidyOpenType env ty - tidy_skol_info env info = (env, info) - ---------------- tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind) tidyKind env k = tidyOpenType env k \end{code} +%************************************************************************ +%* * + Tidying coercions +%* * +%************************************************************************ + +\begin{code} + +tidyCo :: TidyEnv -> Coercion -> Coercion +tidyCo env@(_, subst) co + = go co + where + go (Refl ty) = Refl (tidyType env ty) + go (TyConAppCo tc cos) = let args = map go cos + in args `seqList` TyConAppCo tc args + go (AppCo co1 co2) = (AppCo $! go co1) $! go co2 + go (ForAllCo tv co) = ForAllCo tvp $! (tidyCo envp co) + where + (envp, tvp) = tidyTyVarBndr env tv + go (CoVarCo cv) = case lookupVarEnv subst cv of + Nothing -> CoVarCo cv + Just cv' -> CoVarCo cv' + go (AxiomInstCo con cos) = let args = tidyCos env cos + in args `seqList` AxiomInstCo con args + go (UnsafeCo ty1 ty2) = (UnsafeCo $! tidyType env ty1) $! tidyType env ty2 + go (SymCo co) = SymCo $! go co + go (TransCo co1 co2) = (TransCo $! go co1) $! go co2 + go (NthCo d co) = NthCo d $! go co + go (InstCo co ty) = (InstCo $! go co) $! tidyType env ty + +tidyCos :: TidyEnv -> [Coercion] -> [Coercion] +tidyCos env = map (tidyCo env) + +\end{code} %************************************************************************ %* * @@ -623,24 +581,22 @@ isTyConableTyVar tv -- not a SigTv = ASSERT( isTcTyVar tv) case tcTyVarDetails tv of - MetaTv (SigTv _) _ -> False - _ -> True + MetaTv SigTv _ -> False + _ -> True isSkolemTyVar tv = ASSERT2( isTcTyVar tv, ppr tv ) case tcTyVarDetails tv of - SkolemTv {} -> True - FlatSkol {} -> True - MetaTv {} -> False + SkolemTv {} -> True + FlatSkol {} -> True + RuntimeUnk {} -> True + MetaTv {} -> False --- isOverlappableTyVar has a unique purpose. --- See Note [Binding when looking up instances] in InstEnv. isOverlappableTyVar tv = ASSERT( isTcTyVar tv ) case tcTyVarDetails tv of - SkolemTv (PatSkol {}) -> True - SkolemTv (InstSkol {}) -> True - _ -> False + SkolemTv overlappable -> overlappable + _ -> False isMetaTyVar tv = ASSERT2( isTcTyVar tv, ppr tv ) @@ -656,8 +612,8 @@ isSigTyVar :: Var -> Bool isSigTyVar tv = ASSERT( isTcTyVar tv ) case tcTyVarDetails tv of - MetaTv (SigTv _) _ -> True - _ -> False + MetaTv SigTv _ -> True + _ -> False metaTvRef :: TyVar -> IORef MetaDetails metaTvRef tv @@ -675,15 +631,9 @@ isIndirect _ = False isRuntimeUnkSkol :: TyVar -> Bool -- Called only in TcErrors; see Note [Runtime skolems] there -isRuntimeUnkSkol x | isTcTyVar x - , SkolemTv RuntimeUnkSkol <- tcTyVarDetails x - = True - | otherwise = False - -isUnkSkol :: TyVar -> Bool -isUnkSkol x | isTcTyVar x - , SkolemTv UnkSkol <- tcTyVarDetails x = True - | otherwise = False +isRuntimeUnkSkol x + | isTcTyVar x, RuntimeUnk <- tcTyVarDetails x = True + | otherwise = False \end{code} @@ -713,7 +663,6 @@ isTauTy (FunTy a b) = isTauTy a && isTauTy b isTauTy (PredTy _) = True -- Don't look through source types isTauTy _ = False - isTauTyCon :: TyCon -> Bool -- Returns False for type synonyms whose expansion is a polytype isTauTyCon tc @@ -721,24 +670,7 @@ isTauTyCon tc | otherwise = True --------------- -isRigidTy :: TcType -> Bool --- A type is rigid if it has no meta type variables in it -isRigidTy ty = all isImmutableTyVar (varSetElems (tcTyVarsOfType ty)) - -isRefineableTy :: TcType -> (Bool,Bool) --- A type should have type refinements applied to it if it has --- free type variables, and they are all rigid -isRefineableTy ty = (null tc_tvs, all isImmutableTyVar tc_tvs) - where - tc_tvs = varSetElems (tcTyVarsOfType ty) - -isRefineablePred :: TcPredType -> Bool -isRefineablePred pred = not (null tc_tvs) && all isImmutableTyVar tc_tvs - where - tc_tvs = varSetElems (tcTyVarsOfPred pred) - ---------------- -getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to +getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to -- construct a dictionary function name getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty' getDFunTyKey (TyVarTy tv) = getOccName tv @@ -769,22 +701,19 @@ tcSplitForAllTys :: Type -> ([TyVar], Type) tcSplitForAllTys ty = split ty ty [] where split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs - split _ (ForAllTy tv ty) tvs - | not (isCoVar tv) = split ty ty (tv:tvs) - split orig_ty _ tvs = (reverse tvs, orig_ty) + split _ (ForAllTy tv ty) tvs = split ty ty (tv:tvs) + split orig_ty _ tvs = (reverse tvs, orig_ty) tcIsForAllTy :: Type -> Bool tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty' -tcIsForAllTy (ForAllTy tv _) = not (isCoVar tv) -tcIsForAllTy _ = False +tcIsForAllTy (ForAllTy {}) = True +tcIsForAllTy _ = False tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type) -- Split off the first predicate argument from a type tcSplitPredFunTy_maybe ty | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty' -tcSplitPredFunTy_maybe (ForAllTy tv ty) - | isCoVar tv = Just (coVarPred tv, ty) tcSplitPredFunTy_maybe (FunTy arg res) - | Just p <- tcSplitPredTy_maybe arg = Just (p, res) + | Just p <- splitPredTy_maybe arg = Just (p, res) tcSplitPredFunTy_maybe _ = Nothing @@ -934,13 +863,12 @@ tcSplitDFunTy ty -- coercion and class constraints; or (in the general NDP case) -- some other function argument split_dfun_args n ty | Just ty' <- tcView ty = split_dfun_args n ty' - split_dfun_args n (ForAllTy tv ty) = ASSERT( isCoVar tv ) split_dfun_args (n+1) ty split_dfun_args n (FunTy _ ty) = split_dfun_args (n+1) ty split_dfun_args n ty = (n, ty) tcSplitDFunHead :: Type -> (Class, [Type]) tcSplitDFunHead tau - = case tcSplitPredTy_maybe tau of + = case splitPredTy_maybe tau of Just (ClassP clas tys) -> (clas, tys) _ -> pprPanic "tcSplitDFunHead" (ppr tau) @@ -983,105 +911,33 @@ tcInstHeadTyAppAllTyVars ty %* * %************************************************************************ -\begin{code} -evVarPred :: EvVar -> PredType -evVarPred var - = case tcSplitPredTy_maybe (varType var) of - Just pred -> pred - Nothing -> pprPanic "evVarPred" (ppr var <+> ppr (varType var)) - -tcSplitPredTy_maybe :: Type -> Maybe PredType - -- Returns Just for predicates only -tcSplitPredTy_maybe ty | Just ty' <- tcView ty = tcSplitPredTy_maybe ty' -tcSplitPredTy_maybe (PredTy p) = Just p -tcSplitPredTy_maybe _ = Nothing - -predTyUnique :: PredType -> Unique -predTyUnique (IParam n _) = getUnique (ipNameName n) -predTyUnique (ClassP clas _) = getUnique clas -predTyUnique (EqPred a b) = pprPanic "predTyUnique" (ppr (EqPred a b)) -\end{code} - - ---------------------- Dictionary types --------------------------------- +Superclasses \begin{code} -mkClassPred :: Class -> [Type] -> PredType -mkClassPred clas tys = ClassP clas tys - -isClassPred :: PredType -> Bool -isClassPred (ClassP _ _) = True -isClassPred _ = False - -isTyVarClassPred :: PredType -> Bool -isTyVarClassPred (ClassP _ tys) = all tcIsTyVarTy tys -isTyVarClassPred _ = False - -getClassPredTys_maybe :: PredType -> Maybe (Class, [Type]) -getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys) -getClassPredTys_maybe _ = Nothing - -getClassPredTys :: PredType -> (Class, [Type]) -getClassPredTys (ClassP clas tys) = (clas, tys) -getClassPredTys _ = panic "getClassPredTys" - -mkDictTy :: Class -> [Type] -> Type -mkDictTy clas tys = mkPredTy (ClassP clas tys) - -isDictLikeTy :: Type -> Bool --- Note [Dictionary-like types] -isDictLikeTy ty | Just ty' <- tcView ty = isDictTy ty' -isDictLikeTy (PredTy p) = isClassPred p -isDictLikeTy (TyConApp tc tys) - | isTupleTyCon tc = all isDictLikeTy tys -isDictLikeTy _ = False -\end{code} - -Note [Dictionary-like types] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Being "dictionary-like" means either a dictionary type or a tuple thereof. -In GHC 6.10 we build implication constraints which construct such tuples, -and if we land up with a binding - t :: (C [a], Eq [a]) - t = blah -then we want to treat t as cheap under "-fdicts-cheap" for example. -(Implication constraints are normally inlined, but sadly not if the -occurrence is itself inside an INLINE function! Until we revise the -handling of implication constraints, that is.) This turned out to -be important in getting good arities in DPH code. Example: - - class C a - class D a where { foo :: a -> a } - instance C a => D (Maybe a) where { foo x = x } - - bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b) - {-# INLINE bar #-} - bar x y = (foo (Just x), foo (Just y)) - -Then 'bar' should jolly well have arity 4 (two dicts, two args), but -we ended up with something like - bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ... - in \x,y. ) - -This is all a bit ad-hoc; eg it relies on knowing that implication -constraints build tuples. - ---------------------- Implicit parameters --------------------------------- - -\begin{code} -mkIPPred :: IPName Name -> Type -> PredType -mkIPPred ip ty = IParam ip ty - -isIPPred :: PredType -> Bool -isIPPred (IParam _ _) = True -isIPPred _ = False -\end{code} - ---------------------- Equality predicates --------------------------------- -\begin{code} -substEqSpec :: TvSubst -> [(TyVar,Type)] -> [(TcType,TcType)] -substEqSpec subst eq_spec = [ (substTyVar subst tv, substTy subst ty) - | (tv,ty) <- eq_spec] +mkMinimalBySCs :: [PredType] -> [PredType] +-- Remove predicates that can be deduced from others by superclasses +mkMinimalBySCs ptys = [ ploc | ploc <- ptys + , ploc `not_in_preds` rec_scs ] + where + rec_scs = concatMap trans_super_classes ptys + not_in_preds p ps = null (filter (eqPred p) ps) + trans_super_classes (ClassP cls tys) = transSuperClasses cls tys + trans_super_classes _other_pty = [] + +transSuperClasses :: Class -> [Type] -> [PredType] +transSuperClasses cls tys + = foldl (\pts p -> trans_sc p ++ pts) [] $ + immSuperClasses cls tys + where trans_sc :: PredType -> [PredType] + trans_sc this_pty@(ClassP cls tys) + = foldl (\pts p -> trans_sc p ++ pts) [this_pty] $ + immSuperClasses cls tys + trans_sc pty = [pty] + +immSuperClasses :: Class -> [Type] -> [PredType] +immSuperClasses cls tys + = substTheta (zipTopTvSubst tyvars tys) sc_theta + where (tyvars,sc_theta,_,_) = classBigSig cls \end{code} @@ -1105,17 +961,10 @@ isSigmaTy _ = False isOverloadedTy :: Type -> Bool -- Yes for a type of a function that might require evidence-passing -- Used only by bindLocalMethods --- NB: be sure to check for type with an equality predicate; hence isCoVar isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty' -isOverloadedTy (ForAllTy tv ty) = isCoVar tv || isOverloadedTy ty -isOverloadedTy (FunTy a _) = isPredTy a -isOverloadedTy _ = False - -isPredTy :: Type -> Bool -- Belongs in TcType because it does - -- not look through newtypes, or predtypes (of course) -isPredTy ty | Just ty' <- tcView ty = isPredTy ty' -isPredTy (PredTy _) = True -isPredTy _ = False +isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty +isOverloadedTy (FunTy a _) = isPredTy a +isOverloadedTy _ = False \end{code} \begin{code} @@ -1177,14 +1026,9 @@ tcTyVarsOfType (TyConApp _ tys) = tcTyVarsOfTypes tys tcTyVarsOfType (PredTy sty) = tcTyVarsOfPred sty tcTyVarsOfType (FunTy arg res) = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res tcTyVarsOfType (AppTy fun arg) = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg -tcTyVarsOfType (ForAllTy tyvar ty) = (tcTyVarsOfType ty `delVarSet` tyvar) - `unionVarSet` tcTyVarsOfTyVar tyvar +tcTyVarsOfType (ForAllTy tyvar ty) = tcTyVarsOfType ty `delVarSet` tyvar -- We do sometimes quantify over skolem TcTyVars -tcTyVarsOfTyVar :: TcTyVar -> TyVarSet -tcTyVarsOfTyVar tv | isCoVar tv = tcTyVarsOfType (tyVarKind tv) - | otherwise = emptyVarSet - tcTyVarsOfTypes :: [Type] -> TyVarSet tcTyVarsOfTypes tys = foldr (unionVarSet.tcTyVarsOfType) emptyVarSet tys @@ -1194,88 +1038,58 @@ tcTyVarsOfPred (ClassP _ tys) = tcTyVarsOfTypes tys tcTyVarsOfPred (EqPred ty1 ty2) = tcTyVarsOfType ty1 `unionVarSet` tcTyVarsOfType ty2 \end{code} -Note [Silly type synonym] -~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - type T a = Int -What are the free tyvars of (T x)? Empty, of course! -Here's the example that Ralf Laemmel showed me: - foo :: (forall a. C u a -> C u a) -> u - mappend :: Monoid u => u -> u -> u - - bar :: Monoid u => u - bar = foo (\t -> t `mappend` t) -We have to generalise at the arg to f, and we don't -want to capture the constraint (Monad (C u a)) because -it appears to mention a. Pretty silly, but it was useful to him. - -exactTyVarsOfType is used by the type checker to figure out exactly -which type variables are mentioned in a type. It's also used in the -smart-app checking code --- see TcExpr.tcIdApp - -On the other hand, consider a *top-level* definition - f = (\x -> x) :: T a -> T a -If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then -if we have an application like (f "x") we get a confusing error message -involving Any. So the conclusion is this: when generalising - - at top level use tyVarsOfType - - in nested bindings use exactTyVarsOfType -See Trac #1813 for example. - -\begin{code} -exactTyVarsOfType :: TcType -> TyVarSet --- Find the free type variables (of any kind) --- but *expand* type synonyms. See Note [Silly type synonym] above. -exactTyVarsOfType ty - = go ty - where - go ty | Just ty' <- tcView ty = go ty' -- This is the key line - go (TyVarTy tv) = unitVarSet tv - go (TyConApp _ tys) = exactTyVarsOfTypes tys - go (PredTy ty) = go_pred ty - go (FunTy arg res) = go arg `unionVarSet` go res - go (AppTy fun arg) = go fun `unionVarSet` go arg - go (ForAllTy tyvar ty) = delVarSet (go ty) tyvar - `unionVarSet` go_tv tyvar - - go_pred (IParam _ ty) = go ty - go_pred (ClassP _ tys) = exactTyVarsOfTypes tys - go_pred (EqPred ty1 ty2) = go ty1 `unionVarSet` go ty2 - - go_tv tyvar | isCoVar tyvar = go (tyVarKind tyvar) - | otherwise = emptyVarSet - -exactTyVarsOfTypes :: [TcType] -> TyVarSet -exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys -\end{code} - Find the free tycons and classes of a type. This is used in the front end of the compiler. \begin{code} -tyClsNamesOfType :: Type -> NameSet -tyClsNamesOfType (TyVarTy _) = emptyNameSet -tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys -tyClsNamesOfType (PredTy (IParam _ ty)) = tyClsNamesOfType ty -tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys -tyClsNamesOfType (PredTy (EqPred ty1 ty2)) = tyClsNamesOfType ty1 `unionNameSets` tyClsNamesOfType ty2 -tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res -tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg -tyClsNamesOfType (ForAllTy _ ty) = tyClsNamesOfType ty - -tyClsNamesOfTypes :: [Type] -> NameSet -tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys - -tyClsNamesOfDFunHead :: Type -> NameSet +orphNamesOfType :: Type -> NameSet +orphNamesOfType ty | Just ty' <- tcView ty = orphNamesOfType ty' + -- Look through type synonyms (Trac #4912) +orphNamesOfType (TyVarTy _) = emptyNameSet +orphNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) + `unionNameSets` orphNamesOfTypes tys +orphNamesOfType (PredTy (IParam _ ty)) = orphNamesOfType ty +orphNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) + `unionNameSets` orphNamesOfTypes tys +orphNamesOfType (PredTy (EqPred ty1 ty2)) = orphNamesOfType ty1 + `unionNameSets` orphNamesOfType ty2 +orphNamesOfType (FunTy arg res) = orphNamesOfType arg `unionNameSets` orphNamesOfType res +orphNamesOfType (AppTy fun arg) = orphNamesOfType fun `unionNameSets` orphNamesOfType arg +orphNamesOfType (ForAllTy _ ty) = orphNamesOfType ty + +orphNamesOfTypes :: [Type] -> NameSet +orphNamesOfTypes tys = foldr (unionNameSets . orphNamesOfType) emptyNameSet tys + +orphNamesOfDFunHead :: Type -> NameSet -- Find the free type constructors and classes -- of the head of the dfun instance type -- The 'dfun_head_type' is because of -- instance Foo a => Baz T where ... -- The decl is an orphan if Baz and T are both not locally defined, -- even if Foo *is* locally defined -tyClsNamesOfDFunHead dfun_ty +orphNamesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of - (_, _, head_ty) -> tyClsNamesOfType head_ty + (_, _, head_ty) -> orphNamesOfType head_ty + +orphNamesOfCo :: Coercion -> NameSet +orphNamesOfCo (Refl ty) = orphNamesOfType ty +orphNamesOfCo (TyConAppCo tc cos) = unitNameSet (getName tc) `unionNameSets` orphNamesOfCos cos +orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSets` orphNamesOfCo co2 +orphNamesOfCo (ForAllCo _ co) = orphNamesOfCo co +orphNamesOfCo (CoVarCo _) = emptyNameSet +orphNamesOfCo (AxiomInstCo con cos) = orphNamesOfCoCon con `unionNameSets` orphNamesOfCos cos +orphNamesOfCo (UnsafeCo ty1 ty2) = orphNamesOfType ty1 `unionNameSets` orphNamesOfType ty2 +orphNamesOfCo (SymCo co) = orphNamesOfCo co +orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSets` orphNamesOfCo co2 +orphNamesOfCo (NthCo _ co) = orphNamesOfCo co +orphNamesOfCo (InstCo co ty) = orphNamesOfCo co `unionNameSets` orphNamesOfType ty + +orphNamesOfCos :: [Coercion] -> NameSet +orphNamesOfCos = foldr (unionNameSets . orphNamesOfCo) emptyNameSet + +orphNamesOfCoCon :: CoAxiom -> NameSet +orphNamesOfCoCon (CoAxiom { co_ax_lhs = ty1, co_ax_rhs = ty2 }) + = orphNamesOfType ty1 `unionNameSets` orphNamesOfType ty2 \end{code} @@ -1290,7 +1104,7 @@ restricted set of types as arguments and results (the restricting factor being the ) \begin{code} -tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type, CoercionI) +tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type, Coercion) -- (isIOType t) returns Just (IO,t',co) -- if co : t ~ IO t' -- returns Nothing otherwise @@ -1301,7 +1115,7 @@ tcSplitIOType_maybe ty Just (io_tycon, [io_res_ty]) | io_tycon `hasKey` ioTyConKey - -> Just (io_tycon, io_res_ty, IdCo ty) + -> Just (io_tycon, io_res_ty, mkReflCo ty) Just (tc, tys) | not (isRecursiveTyCon tc) @@ -1309,7 +1123,7 @@ tcSplitIOType_maybe ty -- Newtypes that require a coercion are ok -> case tcSplitIOType_maybe ty of Nothing -> Nothing - Just (tc, ty', co2) -> Just (tc, ty', co1 `mkTransCoI` co2) + Just (tc, ty', co2) -> Just (tc, ty', co1 `mkTransCo` co2) _ -> Nothing