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 --------------------------------
25 Expected(..), TcRef, TcTyVarDetails(..),
26 MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo,
27 isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef,
30 --------------------------------
32 mkPhiTy, mkSigmaTy, hoistForAllTys,
34 --------------------------------
36 -- These are important because they do not look through newtypes
37 tcSplitForAllTys, tcSplitPhiTy,
38 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
39 tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
40 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
41 tcGetTyVar_maybe, tcGetTyVar,
43 ---------------------------------
45 -- Again, newtypes are opaque
46 tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
47 isSigmaTy, isOverloadedTy,
48 isDoubleTy, isFloatTy, isIntTy, isStringTy,
49 isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
50 isTauTy, tcIsTyVarTy, tcIsForAllTy,
52 ---------------------------------
53 -- Misc type manipulators
54 deNoteType, classesOfTheta,
55 tyClsNamesOfType, tyClsNamesOfDFunHead,
58 ---------------------------------
60 getClassPredTys_maybe, getClassPredTys,
61 isClassPred, isTyVarClassPred,
62 mkDictTy, tcSplitPredTy_maybe,
63 isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique,
64 mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
66 ---------------------------------
67 -- Foreign import and export
68 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
69 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
70 isFFIExportResultTy, -- :: Type -> Bool
71 isFFIExternalTy, -- :: Type -> Bool
72 isFFIDynArgumentTy, -- :: Type -> Bool
73 isFFIDynResultTy, -- :: Type -> Bool
74 isFFILabelTy, -- :: Type -> Bool
75 isFFIDotnetTy, -- :: DynFlags -> Type -> Bool
76 isFFIDotnetObjTy, -- :: Type -> Bool
77 isFFITy, -- :: Type -> Bool
79 toDNType, -- :: Type -> DNType
81 --------------------------------
82 -- Rexported from Type
83 Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
84 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
85 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
86 isArgTypeKind, isSubKind, defaultKind,
88 Type, PredType(..), ThetaType,
89 mkForAllTy, mkForAllTys,
90 mkFunTy, mkFunTys, zipFunTys,
91 mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
92 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
95 TvSubst(..), -- Representation visible to a few friends
96 TvSubstEnv, emptyTvSubst,
97 mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
98 getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
99 extendTvSubst, extendTvSubstList, isInScope,
100 substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
102 isUnLiftedType, -- Source types are always lifted
103 isUnboxedTupleType, -- Ditto
106 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
107 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
110 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
112 pprKind, pprParendKind,
113 pprType, pprParendType, pprTyThingCategory,
114 pprPred, pprTheta, pprThetaArrow, pprClassPred
118 #include "HsVersions.h"
121 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
123 import Type ( -- Re-exports
124 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
125 tyVarsOfTheta, Kind, PredType(..),
126 ThetaType, unliftedTypeKind,
127 liftedTypeKind, openTypeKind, mkArrowKind,
128 isLiftedTypeKind, isUnliftedTypeKind,
129 mkArrowKinds, mkForAllTy, mkForAllTys,
130 defaultKind, isArgTypeKind, isOpenTypeKind,
131 mkFunTy, mkFunTys, zipFunTys,
132 mkTyConApp, mkGenTyConApp, mkAppTy,
133 mkAppTys, mkSynTy, applyTy, applyTys,
134 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
135 mkPredTys, isUnLiftedType,
136 isUnboxedTupleType, isPrimitiveType,
138 tidyTopType, tidyType, tidyPred, tidyTypes,
139 tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
140 tidyTyVarBndr, tidyOpenTyVar,
142 isSubKind, deShadowTy,
144 tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
145 tcEqPred, tcCmpPred, tcEqTypeX,
148 TvSubstEnv, emptyTvSubst,
149 mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
150 getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
151 extendTvSubst, extendTvSubstList, isInScope,
152 substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
155 pprKind, pprParendKind,
156 pprType, pprParendType, pprTyThingCategory,
157 pprPred, pprTheta, pprThetaArrow, pprClassPred
159 import TyCon ( TyCon, isUnLiftedTyCon, tyConUnique )
160 import DataCon ( DataCon )
161 import Class ( Class )
162 import Var ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
163 import ForeignCall ( Safety, playSafe, DNType(..) )
167 import DynFlags ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
168 import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
170 import VarEnv ( TidyEnv )
171 import OccName ( OccName, mkDictOcc )
172 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
173 import TysWiredIn ( unitTyCon, charTyCon, listTyCon )
174 import BasicTypes ( IPName(..), ipNameName )
175 import SrcLoc ( SrcLoc, SrcSpan )
176 import Util ( snocView )
177 import Maybes ( maybeToBool, expectJust )
183 %************************************************************************
187 %************************************************************************
189 The type checker divides the generic Type world into the
190 following more structured beasts:
192 sigma ::= forall tyvars. phi
193 -- A sigma type is a qualified type
195 -- Note that even if 'tyvars' is empty, theta
196 -- may not be: e.g. (?x::Int) => Int
198 -- Note that 'sigma' is in prenex form:
199 -- all the foralls are at the front.
200 -- A 'phi' type has no foralls to the right of
208 -- A 'tau' type has no quantification anywhere
209 -- Note that the args of a type constructor must be taus
211 | tycon tau_1 .. tau_n
215 -- In all cases, a (saturated) type synonym application is legal,
216 -- provided it expands to the required form.
219 type TcType = Type -- A TcType can have mutable type variables
220 -- Invariant on ForAllTy in TcTypes:
222 -- a cannot occur inside a MutTyVar in T; that is,
223 -- T is "flattened" before quantifying over a
225 type TcPredType = PredType
226 type TcThetaType = ThetaType
227 type TcSigmaType = TcType
228 type TcRhoType = TcType
229 type TcTauType = TcType
231 type TcTyVarSet = TyVarSet
233 type TcRef a = IORef a
234 data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference
235 | Check ty -- The type to check during type checking
239 %************************************************************************
241 \subsection{TyVarDetails}
243 %************************************************************************
245 TyVarDetails gives extra info about type variables, used during type
246 checking. It's attached to mutable type variables only.
247 It's knot-tied back to Var.lhs. There is no reason in principle
248 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
250 Note [Signature skolems]
251 ~~~~~~~~~~~~~~~~~~~~~~~~
256 (x,y,z) = ([y,z], z, head x)
258 Here, x and y have type sigs, which go into the environment. We used to
259 instantiate their types with skolem constants, and push those types into
260 the RHS, so we'd typecheck the RHS with type
262 where a*, b* are skolem constants, and c is an ordinary meta type varible.
264 The trouble is that the occurrences of z in the RHS force a* and b* to
265 be the *same*, so we can't make them into skolem constants that don't unify
266 with each other. Alas.
268 On the other hand, we *must* use skolems for signature type variables,
269 becuase GADT type refinement refines skolems only.
271 One solution woudl be insist that in the above defn the programmer uses
272 the same type variable in both type signatures. But that takes explanation.
274 The alternative (currently implemented) is to have a special kind of skolem
275 constant, SigSkokTv, which can unify with other SigSkolTvs.
279 type TcTyVar = TyVar -- Used only during type inference
281 -- A TyVarDetails is inside a TyVar
283 = MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type
284 | SkolemTv SkolemInfo -- A skolem constant
285 | SigSkolTv Name (IORef MetaDetails) -- Ditto, but from a type signature;
286 -- see Note [Signature skolems]
287 -- The MetaDetails, if filled in, will
288 -- always be another SigSkolTv
291 = SigSkol Name -- Bound at a type signature
292 | ClsSkol Class -- Bound at a class decl
293 | InstSkol Id -- Bound at an instance decl
294 | PatSkol DataCon -- An existential type variable bound by a pattern for
295 SrcSpan -- a data constructor with an existential type. E.g.
296 -- data T = forall a. Eq a => MkT a
298 -- The pattern MkT x will allocate an existential type
300 | ArrowSkol SrcSpan -- An arrow form (see TcArrows)
302 | GenSkol [TcTyVar] -- Bound when doing a subsumption check for
303 TcType -- (forall tvs. ty)
307 = Flexi -- Flexi type variables unify to become
310 | Indirect TcType -- Type indirections, treated as wobbly
311 -- for the purpose of GADT unification.
313 tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
314 -- Tidy the type inside a GenSkol, preparatory to printing it
315 tidySkolemTyVar env tv
316 = ASSERT( isSkolemTyVar tv )
317 (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
319 (env1, info1) = case tcTyVarDetails tv of
320 SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc))
322 (env1, tvs1) = tidyOpenTyVars env tvs
323 (env2, ty1) = tidyOpenType env1 ty
326 pprTcTyVar :: TcTyVar -> SDoc
327 -- Print tyvar with info about its binding
329 = quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
331 ppr_details (MetaTv _) = ptext SLIT("is a meta type variable")
332 ppr_details (SigSkolTv id _) = ptext SLIT("is bound by") <+> pprSkolInfo (SigSkol id)
333 ppr_details (SkolemTv info) = ptext SLIT("is bound by") <+> pprSkolInfo info
335 pprSkolInfo :: SkolemInfo -> SDoc
336 pprSkolInfo (SigSkol id) = ptext SLIT("the type signature for") <+> quotes (ppr id)
337 pprSkolInfo (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
338 pprSkolInfo (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
339 pprSkolInfo (ArrowSkol loc) = ptext SLIT("the arrow form at") <+> ppr loc
340 pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
341 nest 2 (ptext SLIT("at") <+> ppr loc)]
342 pprSkolInfo (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type")
343 <+> quotes (ppr (mkForAllTys tvs ty)),
344 nest 2 (ptext SLIT("at") <+> ppr loc)]
346 instance Outputable MetaDetails where
347 ppr Flexi = ptext SLIT("Flexi")
348 ppr (Indirect ty) = ptext SLIT("Indirect") <+> ppr ty
350 isImmutableTyVar, isSkolemTyVar, isExistentialTyVar, isMetaTyVar :: TyVar -> Bool
352 | isTcTyVar tv = isSkolemTyVar tv
356 = ASSERT( isTcTyVar tv )
357 case tcTyVarDetails tv of
359 SigSkolTv _ _ -> True
362 isExistentialTyVar tv -- Existential type variable, bound by a pattern
363 = ASSERT( isTcTyVar tv )
364 case tcTyVarDetails tv of
365 SkolemTv (PatSkol _ _) -> True
369 = ASSERT( isTcTyVar tv )
370 case tcTyVarDetails tv of
374 metaTvRef :: TyVar -> IORef MetaDetails
376 = ASSERT( isTcTyVar tv )
377 case tcTyVarDetails tv of
379 other -> pprPanic "metaTvRef" (ppr tv)
381 isFlexi, isIndirect :: MetaDetails -> Bool
383 isFlexi other = False
385 isIndirect (Indirect _) = True
386 isIndirect other = False
390 %************************************************************************
392 \subsection{Tau, sigma and rho}
394 %************************************************************************
397 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
399 mkPhiTy :: [PredType] -> Type -> Type
400 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
403 @isTauTy@ tests for nested for-alls.
406 isTauTy :: Type -> Bool
407 isTauTy (TyVarTy v) = True
408 isTauTy (TyConApp _ tys) = all isTauTy tys
409 isTauTy (AppTy a b) = isTauTy a && isTauTy b
410 isTauTy (FunTy a b) = isTauTy a && isTauTy b
411 isTauTy (PredTy p) = True -- Don't look through source types
412 isTauTy (NoteTy _ ty) = isTauTy ty
413 isTauTy other = False
417 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
418 -- construct a dictionary function name
419 getDFunTyKey (TyVarTy tv) = getOccName tv
420 getDFunTyKey (TyConApp tc _) = getOccName tc
421 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
422 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
423 getDFunTyKey (FunTy arg _) = getOccName funTyCon
424 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
425 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
426 -- PredTy shouldn't happen
430 %************************************************************************
432 \subsection{Expanding and splitting}
434 %************************************************************************
436 These tcSplit functions are like their non-Tc analogues, but
437 a) they do not look through newtypes
438 b) they do not look through PredTys
439 c) [future] they ignore usage-type annotations
441 However, they are non-monadic and do not follow through mutable type
442 variables. It's up to you to make sure this doesn't matter.
445 tcSplitForAllTys :: Type -> ([TyVar], Type)
446 tcSplitForAllTys ty = split ty ty []
448 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
449 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
450 split orig_ty t tvs = (reverse tvs, orig_ty)
452 tcIsForAllTy (ForAllTy tv ty) = True
453 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
454 tcIsForAllTy t = False
456 tcSplitPhiTy :: Type -> ([PredType], Type)
457 tcSplitPhiTy ty = split ty ty []
459 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
460 Just p -> split res res (p:ts)
461 Nothing -> (reverse ts, orig_ty)
462 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
463 split orig_ty ty ts = (reverse ts, orig_ty)
465 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
466 (tvs, rho) -> case tcSplitPhiTy rho of
467 (theta, tau) -> (tvs, theta, tau)
469 tcTyConAppTyCon :: Type -> TyCon
470 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
472 tcTyConAppArgs :: Type -> [Type]
473 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
475 tcSplitTyConApp :: Type -> (TyCon, [Type])
476 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
478 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
480 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
481 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
482 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
483 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
484 -- Newtypes are opaque, so they may be split
485 -- However, predicates are not treated
486 -- as tycon applications by the type checker
487 tcSplitTyConApp_maybe other = Nothing
489 tcSplitFunTys :: Type -> ([Type], Type)
490 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
492 Just (arg,res) -> (arg:args, res')
494 (args,res') = tcSplitFunTys res
496 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
497 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
498 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
499 tcSplitFunTy_maybe other = Nothing
501 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
502 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
505 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
506 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
507 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
508 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
509 tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
510 Just (tys', ty') -> Just (TyConApp tc tys', ty')
512 tcSplitAppTy_maybe other = Nothing
514 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
516 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
518 tcSplitAppTys :: Type -> (Type, [Type])
522 go ty args = case tcSplitAppTy_maybe ty of
523 Just (ty', arg) -> go ty' (arg:args)
526 tcGetTyVar_maybe :: Type -> Maybe TyVar
527 tcGetTyVar_maybe (TyVarTy tv) = Just tv
528 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
529 tcGetTyVar_maybe other = Nothing
531 tcGetTyVar :: String -> Type -> TyVar
532 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
534 tcIsTyVarTy :: Type -> Bool
535 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
537 tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
538 -- Split the type of a dictionary function
540 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
541 case tcSplitDFunHead tau of { (clas, tys) ->
542 (tvs, theta, clas, tys) }}
544 tcSplitDFunHead :: Type -> (Class, [Type])
546 = case tcSplitPredTy_maybe tau of
547 Just (ClassP clas tys) -> (clas, tys)
552 %************************************************************************
554 \subsection{Predicate types}
556 %************************************************************************
559 tcSplitPredTy_maybe :: Type -> Maybe PredType
560 -- Returns Just for predicates only
561 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
562 tcSplitPredTy_maybe (PredTy p) = Just p
563 tcSplitPredTy_maybe other = Nothing
565 predTyUnique :: PredType -> Unique
566 predTyUnique (IParam n _) = getUnique (ipNameName n)
567 predTyUnique (ClassP clas tys) = getUnique clas
569 mkPredName :: Unique -> SrcLoc -> PredType -> Name
570 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
571 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
575 --------------------- Dictionary types ---------------------------------
578 mkClassPred clas tys = ClassP clas tys
580 isClassPred :: PredType -> Bool
581 isClassPred (ClassP clas tys) = True
582 isClassPred other = False
584 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
585 isTyVarClassPred other = False
587 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
588 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
589 getClassPredTys_maybe _ = Nothing
591 getClassPredTys :: PredType -> (Class, [Type])
592 getClassPredTys (ClassP clas tys) = (clas, tys)
594 mkDictTy :: Class -> [Type] -> Type
595 mkDictTy clas tys = mkPredTy (ClassP clas tys)
597 isDictTy :: Type -> Bool
598 isDictTy (PredTy p) = isClassPred p
599 isDictTy (NoteTy _ ty) = isDictTy ty
600 isDictTy other = False
603 --------------------- Implicit parameters ---------------------------------
606 isIPPred :: PredType -> Bool
607 isIPPred (IParam _ _) = True
608 isIPPred other = False
610 isInheritablePred :: PredType -> Bool
611 -- Can be inherited by a context. For example, consider
612 -- f x = let g y = (?v, y+x)
613 -- in (g 3 with ?v = 8,
615 -- The point is that g's type must be quantifed over ?v:
616 -- g :: (?v :: a) => a -> a
617 -- but it doesn't need to be quantified over the Num a dictionary
618 -- which can be free in g's rhs, and shared by both calls to g
619 isInheritablePred (ClassP _ _) = True
620 isInheritablePred other = False
622 isLinearPred :: TcPredType -> Bool
623 isLinearPred (IParam (Linear n) _) = True
624 isLinearPred other = False
628 %************************************************************************
630 \subsection{Predicates}
632 %************************************************************************
634 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
636 f :: (?x::Int) => Int -> Int
639 isSigmaTy :: Type -> Bool
640 isSigmaTy (ForAllTy tyvar ty) = True
641 isSigmaTy (FunTy a b) = isPredTy a
642 isSigmaTy (NoteTy n ty) = isSigmaTy ty
645 isOverloadedTy :: Type -> Bool
646 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
647 isOverloadedTy (FunTy a b) = isPredTy a
648 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
649 isOverloadedTy _ = False
651 isPredTy :: Type -> Bool -- Belongs in TcType because it does
652 -- not look through newtypes, or predtypes (of course)
653 isPredTy (NoteTy _ ty) = isPredTy ty
654 isPredTy (PredTy sty) = True
659 isFloatTy = is_tc floatTyConKey
660 isDoubleTy = is_tc doubleTyConKey
661 isIntegerTy = is_tc integerTyConKey
662 isIntTy = is_tc intTyConKey
663 isAddrTy = is_tc addrTyConKey
664 isBoolTy = is_tc boolTyConKey
665 isUnitTy = is_tc unitTyConKey
667 is_tc :: Unique -> Type -> Bool
668 -- Newtypes are opaque to this
669 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
670 Just (tc, _) -> uniq == getUnique tc
677 %************************************************************************
681 %************************************************************************
683 hoistForAllTys is used for user-written type signatures only
684 We want to 'look through' type synonyms when doing this
685 so it's better done on the Type than the HsType
687 It moves all the foralls and constraints to the top
688 e.g. T -> forall a. a ==> forall a. T -> a
689 T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
691 Also: it eliminates duplicate constraints. These can show up
692 when hoisting constraints, notably implicit parameters.
694 It tries hard to retain type synonyms if hoisting does not break one
695 up. Not only does this improve error messages, but there's a tricky
696 interaction with Haskell 98. H98 requires no unsaturated type
697 synonyms, which is checked by checkValidType. This runs after
698 hoisting, so we don't want hoisting to remove the SynNotes! (We can't
699 run validity checking before hoisting because in mutually-recursive
700 type definitions we postpone validity checking until after the knot is
704 hoistForAllTys :: Type -> Type
707 -- Running over ty with an empty substitution gives it the
708 -- no-shadowing property. This is important. For example:
709 -- type Foo r = forall a. a -> r
710 -- foo :: Foo (Foo ())
711 -- Here the hoisting should give
712 -- foo :: forall a a1. a -> a1 -> ()
714 -- What about type vars that are lexically in scope in the envt?
715 -- We simply rely on them having a different unique to any
716 -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
717 -- out of the envt, which is boring and (I think) not necessary.
720 go (TyVarTy tv) = TyVarTy tv
721 go (TyConApp tc tys) = TyConApp tc (map go tys)
722 go (PredTy pred) = PredTy pred -- No nested foralls
723 go (NoteTy (SynNote ty1) ty2) = NoteTy (SynNote (go ty1)) (go ty2)
724 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard the free tyvar note
725 go (FunTy arg res) = mk_fun_ty (go arg) (go res)
726 go (AppTy fun arg) = AppTy (go fun) (go arg)
727 go (ForAllTy tv ty) = ForAllTy tv (go ty)
729 -- mk_fun_ty does all the work.
730 -- It's building t1 -> t2:
731 -- if t2 is a for-all type, push t1 inside it
732 -- if t2 is (pred -> t3), check for duplicates
734 | not (isSigmaTy ty2) -- No forall's, or context =>
736 | PredTy p1 <- ty1 -- ty1 is a predicate
737 = if p1 `elem` theta then -- so check for duplicates
740 mkSigmaTy tvs (p1:theta) tau
742 = mkSigmaTy tvs theta (FunTy ty1 tau)
744 (tvs, theta, tau) = tcSplitSigmaTy ty2
748 %************************************************************************
752 %************************************************************************
755 deNoteType :: Type -> Type
756 -- Remove *outermost* type synonyms and other notes
757 deNoteType (NoteTy _ ty) = deNoteType ty
761 Find the free tycons and classes of a type. This is used in the front
765 tyClsNamesOfType :: Type -> NameSet
766 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
767 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
768 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
769 tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
770 tyClsNamesOfType (PredTy (IParam n ty)) = tyClsNamesOfType ty
771 tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
772 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
773 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
774 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
776 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
778 tyClsNamesOfDFunHead :: Type -> NameSet
779 -- Find the free type constructors and classes
780 -- of the head of the dfun instance type
781 -- The 'dfun_head_type' is because of
782 -- instance Foo a => Baz T where ...
783 -- The decl is an orphan if Baz and T are both not locally defined,
784 -- even if Foo *is* locally defined
785 tyClsNamesOfDFunHead dfun_ty
786 = case tcSplitSigmaTy dfun_ty of
787 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
789 classesOfTheta :: ThetaType -> [Class]
790 -- Looks just for ClassP things; maybe it should check
791 classesOfTheta preds = [ c | ClassP c _ <- preds ]
795 %************************************************************************
797 \subsection[TysWiredIn-ext-type]{External types}
799 %************************************************************************
801 The compiler's foreign function interface supports the passing of a
802 restricted set of types as arguments and results (the restricting factor
806 isFFITy :: Type -> Bool
807 -- True for any TyCon that can possibly be an arg or result of an FFI call
808 isFFITy ty = checkRepTyCon legalFFITyCon ty
810 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
811 -- Checks for valid argument type for a 'foreign import'
812 isFFIArgumentTy dflags safety ty
813 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
815 isFFIExternalTy :: Type -> Bool
816 -- Types that are allowed as arguments of a 'foreign export'
817 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
819 isFFIImportResultTy :: DynFlags -> Type -> Bool
820 isFFIImportResultTy dflags ty
821 = checkRepTyCon (legalFIResultTyCon dflags) ty
823 isFFIExportResultTy :: Type -> Bool
824 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
826 isFFIDynArgumentTy :: Type -> Bool
827 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
828 -- or a newtype of either.
829 isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
831 isFFIDynResultTy :: Type -> Bool
832 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
833 -- or a newtype of either.
834 isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
836 isFFILabelTy :: Type -> Bool
837 -- The type of a foreign label must be Ptr, FunPtr, Addr,
838 -- or a newtype of either.
839 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
841 isFFIDotnetTy :: DynFlags -> Type -> Bool
842 isFFIDotnetTy dflags ty
843 = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
844 (legalFIResultTyCon dflags tc ||
845 isFFIDotnetObjTy ty || isStringTy ty)) ty
847 -- Support String as an argument or result from a .NET FFI call.
849 case tcSplitTyConApp_maybe (repType ty) of
852 case tcSplitTyConApp_maybe (repType arg_ty) of
853 Just (cc,[]) -> cc == charTyCon
857 -- Support String as an argument or result from a .NET FFI call.
858 isFFIDotnetObjTy ty =
860 (_, t_ty) = tcSplitForAllTys ty
862 case tcSplitTyConApp_maybe (repType t_ty) of
863 Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
866 toDNType :: Type -> DNType
868 | isStringTy ty = DNString
869 | isFFIDotnetObjTy ty = DNObject
870 | Just (tc,argTys) <- tcSplitTyConApp_maybe ty =
871 case lookup (getUnique tc) dn_assoc of
874 | tc `hasKey` ioTyConKey -> toDNType (head argTys)
875 | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
877 dn_assoc :: [ (Unique, DNType) ]
878 dn_assoc = [ (unitTyConKey, DNUnit)
879 , (intTyConKey, DNInt)
880 , (int8TyConKey, DNInt8)
881 , (int16TyConKey, DNInt16)
882 , (int32TyConKey, DNInt32)
883 , (int64TyConKey, DNInt64)
884 , (wordTyConKey, DNInt)
885 , (word8TyConKey, DNWord8)
886 , (word16TyConKey, DNWord16)
887 , (word32TyConKey, DNWord32)
888 , (word64TyConKey, DNWord64)
889 , (floatTyConKey, DNFloat)
890 , (doubleTyConKey, DNDouble)
891 , (addrTyConKey, DNPtr)
892 , (ptrTyConKey, DNPtr)
893 , (funPtrTyConKey, DNPtr)
894 , (charTyConKey, DNChar)
895 , (boolTyConKey, DNBool)
898 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
899 -- Look through newtypes
900 -- Non-recursive ones are transparent to splitTyConApp,
901 -- but recursive ones aren't. Manuel had:
902 -- newtype T = MkT (Ptr T)
903 -- and wanted it to work...
904 checkRepTyCon check_tc ty
905 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
908 checkRepTyConKey :: [Unique] -> Type -> Bool
909 -- Like checkRepTyCon, but just looks at the TyCon key
910 checkRepTyConKey keys
911 = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
914 ----------------------------------------------
915 These chaps do the work; they are not exported
916 ----------------------------------------------
919 legalFEArgTyCon :: TyCon -> Bool
920 -- It's illegal to return foreign objects and (mutable)
921 -- bytearrays from a _ccall_ / foreign declaration
922 -- (or be passed them as arguments in foreign exported functions).
924 | isByteArrayLikeTyCon tc
926 -- It's also illegal to make foreign exports that take unboxed
927 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
929 = boxedMarshalableTyCon tc
931 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
932 legalFIResultTyCon dflags tc
933 | isByteArrayLikeTyCon tc = False
934 | tc == unitTyCon = True
935 | otherwise = marshalableTyCon dflags tc
937 legalFEResultTyCon :: TyCon -> Bool
938 legalFEResultTyCon tc
939 | isByteArrayLikeTyCon tc = False
940 | tc == unitTyCon = True
941 | otherwise = boxedMarshalableTyCon tc
943 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
944 -- Checks validity of types going from Haskell -> external world
945 legalOutgoingTyCon dflags safety tc
946 | playSafe safety && isByteArrayLikeTyCon tc
949 = marshalableTyCon dflags tc
951 legalFFITyCon :: TyCon -> Bool
952 -- True for any TyCon that can possibly be an arg or result of an FFI call
954 = isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon
956 marshalableTyCon dflags tc
957 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
958 || boxedMarshalableTyCon tc
960 boxedMarshalableTyCon tc
961 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
962 , int32TyConKey, int64TyConKey
963 , wordTyConKey, word8TyConKey, word16TyConKey
964 , word32TyConKey, word64TyConKey
965 , floatTyConKey, doubleTyConKey
966 , addrTyConKey, ptrTyConKey, funPtrTyConKey
969 , byteArrayTyConKey, mutableByteArrayTyConKey
973 isByteArrayLikeTyCon :: TyCon -> Bool
974 isByteArrayLikeTyCon tc =
975 getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]