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,
50 ---------------------------------
51 -- Misc type manipulators
52 hoistForAllTys, deNoteType,
53 namesOfType, namesOfDFunHead,
56 ---------------------------------
58 PredType, getClassPredTys_maybe, getClassPredTys,
59 isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
60 mkDictTy, tcSplitPredTy_maybe, predTyUnique,
61 isDictTy, tcSplitDFunTy, predTyUnique,
62 mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
64 ---------------------------------
65 -- Foreign import and export
66 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
67 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
68 isFFIExportResultTy, -- :: Type -> Bool
69 isFFIExternalTy, -- :: Type -> Bool
70 isFFIDynArgumentTy, -- :: Type -> Bool
71 isFFIDynResultTy, -- :: Type -> Bool
72 isFFILabelTy, -- :: Type -> Bool
74 ---------------------------------
75 -- Unifier and matcher
76 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
256 isHoleTyVar :: TcTyVar -> Bool
257 -- NB: the hole might be filled in by now, and this
258 -- function does not check for that
259 isHoleTyVar tv = ASSERT( isMutTyVar tv )
260 case mutTyVarDetails tv of
264 tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
267 = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
268 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
272 details SigTv = ptext SLIT("type signature")
273 details ClsTv = ptext SLIT("class declaration")
274 details InstTv = ptext SLIT("instance declaration")
275 details PatSigTv = ptext SLIT("pattern type signature")
276 details HoleTv = ptext SLIT("//hole//") -- Should not happen
277 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
281 %************************************************************************
283 \subsection{Tau, sigma and rho}
285 %************************************************************************
288 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
290 mkRhoTy :: [SourceType] -> Type -> Type
291 mkRhoTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
295 @isTauTy@ tests for nested for-alls.
298 isTauTy :: Type -> Bool
299 isTauTy (TyVarTy v) = True
300 isTauTy (TyConApp _ tys) = all isTauTy tys
301 isTauTy (AppTy a b) = isTauTy a && isTauTy b
302 isTauTy (FunTy a b) = isTauTy a && isTauTy b
303 isTauTy (SourceTy p) = True -- Don't look through source types
304 isTauTy (NoteTy _ ty) = isTauTy ty
305 isTauTy other = False
309 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
310 -- construct a dictionary function name
311 getDFunTyKey (TyVarTy tv) = getOccName tv
312 getDFunTyKey (TyConApp tc _) = getOccName tc
313 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
314 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
315 getDFunTyKey (FunTy arg _) = getOccName funTyCon
316 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
317 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
318 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
319 -- SourceTy shouldn't happen
323 %************************************************************************
325 \subsection{Expanding and splitting}
327 %************************************************************************
329 These tcSplit functions are like their non-Tc analogues, but
330 a) they do not look through newtypes
331 b) they do not look through PredTys
332 c) [future] they ignore usage-type annotations
334 However, they are non-monadic and do not follow through mutable type
335 variables. It's up to you to make sure this doesn't matter.
338 tcSplitForAllTys :: Type -> ([TyVar], Type)
339 tcSplitForAllTys ty = split ty ty []
341 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
342 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
343 split orig_ty t tvs = (reverse tvs, orig_ty)
345 tcIsForAllTy (ForAllTy tv ty) = True
346 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
347 tcIsForAllTy t = False
349 tcSplitRhoTy :: Type -> ([PredType], Type)
350 tcSplitRhoTy ty = split ty ty []
352 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
353 Just p -> split res res (p:ts)
354 Nothing -> (reverse ts, orig_ty)
355 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
356 split orig_ty ty ts = (reverse ts, orig_ty)
358 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
359 (tvs, rho) -> case tcSplitRhoTy rho of
360 (theta, tau) -> (tvs, theta, tau)
362 tcTyConAppTyCon :: Type -> TyCon
363 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
365 tcTyConAppArgs :: Type -> [Type]
366 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
368 tcSplitTyConApp :: Type -> (TyCon, [Type])
369 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
371 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
373 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
374 -- Newtypes are opaque, so they may be split
375 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
376 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
377 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
378 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
379 -- However, predicates are not treated
380 -- as tycon applications by the type checker
381 tcSplitTyConApp_maybe other = Nothing
383 tcSplitFunTys :: Type -> ([Type], Type)
384 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
386 Just (arg,res) -> (arg:args, res')
388 (args,res') = tcSplitFunTys res
390 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
391 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
392 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
393 tcSplitFunTy_maybe other = Nothing
395 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
396 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
399 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
400 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
401 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
402 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
403 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
404 --- Don't forget that newtype!
405 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
406 tcSplitAppTy_maybe other = Nothing
408 tc_split_app tc [] = Nothing
409 tc_split_app tc tys = split tys []
411 split [ty2] acc = Just (TyConApp tc (reverse acc), ty2)
412 split (ty:tys) acc = split tys (ty:acc)
414 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
416 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
418 tcGetTyVar_maybe :: Type -> Maybe TyVar
419 tcGetTyVar_maybe (TyVarTy tv) = Just tv
420 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
421 tcGetTyVar_maybe other = Nothing
423 tcGetTyVar :: String -> Type -> TyVar
424 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
426 tcIsTyVarTy :: Type -> Bool
427 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
430 The type of a method for class C is always of the form:
431 Forall a1..an. C a1..an => sig_ty
432 where sig_ty is the type given by the method's signature, and thus in general
433 is a ForallTy. At the point that splitMethodTy is called, it is expected
434 that the outer Forall has already been stripped off. splitMethodTy then
435 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
439 tcSplitMethodTy :: Type -> (PredType, Type)
440 tcSplitMethodTy ty = split ty
442 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
444 Nothing -> panic "splitMethodTy"
445 split (NoteTy n ty) = split ty
446 split _ = panic "splitMethodTy"
448 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
449 -- Split the type of a dictionary function
451 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
452 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
453 (tvs, theta, clas, tys) }}
457 %************************************************************************
459 \subsection{Predicate types}
461 %************************************************************************
463 "Predicates" are particular source types, namelyClassP or IParams
466 isPred :: SourceType -> Bool
467 isPred (ClassP _ _) = True
468 isPred (IParam _ _) = True
469 isPred (NType _ _) = False
471 isPredTy :: Type -> Bool
472 isPredTy (NoteTy _ ty) = isPredTy ty
473 isPredTy (SourceTy sty) = isPred sty
476 tcSplitPredTy_maybe :: Type -> Maybe PredType
477 -- Returns Just for predicates only
478 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
479 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
480 tcSplitPredTy_maybe other = Nothing
482 predTyUnique :: PredType -> Unique
483 predTyUnique (IParam n _) = getUnique (ipNameName n)
484 predTyUnique (ClassP clas tys) = getUnique clas
486 predHasFDs :: PredType -> Bool
487 -- True if the predicate has functional depenencies;
488 -- I.e. should participate in improvement
489 predHasFDs (IParam _ _) = True
490 predHasFDs (ClassP cls _) = classHasFDs cls
492 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
493 mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
494 mkPredName uniq loc (IParam ip ty) = mkLocalName uniq (getOccName (ipNameName ip)) loc
498 --------------------- Dictionary types ---------------------------------
501 mkClassPred clas tys = ClassP clas tys
503 isClassPred :: SourceType -> Bool
504 isClassPred (ClassP clas tys) = True
505 isClassPred other = False
507 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
508 isTyVarClassPred other = False
510 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
511 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
512 getClassPredTys_maybe _ = Nothing
514 getClassPredTys :: PredType -> (Class, [Type])
515 getClassPredTys (ClassP clas tys) = (clas, tys)
517 mkDictTy :: Class -> [Type] -> Type
518 mkDictTy clas tys = mkPredTy (ClassP clas tys)
520 isDictTy :: Type -> Bool
521 isDictTy (SourceTy p) = isClassPred p
522 isDictTy (NoteTy _ ty) = isDictTy ty
523 isDictTy other = False
526 --------------------- Implicit parameters ---------------------------------
529 isIPPred :: SourceType -> Bool
530 isIPPred (IParam _ _) = True
531 isIPPred other = False
533 isInheritablePred :: PredType -> Bool
534 -- Can be inherited by a context. For example, consider
535 -- f x = let g y = (?v, y+x)
536 -- in (g 3 with ?v = 8,
538 -- The point is that g's type must be quantifed over ?v:
539 -- g :: (?v :: a) => a -> a
540 -- but it doesn't need to be quantified over the Num a dictionary
541 -- which can be free in g's rhs, and shared by both calls to g
542 isInheritablePred (ClassP _ _) = True
543 isInheritablePred other = False
545 isLinearPred :: TcPredType -> Bool
546 isLinearPred (IParam (Linear n) _) = True
547 isLinearPred other = False
551 %************************************************************************
553 \subsection{Comparison}
555 %************************************************************************
557 Comparison, taking note of newtypes, predicates, etc,
558 But ignoring usage types
561 tcEqType :: Type -> Type -> Bool
562 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
564 tcEqTypes :: [Type] -> [Type] -> Bool
565 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
567 tcEqPred :: PredType -> PredType -> Bool
568 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
571 tcCmpType :: Type -> Type -> Ordering
572 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
574 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
576 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
578 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
581 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
582 -- The "env" maps type variables in ty1 to type variables in ty2
583 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
584 -- we in effect substitute tv2 for tv1 in t1 before continuing
586 -- Look through NoteTy
587 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
588 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
590 -- Deal with equal constructors
591 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
592 Just tv1a -> tv1a `compare` tv2
593 Nothing -> tv1 `compare` tv2
595 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
596 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
597 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
598 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
599 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
601 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
602 cmpTy env (AppTy _ _) (TyVarTy _) = GT
604 cmpTy env (FunTy _ _) (TyVarTy _) = GT
605 cmpTy env (FunTy _ _) (AppTy _ _) = GT
607 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
608 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
609 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
611 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
612 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
613 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
614 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
616 cmpTy env (SourceTy _) t2 = GT
622 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
623 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
624 -- Compare types as well as names for implicit parameters
625 -- This comparison is used exclusively (I think) for the
626 -- finite map built in TcSimplify
627 cmpSourceTy env (IParam _ _) sty = LT
629 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
630 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
631 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
633 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
634 cmpSourceTy env (NType _ _) sty = GT
637 PredTypes are used as a FM key in TcSimplify,
638 so we take the easy path and make them an instance of Ord
641 instance Eq SourceType where { (==) = tcEqPred }
642 instance Ord SourceType where { compare = tcCmpPred }
646 %************************************************************************
648 \subsection{Predicates}
650 %************************************************************************
652 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
654 f :: (?x::Int) => Int -> Int
657 isSigmaTy :: Type -> Bool
658 isSigmaTy (ForAllTy tyvar ty) = True
659 isSigmaTy (FunTy a b) = isPredTy a
660 isSigmaTy (NoteTy n ty) = isSigmaTy ty
663 isOverloadedTy :: Type -> Bool
664 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
665 isOverloadedTy (FunTy a b) = isPredTy a
666 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
667 isOverloadedTy _ = False
671 isFloatTy = is_tc floatTyConKey
672 isDoubleTy = is_tc doubleTyConKey
673 isForeignPtrTy = is_tc foreignPtrTyConKey
674 isIntegerTy = is_tc integerTyConKey
675 isIntTy = is_tc intTyConKey
676 isAddrTy = is_tc addrTyConKey
677 isBoolTy = is_tc boolTyConKey
678 isUnitTy = is_tc unitTyConKey
680 is_tc :: Unique -> Type -> Bool
681 -- Newtypes are opaque to this
682 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
683 Just (tc, _) -> uniq == getUnique tc
688 %************************************************************************
692 %************************************************************************
695 hoistForAllTys :: Type -> Type
696 -- Used for user-written type signatures only
697 -- Move all the foralls and constraints to the top
698 -- e.g. T -> forall a. a ==> forall a. T -> a
699 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
701 -- We want to 'look through' type synonyms when doing this
702 -- so it's better done on the Type than the HsType
705 = case hoist ty ty of
706 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys theta body)
708 hoist orig_ty (ForAllTy tv ty) = case hoist ty ty of
709 (tvs,theta,tau) -> (tv:tvs,theta,tau)
710 hoist orig_ty (FunTy arg res)
711 | isPredTy arg = case hoist res res of
712 (tvs,theta,tau) -> (tvs,arg:theta,tau)
713 | otherwise = case hoist res res of
714 (tvs,theta,tau) -> (tvs,theta,mkFunTy arg tau)
716 hoist orig_ty (NoteTy _ ty) = hoist orig_ty ty
717 hoist orig_ty ty = ([], [], orig_ty)
722 deNoteType :: Type -> Type
723 -- Remove synonyms, but not source types
724 deNoteType ty@(TyVarTy tyvar) = ty
725 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
726 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
727 deNoteType (NoteTy _ ty) = deNoteType ty
728 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
729 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
730 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
732 deNoteSourceType :: SourceType -> SourceType
733 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
734 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
735 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
738 Find the free names of a type, including the type constructors and classes it mentions
739 This is used in the front end of the compiler
742 namesOfType :: Type -> NameSet
743 namesOfType (TyVarTy tv) = unitNameSet (getName tv)
744 namesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
745 namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
746 namesOfType (NoteTy other_note ty2) = namesOfType ty2
747 namesOfType (SourceTy (IParam n ty)) = namesOfType ty
748 namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
749 namesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
750 namesOfType (FunTy arg res) = namesOfType arg `unionNameSets` namesOfType res
751 namesOfType (AppTy fun arg) = namesOfType fun `unionNameSets` namesOfType arg
752 namesOfType (ForAllTy tyvar ty) = namesOfType ty `delFromNameSet` getName tyvar
754 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
756 namesOfDFunHead :: Type -> NameSet
757 -- Find the free type constructors and classes
758 -- of the head of the dfun instance type
759 -- The 'dfun_head_type' is because of
760 -- instance Foo a => Baz T where ...
761 -- The decl is an orphan if Baz and T are both not locally defined,
762 -- even if Foo *is* locally defined
763 namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
764 (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
769 %************************************************************************
771 \subsection[TysWiredIn-ext-type]{External types}
773 %************************************************************************
775 The compiler's foreign function interface supports the passing of a
776 restricted set of types as arguments and results (the restricting factor
780 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
781 -- Checks for valid argument type for a 'foreign import'
782 isFFIArgumentTy dflags safety ty
783 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
785 isFFIExternalTy :: Type -> Bool
786 -- Types that are allowed as arguments of a 'foreign export'
787 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
789 isFFIImportResultTy :: DynFlags -> Type -> Bool
790 isFFIImportResultTy dflags ty
791 = checkRepTyCon (legalFIResultTyCon dflags) ty
793 isFFIExportResultTy :: Type -> Bool
794 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
796 isFFIDynArgumentTy :: Type -> Bool
797 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
798 -- or a newtype of either.
799 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
801 isFFIDynResultTy :: Type -> Bool
802 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
803 -- or a newtype of either.
804 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
806 isFFILabelTy :: Type -> Bool
807 -- The type of a foreign label must be Ptr, FunPtr, Addr,
808 -- or a newtype of either.
809 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
811 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
812 -- Look through newtypes
813 -- Non-recursive ones are transparent to splitTyConApp,
814 -- but recursive ones aren't; hence the splitNewType_maybe
815 checkRepTyCon check_tc ty
816 | Just ty' <- splitNewType_maybe ty = checkRepTyCon check_tc ty'
817 | Just (tc,_) <- splitTyConApp_maybe ty = check_tc tc
821 ----------------------------------------------
822 These chaps do the work; they are not exported
823 ----------------------------------------------
826 legalFEArgTyCon :: TyCon -> Bool
827 -- It's illegal to return foreign objects and (mutable)
828 -- bytearrays from a _ccall_ / foreign declaration
829 -- (or be passed them as arguments in foreign exported functions).
831 | getUnique tc `elem` [ foreignObjTyConKey, foreignPtrTyConKey,
832 byteArrayTyConKey, mutableByteArrayTyConKey ]
834 -- It's also illegal to make foreign exports that take unboxed
835 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
837 = boxedMarshalableTyCon tc
839 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
840 legalFIResultTyCon dflags tc
841 | getUnique tc `elem`
842 [ foreignObjTyConKey, foreignPtrTyConKey,
843 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
844 | tc == unitTyCon = True
845 | otherwise = marshalableTyCon dflags tc
847 legalFEResultTyCon :: TyCon -> Bool
848 legalFEResultTyCon tc
849 | getUnique tc `elem`
850 [ foreignObjTyConKey, foreignPtrTyConKey,
851 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
852 | tc == unitTyCon = True
853 | otherwise = boxedMarshalableTyCon tc
855 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
856 -- Checks validity of types going from Haskell -> external world
857 legalOutgoingTyCon dflags safety tc
858 | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
861 = marshalableTyCon dflags tc
863 marshalableTyCon dflags tc
864 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
865 || boxedMarshalableTyCon tc
867 boxedMarshalableTyCon tc
868 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
869 , int32TyConKey, int64TyConKey
870 , wordTyConKey, word8TyConKey, word16TyConKey
871 , word32TyConKey, word64TyConKey
872 , floatTyConKey, doubleTyConKey
873 , addrTyConKey, ptrTyConKey, funPtrTyConKey
874 , charTyConKey, foreignObjTyConKey
877 , byteArrayTyConKey, mutableByteArrayTyConKey
883 %************************************************************************
885 \subsection{Unification with an explicit substitution}
887 %************************************************************************
889 (allDistinctTyVars tys tvs) = True
891 all the types tys are type variables,
892 distinct from each other and from tvs.
894 This is useful when checking that unification hasn't unified signature
895 type variables. For example, if the type sig is
896 f :: forall a b. a -> b -> b
897 we want to check that 'a' and 'b' havn't
898 (a) been unified with a non-tyvar type
899 (b) been unified with each other (all distinct)
900 (c) been unified with a variable free in the environment
903 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
905 allDistinctTyVars [] acc
907 allDistinctTyVars (ty:tys) acc
908 = case tcGetTyVar_maybe ty of
909 Nothing -> False -- (a)
910 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
911 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
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