--------------------------------
-- 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
-- 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, substTyVarBndr,
isPrimitiveType,
tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
- tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
+ tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
typeKind,
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
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, substTyVarBndr,
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 VarSet
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 )
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}
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
-- 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
| 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")
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 )
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
\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}
projects / ghc-hetmet.git / blobdiff