X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcType.lhs;h=ce31dd5f6e6f456c3206b2ab6ad9b9aee354d989;hb=8e67f5502e2e316245806ee3735a2f41a844b611;hp=379b370b525a39718e287c3d23e172b124e0e4a0;hpb=837824d2ff329a0f68c1434ae6812bea3ac7ec5f;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index 379b370..ce31dd5 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -22,14 +22,14 @@ module TcType ( -------------------------------- -- MetaDetails - TcTyVarDetails(..), + Expected(..), TcRef, TcTyVarDetails(..), MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolemTyVar, isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, skolemTvInfo, metaTvRef, isFlexi, isIndirect, -------------------------------- -- Builders - mkPhiTy, mkSigmaTy, + mkPhiTy, mkSigmaTy, hoistForAllTys, -------------------------------- -- Splitters @@ -38,12 +38,12 @@ module TcType ( tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs, tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy, - tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar, + tcGetTyVar_maybe, tcGetTyVar, --------------------------------- -- Predicates. -- Again, newtypes are opaque - tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, + tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX, isSigmaTy, isOverloadedTy, isDoubleTy, isFloatTy, isIntTy, isIntegerTy, isAddrTy, isBoolTy, isUnitTy, @@ -60,7 +60,7 @@ module TcType ( getClassPredTys_maybe, getClassPredTys, isClassPred, isTyVarClassPred, mkDictTy, tcSplitPredTy_maybe, - isPredTy, isDictTy, tcSplitDFunTy, predTyUnique, + isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique, mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, --------------------------------- @@ -94,17 +94,17 @@ module TcType ( -- Type substitutions TvSubst(..), -- Representation visible to a few friends TvSubstEnv, emptyTvSubst, - mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst, + mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, extendTvSubst, extendTvSubstList, isInScope, - substTy, substTys, substTyWith, substTheta, substTyVar, + substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr, isUnLiftedType, -- Source types are always lifted isUnboxedTupleType, -- Ditto isPrimitiveType, tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes, - tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, + tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar, typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta, @@ -122,11 +122,10 @@ import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend import Type ( -- Re-exports tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, - tyVarsOfTheta, Kind, Type, PredType(..), + tyVarsOfTheta, Kind, PredType(..), ThetaType, unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, isLiftedTypeKind, isUnliftedTypeKind, - isOpenTypeKind, mkArrowKinds, mkForAllTy, mkForAllTys, defaultKind, isArgTypeKind, isOpenTypeKind, mkFunTy, mkFunTys, zipFunTys, @@ -140,13 +139,17 @@ import Type ( -- Re-exports tidyFreeTyVars, tidyOpenType, tidyOpenTypes, tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, - isSubKind, + isSubKind, deShadowTy, + + tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, + tcEqPred, tcCmpPred, tcEqTypeX, + TvSubst(..), TvSubstEnv, emptyTvSubst, - mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst, + mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, extendTvSubst, extendTvSubstList, isInScope, - substTy, substTys, substTyWith, substTheta, substTyVar, + substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr, typeKind, repType, pprKind, pprParendKind, @@ -156,22 +159,21 @@ import Type ( -- Re-exports import TyCon ( TyCon, isUnLiftedTyCon, tyConUnique ) import DataCon ( DataCon ) import Class ( Class ) -import Var ( TyVar, Id, isTcTyVar, tcTyVarDetails ) +import Var ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails ) import ForeignCall ( Safety, playSafe, DNType(..) ) -import VarEnv import VarSet -- others: import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt ) import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc ) import NameSet +import VarEnv ( TidyEnv ) import OccName ( OccName, mkDictOcc ) import PrelNames -- Lots (e.g. in isFFIArgumentTy) import TysWiredIn ( unitTyCon, charTyCon, listTyCon ) import BasicTypes ( IPName(..), ipNameName ) -import Unique ( Unique, Uniquable(..) ) import SrcLoc ( SrcLoc, SrcSpan ) -import Util ( cmpList, thenCmp, snocView ) +import Util ( snocView ) import Maybes ( maybeToBool, expectJust ) import Outputable import DATA_IOREF @@ -227,6 +229,10 @@ type TcRhoType = TcType type TcTauType = TcType type TcKind = Kind type TcTyVarSet = TyVarSet + +type TcRef a = IORef a +data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference + | Check ty -- The type to check during type checking \end{code} @@ -261,7 +267,8 @@ data SkolemInfo -- variable for 'a'. | ArrowSkol SrcSpan -- An arrow form (see TcArrows) - | GenSkol TcType -- Bound when doing a subsumption check for this type + | GenSkol [TcTyVar] -- Bound when doing a subsumption check for + TcType -- (forall tvs. ty) SrcSpan data MetaDetails @@ -271,6 +278,19 @@ data MetaDetails | Indirect TcType -- Type indirections, treated as wobbly -- for the purpose of GADT unification. +tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar) +-- Tidy the type inside a GenSkol, preparatory to printing it +tidySkolemTyVar env tv + = ASSERT( isSkolemTyVar tv ) + (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info1)) + where + (env1, info1) = case skolemTvInfo tv of + GenSkol tvs ty loc -> (env2, GenSkol tvs1 ty1 loc) + where + (env1, tvs1) = tidyOpenTyVars env tvs + (env2, ty1) = tidyOpenType env1 ty + info -> (env, info) + pprSkolemTyVar :: TcTyVar -> SDoc pprSkolemTyVar tv = ASSERT( isSkolemTyVar tv ) @@ -283,8 +303,9 @@ instance Outputable SkolemInfo where ppr (ArrowSkol loc) = ptext SLIT("the arrow form at") <+> ppr loc ppr (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc), nest 2 (ptext SLIT("at") <+> ppr loc)] - ppr (GenSkol ty loc) = sep [ptext SLIT("the polymorphic type") <+> quotes (ppr ty), - nest 2 (ptext SLIT("at") <+> ppr loc)] + ppr (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type") + <+> quotes (ppr (mkForAllTys tvs ty)), + nest 2 (ptext SLIT("at") <+> ppr loc)] instance Outputable MetaDetails where ppr Flexi = ptext SLIT("Flexi") @@ -480,31 +501,18 @@ tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty) tcIsTyVarTy :: Type -> Bool tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty) -\end{code} - -The type of a method for class C is always of the form: - Forall a1..an. C a1..an => sig_ty -where sig_ty is the type given by the method's signature, and thus in general -is a ForallTy. At the point that splitMethodTy is called, it is expected -that the outer Forall has already been stripped off. splitMethodTy then -returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off. - -\begin{code} -tcSplitMethodTy :: Type -> (PredType, Type) -tcSplitMethodTy ty = split ty - where - split (FunTy arg res) = case tcSplitPredTy_maybe arg of - Just p -> (p, res) - Nothing -> panic "splitMethodTy" - split (NoteTy n ty) = split ty - split _ = panic "splitMethodTy" tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type]) -- Split the type of a dictionary function tcSplitDFunTy ty - = case tcSplitSigmaTy ty of { (tvs, theta, tau) -> - case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) -> + = case tcSplitSigmaTy ty of { (tvs, theta, tau) -> + case tcSplitDFunHead tau of { (clas, tys) -> (tvs, theta, clas, tys) }} + +tcSplitDFunHead :: Type -> (Class, [Type]) +tcSplitDFunHead tau + = case tcSplitPredTy_maybe tau of + Just (ClassP clas tys) -> (clas, tys) \end{code} @@ -587,95 +595,6 @@ isLinearPred other = False %************************************************************************ %* * -\subsection{Comparison} -%* * -%************************************************************************ - -Comparison, taking note of newtypes, predicates, etc, - -\begin{code} -tcEqType :: Type -> Type -> Bool -tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False } - -tcEqTypes :: [Type] -> [Type] -> Bool -tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False } - -tcEqPred :: PredType -> PredType -> Bool -tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False } - -------------- -tcCmpType :: Type -> Type -> Ordering -tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2 - -tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2 - -tcCmpPred p1 p2 = cmpPredTy emptyVarEnv p1 p2 -------------- -cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2 - -------------- -cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering - -- The "env" maps type variables in ty1 to type variables in ty2 - -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2) - -- we in effect substitute tv2 for tv1 in t1 before continuing - - -- Look through NoteTy -cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2 -cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2 - - -- Deal with equal constructors -cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of - Just tv1a -> tv1a `compare` tv2 - Nothing -> tv1 `compare` tv2 - -cmpTy env (PredTy p1) (PredTy p2) = cmpPredTy env p1 p2 -cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2 -cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2 -cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2) -cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2 - - -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy -cmpTy env (AppTy _ _) (TyVarTy _) = GT - -cmpTy env (FunTy _ _) (TyVarTy _) = GT -cmpTy env (FunTy _ _) (AppTy _ _) = GT - -cmpTy env (TyConApp _ _) (TyVarTy _) = GT -cmpTy env (TyConApp _ _) (AppTy _ _) = GT -cmpTy env (TyConApp _ _) (FunTy _ _) = GT - -cmpTy env (ForAllTy _ _) (TyVarTy _) = GT -cmpTy env (ForAllTy _ _) (AppTy _ _) = GT -cmpTy env (ForAllTy _ _) (FunTy _ _) = GT -cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT - -cmpTy env (PredTy _) t2 = GT - -cmpTy env _ _ = LT -\end{code} - -\begin{code} -cmpPredTy :: TyVarEnv TyVar -> PredType -> PredType -> Ordering -cmpPredTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2) - -- Compare types as well as names for implicit parameters - -- This comparison is used exclusively (I think) for the - -- finite map built in TcSimplify -cmpPredTy env (IParam _ _) (ClassP _ _) = LT -cmpPredTy env (ClassP _ _) (IParam _ _) = GT -cmpPredTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2) -\end{code} - -PredTypes are used as a FM key in TcSimplify, -so we take the easy path and make them an instance of Ord - -\begin{code} -instance Eq PredType where { (==) = tcEqPred } -instance Ord PredType where { compare = tcCmpPred } -\end{code} - - -%************************************************************************ -%* * \subsection{Predicates} %* * %************************************************************************ @@ -721,6 +640,79 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of \end{code} + + +%************************************************************************ +%* * + Hoisting for-alls +%* * +%************************************************************************ + +hoistForAllTys is used for user-written type signatures only +We want to 'look through' type synonyms when doing this +so it's better done on the Type than the HsType + +It moves all the foralls and constraints to the top +e.g. T -> forall a. a ==> forall a. T -> a + T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int + +Also: it eliminates duplicate constraints. These can show up +when hoisting constraints, notably implicit parameters. + +It tries hard to retain type synonyms if hoisting does not break one +up. Not only does this improve error messages, but there's a tricky +interaction with Haskell 98. H98 requires no unsaturated type +synonyms, which is checked by checkValidType. This runs after +hoisting, so we don't want hoisting to remove the SynNotes! (We can't +run validity checking before hoisting because in mutually-recursive +type definitions we postpone validity checking until after the knot is +tied.) + +\begin{code} +hoistForAllTys :: Type -> Type +hoistForAllTys ty + = go (deShadowTy ty) + -- Running over ty with an empty substitution gives it the + -- no-shadowing property. This is important. For example: + -- type Foo r = forall a. a -> r + -- foo :: Foo (Foo ()) + -- Here the hoisting should give + -- foo :: forall a a1. a -> a1 -> () + -- + -- What about type vars that are lexically in scope in the envt? + -- We simply rely on them having a different unique to any + -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars + -- out of the envt, which is boring and (I think) not necessary. + + where + go (TyVarTy tv) = TyVarTy tv + go (TyConApp tc tys) = TyConApp tc (map go tys) + go (PredTy pred) = PredTy pred -- No nested foralls + go (NoteTy (SynNote ty1) ty2) = NoteTy (SynNote (go ty1)) (go ty2) + go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard the free tyvar note + go (FunTy arg res) = mk_fun_ty (go arg) (go res) + go (AppTy fun arg) = AppTy (go fun) (go arg) + go (ForAllTy tv ty) = ForAllTy tv (go ty) + + -- mk_fun_ty does all the work. + -- It's building t1 -> t2: + -- if t2 is a for-all type, push t1 inside it + -- if t2 is (pred -> t3), check for duplicates + mk_fun_ty ty1 ty2 + | not (isSigmaTy ty2) -- No forall's, or context => + = FunTy ty1 ty2 + | PredTy p1 <- ty1 -- ty1 is a predicate + = if p1 `elem` theta then -- so check for duplicates + ty2 + else + mkSigmaTy tvs (p1:theta) tau + | otherwise + = mkSigmaTy tvs theta (FunTy ty1 tau) + where + (tvs, theta, tau) = tcSplitSigmaTy ty2 +\end{code} + + %************************************************************************ %* * \subsection{Misc}