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, TcPhiType, 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, tcSplitRhoTy,
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, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
91 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
93 isUnLiftedType, -- Source types are always lifted
94 isUnboxedTupleType, -- Ditto
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,
118 mkTyConApp, 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(..), mkLocalName, 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. theta => 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
172 -- A 'tau' type has no quantification anywhere
173 -- Note that the args of a type constructor must be taus
175 | tycon tau_1 .. tau_n
179 -- In all cases, a (saturated) type synonym application is legal,
180 -- provided it expands to the required form.
184 type SigmaType = Type
190 type TcTyVar = TyVar -- Might be a mutable tyvar
191 type TcTyVarSet = TyVarSet
193 type TcType = Type -- A TcType can have mutable type variables
194 -- Invariant on ForAllTy in TcTypes:
196 -- a cannot occur inside a MutTyVar in T; that is,
197 -- T is "flattened" before quantifying over a
199 type TcPredType = PredType
200 type TcThetaType = ThetaType
201 type TcSigmaType = TcType
202 type TcPhiType = TcType
203 type TcTauType = TcType
208 %************************************************************************
210 \subsection{TyVarDetails}
212 %************************************************************************
214 TyVarDetails gives extra info about type variables, used during type
215 checking. It's attached to mutable type variables only.
216 It's knot-tied back to Var.lhs. There is no reason in principle
217 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
221 = HoleTv -- Used *only* by the type checker when passing in a type
222 -- variable that should be side-effected to the result type.
223 -- Always has kind openTypeKind.
224 -- Never appears in types
226 | SigTv -- Introduced when instantiating a type signature,
227 -- prior to checking that the defn of a fn does
228 -- have the expected type. Should not be instantiated.
230 -- f :: forall a. a -> a
232 -- When checking e, with expected type (a->a), we
233 -- should not instantiate a
235 | ClsTv -- Scoped type variable introduced by a class decl
236 -- class C a where ...
238 | InstTv -- Ditto, but instance decl
240 | PatSigTv -- Scoped type variable, introduced by a pattern
244 | VanillaTv -- Everything else
246 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
247 isUserTyVar tv = case mutTyVarDetails tv of
251 isSkolemTyVar :: TcTyVar -> Bool
252 isSkolemTyVar tv = case mutTyVarDetails tv of
258 isHoleTyVar :: TcTyVar -> Bool
259 -- NB: the hole might be filled in by now, and this
260 -- function does not check for that
261 isHoleTyVar tv = ASSERT( isMutTyVar tv )
262 case mutTyVarDetails tv of
266 tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
269 = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
270 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
274 details SigTv = ptext SLIT("type signature")
275 details ClsTv = ptext SLIT("class declaration")
276 details InstTv = ptext SLIT("instance declaration")
277 details PatSigTv = ptext SLIT("pattern type signature")
278 details HoleTv = ptext SLIT("//hole//") -- Should not happen
279 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
283 %************************************************************************
285 \subsection{Tau, sigma and rho}
287 %************************************************************************
290 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
292 mkRhoTy :: [SourceType] -> Type -> Type
293 mkRhoTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
297 @isTauTy@ tests for nested for-alls.
300 isTauTy :: Type -> Bool
301 isTauTy (TyVarTy v) = True
302 isTauTy (TyConApp _ tys) = all isTauTy tys
303 isTauTy (AppTy a b) = isTauTy a && isTauTy b
304 isTauTy (FunTy a b) = isTauTy a && isTauTy b
305 isTauTy (SourceTy p) = True -- Don't look through source types
306 isTauTy (NoteTy _ ty) = isTauTy ty
307 isTauTy other = False
311 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
312 -- construct a dictionary function name
313 getDFunTyKey (TyVarTy tv) = getOccName tv
314 getDFunTyKey (TyConApp tc _) = getOccName tc
315 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
316 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
317 getDFunTyKey (FunTy arg _) = getOccName funTyCon
318 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
319 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
320 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
321 -- SourceTy shouldn't happen
325 %************************************************************************
327 \subsection{Expanding and splitting}
329 %************************************************************************
331 These tcSplit functions are like their non-Tc analogues, but
332 a) they do not look through newtypes
333 b) they do not look through PredTys
334 c) [future] they ignore usage-type annotations
336 However, they are non-monadic and do not follow through mutable type
337 variables. It's up to you to make sure this doesn't matter.
340 tcSplitForAllTys :: Type -> ([TyVar], Type)
341 tcSplitForAllTys ty = split ty ty []
343 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
344 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
345 split orig_ty t tvs = (reverse tvs, orig_ty)
347 tcIsForAllTy (ForAllTy tv ty) = True
348 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
349 tcIsForAllTy t = False
351 tcSplitRhoTy :: Type -> ([PredType], Type)
352 tcSplitRhoTy ty = split ty ty []
354 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
355 Just p -> split res res (p:ts)
356 Nothing -> (reverse ts, orig_ty)
357 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
358 split orig_ty ty ts = (reverse ts, orig_ty)
360 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
361 (tvs, rho) -> case tcSplitRhoTy rho of
362 (theta, tau) -> (tvs, theta, tau)
364 tcTyConAppTyCon :: Type -> TyCon
365 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
367 tcTyConAppArgs :: Type -> [Type]
368 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
370 tcSplitTyConApp :: Type -> (TyCon, [Type])
371 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
373 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
375 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
376 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
377 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
378 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
379 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
380 -- Newtypes are opaque, so they may be split
381 -- However, predicates are not treated
382 -- as tycon applications by the type checker
383 tcSplitTyConApp_maybe other = Nothing
385 tcSplitFunTys :: Type -> ([Type], Type)
386 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
388 Just (arg,res) -> (arg:args, res')
390 (args,res') = tcSplitFunTys res
392 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
393 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
394 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
395 tcSplitFunTy_maybe other = Nothing
397 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
398 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
401 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
402 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
403 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
404 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
405 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
406 --- Don't forget that newtype!
407 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
408 tcSplitAppTy_maybe other = Nothing
410 tc_split_app tc [] = Nothing
411 tc_split_app tc tys = split tys []
413 split [ty2] acc = Just (TyConApp tc (reverse acc), ty2)
414 split (ty:tys) acc = split tys (ty:acc)
416 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
418 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
420 tcGetTyVar_maybe :: Type -> Maybe TyVar
421 tcGetTyVar_maybe (TyVarTy tv) = Just tv
422 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
423 tcGetTyVar_maybe other = Nothing
425 tcGetTyVar :: String -> Type -> TyVar
426 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
428 tcIsTyVarTy :: Type -> Bool
429 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
432 The type of a method for class C is always of the form:
433 Forall a1..an. C a1..an => sig_ty
434 where sig_ty is the type given by the method's signature, and thus in general
435 is a ForallTy. At the point that splitMethodTy is called, it is expected
436 that the outer Forall has already been stripped off. splitMethodTy then
437 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
441 tcSplitMethodTy :: Type -> (PredType, Type)
442 tcSplitMethodTy ty = split ty
444 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
446 Nothing -> panic "splitMethodTy"
447 split (NoteTy n ty) = split ty
448 split _ = panic "splitMethodTy"
450 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
451 -- Split the type of a dictionary function
453 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
454 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
455 (tvs, theta, clas, tys) }}
458 (allDistinctTyVars tys tvs) = True
460 all the types tys are type variables,
461 distinct from each other and from tvs.
463 This is useful when checking that unification hasn't unified signature
464 type variables. For example, if the type sig is
465 f :: forall a b. a -> b -> b
466 we want to check that 'a' and 'b' havn't
467 (a) been unified with a non-tyvar type
468 (b) been unified with each other (all distinct)
469 (c) been unified with a variable free in the environment
472 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
474 allDistinctTyVars [] acc
476 allDistinctTyVars (ty:tys) acc
477 = case tcGetTyVar_maybe ty of
478 Nothing -> False -- (a)
479 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
480 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
484 %************************************************************************
486 \subsection{Predicate types}
488 %************************************************************************
490 "Predicates" are particular source types, namelyClassP or IParams
493 isPred :: SourceType -> Bool
494 isPred (ClassP _ _) = True
495 isPred (IParam _ _) = True
496 isPred (NType _ _) = False
498 isPredTy :: Type -> Bool
499 isPredTy (NoteTy _ ty) = isPredTy ty
500 isPredTy (SourceTy sty) = isPred sty
503 tcSplitPredTy_maybe :: Type -> Maybe PredType
504 -- Returns Just for predicates only
505 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
506 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
507 tcSplitPredTy_maybe other = Nothing
509 predTyUnique :: PredType -> Unique
510 predTyUnique (IParam n _) = getUnique (ipNameName n)
511 predTyUnique (ClassP clas tys) = getUnique clas
513 predHasFDs :: PredType -> Bool
514 -- True if the predicate has functional depenencies;
515 -- I.e. should participate in improvement
516 predHasFDs (IParam _ _) = True
517 predHasFDs (ClassP cls _) = classHasFDs cls
519 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
520 mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
521 mkPredName uniq loc (IParam ip ty) = mkLocalName uniq (getOccName (ipNameName ip)) loc
525 --------------------- Dictionary types ---------------------------------
528 mkClassPred clas tys = ClassP clas tys
530 isClassPred :: SourceType -> Bool
531 isClassPred (ClassP clas tys) = True
532 isClassPred other = False
534 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
535 isTyVarClassPred other = False
537 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
538 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
539 getClassPredTys_maybe _ = Nothing
541 getClassPredTys :: PredType -> (Class, [Type])
542 getClassPredTys (ClassP clas tys) = (clas, tys)
544 mkDictTy :: Class -> [Type] -> Type
545 mkDictTy clas tys = mkPredTy (ClassP clas tys)
547 isDictTy :: Type -> Bool
548 isDictTy (SourceTy p) = isClassPred p
549 isDictTy (NoteTy _ ty) = isDictTy ty
550 isDictTy other = False
553 --------------------- Implicit parameters ---------------------------------
556 isIPPred :: SourceType -> Bool
557 isIPPred (IParam _ _) = True
558 isIPPred other = False
560 isInheritablePred :: PredType -> Bool
561 -- Can be inherited by a context. For example, consider
562 -- f x = let g y = (?v, y+x)
563 -- in (g 3 with ?v = 8,
565 -- The point is that g's type must be quantifed over ?v:
566 -- g :: (?v :: a) => a -> a
567 -- but it doesn't need to be quantified over the Num a dictionary
568 -- which can be free in g's rhs, and shared by both calls to g
569 isInheritablePred (ClassP _ _) = True
570 isInheritablePred other = False
572 isLinearPred :: TcPredType -> Bool
573 isLinearPred (IParam (Linear n) _) = True
574 isLinearPred other = False
578 %************************************************************************
580 \subsection{Comparison}
582 %************************************************************************
584 Comparison, taking note of newtypes, predicates, etc,
585 But ignoring usage types
588 tcEqType :: Type -> Type -> Bool
589 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
591 tcEqTypes :: [Type] -> [Type] -> Bool
592 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
594 tcEqPred :: PredType -> PredType -> Bool
595 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
598 tcCmpType :: Type -> Type -> Ordering
599 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
601 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
603 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
605 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
608 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
609 -- The "env" maps type variables in ty1 to type variables in ty2
610 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
611 -- we in effect substitute tv2 for tv1 in t1 before continuing
613 -- Look through NoteTy
614 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
615 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
617 -- Deal with equal constructors
618 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
619 Just tv1a -> tv1a `compare` tv2
620 Nothing -> tv1 `compare` tv2
622 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
623 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
624 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
625 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
626 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
628 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
629 cmpTy env (AppTy _ _) (TyVarTy _) = GT
631 cmpTy env (FunTy _ _) (TyVarTy _) = GT
632 cmpTy env (FunTy _ _) (AppTy _ _) = GT
634 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
635 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
636 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
638 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
639 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
640 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
641 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
643 cmpTy env (SourceTy _) t2 = GT
649 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
650 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
651 -- Compare types as well as names for implicit parameters
652 -- This comparison is used exclusively (I think) for the
653 -- finite map built in TcSimplify
654 cmpSourceTy env (IParam _ _) sty = LT
656 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
657 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
658 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
660 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
661 cmpSourceTy env (NType _ _) sty = GT
664 PredTypes are used as a FM key in TcSimplify,
665 so we take the easy path and make them an instance of Ord
668 instance Eq SourceType where { (==) = tcEqPred }
669 instance Ord SourceType where { compare = tcCmpPred }
673 %************************************************************************
675 \subsection{Predicates}
677 %************************************************************************
679 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
681 f :: (?x::Int) => Int -> Int
684 isSigmaTy :: Type -> Bool
685 isSigmaTy (ForAllTy tyvar ty) = True
686 isSigmaTy (FunTy a b) = isPredTy a
687 isSigmaTy (NoteTy n ty) = isSigmaTy ty
690 isOverloadedTy :: Type -> Bool
691 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
692 isOverloadedTy (FunTy a b) = isPredTy a
693 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
694 isOverloadedTy _ = False
698 isFloatTy = is_tc floatTyConKey
699 isDoubleTy = is_tc doubleTyConKey
700 isForeignPtrTy = is_tc foreignPtrTyConKey
701 isIntegerTy = is_tc integerTyConKey
702 isIntTy = is_tc intTyConKey
703 isAddrTy = is_tc addrTyConKey
704 isBoolTy = is_tc boolTyConKey
705 isUnitTy = is_tc unitTyConKey
707 is_tc :: Unique -> Type -> Bool
708 -- Newtypes are opaque to this
709 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
710 Just (tc, _) -> uniq == getUnique tc
715 %************************************************************************
719 %************************************************************************
722 hoistForAllTys :: Type -> Type
723 -- Used for user-written type signatures only
724 -- Move all the foralls and constraints to the top
725 -- e.g. T -> forall a. a ==> forall a. T -> a
726 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
728 -- We want to 'look through' type synonyms when doing this
729 -- so it's better done on the Type than the HsType
732 = case hoist ty ty of
733 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys theta body)
735 hoist orig_ty (ForAllTy tv ty) = case hoist ty ty of
736 (tvs,theta,tau) -> (tv:tvs,theta,tau)
737 hoist orig_ty (FunTy arg res)
738 | isPredTy arg = case hoist res res of
739 (tvs,theta,tau) -> (tvs,arg:theta,tau)
740 | otherwise = case hoist res res of
741 (tvs,theta,tau) -> (tvs,theta,mkFunTy arg tau)
743 hoist orig_ty (NoteTy _ ty) = hoist orig_ty ty
744 hoist orig_ty ty = ([], [], orig_ty)
749 deNoteType :: Type -> Type
750 -- Remove synonyms, but not source types
751 deNoteType ty@(TyVarTy tyvar) = ty
752 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
753 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
754 deNoteType (NoteTy _ ty) = deNoteType ty
755 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
756 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
757 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
759 deNoteSourceType :: SourceType -> SourceType
760 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
761 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
762 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
765 Find the free names of a type, including the type constructors and classes it mentions
766 This is used in the front end of the compiler
769 namesOfType :: Type -> NameSet
770 namesOfType (TyVarTy tv) = unitNameSet (getName tv)
771 namesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
772 namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
773 namesOfType (NoteTy other_note ty2) = namesOfType ty2
774 namesOfType (SourceTy (IParam n ty)) = namesOfType ty
775 namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
776 namesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
777 namesOfType (FunTy arg res) = namesOfType arg `unionNameSets` namesOfType res
778 namesOfType (AppTy fun arg) = namesOfType fun `unionNameSets` namesOfType arg
779 namesOfType (ForAllTy tyvar ty) = namesOfType ty `delFromNameSet` getName tyvar
781 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
783 namesOfDFunHead :: Type -> NameSet
784 -- Find the free type constructors and classes
785 -- of the head of the dfun instance type
786 -- The 'dfun_head_type' is because of
787 -- instance Foo a => Baz T where ...
788 -- The decl is an orphan if Baz and T are both not locally defined,
789 -- even if Foo *is* locally defined
790 namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
791 (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
796 %************************************************************************
798 \subsection[TysWiredIn-ext-type]{External types}
800 %************************************************************************
802 The compiler's foreign function interface supports the passing of a
803 restricted set of types as arguments and results (the restricting factor
807 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
808 -- Checks for valid argument type for a 'foreign import'
809 isFFIArgumentTy dflags safety ty
810 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
812 isFFIExternalTy :: Type -> Bool
813 -- Types that are allowed as arguments of a 'foreign export'
814 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
816 isFFIImportResultTy :: DynFlags -> Type -> Bool
817 isFFIImportResultTy dflags ty
818 = checkRepTyCon (legalFIResultTyCon dflags) ty
820 isFFIExportResultTy :: Type -> Bool
821 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
823 isFFIDynArgumentTy :: Type -> Bool
824 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
825 -- or a newtype of either.
826 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
828 isFFIDynResultTy :: Type -> Bool
829 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
830 -- or a newtype of either.
831 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
833 isFFILabelTy :: Type -> Bool
834 -- The type of a foreign label must be Ptr, FunPtr, Addr,
835 -- or a newtype of either.
836 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
838 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
839 -- Look through newtypes
840 -- Non-recursive ones are transparent to splitTyConApp,
841 -- but recursive ones aren't; hence the splitNewType_maybe
842 checkRepTyCon check_tc ty
843 | Just ty' <- splitNewType_maybe ty = checkRepTyCon check_tc ty'
844 | Just (tc,_) <- splitTyConApp_maybe ty = check_tc tc
848 ----------------------------------------------
849 These chaps do the work; they are not exported
850 ----------------------------------------------
853 legalFEArgTyCon :: TyCon -> Bool
854 -- It's illegal to return foreign objects and (mutable)
855 -- bytearrays from a _ccall_ / foreign declaration
856 -- (or be passed them as arguments in foreign exported functions).
858 | getUnique tc `elem` [ foreignObjTyConKey, foreignPtrTyConKey,
859 byteArrayTyConKey, mutableByteArrayTyConKey ]
861 -- It's also illegal to make foreign exports that take unboxed
862 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
864 = boxedMarshalableTyCon tc
866 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
867 legalFIResultTyCon dflags tc
868 | getUnique tc `elem`
869 [ foreignObjTyConKey, foreignPtrTyConKey,
870 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
871 | tc == unitTyCon = True
872 | otherwise = marshalableTyCon dflags tc
874 legalFEResultTyCon :: TyCon -> Bool
875 legalFEResultTyCon tc
876 | getUnique tc `elem`
877 [ foreignObjTyConKey, foreignPtrTyConKey,
878 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
879 | tc == unitTyCon = True
880 | otherwise = boxedMarshalableTyCon tc
882 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
883 -- Checks validity of types going from Haskell -> external world
884 legalOutgoingTyCon dflags safety tc
885 | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
888 = marshalableTyCon dflags tc
890 marshalableTyCon dflags tc
891 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
892 || boxedMarshalableTyCon tc
894 boxedMarshalableTyCon tc
895 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
896 , int32TyConKey, int64TyConKey
897 , wordTyConKey, word8TyConKey, word16TyConKey
898 , word32TyConKey, word64TyConKey
899 , floatTyConKey, doubleTyConKey
900 , addrTyConKey, ptrTyConKey, funPtrTyConKey
901 , charTyConKey, foreignObjTyConKey
904 , byteArrayTyConKey, mutableByteArrayTyConKey
910 %************************************************************************
912 \subsection{Unification with an explicit substitution}
914 %************************************************************************
916 Unify types with an explicit substitution and no monad.
917 Ignore usage annotations.
921 = (TyVarSet, -- Set of template tyvars
922 TyVarSubstEnv) -- Not necessarily idempotent
924 unifyTysX :: TyVarSet -- Template tyvars
927 -> Maybe TyVarSubstEnv
928 unifyTysX tmpl_tyvars ty1 ty2
929 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
931 unifyExtendTysX :: TyVarSet -- Template tyvars
932 -> TyVarSubstEnv -- Substitution to start with
935 -> Maybe TyVarSubstEnv -- Extended substitution
936 unifyExtendTysX tmpl_tyvars subst ty1 ty2
937 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
939 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
940 -> Maybe TyVarSubstEnv
941 unifyTyListsX tmpl_tyvars tys1 tys2
942 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
947 -> (MySubst -> Maybe result)
951 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
952 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
954 -- Variables; go for uVar
955 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
958 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
959 | tyvar1 `elemVarSet` tmpls
960 = uVarX tyvar1 ty2 k subst
961 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
962 | tyvar2 `elemVarSet` tmpls
963 = uVarX tyvar2 ty1 k subst
966 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
967 | n1 == n2 = uTysX t1 t2 k subst
968 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
969 | c1 == c2 = uTyListsX tys1 tys2 k subst
970 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
971 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
973 -- Functions; just check the two parts
974 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
975 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
977 -- Type constructors must match
978 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
979 | (con1 == con2 && equalLength tys1 tys2)
980 = uTyListsX tys1 tys2 k subst
982 -- Applications need a bit of care!
983 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
984 -- NB: we've already dealt with type variables and Notes,
985 -- so if one type is an App the other one jolly well better be too
986 uTysX (AppTy s1 t1) ty2 k subst
987 = case tcSplitAppTy_maybe ty2 of
988 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
989 Nothing -> Nothing -- Fail
991 uTysX ty1 (AppTy s2 t2) k subst
992 = case tcSplitAppTy_maybe ty1 of
993 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
994 Nothing -> Nothing -- Fail
996 -- Not expecting for-alls in unification
998 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
999 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1002 -- Anything else fails
1003 uTysX ty1 ty2 k subst = Nothing
1006 uTyListsX [] [] k subst = k subst
1007 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1008 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1012 -- Invariant: tv1 is a unifiable variable
1013 uVarX tv1 ty2 k subst@(tmpls, env)
1014 = case lookupSubstEnv env tv1 of
1015 Just (DoneTy ty1) -> -- Already bound
1016 uTysX ty1 ty2 k subst
1018 Nothing -- Not already bound
1019 | typeKind ty2 `eqKind` tyVarKind tv1
1020 && occur_check_ok ty2
1021 -> -- No kind mismatch nor occur check
1022 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1024 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1026 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1027 occur_check_ok_tv tv | tv1 == tv = False
1028 | otherwise = case lookupSubstEnv env tv of
1030 Just (DoneTy ty) -> occur_check_ok ty
1035 %************************************************************************
1037 \subsection{Matching on types}
1039 %************************************************************************
1041 Matching is a {\em unidirectional} process, matching a type against a
1042 template (which is just a type with type variables in it). The
1043 matcher assumes that there are no repeated type variables in the
1044 template, so that it simply returns a mapping of type variables to
1045 types. It also fails on nested foralls.
1047 @matchTys@ matches corresponding elements of a list of templates and
1048 types. It and @matchTy@ both ignore usage annotations, unlike the
1049 main function @match@.
1052 matchTy :: TyVarSet -- Template tyvars
1054 -> Type -- Proposed instance of template
1055 -> Maybe TyVarSubstEnv -- Matching substitution
1058 matchTys :: TyVarSet -- Template tyvars
1059 -> [Type] -- Templates
1060 -> [Type] -- Proposed instance of template
1061 -> Maybe (TyVarSubstEnv, -- Matching substitution
1062 [Type]) -- Left over instance types
1064 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1066 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1067 (\ (senv,tys) -> Just (senv,tys))
1071 @match@ is the main function. It takes a flag indicating whether
1072 usage annotations are to be respected.
1075 match :: Type -> Type -- Current match pair
1076 -> TyVarSet -- Template vars
1077 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1078 -> TyVarSubstEnv -- Current subst
1081 -- When matching against a type variable, see if the variable
1082 -- has already been bound. If so, check that what it's bound to
1083 -- is the same as ty; if not, bind it and carry on.
1085 match (TyVarTy v) ty tmpls k senv
1086 | v `elemVarSet` tmpls
1087 = -- v is a template variable
1088 case lookupSubstEnv senv v of
1089 Nothing | typeKind ty `eqKind` tyVarKind v
1090 -- We do a kind check, just as in the uVarX above
1091 -- The kind check is needed to avoid bogus matches
1092 -- of (a b) with (c d), where the kinds don't match
1093 -- An occur check isn't needed when matching.
1094 -> k (extendSubstEnv senv v (DoneTy ty))
1096 | otherwise -> Nothing -- Fails
1098 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1099 | otherwise -> Nothing -- Fails
1102 = -- v is not a template variable; ty had better match
1103 -- Can't use (==) because types differ
1104 case tcGetTyVar_maybe ty of
1105 Just v' | v == v' -> k senv -- Success
1106 other -> Nothing -- Failure
1107 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1108 -- I guess the reason the Note-stripping case is *last* rather than first
1109 -- is to preserve type synonyms etc., so I'm not moving it to the
1110 -- top; but this means that (without the deNotetype) a type
1111 -- variable may not match the pattern (TyVarTy v') as one would
1112 -- expect, due to an intervening Note. KSW 2000-06.
1115 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1116 | n1 == n2 = match t1 t2 tmpls k senv
1117 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1118 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1119 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1120 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1122 -- Functions; just check the two parts
1123 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1124 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1126 match (AppTy fun1 arg1) ty2 tmpls k senv
1127 = case tcSplitAppTy_maybe ty2 of
1128 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1129 Nothing -> Nothing -- Fail
1131 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1132 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1134 -- Newtypes are opaque; other source types should not happen
1135 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1136 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1138 -- With type synonyms, we have to be careful for the exact
1139 -- same reasons as in the unifier. Please see the
1140 -- considerable commentary there before changing anything
1141 -- here! (WDP 95/05)
1142 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1143 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1146 match _ _ _ _ _ = Nothing
1148 match_list_exactly tys1 tys2 tmpls k senv
1149 = match_list tys1 tys2 tmpls k' senv
1151 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1152 | otherwise = Nothing -- Fail
1154 match_list [] tys2 tmpls k senv = k (senv, tys2)
1155 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1156 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1157 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv