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 synonyms, but not predicate types
757 deNoteType ty@(TyVarTy tyvar) = ty
758 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
759 deNoteType (PredTy p) = PredTy (deNotePredType p)
760 deNoteType (NoteTy _ ty) = deNoteType ty
761 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
762 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
763 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
765 deNotePredType :: PredType -> PredType
766 deNotePredType (ClassP c tys) = ClassP c (map deNoteType tys)
767 deNotePredType (IParam n ty) = IParam n (deNoteType ty)
770 Find the free tycons and classes of a type. This is used in the front
774 tyClsNamesOfType :: Type -> NameSet
775 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
776 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
777 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
778 tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
779 tyClsNamesOfType (PredTy (IParam n ty)) = tyClsNamesOfType ty
780 tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
781 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
782 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
783 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
785 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
787 tyClsNamesOfDFunHead :: Type -> NameSet
788 -- Find the free type constructors and classes
789 -- of the head of the dfun instance type
790 -- The 'dfun_head_type' is because of
791 -- instance Foo a => Baz T where ...
792 -- The decl is an orphan if Baz and T are both not locally defined,
793 -- even if Foo *is* locally defined
794 tyClsNamesOfDFunHead dfun_ty
795 = case tcSplitSigmaTy dfun_ty of
796 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
798 classesOfTheta :: ThetaType -> [Class]
799 -- Looks just for ClassP things; maybe it should check
800 classesOfTheta preds = [ c | ClassP c _ <- preds ]
804 %************************************************************************
806 \subsection[TysWiredIn-ext-type]{External types}
808 %************************************************************************
810 The compiler's foreign function interface supports the passing of a
811 restricted set of types as arguments and results (the restricting factor
815 isFFITy :: Type -> Bool
816 -- True for any TyCon that can possibly be an arg or result of an FFI call
817 isFFITy ty = checkRepTyCon legalFFITyCon ty
819 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
820 -- Checks for valid argument type for a 'foreign import'
821 isFFIArgumentTy dflags safety ty
822 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
824 isFFIExternalTy :: Type -> Bool
825 -- Types that are allowed as arguments of a 'foreign export'
826 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
828 isFFIImportResultTy :: DynFlags -> Type -> Bool
829 isFFIImportResultTy dflags ty
830 = checkRepTyCon (legalFIResultTyCon dflags) ty
832 isFFIExportResultTy :: Type -> Bool
833 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
835 isFFIDynArgumentTy :: Type -> Bool
836 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
837 -- or a newtype of either.
838 isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
840 isFFIDynResultTy :: Type -> Bool
841 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
842 -- or a newtype of either.
843 isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
845 isFFILabelTy :: Type -> Bool
846 -- The type of a foreign label must be Ptr, FunPtr, Addr,
847 -- or a newtype of either.
848 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
850 isFFIDotnetTy :: DynFlags -> Type -> Bool
851 isFFIDotnetTy dflags ty
852 = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
853 (legalFIResultTyCon dflags tc ||
854 isFFIDotnetObjTy ty || isStringTy ty)) ty
856 -- Support String as an argument or result from a .NET FFI call.
858 case tcSplitTyConApp_maybe (repType ty) of
861 case tcSplitTyConApp_maybe (repType arg_ty) of
862 Just (cc,[]) -> cc == charTyCon
866 -- Support String as an argument or result from a .NET FFI call.
867 isFFIDotnetObjTy ty =
869 (_, t_ty) = tcSplitForAllTys ty
871 case tcSplitTyConApp_maybe (repType t_ty) of
872 Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
875 toDNType :: Type -> DNType
877 | isStringTy ty = DNString
878 | isFFIDotnetObjTy ty = DNObject
879 | Just (tc,argTys) <- tcSplitTyConApp_maybe ty =
880 case lookup (getUnique tc) dn_assoc of
883 | tc `hasKey` ioTyConKey -> toDNType (head argTys)
884 | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
886 dn_assoc :: [ (Unique, DNType) ]
887 dn_assoc = [ (unitTyConKey, DNUnit)
888 , (intTyConKey, DNInt)
889 , (int8TyConKey, DNInt8)
890 , (int16TyConKey, DNInt16)
891 , (int32TyConKey, DNInt32)
892 , (int64TyConKey, DNInt64)
893 , (wordTyConKey, DNInt)
894 , (word8TyConKey, DNWord8)
895 , (word16TyConKey, DNWord16)
896 , (word32TyConKey, DNWord32)
897 , (word64TyConKey, DNWord64)
898 , (floatTyConKey, DNFloat)
899 , (doubleTyConKey, DNDouble)
900 , (addrTyConKey, DNPtr)
901 , (ptrTyConKey, DNPtr)
902 , (funPtrTyConKey, DNPtr)
903 , (charTyConKey, DNChar)
904 , (boolTyConKey, DNBool)
907 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
908 -- Look through newtypes
909 -- Non-recursive ones are transparent to splitTyConApp,
910 -- but recursive ones aren't. Manuel had:
911 -- newtype T = MkT (Ptr T)
912 -- and wanted it to work...
913 checkRepTyCon check_tc ty
914 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
917 checkRepTyConKey :: [Unique] -> Type -> Bool
918 -- Like checkRepTyCon, but just looks at the TyCon key
919 checkRepTyConKey keys
920 = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
923 ----------------------------------------------
924 These chaps do the work; they are not exported
925 ----------------------------------------------
928 legalFEArgTyCon :: TyCon -> Bool
929 -- It's illegal to return foreign objects and (mutable)
930 -- bytearrays from a _ccall_ / foreign declaration
931 -- (or be passed them as arguments in foreign exported functions).
933 | isByteArrayLikeTyCon tc
935 -- It's also illegal to make foreign exports that take unboxed
936 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
938 = boxedMarshalableTyCon tc
940 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
941 legalFIResultTyCon dflags tc
942 | isByteArrayLikeTyCon tc = False
943 | tc == unitTyCon = True
944 | otherwise = marshalableTyCon dflags tc
946 legalFEResultTyCon :: TyCon -> Bool
947 legalFEResultTyCon tc
948 | isByteArrayLikeTyCon tc = False
949 | tc == unitTyCon = True
950 | otherwise = boxedMarshalableTyCon tc
952 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
953 -- Checks validity of types going from Haskell -> external world
954 legalOutgoingTyCon dflags safety tc
955 | playSafe safety && isByteArrayLikeTyCon tc
958 = marshalableTyCon dflags tc
960 legalFFITyCon :: TyCon -> Bool
961 -- True for any TyCon that can possibly be an arg or result of an FFI call
963 = isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon
965 marshalableTyCon dflags tc
966 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
967 || boxedMarshalableTyCon tc
969 boxedMarshalableTyCon tc
970 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
971 , int32TyConKey, int64TyConKey
972 , wordTyConKey, word8TyConKey, word16TyConKey
973 , word32TyConKey, word64TyConKey
974 , floatTyConKey, doubleTyConKey
975 , addrTyConKey, ptrTyConKey, funPtrTyConKey
978 , byteArrayTyConKey, mutableByteArrayTyConKey
982 isByteArrayLikeTyCon :: TyCon -> Bool
983 isByteArrayLikeTyCon tc =
984 getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]