2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcType]{Types used in the typechecker}
6 This module provides the Type interface for front-end parts of the
9 * treat "source types" as opaque:
10 newtypes, and predicates are meaningful.
11 * look through usage types
13 The "tc" prefix is for "typechechecker", because the type checker
14 is the principal client.
18 --------------------------------
20 TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
21 TcTyVar, TcTyVarSet, TcKind,
23 BoxyTyVar, BoxySigmaType, BoxyRhoType, BoxyThetaType, BoxyType,
25 --------------------------------
27 UserTypeCtxt(..), pprUserTypeCtxt,
28 TcTyVarDetails(..), BoxInfo(..), pprTcTyVarDetails,
29 MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolTvBinding, pprSkolInfo,
30 isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isBoxyTyVar, isSigTyVar, isExistentialTyVar,
34 --------------------------------
38 --------------------------------
40 -- These are important because they do not look through newtypes
42 tcSplitForAllTys, tcSplitPhiTy,
43 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
44 tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
45 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys,
46 tcValidInstHeadTy, tcGetTyVar_maybe, tcGetTyVar,
47 tcSplitSigmaTy, tcMultiSplitSigmaTy,
49 ---------------------------------
51 -- Again, newtypes are opaque
52 tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
53 isSigmaTy, isOverloadedTy, isRigidTy, isBoxyTy,
54 isDoubleTy, isFloatTy, isIntTy, isStringTy,
55 isIntegerTy, isBoolTy, isUnitTy,
56 isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
58 ---------------------------------
59 -- Misc type manipulators
60 deNoteType, classesOfTheta,
61 tyClsNamesOfType, tyClsNamesOfDFunHead,
64 ---------------------------------
66 getClassPredTys_maybe, getClassPredTys,
67 isClassPred, isTyVarClassPred,
68 mkDictTy, tcSplitPredTy_maybe,
69 isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique,
70 mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
71 dataConsStupidTheta, isRefineableTy,
73 ---------------------------------
74 -- Foreign import and export
75 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
76 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
77 isFFIExportResultTy, -- :: Type -> Bool
78 isFFIExternalTy, -- :: Type -> Bool
79 isFFIDynArgumentTy, -- :: Type -> Bool
80 isFFIDynResultTy, -- :: Type -> Bool
81 isFFILabelTy, -- :: Type -> Bool
82 isFFIDotnetTy, -- :: DynFlags -> Type -> Bool
83 isFFIDotnetObjTy, -- :: Type -> Bool
84 isFFITy, -- :: Type -> Bool
85 tcSplitIOType_maybe, -- :: Type -> Maybe Type
86 toDNType, -- :: Type -> DNType
88 --------------------------------
89 -- Rexported from Type
90 Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
91 unliftedTypeKind, liftedTypeKind, unboxedTypeKind,
92 openTypeKind, mkArrowKind, mkArrowKinds,
93 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
94 isArgTypeKind, isSubKind, defaultKind,
96 Type, PredType(..), ThetaType,
97 mkForAllTy, mkForAllTys,
98 mkFunTy, mkFunTys, zipFunTys,
99 mkTyConApp, mkAppTy, mkAppTys, applyTy, applyTys,
100 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
102 -- Type substitutions
103 TvSubst(..), -- Representation visible to a few friends
104 TvSubstEnv, emptyTvSubst,
105 mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
106 getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, lookupTyVar,
107 extendTvSubst, extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
108 substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
110 isUnLiftedType, -- Source types are always lifted
111 isUnboxedTupleType, -- Ditto
114 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
115 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
118 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
119 tcTyVarsOfType, tcTyVarsOfTypes, exactTyVarsOfType, exactTyVarsOfTypes,
121 pprKind, pprParendKind,
122 pprType, pprParendType, pprTyThingCategory,
123 pprPred, pprTheta, pprThetaArrow, pprClassPred
127 #include "HsVersions.h"
130 import TypeRep ( Type(..), funTyCon ) -- friend
132 import Type ( -- Re-exports
133 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
134 tyVarsOfTheta, Kind, PredType(..),
135 ThetaType, unliftedTypeKind, unboxedTypeKind,
136 liftedTypeKind, openTypeKind, mkArrowKind,
137 isLiftedTypeKind, isUnliftedTypeKind,
138 mkArrowKinds, mkForAllTy, mkForAllTys,
139 defaultKind, isArgTypeKind, isOpenTypeKind,
140 mkFunTy, mkFunTys, zipFunTys,
142 mkAppTys, applyTy, applyTys,
143 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
144 mkPredTys, isUnLiftedType,
145 isUnboxedTupleType, isPrimitiveType,
147 tidyTopType, tidyType, tidyPred, tidyTypes,
148 tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
149 tidyTyVarBndr, tidyOpenTyVar,
150 tidyOpenTyVars, tidyKind,
153 tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
154 tcEqPred, tcCmpPred, tcEqTypeX,
157 TvSubstEnv, emptyTvSubst, mkTvSubst, zipTyEnv,
158 mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
159 getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
160 extendTvSubst, extendTvSubstList, isInScope, notElemTvSubst,
161 substTy, substTys, substTyWith, substTheta,
162 substTyVar, substTyVarBndr, substPred, lookupTyVar,
164 typeKind, repType, coreView,
165 pprKind, pprParendKind,
166 pprType, pprParendType, pprTyThingCategory,
167 pprPred, pprTheta, pprThetaArrow, pprClassPred
169 import TyCon ( TyCon, isUnLiftedTyCon, isSynTyCon, synTyConDefn, tyConUnique )
170 import DataCon ( DataCon, dataConStupidTheta, dataConResTys )
171 import Class ( Class )
172 import Var ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
173 import ForeignCall ( Safety, playSafe, DNType(..) )
174 import Unify ( tcMatchTys )
178 import DynFlags ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
179 import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
181 import VarEnv ( TidyEnv )
182 import OccName ( OccName, mkDictOcc )
183 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
184 import TysWiredIn ( unitTyCon, charTyCon, listTyCon )
185 import BasicTypes ( IPName(..), Arity, ipNameName )
186 import SrcLoc ( SrcLoc, SrcSpan )
187 import Util ( snocView, equalLength )
188 import Maybes ( maybeToBool, expectJust, mapCatMaybes )
189 import ListSetOps ( hasNoDups )
190 import List ( nubBy )
196 %************************************************************************
200 %************************************************************************
202 The type checker divides the generic Type world into the
203 following more structured beasts:
205 sigma ::= forall tyvars. phi
206 -- A sigma type is a qualified type
208 -- Note that even if 'tyvars' is empty, theta
209 -- may not be: e.g. (?x::Int) => Int
211 -- Note that 'sigma' is in prenex form:
212 -- all the foralls are at the front.
213 -- A 'phi' type has no foralls to the right of
221 -- A 'tau' type has no quantification anywhere
222 -- Note that the args of a type constructor must be taus
224 | tycon tau_1 .. tau_n
228 -- In all cases, a (saturated) type synonym application is legal,
229 -- provided it expands to the required form.
232 type TcTyVar = TyVar -- Used only during type inference
233 type TcType = Type -- A TcType can have mutable type variables
234 -- Invariant on ForAllTy in TcTypes:
236 -- a cannot occur inside a MutTyVar in T; that is,
237 -- T is "flattened" before quantifying over a
239 -- These types do not have boxy type variables in them
240 type TcPredType = PredType
241 type TcThetaType = ThetaType
242 type TcSigmaType = TcType
243 type TcRhoType = TcType
244 type TcTauType = TcType
246 type TcTyVarSet = TyVarSet
248 -- These types may have boxy type variables in them
249 type BoxyTyVar = TcTyVar
250 type BoxyRhoType = TcType
251 type BoxyThetaType = TcThetaType
252 type BoxySigmaType = TcType
253 type BoxyType = TcType
257 %************************************************************************
259 \subsection{TyVarDetails}
261 %************************************************************************
263 TyVarDetails gives extra info about type variables, used during type
264 checking. It's attached to mutable type variables only.
265 It's knot-tied back to Var.lhs. There is no reason in principle
266 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
269 Note [Signature skolems]
270 ~~~~~~~~~~~~~~~~~~~~~~~~
275 (x,y,z) = ([y,z], z, head x)
277 Here, x and y have type sigs, which go into the environment. We used to
278 instantiate their types with skolem constants, and push those types into
279 the RHS, so we'd typecheck the RHS with type
281 where a*, b* are skolem constants, and c is an ordinary meta type varible.
283 The trouble is that the occurrences of z in the RHS force a* and b* to
284 be the *same*, so we can't make them into skolem constants that don't unify
285 with each other. Alas.
287 On the other hand, we *must* use skolems for signature type variables,
288 becuase GADT type refinement refines skolems only.
290 One solution would be insist that in the above defn the programmer uses
291 the same type variable in both type signatures. But that takes explanation.
293 The alternative (currently implemented) is to have a special kind of skolem
294 constant, SigSkokTv, which can unify with other SigSkolTvs.
298 -- A TyVarDetails is inside a TyVar
300 = SkolemTv SkolemInfo -- A skolem constant
302 | MetaTv BoxInfo (IORef MetaDetails)
305 = BoxTv -- The contents is a (non-boxy) sigma-type
306 -- That is, this MetaTv is a "box"
308 | TauTv -- The contents is a (non-boxy) tau-type
309 -- That is, this MetaTv is an ordinary unification variable
311 | SigTv SkolemInfo -- A variant of TauTv, except that it should not be
312 -- unified with a type, only with a type variable
313 -- SigTvs are only distinguished to improve error messages
314 -- see Note [Signature skolems]
315 -- The MetaDetails, if filled in, will
316 -- always be another SigTv or a SkolemTv
319 -- A TauTv is always filled in with a tau-type, which
320 -- never contains any BoxTvs, nor any ForAlls
322 -- However, a BoxTv can contain a type that contains further BoxTvs
323 -- Notably, when typechecking an explicit list, say [e1,e2], with
324 -- expected type being a box b1, we fill in b1 with (List b2), where
325 -- b2 is another (currently empty) box.
328 = Flexi -- Flexi type variables unify to become
331 | Indirect TcType -- INVARIANT:
332 -- For a BoxTv, this type must be non-boxy
333 -- For a TauTv, this type must be a tau-type
336 = SigSkol UserTypeCtxt -- A skolem that is created by instantiating
337 -- a programmer-supplied type signature
338 -- Location of the binding site is on the TyVar
340 -- The rest are for non-scoped skolems
341 | ClsSkol Class -- Bound at a class decl
342 | InstSkol Id -- Bound at an instance decl
343 | PatSkol DataCon -- An existential type variable bound by a pattern for
344 SrcSpan -- a data constructor with an existential type. E.g.
345 -- data T = forall a. Eq a => MkT a
347 -- The pattern MkT x will allocate an existential type
349 | ArrowSkol SrcSpan -- An arrow form (see TcArrows)
351 | GenSkol [TcTyVar] -- Bound when doing a subsumption check for
352 TcType -- (forall tvs. ty)
355 | UnkSkol -- Unhelpful info (until I improve it)
357 -------------------------------------
358 -- UserTypeCtxt describes the places where a
359 -- programmer-written type signature can occur
361 = FunSigCtxt Name -- Function type signature
362 -- Also used for types in SPECIALISE pragmas
363 | ExprSigCtxt -- Expression type signature
364 | ConArgCtxt Name -- Data constructor argument
365 | TySynCtxt Name -- RHS of a type synonym decl
366 | GenPatCtxt -- Pattern in generic decl
367 -- f{| a+b |} (Inl x) = ...
368 | LamPatSigCtxt -- Type sig in lambda pattern
370 | BindPatSigCtxt -- Type sig in pattern binding pattern
372 | ResSigCtxt -- Result type sig
374 | ForSigCtxt Name -- Foreign inport or export signature
375 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
376 | DefaultDeclCtxt -- Types in a default declaration
377 | SpecInstCtxt -- SPECIALISE instance pragma
379 -- Notes re TySynCtxt
380 -- We allow type synonyms that aren't types; e.g. type List = []
382 -- If the RHS mentions tyvars that aren't in scope, we'll
383 -- quantify over them:
384 -- e.g. type T = a->a
385 -- will become type T = forall a. a->a
387 -- With gla-exts that's right, but for H98 we should complain.
390 %************************************************************************
394 %************************************************************************
397 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
399 pprTcTyVarDetails (SkolemTv _) = ptext SLIT("sk")
400 pprTcTyVarDetails (MetaTv BoxTv _) = ptext SLIT("box")
401 pprTcTyVarDetails (MetaTv TauTv _) = ptext SLIT("tau")
402 pprTcTyVarDetails (MetaTv (SigTv _) _) = ptext SLIT("sig")
404 pprUserTypeCtxt :: UserTypeCtxt -> SDoc
405 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
406 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
407 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of the constructor") <+> quotes (ppr c)
408 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of the type synonym") <+> quotes (ppr c)
409 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
410 pprUserTypeCtxt LamPatSigCtxt = ptext SLIT("a pattern type signature")
411 pprUserTypeCtxt BindPatSigCtxt = ptext SLIT("a pattern type signature")
412 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
413 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign declaration for") <+> quotes (ppr n)
414 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
415 pprUserTypeCtxt DefaultDeclCtxt = ptext SLIT("a type in a `default' declaration")
416 pprUserTypeCtxt SpecInstCtxt = ptext SLIT("a SPECIALISE instance pragma")
419 --------------------------------
420 tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
421 -- Tidy the type inside a GenSkol, preparatory to printing it
422 tidySkolemTyVar env tv
423 = ASSERT( isSkolemTyVar tv )
424 (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
426 (env1, info1) = case tcTyVarDetails tv of
427 SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc))
429 (env1, tvs1) = tidyOpenTyVars env tvs
430 (env2, ty1) = tidyOpenType env1 ty
433 pprSkolTvBinding :: TcTyVar -> SDoc
434 -- Print info about the binding of a skolem tyvar,
435 -- or nothing if we don't have anything useful to say
437 = ppr_details (tcTyVarDetails tv)
439 ppr_details (MetaTv TauTv _) = quotes (ppr tv) <+> ptext SLIT("is a meta type variable")
440 ppr_details (MetaTv BoxTv _) = quotes (ppr tv) <+> ptext SLIT("is a boxy type variable")
441 ppr_details (MetaTv (SigTv info) _) = ppr_skol info
442 ppr_details (SkolemTv info) = ppr_skol info
444 ppr_skol UnkSkol = empty -- Unhelpful; omit
445 ppr_skol (SigSkol ctxt) = sep [quotes (ppr tv) <+> ptext SLIT("is bound by") <+> pprUserTypeCtxt ctxt,
446 nest 2 (ptext SLIT("at") <+> ppr (getSrcLoc tv))]
447 ppr_skol info = quotes (ppr tv) <+> pprSkolInfo info
449 pprSkolInfo :: SkolemInfo -> SDoc
450 pprSkolInfo (SigSkol ctxt) = ptext SLIT("is bound by") <+> pprUserTypeCtxt ctxt
451 pprSkolInfo (ClsSkol cls) = ptext SLIT("is bound by the class declaration for") <+> quotes (ppr cls)
452 pprSkolInfo (InstSkol df) = ptext SLIT("is bound by the instance declaration at") <+> ppr (getSrcLoc df)
453 pprSkolInfo (ArrowSkol loc) = ptext SLIT("is bound by the arrow form at") <+> ppr loc
454 pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("is bound by the pattern for") <+> quotes (ppr dc),
455 nest 2 (ptext SLIT("at") <+> ppr loc)]
456 pprSkolInfo (GenSkol tvs ty loc) = sep [sep [ptext SLIT("is bound by the polymorphic type"),
457 nest 2 (quotes (ppr (mkForAllTys tvs ty)))],
458 nest 2 (ptext SLIT("at") <+> ppr loc)]
460 -- For type variables the others are dealt with by pprSkolTvBinding.
461 -- For Insts, these cases should not happen
462 pprSkolInfo UnkSkol = panic "UnkSkol"
464 instance Outputable MetaDetails where
465 ppr Flexi = ptext SLIT("Flexi")
466 ppr (Indirect ty) = ptext SLIT("Indirect") <+> ppr ty
470 %************************************************************************
474 %************************************************************************
477 isImmutableTyVar, isSkolemTyVar, isExistentialTyVar, isBoxyTyVar, isMetaTyVar :: TyVar -> Bool
479 | isTcTyVar tv = isSkolemTyVar tv
483 = ASSERT( isTcTyVar tv )
484 case tcTyVarDetails tv of
488 isExistentialTyVar tv -- Existential type variable, bound by a pattern
489 = ASSERT( isTcTyVar tv )
490 case tcTyVarDetails tv of
491 SkolemTv (PatSkol _ _) -> True
495 = ASSERT2( isTcTyVar tv, ppr tv )
496 case tcTyVarDetails tv of
501 = ASSERT( isTcTyVar tv )
502 case tcTyVarDetails tv of
503 MetaTv BoxTv _ -> True
507 = ASSERT( isTcTyVar tv )
508 case tcTyVarDetails tv of
509 MetaTv (SigTv _) _ -> True
512 metaTvRef :: TyVar -> IORef MetaDetails
514 = ASSERT( isTcTyVar tv )
515 case tcTyVarDetails tv of
517 other -> pprPanic "metaTvRef" (ppr tv)
519 isFlexi, isIndirect :: MetaDetails -> Bool
521 isFlexi other = False
523 isIndirect (Indirect _) = True
524 isIndirect other = False
528 %************************************************************************
530 \subsection{Tau, sigma and rho}
532 %************************************************************************
535 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
537 mkPhiTy :: [PredType] -> Type -> Type
538 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
541 @isTauTy@ tests for nested for-alls. It should not be called on a boxy type.
544 isTauTy :: Type -> Bool
545 isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
546 isTauTy (TyVarTy tv) = ASSERT( not (isTcTyVar tv && isBoxyTyVar tv) )
548 isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
549 isTauTy (AppTy a b) = isTauTy a && isTauTy b
550 isTauTy (FunTy a b) = isTauTy a && isTauTy b
551 isTauTy (PredTy p) = True -- Don't look through source types
552 isTauTy other = False
555 isTauTyCon :: TyCon -> Bool
556 -- Returns False for type synonyms whose expansion is a polytype
557 isTauTyCon tc | isSynTyCon tc = isTauTy (snd (synTyConDefn tc))
561 isBoxyTy :: TcType -> Bool
562 isBoxyTy ty = any isBoxyTyVar (varSetElems (tcTyVarsOfType ty))
564 isRigidTy :: TcType -> Bool
565 -- A type is rigid if it has no meta type variables in it
566 isRigidTy ty = all isSkolemTyVar (varSetElems (tcTyVarsOfType ty))
568 isRefineableTy :: TcType -> Bool
569 -- A type should have type refinements applied to it if it has
570 -- free type variables, and they are all rigid
571 isRefineableTy ty = not (null tc_tvs) && all isSkolemTyVar tc_tvs
573 tc_tvs = varSetElems (tcTyVarsOfType ty)
576 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
577 -- construct a dictionary function name
578 getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
579 getDFunTyKey (TyVarTy tv) = getOccName tv
580 getDFunTyKey (TyConApp tc _) = getOccName tc
581 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
582 getDFunTyKey (FunTy arg _) = getOccName funTyCon
583 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
584 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
585 -- PredTy shouldn't happen
589 %************************************************************************
591 \subsection{Expanding and splitting}
593 %************************************************************************
595 These tcSplit functions are like their non-Tc analogues, but
596 a) they do not look through newtypes
597 b) they do not look through PredTys
598 c) [future] they ignore usage-type annotations
600 However, they are non-monadic and do not follow through mutable type
601 variables. It's up to you to make sure this doesn't matter.
604 tcSplitForAllTys :: Type -> ([TyVar], Type)
605 tcSplitForAllTys ty = split ty ty []
607 split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
608 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
609 split orig_ty t tvs = (reverse tvs, orig_ty)
611 tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
612 tcIsForAllTy (ForAllTy tv ty) = True
613 tcIsForAllTy t = False
615 tcSplitPhiTy :: Type -> ([PredType], Type)
616 tcSplitPhiTy ty = split ty ty []
618 split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
619 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
620 Just p -> split res res (p:ts)
621 Nothing -> (reverse ts, orig_ty)
622 split orig_ty ty ts = (reverse ts, orig_ty)
624 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
625 (tvs, rho) -> case tcSplitPhiTy rho of
626 (theta, tau) -> (tvs, theta, tau)
628 -----------------------
631 -> ( [([TyVar], ThetaType)], -- forall as.C => forall bs.D
632 TcSigmaType) -- The rest of the type
634 -- We need a loop here because we are now prepared to entertain
636 -- f:: forall a. Eq a => forall b. Baz b => tau
637 -- We want to instantiate this to
638 -- f2::tau {f2 = f1 b (Baz b), f1 = f a (Eq a)}
640 tcMultiSplitSigmaTy sigma
641 = case (tcSplitSigmaTy sigma) of
642 ([],[],ty) -> ([], sigma)
643 (tvs, theta, ty) -> case tcMultiSplitSigmaTy ty of
644 (pairs, rest) -> ((tvs,theta):pairs, rest)
646 -----------------------
647 tcTyConAppTyCon :: Type -> TyCon
648 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
650 tcTyConAppArgs :: Type -> [Type]
651 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
653 tcSplitTyConApp :: Type -> (TyCon, [Type])
654 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
656 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
658 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
659 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
660 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
661 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
662 -- Newtypes are opaque, so they may be split
663 -- However, predicates are not treated
664 -- as tycon applications by the type checker
665 tcSplitTyConApp_maybe other = Nothing
667 -----------------------
668 tcSplitFunTys :: Type -> ([Type], Type)
669 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
671 Just (arg,res) -> (arg:args, res')
673 (args,res') = tcSplitFunTys res
675 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
676 tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
677 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
678 tcSplitFunTy_maybe other = Nothing
682 -> Arity -- N: Number of desired args
683 -> ([TcSigmaType], -- Arg types (N or fewer)
684 TcSigmaType) -- The rest of the type
686 tcSplitFunTysN ty n_args
689 | Just (arg,res) <- tcSplitFunTy_maybe ty
690 = case tcSplitFunTysN res (n_args - 1) of
691 (args, res) -> (arg:args, res)
695 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
696 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
699 -----------------------
700 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
701 tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
702 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
703 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
704 tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
705 Just (tys', ty') -> Just (TyConApp tc tys', ty')
707 tcSplitAppTy_maybe other = Nothing
709 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
711 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
713 tcSplitAppTys :: Type -> (Type, [Type])
717 go ty args = case tcSplitAppTy_maybe ty of
718 Just (ty', arg) -> go ty' (arg:args)
721 -----------------------
722 tcGetTyVar_maybe :: Type -> Maybe TyVar
723 tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
724 tcGetTyVar_maybe (TyVarTy tv) = Just tv
725 tcGetTyVar_maybe other = Nothing
727 tcGetTyVar :: String -> Type -> TyVar
728 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
730 tcIsTyVarTy :: Type -> Bool
731 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
733 -----------------------
734 tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
735 -- Split the type of a dictionary function
737 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
738 case tcSplitDFunHead tau of { (clas, tys) ->
739 (tvs, theta, clas, tys) }}
741 tcSplitDFunHead :: Type -> (Class, [Type])
743 = case tcSplitPredTy_maybe tau of
744 Just (ClassP clas tys) -> (clas, tys)
746 tcValidInstHeadTy :: Type -> Bool
747 -- Used in Haskell-98 mode, for the argument types of an instance head
748 -- These must not be type synonyms, but everywhere else type synonyms
749 -- are transparent, so we need a special function here
752 NoteTy _ ty -> tcValidInstHeadTy ty
753 TyConApp tc tys -> not (isSynTyCon tc) && ok tys
754 FunTy arg res -> ok [arg, res]
757 -- Check that all the types are type variables,
758 -- and that each is distinct
759 ok tys = equalLength tvs tys && hasNoDups tvs
761 tvs = mapCatMaybes get_tv tys
763 get_tv (NoteTy _ ty) = get_tv ty -- Again, do not look
764 get_tv (TyVarTy tv) = Just tv -- through synonyms
765 get_tv other = Nothing
770 %************************************************************************
772 \subsection{Predicate types}
774 %************************************************************************
777 tcSplitPredTy_maybe :: Type -> Maybe PredType
778 -- Returns Just for predicates only
779 tcSplitPredTy_maybe ty | Just ty' <- tcView ty = tcSplitPredTy_maybe ty'
780 tcSplitPredTy_maybe (PredTy p) = Just p
781 tcSplitPredTy_maybe other = Nothing
783 predTyUnique :: PredType -> Unique
784 predTyUnique (IParam n _) = getUnique (ipNameName n)
785 predTyUnique (ClassP clas tys) = getUnique clas
787 mkPredName :: Unique -> SrcLoc -> PredType -> Name
788 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
789 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
793 --------------------- Dictionary types ---------------------------------
796 mkClassPred clas tys = ClassP clas tys
798 isClassPred :: PredType -> Bool
799 isClassPred (ClassP clas tys) = True
800 isClassPred other = False
802 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
803 isTyVarClassPred other = False
805 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
806 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
807 getClassPredTys_maybe _ = Nothing
809 getClassPredTys :: PredType -> (Class, [Type])
810 getClassPredTys (ClassP clas tys) = (clas, tys)
812 mkDictTy :: Class -> [Type] -> Type
813 mkDictTy clas tys = mkPredTy (ClassP clas tys)
815 isDictTy :: Type -> Bool
816 isDictTy ty | Just ty' <- tcView ty = isDictTy ty'
817 isDictTy (PredTy p) = isClassPred p
818 isDictTy other = False
821 --------------------- Implicit parameters ---------------------------------
824 isIPPred :: PredType -> Bool
825 isIPPred (IParam _ _) = True
826 isIPPred other = False
828 isInheritablePred :: PredType -> Bool
829 -- Can be inherited by a context. For example, consider
830 -- f x = let g y = (?v, y+x)
831 -- in (g 3 with ?v = 8,
833 -- The point is that g's type must be quantifed over ?v:
834 -- g :: (?v :: a) => a -> a
835 -- but it doesn't need to be quantified over the Num a dictionary
836 -- which can be free in g's rhs, and shared by both calls to g
837 isInheritablePred (ClassP _ _) = True
838 isInheritablePred other = False
840 isLinearPred :: TcPredType -> Bool
841 isLinearPred (IParam (Linear n) _) = True
842 isLinearPred other = False
845 --------------------- The stupid theta (sigh) ---------------------------------
848 dataConsStupidTheta :: [DataCon] -> ThetaType
849 -- Union the stupid thetas from all the specified constructors (non-empty)
850 -- All the constructors should have the same result type, modulo alpha conversion
851 -- The resulting ThetaType uses type variables from the *first* constructor in the list
853 -- It's here because it's used in MkId.mkRecordSelId, and in TcExpr
854 dataConsStupidTheta (con1:cons)
855 = nubBy tcEqPred all_preds
857 all_preds = dataConStupidTheta con1 ++ other_stupids
858 res_tys1 = dataConResTys con1
859 tvs1 = tyVarsOfTypes res_tys1
860 other_stupids = [ substPred subst pred
862 , let Just subst = tcMatchTys tvs1 res_tys1 (dataConResTys con)
863 , pred <- dataConStupidTheta con ]
867 %************************************************************************
869 \subsection{Predicates}
871 %************************************************************************
873 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
875 f :: (?x::Int) => Int -> Int
878 isSigmaTy :: Type -> Bool
879 isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
880 isSigmaTy (ForAllTy tyvar ty) = True
881 isSigmaTy (FunTy a b) = isPredTy a
884 isOverloadedTy :: Type -> Bool
885 isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
886 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
887 isOverloadedTy (FunTy a b) = isPredTy a
888 isOverloadedTy _ = False
890 isPredTy :: Type -> Bool -- Belongs in TcType because it does
891 -- not look through newtypes, or predtypes (of course)
892 isPredTy ty | Just ty' <- tcView ty = isPredTy ty'
893 isPredTy (PredTy sty) = True
898 isFloatTy = is_tc floatTyConKey
899 isDoubleTy = is_tc doubleTyConKey
900 isIntegerTy = is_tc integerTyConKey
901 isIntTy = is_tc intTyConKey
902 isBoolTy = is_tc boolTyConKey
903 isUnitTy = is_tc unitTyConKey
905 is_tc :: Unique -> Type -> Bool
906 -- Newtypes are opaque to this
907 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
908 Just (tc, _) -> uniq == getUnique tc
913 %************************************************************************
917 %************************************************************************
920 deNoteType :: Type -> Type
921 -- Remove all *outermost* type synonyms and other notes
922 deNoteType ty | Just ty' <- tcView ty = deNoteType ty'
927 tcTyVarsOfType :: Type -> TcTyVarSet
928 -- Just the tc type variables free in the type
929 tcTyVarsOfType (TyVarTy tv) = if isTcTyVar tv then unitVarSet tv
931 tcTyVarsOfType (TyConApp tycon tys) = tcTyVarsOfTypes tys
932 tcTyVarsOfType (NoteTy _ ty) = tcTyVarsOfType ty
933 tcTyVarsOfType (PredTy sty) = tcTyVarsOfPred sty
934 tcTyVarsOfType (FunTy arg res) = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
935 tcTyVarsOfType (AppTy fun arg) = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
936 tcTyVarsOfType (ForAllTy tyvar ty) = tcTyVarsOfType ty `delVarSet` tyvar
937 -- We do sometimes quantify over skolem TcTyVars
939 tcTyVarsOfTypes :: [Type] -> TyVarSet
940 tcTyVarsOfTypes tys = foldr (unionVarSet.tcTyVarsOfType) emptyVarSet tys
942 tcTyVarsOfPred :: PredType -> TyVarSet
943 tcTyVarsOfPred (IParam _ ty) = tcTyVarsOfType ty
944 tcTyVarsOfPred (ClassP _ tys) = tcTyVarsOfTypes tys
947 Note [Silly type synonym]
948 ~~~~~~~~~~~~~~~~~~~~~~~~~
951 What are the free tyvars of (T x)? Empty, of course!
952 Here's the example that Ralf Laemmel showed me:
953 foo :: (forall a. C u a -> C u a) -> u
954 mappend :: Monoid u => u -> u -> u
957 bar = foo (\t -> t `mappend` t)
958 We have to generalise at the arg to f, and we don't
959 want to capture the constraint (Monad (C u a)) because
960 it appears to mention a. Pretty silly, but it was useful to him.
962 exactTyVarsOfType is used by the type checker to figure out exactly
963 which type variables are mentioned in a type. It's also used in the
964 smart-app checking code --- see TcExpr.tcIdApp
967 exactTyVarsOfType :: TcType -> TyVarSet
968 -- Find the free type variables (of any kind)
969 -- but *expand* type synonyms. See Note [Silly type synonym] belos.
973 go ty | Just ty' <- tcView ty = go ty' -- This is the key line
974 go (TyVarTy tv) = unitVarSet tv
975 go (TyConApp tycon tys) = exactTyVarsOfTypes tys
976 go (PredTy ty) = go_pred ty
977 go (FunTy arg res) = go arg `unionVarSet` go res
978 go (AppTy fun arg) = go fun `unionVarSet` go arg
979 go (ForAllTy tyvar ty) = delVarSet (go ty) tyvar
981 go_pred (IParam _ ty) = go ty
982 go_pred (ClassP _ tys) = exactTyVarsOfTypes tys
984 exactTyVarsOfTypes :: [TcType] -> TyVarSet
985 exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
988 Find the free tycons and classes of a type. This is used in the front
992 tyClsNamesOfType :: Type -> NameSet
993 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
994 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
995 tyClsNamesOfType (NoteTy _ ty2) = tyClsNamesOfType ty2
996 tyClsNamesOfType (PredTy (IParam n ty)) = tyClsNamesOfType ty
997 tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
998 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
999 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
1000 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
1002 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
1004 tyClsNamesOfDFunHead :: Type -> NameSet
1005 -- Find the free type constructors and classes
1006 -- of the head of the dfun instance type
1007 -- The 'dfun_head_type' is because of
1008 -- instance Foo a => Baz T where ...
1009 -- The decl is an orphan if Baz and T are both not locally defined,
1010 -- even if Foo *is* locally defined
1011 tyClsNamesOfDFunHead dfun_ty
1012 = case tcSplitSigmaTy dfun_ty of
1013 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
1015 classesOfTheta :: ThetaType -> [Class]
1016 -- Looks just for ClassP things; maybe it should check
1017 classesOfTheta preds = [ c | ClassP c _ <- preds ]
1021 %************************************************************************
1023 \subsection[TysWiredIn-ext-type]{External types}
1025 %************************************************************************
1027 The compiler's foreign function interface supports the passing of a
1028 restricted set of types as arguments and results (the restricting factor
1032 tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type)
1033 -- (isIOType t) returns (Just (IO,t')) if t is of the form (IO t'), or
1034 -- some newtype wrapping thereof
1035 -- returns Nothing otherwise
1036 tcSplitIOType_maybe ty
1037 | Just (io_tycon, [io_res_ty]) <- tcSplitTyConApp_maybe ty,
1038 -- This split absolutely has to be a tcSplit, because we must
1039 -- see the IO type; and it's a newtype which is transparent to splitTyConApp.
1040 io_tycon `hasKey` ioTyConKey
1041 = Just (io_tycon, io_res_ty)
1043 | Just ty' <- coreView ty -- Look through non-recursive newtypes
1044 = tcSplitIOType_maybe ty'
1049 isFFITy :: Type -> Bool
1050 -- True for any TyCon that can possibly be an arg or result of an FFI call
1051 isFFITy ty = checkRepTyCon legalFFITyCon ty
1053 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
1054 -- Checks for valid argument type for a 'foreign import'
1055 isFFIArgumentTy dflags safety ty
1056 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
1058 isFFIExternalTy :: Type -> Bool
1059 -- Types that are allowed as arguments of a 'foreign export'
1060 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
1062 isFFIImportResultTy :: DynFlags -> Type -> Bool
1063 isFFIImportResultTy dflags ty
1064 = checkRepTyCon (legalFIResultTyCon dflags) ty
1066 isFFIExportResultTy :: Type -> Bool
1067 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
1069 isFFIDynArgumentTy :: Type -> Bool
1070 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
1071 -- or a newtype of either.
1072 isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
1074 isFFIDynResultTy :: Type -> Bool
1075 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
1076 -- or a newtype of either.
1077 isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
1079 isFFILabelTy :: Type -> Bool
1080 -- The type of a foreign label must be Ptr, FunPtr, Addr,
1081 -- or a newtype of either.
1082 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
1084 isFFIDotnetTy :: DynFlags -> Type -> Bool
1085 isFFIDotnetTy dflags ty
1086 = checkRepTyCon (\ tc -> (legalFIResultTyCon dflags tc ||
1087 isFFIDotnetObjTy ty || isStringTy ty)) ty
1089 -- Support String as an argument or result from a .NET FFI call.
1091 case tcSplitTyConApp_maybe (repType ty) of
1093 | tc == listTyCon ->
1094 case tcSplitTyConApp_maybe (repType arg_ty) of
1095 Just (cc,[]) -> cc == charTyCon
1099 -- Support String as an argument or result from a .NET FFI call.
1100 isFFIDotnetObjTy ty =
1102 (_, t_ty) = tcSplitForAllTys ty
1104 case tcSplitTyConApp_maybe (repType t_ty) of
1105 Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
1108 toDNType :: Type -> DNType
1110 | isStringTy ty = DNString
1111 | isFFIDotnetObjTy ty = DNObject
1112 | Just (tc,argTys) <- tcSplitTyConApp_maybe ty =
1113 case lookup (getUnique tc) dn_assoc of
1116 | tc `hasKey` ioTyConKey -> toDNType (head argTys)
1117 | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
1119 dn_assoc :: [ (Unique, DNType) ]
1120 dn_assoc = [ (unitTyConKey, DNUnit)
1121 , (intTyConKey, DNInt)
1122 , (int8TyConKey, DNInt8)
1123 , (int16TyConKey, DNInt16)
1124 , (int32TyConKey, DNInt32)
1125 , (int64TyConKey, DNInt64)
1126 , (wordTyConKey, DNInt)
1127 , (word8TyConKey, DNWord8)
1128 , (word16TyConKey, DNWord16)
1129 , (word32TyConKey, DNWord32)
1130 , (word64TyConKey, DNWord64)
1131 , (floatTyConKey, DNFloat)
1132 , (doubleTyConKey, DNDouble)
1133 , (ptrTyConKey, DNPtr)
1134 , (funPtrTyConKey, DNPtr)
1135 , (charTyConKey, DNChar)
1136 , (boolTyConKey, DNBool)
1139 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
1140 -- Look through newtypes
1141 -- Non-recursive ones are transparent to splitTyConApp,
1142 -- but recursive ones aren't. Manuel had:
1143 -- newtype T = MkT (Ptr T)
1144 -- and wanted it to work...
1145 checkRepTyCon check_tc ty
1146 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
1149 checkRepTyConKey :: [Unique] -> Type -> Bool
1150 -- Like checkRepTyCon, but just looks at the TyCon key
1151 checkRepTyConKey keys
1152 = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
1155 ----------------------------------------------
1156 These chaps do the work; they are not exported
1157 ----------------------------------------------
1160 legalFEArgTyCon :: TyCon -> Bool
1162 -- It's illegal to make foreign exports that take unboxed
1163 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
1164 = boxedMarshalableTyCon tc
1166 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
1167 legalFIResultTyCon dflags tc
1168 | tc == unitTyCon = True
1169 | otherwise = marshalableTyCon dflags tc
1171 legalFEResultTyCon :: TyCon -> Bool
1172 legalFEResultTyCon tc
1173 | tc == unitTyCon = True
1174 | otherwise = boxedMarshalableTyCon tc
1176 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
1177 -- Checks validity of types going from Haskell -> external world
1178 legalOutgoingTyCon dflags safety tc
1179 = marshalableTyCon dflags tc
1181 legalFFITyCon :: TyCon -> Bool
1182 -- True for any TyCon that can possibly be an arg or result of an FFI call
1184 = isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon
1186 marshalableTyCon dflags tc
1187 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
1188 || boxedMarshalableTyCon tc
1190 boxedMarshalableTyCon tc
1191 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
1192 , int32TyConKey, int64TyConKey
1193 , wordTyConKey, word8TyConKey, word16TyConKey
1194 , word32TyConKey, word64TyConKey
1195 , floatTyConKey, doubleTyConKey
1196 , ptrTyConKey, funPtrTyConKey