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 TyVarDetails(..), isUserTyVar, isSkolemTyVar, isHoleTyVar,
28 --------------------------------
32 --------------------------------
34 -- These are important because they do not look through newtypes
35 tcSplitForAllTys, tcSplitPhiTy,
36 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
37 tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
38 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitSigmaTy,
39 tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
41 ---------------------------------
43 -- Again, newtypes are opaque
44 tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
45 isSigmaTy, isOverloadedTy,
46 isDoubleTy, isFloatTy, isIntTy,
47 isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy,
48 isTauTy, tcIsTyVarTy, tcIsForAllTy,
51 ---------------------------------
52 -- Misc type manipulators
53 hoistForAllTys, deNoteType,
54 namesOfType, namesOfDFunHead,
57 ---------------------------------
59 PredType, getClassPredTys_maybe, getClassPredTys,
60 isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
61 mkDictTy, tcSplitPredTy_maybe, predTyUnique,
62 isDictTy, tcSplitDFunTy, predTyUnique,
63 mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
65 ---------------------------------
66 -- Foreign import and export
67 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
68 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
69 isFFIExportResultTy, -- :: Type -> Bool
70 isFFIExternalTy, -- :: Type -> Bool
71 isFFIDynArgumentTy, -- :: Type -> Bool
72 isFFIDynResultTy, -- :: Type -> Bool
73 isFFILabelTy, -- :: Type -> Bool
75 ---------------------------------
76 -- Unifier and matcher
77 unifyTysX, unifyTyListsX, unifyExtendTysX,
78 matchTy, matchTys, match,
80 --------------------------------
81 -- Rexported from Type
82 Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
83 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
84 superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
85 isTypeKind, isAnyTypeKind,
87 Type, SourceType(..), PredType, ThetaType,
88 mkForAllTy, mkForAllTys,
89 mkFunTy, mkFunTys, zipFunTys,
90 mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
91 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
93 isUnLiftedType, -- Source types are always lifted
94 isUnboxedTupleType, -- Ditto
95 isPrimitiveType, isTyVarTy,
97 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
98 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
99 typeKind, eqKind, eqUsage,
101 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
104 #include "HsVersions.h"
107 import {-# SOURCE #-} PprType( pprType )
110 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
112 import Type ( -- Re-exports
113 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
114 Kind, Type, SourceType(..), PredType, ThetaType,
115 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
116 mkForAllTy, mkForAllTys, defaultKind, isTypeKind, isAnyTypeKind,
117 mkFunTy, mkFunTys, zipFunTys, isTyVarTy,
118 mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
119 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
120 isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
121 splitNewType_maybe, splitTyConApp_maybe,
122 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
123 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
124 hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
126 import TyCon ( TyCon, isUnLiftedTyCon )
127 import Class ( classHasFDs, Class )
128 import Var ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
129 import ForeignCall ( Safety, playSafe )
134 import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
135 import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
136 import OccName ( OccName, mkDictOcc )
138 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
139 import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
140 import BasicTypes ( IPName(..), ipNameName )
141 import Unique ( Unique, Uniquable(..) )
142 import SrcLoc ( SrcLoc )
143 import Util ( cmpList, thenCmp, equalLength )
144 import Maybes ( maybeToBool, expectJust )
149 %************************************************************************
153 %************************************************************************
155 The type checker divides the generic Type world into the
156 following more structured beasts:
158 sigma ::= forall tyvars. phi
159 -- A sigma type is a qualified type
161 -- Note that even if 'tyvars' is empty, theta
162 -- may not be: e.g. (?x::Int) => Int
164 -- Note that 'sigma' is in prenex form:
165 -- all the foralls are at the front.
166 -- A 'phi' type has no foralls to the right of
174 -- A 'tau' type has no quantification anywhere
175 -- Note that the args of a type constructor must be taus
177 | tycon tau_1 .. tau_n
181 -- In all cases, a (saturated) type synonym application is legal,
182 -- provided it expands to the required form.
186 type SigmaType = Type
192 type TcTyVar = TyVar -- Might be a mutable tyvar
193 type TcTyVarSet = TyVarSet
195 type TcType = Type -- A TcType can have mutable type variables
196 -- Invariant on ForAllTy in TcTypes:
198 -- a cannot occur inside a MutTyVar in T; that is,
199 -- T is "flattened" before quantifying over a
201 type TcPredType = PredType
202 type TcThetaType = ThetaType
203 type TcSigmaType = TcType
204 type TcRhoType = TcType
205 type TcTauType = TcType
210 %************************************************************************
212 \subsection{TyVarDetails}
214 %************************************************************************
216 TyVarDetails gives extra info about type variables, used during type
217 checking. It's attached to mutable type variables only.
218 It's knot-tied back to Var.lhs. There is no reason in principle
219 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
223 = HoleTv -- Used *only* by the type checker when passing in a type
224 -- variable that should be side-effected to the result type.
225 -- Always has kind openTypeKind.
226 -- Never appears in types
228 | SigTv -- Introduced when instantiating a type signature,
229 -- prior to checking that the defn of a fn does
230 -- have the expected type. Should not be instantiated.
232 -- f :: forall a. a -> a
234 -- When checking e, with expected type (a->a), we
235 -- should not instantiate a
237 | ClsTv -- Scoped type variable introduced by a class decl
238 -- class C a where ...
240 | InstTv -- Ditto, but instance decl
242 | PatSigTv -- Scoped type variable, introduced by a pattern
246 | VanillaTv -- Everything else
248 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
249 isUserTyVar tv = case mutTyVarDetails tv of
253 isSkolemTyVar :: TcTyVar -> Bool
254 isSkolemTyVar tv = case mutTyVarDetails tv of
260 isHoleTyVar :: TcTyVar -> Bool
261 -- NB: the hole might be filled in by now, and this
262 -- function does not check for that
263 isHoleTyVar tv = ASSERT( isMutTyVar tv )
264 case mutTyVarDetails tv of
268 tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
271 = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
272 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
276 details SigTv = ptext SLIT("type signature")
277 details ClsTv = ptext SLIT("class declaration")
278 details InstTv = ptext SLIT("instance declaration")
279 details PatSigTv = ptext SLIT("pattern type signature")
280 details HoleTv = ptext SLIT("//hole//") -- Should not happen
281 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
285 %************************************************************************
287 \subsection{Tau, sigma and rho}
289 %************************************************************************
292 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
294 mkPhiTy :: [SourceType] -> Type -> Type
295 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
299 @isTauTy@ tests for nested for-alls.
302 isTauTy :: Type -> Bool
303 isTauTy (TyVarTy v) = True
304 isTauTy (TyConApp _ tys) = all isTauTy tys
305 isTauTy (AppTy a b) = isTauTy a && isTauTy b
306 isTauTy (FunTy a b) = isTauTy a && isTauTy b
307 isTauTy (SourceTy p) = True -- Don't look through source types
308 isTauTy (NoteTy _ ty) = isTauTy ty
309 isTauTy other = False
313 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
314 -- construct a dictionary function name
315 getDFunTyKey (TyVarTy tv) = getOccName tv
316 getDFunTyKey (TyConApp tc _) = getOccName tc
317 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
318 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
319 getDFunTyKey (FunTy arg _) = getOccName funTyCon
320 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
321 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
322 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
323 -- SourceTy shouldn't happen
327 %************************************************************************
329 \subsection{Expanding and splitting}
331 %************************************************************************
333 These tcSplit functions are like their non-Tc analogues, but
334 a) they do not look through newtypes
335 b) they do not look through PredTys
336 c) [future] they ignore usage-type annotations
338 However, they are non-monadic and do not follow through mutable type
339 variables. It's up to you to make sure this doesn't matter.
342 tcSplitForAllTys :: Type -> ([TyVar], Type)
343 tcSplitForAllTys ty = split ty ty []
345 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
346 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
347 split orig_ty t tvs = (reverse tvs, orig_ty)
349 tcIsForAllTy (ForAllTy tv ty) = True
350 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
351 tcIsForAllTy t = False
353 tcSplitPhiTy :: Type -> ([PredType], Type)
354 tcSplitPhiTy ty = split ty ty []
356 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
357 Just p -> split res res (p:ts)
358 Nothing -> (reverse ts, orig_ty)
359 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
360 split orig_ty ty ts = (reverse ts, orig_ty)
362 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
363 (tvs, rho) -> case tcSplitPhiTy rho of
364 (theta, tau) -> (tvs, theta, tau)
366 tcTyConAppTyCon :: Type -> TyCon
367 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
369 tcTyConAppArgs :: Type -> [Type]
370 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
372 tcSplitTyConApp :: Type -> (TyCon, [Type])
373 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
375 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
377 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
378 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
379 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
380 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
381 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
382 -- Newtypes are opaque, so they may be split
383 -- However, predicates are not treated
384 -- as tycon applications by the type checker
385 tcSplitTyConApp_maybe other = Nothing
387 tcSplitFunTys :: Type -> ([Type], Type)
388 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
390 Just (arg,res) -> (arg:args, res')
392 (args,res') = tcSplitFunTys res
394 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
395 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
396 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
397 tcSplitFunTy_maybe other = Nothing
399 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
400 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
403 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
404 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
405 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
406 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
407 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
408 --- Don't forget that newtype!
409 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
410 tcSplitAppTy_maybe other = Nothing
412 tc_split_app tc [] = Nothing
413 tc_split_app tc tys = split tys []
415 split [ty2] acc = Just (TyConApp tc (reverse acc), ty2)
416 split (ty:tys) acc = split tys (ty:acc)
418 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
420 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
422 tcGetTyVar_maybe :: Type -> Maybe TyVar
423 tcGetTyVar_maybe (TyVarTy tv) = Just tv
424 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
425 tcGetTyVar_maybe other = Nothing
427 tcGetTyVar :: String -> Type -> TyVar
428 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
430 tcIsTyVarTy :: Type -> Bool
431 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
434 The type of a method for class C is always of the form:
435 Forall a1..an. C a1..an => sig_ty
436 where sig_ty is the type given by the method's signature, and thus in general
437 is a ForallTy. At the point that splitMethodTy is called, it is expected
438 that the outer Forall has already been stripped off. splitMethodTy then
439 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
443 tcSplitMethodTy :: Type -> (PredType, Type)
444 tcSplitMethodTy ty = split ty
446 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
448 Nothing -> panic "splitMethodTy"
449 split (NoteTy n ty) = split ty
450 split _ = panic "splitMethodTy"
452 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
453 -- Split the type of a dictionary function
455 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
456 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
457 (tvs, theta, clas, tys) }}
460 (allDistinctTyVars tys tvs) = True
462 all the types tys are type variables,
463 distinct from each other and from tvs.
465 This is useful when checking that unification hasn't unified signature
466 type variables. For example, if the type sig is
467 f :: forall a b. a -> b -> b
468 we want to check that 'a' and 'b' havn't
469 (a) been unified with a non-tyvar type
470 (b) been unified with each other (all distinct)
471 (c) been unified with a variable free in the environment
474 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
476 allDistinctTyVars [] acc
478 allDistinctTyVars (ty:tys) acc
479 = case tcGetTyVar_maybe ty of
480 Nothing -> False -- (a)
481 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
482 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
486 %************************************************************************
488 \subsection{Predicate types}
490 %************************************************************************
492 "Predicates" are particular source types, namelyClassP or IParams
495 isPred :: SourceType -> Bool
496 isPred (ClassP _ _) = True
497 isPred (IParam _ _) = True
498 isPred (NType _ _) = False
500 isPredTy :: Type -> Bool
501 isPredTy (NoteTy _ ty) = isPredTy ty
502 isPredTy (SourceTy sty) = isPred sty
505 tcSplitPredTy_maybe :: Type -> Maybe PredType
506 -- Returns Just for predicates only
507 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
508 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
509 tcSplitPredTy_maybe other = Nothing
511 predTyUnique :: PredType -> Unique
512 predTyUnique (IParam n _) = getUnique (ipNameName n)
513 predTyUnique (ClassP clas tys) = getUnique clas
515 predHasFDs :: PredType -> Bool
516 -- True if the predicate has functional depenencies;
517 -- I.e. should participate in improvement
518 predHasFDs (IParam _ _) = True
519 predHasFDs (ClassP cls _) = classHasFDs cls
521 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
522 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
523 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
527 --------------------- Dictionary types ---------------------------------
530 mkClassPred clas tys = ClassP clas tys
532 isClassPred :: SourceType -> Bool
533 isClassPred (ClassP clas tys) = True
534 isClassPred other = False
536 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
537 isTyVarClassPred other = False
539 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
540 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
541 getClassPredTys_maybe _ = Nothing
543 getClassPredTys :: PredType -> (Class, [Type])
544 getClassPredTys (ClassP clas tys) = (clas, tys)
546 mkDictTy :: Class -> [Type] -> Type
547 mkDictTy clas tys = mkPredTy (ClassP clas tys)
549 isDictTy :: Type -> Bool
550 isDictTy (SourceTy p) = isClassPred p
551 isDictTy (NoteTy _ ty) = isDictTy ty
552 isDictTy other = False
555 --------------------- Implicit parameters ---------------------------------
558 isIPPred :: SourceType -> Bool
559 isIPPred (IParam _ _) = True
560 isIPPred other = False
562 isInheritablePred :: PredType -> Bool
563 -- Can be inherited by a context. For example, consider
564 -- f x = let g y = (?v, y+x)
565 -- in (g 3 with ?v = 8,
567 -- The point is that g's type must be quantifed over ?v:
568 -- g :: (?v :: a) => a -> a
569 -- but it doesn't need to be quantified over the Num a dictionary
570 -- which can be free in g's rhs, and shared by both calls to g
571 isInheritablePred (ClassP _ _) = True
572 isInheritablePred other = False
574 isLinearPred :: TcPredType -> Bool
575 isLinearPred (IParam (Linear n) _) = True
576 isLinearPred other = False
580 %************************************************************************
582 \subsection{Comparison}
584 %************************************************************************
586 Comparison, taking note of newtypes, predicates, etc,
587 But ignoring usage types
590 tcEqType :: Type -> Type -> Bool
591 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
593 tcEqTypes :: [Type] -> [Type] -> Bool
594 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
596 tcEqPred :: PredType -> PredType -> Bool
597 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
600 tcCmpType :: Type -> Type -> Ordering
601 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
603 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
605 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
607 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
610 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
611 -- The "env" maps type variables in ty1 to type variables in ty2
612 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
613 -- we in effect substitute tv2 for tv1 in t1 before continuing
615 -- Look through NoteTy
616 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
617 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
619 -- Deal with equal constructors
620 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
621 Just tv1a -> tv1a `compare` tv2
622 Nothing -> tv1 `compare` tv2
624 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
625 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
626 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
627 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
628 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
630 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
631 cmpTy env (AppTy _ _) (TyVarTy _) = GT
633 cmpTy env (FunTy _ _) (TyVarTy _) = GT
634 cmpTy env (FunTy _ _) (AppTy _ _) = GT
636 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
637 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
638 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
640 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
641 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
642 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
643 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
645 cmpTy env (SourceTy _) t2 = GT
651 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
652 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
653 -- Compare types as well as names for implicit parameters
654 -- This comparison is used exclusively (I think) for the
655 -- finite map built in TcSimplify
656 cmpSourceTy env (IParam _ _) sty = LT
658 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
659 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
660 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
662 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
663 cmpSourceTy env (NType _ _) sty = GT
666 PredTypes are used as a FM key in TcSimplify,
667 so we take the easy path and make them an instance of Ord
670 instance Eq SourceType where { (==) = tcEqPred }
671 instance Ord SourceType where { compare = tcCmpPred }
675 %************************************************************************
677 \subsection{Predicates}
679 %************************************************************************
681 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
683 f :: (?x::Int) => Int -> Int
686 isSigmaTy :: Type -> Bool
687 isSigmaTy (ForAllTy tyvar ty) = True
688 isSigmaTy (FunTy a b) = isPredTy a
689 isSigmaTy (NoteTy n ty) = isSigmaTy ty
692 isOverloadedTy :: Type -> Bool
693 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
694 isOverloadedTy (FunTy a b) = isPredTy a
695 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
696 isOverloadedTy _ = False
700 isFloatTy = is_tc floatTyConKey
701 isDoubleTy = is_tc doubleTyConKey
702 isForeignPtrTy = is_tc foreignPtrTyConKey
703 isIntegerTy = is_tc integerTyConKey
704 isIntTy = is_tc intTyConKey
705 isAddrTy = is_tc addrTyConKey
706 isBoolTy = is_tc boolTyConKey
707 isUnitTy = is_tc unitTyConKey
709 is_tc :: Unique -> Type -> Bool
710 -- Newtypes are opaque to this
711 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
712 Just (tc, _) -> uniq == getUnique tc
717 %************************************************************************
721 %************************************************************************
724 hoistForAllTys :: Type -> Type
725 -- Used for user-written type signatures only
726 -- Move all the foralls and constraints to the top
727 -- e.g. T -> forall a. a ==> forall a. T -> a
728 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
730 -- We want to 'look through' type synonyms when doing this
731 -- so it's better done on the Type than the HsType
734 = case hoist ty ty of
735 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys theta body)
737 hoist orig_ty (ForAllTy tv ty) = case hoist ty ty of
738 (tvs,theta,tau) -> (tv:tvs,theta,tau)
739 hoist orig_ty (FunTy arg res)
740 | isPredTy arg' = case hoist res res of
741 (tvs,theta,tau) -> (tvs,arg':theta,tau)
742 | otherwise = case hoist res res of
743 (tvs,theta,tau) -> (tvs,theta,mkFunTy arg' tau)
745 arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
746 -- to the argument type
748 hoist orig_ty (NoteTy _ ty) = hoist orig_ty ty
749 hoist orig_ty ty = ([], [], orig_ty)
754 deNoteType :: Type -> Type
755 -- Remove synonyms, but not source types
756 deNoteType ty@(TyVarTy tyvar) = ty
757 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
758 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
759 deNoteType (NoteTy _ ty) = deNoteType ty
760 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
761 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
762 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
764 deNoteSourceType :: SourceType -> SourceType
765 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
766 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
767 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
770 Find the free names of a type, including the type constructors and classes it mentions
771 This is used in the front end of the compiler
774 namesOfType :: Type -> NameSet
775 namesOfType (TyVarTy tv) = unitNameSet (getName tv)
776 namesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
777 namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
778 namesOfType (NoteTy other_note ty2) = namesOfType ty2
779 namesOfType (SourceTy (IParam n ty)) = namesOfType ty
780 namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
781 namesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
782 namesOfType (FunTy arg res) = namesOfType arg `unionNameSets` namesOfType res
783 namesOfType (AppTy fun arg) = namesOfType fun `unionNameSets` namesOfType arg
784 namesOfType (ForAllTy tyvar ty) = namesOfType ty `delFromNameSet` getName tyvar
786 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
788 namesOfDFunHead :: Type -> NameSet
789 -- Find the free type constructors and classes
790 -- of the head of the dfun instance type
791 -- The 'dfun_head_type' is because of
792 -- instance Foo a => Baz T where ...
793 -- The decl is an orphan if Baz and T are both not locally defined,
794 -- even if Foo *is* locally defined
795 namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
796 (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
801 %************************************************************************
803 \subsection[TysWiredIn-ext-type]{External types}
805 %************************************************************************
807 The compiler's foreign function interface supports the passing of a
808 restricted set of types as arguments and results (the restricting factor
812 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
813 -- Checks for valid argument type for a 'foreign import'
814 isFFIArgumentTy dflags safety ty
815 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
817 isFFIExternalTy :: Type -> Bool
818 -- Types that are allowed as arguments of a 'foreign export'
819 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
821 isFFIImportResultTy :: DynFlags -> Type -> Bool
822 isFFIImportResultTy dflags ty
823 = checkRepTyCon (legalFIResultTyCon dflags) ty
825 isFFIExportResultTy :: Type -> Bool
826 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
828 isFFIDynArgumentTy :: Type -> Bool
829 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
830 -- or a newtype of either.
831 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
833 isFFIDynResultTy :: Type -> Bool
834 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
835 -- or a newtype of either.
836 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
838 isFFILabelTy :: Type -> Bool
839 -- The type of a foreign label must be Ptr, FunPtr, Addr,
840 -- or a newtype of either.
841 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
843 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
844 -- Look through newtypes
845 -- Non-recursive ones are transparent to splitTyConApp,
846 -- but recursive ones aren't; hence the splitNewType_maybe
847 checkRepTyCon check_tc ty
848 | Just ty' <- splitNewType_maybe ty = checkRepTyCon check_tc ty'
849 | Just (tc,_) <- splitTyConApp_maybe ty = check_tc tc
853 ----------------------------------------------
854 These chaps do the work; they are not exported
855 ----------------------------------------------
858 legalFEArgTyCon :: TyCon -> Bool
859 -- It's illegal to return foreign objects and (mutable)
860 -- bytearrays from a _ccall_ / foreign declaration
861 -- (or be passed them as arguments in foreign exported functions).
863 | getUnique tc `elem` [ foreignObjTyConKey, foreignPtrTyConKey,
864 byteArrayTyConKey, mutableByteArrayTyConKey ]
866 -- It's also illegal to make foreign exports that take unboxed
867 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
869 = boxedMarshalableTyCon tc
871 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
872 legalFIResultTyCon dflags tc
873 | getUnique tc `elem`
874 [ foreignObjTyConKey, foreignPtrTyConKey,
875 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
876 | tc == unitTyCon = True
877 | otherwise = marshalableTyCon dflags tc
879 legalFEResultTyCon :: TyCon -> Bool
880 legalFEResultTyCon tc
881 | getUnique tc `elem`
882 [ foreignObjTyConKey, foreignPtrTyConKey,
883 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
884 | tc == unitTyCon = True
885 | otherwise = boxedMarshalableTyCon tc
887 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
888 -- Checks validity of types going from Haskell -> external world
889 legalOutgoingTyCon dflags safety tc
890 | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
893 = marshalableTyCon dflags tc
895 marshalableTyCon dflags tc
896 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
897 || boxedMarshalableTyCon tc
899 boxedMarshalableTyCon tc
900 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
901 , int32TyConKey, int64TyConKey
902 , wordTyConKey, word8TyConKey, word16TyConKey
903 , word32TyConKey, word64TyConKey
904 , floatTyConKey, doubleTyConKey
905 , addrTyConKey, ptrTyConKey, funPtrTyConKey
906 , charTyConKey, foreignObjTyConKey
909 , byteArrayTyConKey, mutableByteArrayTyConKey
915 %************************************************************************
917 \subsection{Unification with an explicit substitution}
919 %************************************************************************
921 Unify types with an explicit substitution and no monad.
922 Ignore usage annotations.
926 = (TyVarSet, -- Set of template tyvars
927 TyVarSubstEnv) -- Not necessarily idempotent
929 unifyTysX :: TyVarSet -- Template tyvars
932 -> Maybe TyVarSubstEnv
933 unifyTysX tmpl_tyvars ty1 ty2
934 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
936 unifyExtendTysX :: TyVarSet -- Template tyvars
937 -> TyVarSubstEnv -- Substitution to start with
940 -> Maybe TyVarSubstEnv -- Extended substitution
941 unifyExtendTysX tmpl_tyvars subst ty1 ty2
942 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
944 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
945 -> Maybe TyVarSubstEnv
946 unifyTyListsX tmpl_tyvars tys1 tys2
947 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
952 -> (MySubst -> Maybe result)
956 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
957 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
959 -- Variables; go for uVar
960 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
963 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
964 | tyvar1 `elemVarSet` tmpls
965 = uVarX tyvar1 ty2 k subst
966 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
967 | tyvar2 `elemVarSet` tmpls
968 = uVarX tyvar2 ty1 k subst
971 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
972 | n1 == n2 = uTysX t1 t2 k subst
973 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
974 | c1 == c2 = uTyListsX tys1 tys2 k subst
975 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
976 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
978 -- Functions; just check the two parts
979 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
980 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
982 -- Type constructors must match
983 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
984 | (con1 == con2 && equalLength tys1 tys2)
985 = uTyListsX tys1 tys2 k subst
987 -- Applications need a bit of care!
988 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
989 -- NB: we've already dealt with type variables and Notes,
990 -- so if one type is an App the other one jolly well better be too
991 uTysX (AppTy s1 t1) ty2 k subst
992 = case tcSplitAppTy_maybe ty2 of
993 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
994 Nothing -> Nothing -- Fail
996 uTysX ty1 (AppTy s2 t2) k subst
997 = case tcSplitAppTy_maybe ty1 of
998 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
999 Nothing -> Nothing -- Fail
1001 -- Not expecting for-alls in unification
1003 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
1004 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1007 -- Anything else fails
1008 uTysX ty1 ty2 k subst = Nothing
1011 uTyListsX [] [] k subst = k subst
1012 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1013 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1017 -- Invariant: tv1 is a unifiable variable
1018 uVarX tv1 ty2 k subst@(tmpls, env)
1019 = case lookupSubstEnv env tv1 of
1020 Just (DoneTy ty1) -> -- Already bound
1021 uTysX ty1 ty2 k subst
1023 Nothing -- Not already bound
1024 | typeKind ty2 `eqKind` tyVarKind tv1
1025 && occur_check_ok ty2
1026 -> -- No kind mismatch nor occur check
1027 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1029 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1031 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1032 occur_check_ok_tv tv | tv1 == tv = False
1033 | otherwise = case lookupSubstEnv env tv of
1035 Just (DoneTy ty) -> occur_check_ok ty
1040 %************************************************************************
1042 \subsection{Matching on types}
1044 %************************************************************************
1046 Matching is a {\em unidirectional} process, matching a type against a
1047 template (which is just a type with type variables in it). The
1048 matcher assumes that there are no repeated type variables in the
1049 template, so that it simply returns a mapping of type variables to
1050 types. It also fails on nested foralls.
1052 @matchTys@ matches corresponding elements of a list of templates and
1053 types. It and @matchTy@ both ignore usage annotations, unlike the
1054 main function @match@.
1057 matchTy :: TyVarSet -- Template tyvars
1059 -> Type -- Proposed instance of template
1060 -> Maybe TyVarSubstEnv -- Matching substitution
1063 matchTys :: TyVarSet -- Template tyvars
1064 -> [Type] -- Templates
1065 -> [Type] -- Proposed instance of template
1066 -> Maybe (TyVarSubstEnv, -- Matching substitution
1067 [Type]) -- Left over instance types
1069 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1071 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1072 (\ (senv,tys) -> Just (senv,tys))
1076 @match@ is the main function. It takes a flag indicating whether
1077 usage annotations are to be respected.
1080 match :: Type -> Type -- Current match pair
1081 -> TyVarSet -- Template vars
1082 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1083 -> TyVarSubstEnv -- Current subst
1086 -- When matching against a type variable, see if the variable
1087 -- has already been bound. If so, check that what it's bound to
1088 -- is the same as ty; if not, bind it and carry on.
1090 match (TyVarTy v) ty tmpls k senv
1091 | v `elemVarSet` tmpls
1092 = -- v is a template variable
1093 case lookupSubstEnv senv v of
1094 Nothing | typeKind ty `eqKind` tyVarKind v
1095 -- We do a kind check, just as in the uVarX above
1096 -- The kind check is needed to avoid bogus matches
1097 -- of (a b) with (c d), where the kinds don't match
1098 -- An occur check isn't needed when matching.
1099 -> k (extendSubstEnv senv v (DoneTy ty))
1101 | otherwise -> Nothing -- Fails
1103 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1104 | otherwise -> Nothing -- Fails
1107 = -- v is not a template variable; ty had better match
1108 -- Can't use (==) because types differ
1109 case tcGetTyVar_maybe ty of
1110 Just v' | v == v' -> k senv -- Success
1111 other -> Nothing -- Failure
1112 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1113 -- I guess the reason the Note-stripping case is *last* rather than first
1114 -- is to preserve type synonyms etc., so I'm not moving it to the
1115 -- top; but this means that (without the deNotetype) a type
1116 -- variable may not match the pattern (TyVarTy v') as one would
1117 -- expect, due to an intervening Note. KSW 2000-06.
1120 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1121 | n1 == n2 = match t1 t2 tmpls k senv
1122 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1123 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1124 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1125 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1127 -- Functions; just check the two parts
1128 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1129 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1131 match (AppTy fun1 arg1) ty2 tmpls k senv
1132 = case tcSplitAppTy_maybe ty2 of
1133 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1134 Nothing -> Nothing -- Fail
1136 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1137 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1139 -- Newtypes are opaque; other source types should not happen
1140 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1141 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1143 -- With type synonyms, we have to be careful for the exact
1144 -- same reasons as in the unifier. Please see the
1145 -- considerable commentary there before changing anything
1146 -- here! (WDP 95/05)
1147 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1148 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1151 match _ _ _ _ _ = Nothing
1153 match_list_exactly tys1 tys2 tmpls k senv
1154 = match_list tys1 tys2 tmpls k' senv
1156 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1157 | otherwise = Nothing -- Fail
1159 match_list [] tys2 tmpls k senv = k (senv, tys2)
1160 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1161 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1162 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv