X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcType.lhs;h=b9ff393b608e5a6a9eb9ea9c5fbc94e02665d2bb;hb=ff818166a0a06e77becad9e28ed116f3b7f5cc8b;hp=218d8df6d57579cd1ac3e0be9db9c4e33070860b;hpb=92342d8911151aef493e20ad264ea2afde1f591b;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index 218d8df..b9ff393 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -22,14 +22,14 @@ module TcType ( -------------------------------- -- MetaDetails - TcTyVarDetails(..), - MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolemTyVar, - isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, skolemTvInfo, metaTvRef, - isFlexi, isIndirect, + Expected(..), TcRef, TcTyVarDetails(..), + MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo, + isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef, + isFlexi, isIndirect, -------------------------------- -- Builders - mkPhiTy, mkSigmaTy, + mkPhiTy, mkSigmaTy, hoistForAllTys, -------------------------------- -- Splitters @@ -43,7 +43,7 @@ module TcType ( --------------------------------- -- 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} @@ -241,13 +247,45 @@ checking. It's attached to mutable type variables only. It's knot-tied back to Var.lhs. There is no reason in principle why Var.lhs shouldn't actually have the definition, but it "belongs" here. +Note [Signature skolems] +~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this + + x :: [a] + y :: b + (x,y,z) = ([y,z], z, head x) + +Here, x and y have type sigs, which go into the environment. We used to +instantiate their types with skolem constants, and push those types into +the RHS, so we'd typecheck the RHS with type + ( [a*], b*, c ) +where a*, b* are skolem constants, and c is an ordinary meta type varible. + +The trouble is that the occurrences of z in the RHS force a* and b* to +be the *same*, so we can't make them into skolem constants that don't unify +with each other. Alas. + +On the other hand, we *must* use skolems for signature type variables, +becuase GADT type refinement refines skolems only. + +One solution woudl be insist that in the above defn the programmer uses +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, SigSkokTv, which can unify with other SigSkolTvs. + + \begin{code} type TcTyVar = TyVar -- Used only during type inference -- A TyVarDetails is inside a TyVar data TcTyVarDetails - = SkolemTv SkolemInfo -- A skolem constant - | MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type + = MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type + | SkolemTv SkolemInfo -- A skolem constant + | SigSkolTv Name (IORef MetaDetails) -- Ditto, but from a type signature; + -- see Note [Signature skolems] + -- The MetaDetails, if filled in, will + -- always be another SigSkolTv data SkolemInfo = SigSkol Name -- Bound at a type signature @@ -261,7 +299,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,20 +310,38 @@ data MetaDetails | Indirect TcType -- Type indirections, treated as wobbly -- for the purpose of GADT unification. -pprSkolemTyVar :: TcTyVar -> SDoc -pprSkolemTyVar tv +tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar) +-- Tidy the type inside a GenSkol, preparatory to printing it +tidySkolemTyVar env tv = ASSERT( isSkolemTyVar tv ) - quotes (ppr tv) <+> ptext SLIT("is bound by") <+> ppr (skolemTvInfo tv) - -instance Outputable SkolemInfo where - ppr (SigSkol id) = ptext SLIT("the type signature for") <+> quotes (ppr id) - ppr (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls) - ppr (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df) - 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)] + (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1) + where + (env1, info1) = case tcTyVarDetails tv of + SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc)) + where + (env1, tvs1) = tidyOpenTyVars env tvs + (env2, ty1) = tidyOpenType env1 ty + info -> (env, info) + +pprTcTyVar :: TcTyVar -> SDoc +-- Print tyvar with info about its binding +pprTcTyVar tv + = quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv) + where + ppr_details (MetaTv _) = ptext SLIT("is a meta type variable") + ppr_details (SigSkolTv id _) = ptext SLIT("is bound by") <+> pprSkolInfo (SigSkol id) + ppr_details (SkolemTv info) = ptext SLIT("is bound by") <+> pprSkolInfo info + +pprSkolInfo :: SkolemInfo -> SDoc +pprSkolInfo (SigSkol id) = ptext SLIT("the type signature for") <+> quotes (ppr id) +pprSkolInfo (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls) +pprSkolInfo (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df) +pprSkolInfo (ArrowSkol loc) = ptext SLIT("the arrow form at") <+> ppr loc +pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc), + nest 2 (ptext SLIT("at") <+> ppr loc)] +pprSkolInfo (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") @@ -298,8 +355,9 @@ isImmutableTyVar tv isSkolemTyVar tv = ASSERT( isTcTyVar tv ) case tcTyVarDetails tv of - SkolemTv _ -> True - MetaTv _ -> False + SkolemTv _ -> True + SigSkolTv _ _ -> True + MetaTv _ -> False isExistentialTyVar tv -- Existential type variable, bound by a pattern = ASSERT( isTcTyVar tv ) @@ -310,20 +368,15 @@ isExistentialTyVar tv -- Existential type variable, bound by a pattern isMetaTyVar tv = ASSERT( isTcTyVar tv ) case tcTyVarDetails tv of - SkolemTv _ -> False MetaTv _ -> True - -skolemTvInfo :: TyVar -> SkolemInfo -skolemTvInfo tv - = ASSERT( isTcTyVar tv ) - case tcTyVarDetails tv of - SkolemTv info -> info + other -> False metaTvRef :: TyVar -> IORef MetaDetails metaTvRef tv = ASSERT( isTcTyVar tv ) case tcTyVarDetails tv of - MetaTv ref -> ref + MetaTv ref -> ref + other -> pprPanic "metaTvRef" (ppr tv) isFlexi, isIndirect :: MetaDetails -> Bool isFlexi Flexi = True @@ -484,9 +537,14 @@ tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty) 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} @@ -569,95 +627,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} %* * %************************************************************************ @@ -703,6 +672,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}