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, 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, inheritablePred, 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,
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
111 import Type ( mkUTyM, unUTy ) -- Used locally
113 import Type ( -- Re-exports
114 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
115 Kind, Type, SourceType(..), PredType, ThetaType,
116 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
117 mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
118 mkFunTy, mkFunTys, zipFunTys,
119 mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
120 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
121 isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
122 splitNewType_maybe, splitTyConApp_maybe,
123 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
124 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
125 hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
127 import TyCon ( TyCon, isUnLiftedTyCon )
128 import Class ( classHasFDs, Class )
129 import Var ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
130 import ForeignCall ( Safety, playSafe )
135 import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
136 import Name ( Name, NamedThing(..), mkLocalName, getSrcLoc )
137 import OccName ( OccName, mkDictOcc )
139 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
140 import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
141 import BasicTypes ( ipNameName )
142 import Unique ( Unique, Uniquable(..) )
143 import SrcLoc ( SrcLoc )
144 import Util ( cmpList, thenCmp, equalLength )
145 import Maybes ( maybeToBool, expectJust )
150 %************************************************************************
154 %************************************************************************
156 The type checker divides the generic Type world into the
157 following more structured beasts:
159 sigma ::= forall tyvars. theta => phi
160 -- A sigma type is a qualified type
162 -- Note that even if 'tyvars' is empty, theta
163 -- may not be: e.g. (?x::Int) => Int
165 -- Note that 'sigma' is in prenex form:
166 -- all the foralls are at the front.
167 -- A 'phi' type has no foralls to the right of
173 -- A 'tau' type has no quantification anywhere
174 -- Note that the args of a type constructor must be taus
176 | tycon tau_1 .. tau_n
180 -- In all cases, a (saturated) type synonym application is legal,
181 -- provided it expands to the required form.
185 type SigmaType = Type
191 type TcTyVar = TyVar -- Might be a mutable tyvar
192 type TcTyVarSet = TyVarSet
194 type TcType = Type -- A TcType can have mutable type variables
195 -- Invariant on ForAllTy in TcTypes:
197 -- a cannot occur inside a MutTyVar in T; that is,
198 -- T is "flattened" before quantifying over a
200 type TcPredType = PredType
201 type TcThetaType = ThetaType
202 type TcSigmaType = TcType
203 type TcPhiType = TcType
204 type TcTauType = TcType
209 %************************************************************************
211 \subsection{TyVarDetails}
213 %************************************************************************
215 TyVarDetails gives extra info about type variables, used during type
216 checking. It's attached to mutable type variables only.
217 It's knot-tied back to Var.lhs. There is no reason in principle
218 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
222 = HoleTv -- Used *only* by the type checker when passing in a type
223 -- variable that should be side-effected to the result type.
224 -- Always has kind openTypeKind.
225 -- Never appears in types
227 | SigTv -- Introduced when instantiating a type signature,
228 -- prior to checking that the defn of a fn does
229 -- have the expected type. Should not be instantiated.
231 -- f :: forall a. a -> a
233 -- When checking e, with expected type (a->a), we
234 -- should not instantiate a
236 | ClsTv -- Scoped type variable introduced by a class decl
237 -- class C a where ...
239 | InstTv -- Ditto, but instance decl
241 | PatSigTv -- Scoped type variable, introduced by a pattern
245 | VanillaTv -- Everything else
247 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
248 isUserTyVar tv = case mutTyVarDetails tv of
252 isSkolemTyVar :: TcTyVar -> Bool
253 isSkolemTyVar tv = case mutTyVarDetails tv of
257 isHoleTyVar :: TcTyVar -> Bool
258 -- NB: the hole might be filled in by now, and this
259 -- function does not check for that
260 isHoleTyVar tv = ASSERT( isMutTyVar tv )
261 case mutTyVarDetails tv of
265 tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
268 = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
269 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
273 details SigTv = ptext SLIT("type signature")
274 details ClsTv = ptext SLIT("class declaration")
275 details InstTv = ptext SLIT("instance declaration")
276 details PatSigTv = ptext SLIT("pattern type signature")
277 details HoleTv = ptext SLIT("//hole//") -- Should not happen
278 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
282 %************************************************************************
284 \subsection{Tau, sigma and rho}
286 %************************************************************************
289 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
291 mkRhoTy :: [SourceType] -> Type -> Type
292 mkRhoTy theta ty = UASSERT2( not (isUTy ty), pprType ty )
293 foldr (\p r -> FunTy (mkUTyM (mkPredTy p)) (mkUTyM r)) ty theta
298 @isTauTy@ tests for nested for-alls.
301 isTauTy :: Type -> Bool
302 isTauTy (TyVarTy v) = True
303 isTauTy (TyConApp _ tys) = all isTauTy tys
304 isTauTy (AppTy a b) = isTauTy a && isTauTy b
305 isTauTy (FunTy a b) = isTauTy a && isTauTy b
306 isTauTy (SourceTy p) = True -- Don't look through source types
307 isTauTy (NoteTy _ ty) = isTauTy ty
308 isTauTy (UsageTy _ 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 (UsageTy _ t) = getDFunTyKey t
322 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
323 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
324 -- SourceTy shouldn't happen
328 %************************************************************************
330 \subsection{Expanding and splitting}
332 %************************************************************************
334 These tcSplit functions are like their non-Tc analogues, but
335 a) they do not look through newtypes
336 b) they do not look through PredTys
337 c) [future] they ignore usage-type annotations
339 However, they are non-monadic and do not follow through mutable type
340 variables. It's up to you to make sure this doesn't matter.
343 tcSplitForAllTys :: Type -> ([TyVar], Type)
344 tcSplitForAllTys ty = split ty ty []
346 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
347 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
348 split orig_ty (UsageTy _ ty) tvs = split orig_ty ty tvs
349 split orig_ty t tvs = (reverse tvs, orig_ty)
351 tcIsForAllTy (ForAllTy tv ty) = True
352 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
353 tcIsForAllTy (UsageTy n ty) = tcIsForAllTy ty
354 tcIsForAllTy t = False
356 tcSplitRhoTy :: Type -> ([PredType], Type)
357 tcSplitRhoTy ty = split ty ty []
359 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
360 Just p -> split res res (p:ts)
361 Nothing -> (reverse ts, orig_ty)
362 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
363 split orig_ty (UsageTy _ ty) ts = split orig_ty ty ts
364 split orig_ty ty ts = (reverse ts, orig_ty)
366 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
367 (tvs, rho) -> case tcSplitRhoTy rho of
368 (theta, tau) -> (tvs, theta, tau)
370 tcTyConAppTyCon :: Type -> TyCon
371 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
373 tcTyConAppArgs :: Type -> [Type]
374 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
376 tcSplitTyConApp :: Type -> (TyCon, [Type])
377 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
379 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
381 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
382 -- Newtypes are opaque, so they may be split
383 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
384 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [unUTy arg,unUTy res])
385 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
386 tcSplitTyConApp_maybe (UsageTy _ ty) = tcSplitTyConApp_maybe ty
387 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
388 -- However, predicates are not treated
389 -- as tycon applications by the type checker
390 tcSplitTyConApp_maybe other = Nothing
392 tcSplitFunTys :: Type -> ([Type], Type)
393 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
395 Just (arg,res) -> (arg:args, res')
397 (args,res') = tcSplitFunTys res
399 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
400 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
401 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
402 tcSplitFunTy_maybe (UsageTy _ ty) = tcSplitFunTy_maybe ty
403 tcSplitFunTy_maybe other = Nothing
405 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
406 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
409 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
410 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2)
411 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
412 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
413 tcSplitAppTy_maybe (UsageTy _ ty) = tcSplitAppTy_maybe ty
414 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
415 --- Don't forget that newtype!
416 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
417 tcSplitAppTy_maybe other = Nothing
419 tc_split_app tc [] = Nothing
420 tc_split_app tc tys = split tys []
422 split [ty2] acc = Just (TyConApp tc (reverse acc), ty2)
423 split (ty:tys) acc = split tys (ty:acc)
425 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
427 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
429 tcGetTyVar_maybe :: Type -> Maybe TyVar
430 tcGetTyVar_maybe (TyVarTy tv) = Just tv
431 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
432 tcGetTyVar_maybe ty@(UsageTy _ _) = pprPanic "tcGetTyVar_maybe: UTy:" (pprType ty)
433 tcGetTyVar_maybe other = Nothing
435 tcGetTyVar :: String -> Type -> TyVar
436 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
438 tcIsTyVarTy :: Type -> Bool
439 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
442 The type of a method for class C is always of the form:
443 Forall a1..an. C a1..an => sig_ty
444 where sig_ty is the type given by the method's signature, and thus in general
445 is a ForallTy. At the point that splitMethodTy is called, it is expected
446 that the outer Forall has already been stripped off. splitMethodTy then
447 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
451 tcSplitMethodTy :: Type -> (PredType, Type)
452 tcSplitMethodTy ty = split ty
454 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
456 Nothing -> panic "splitMethodTy"
457 split (NoteTy n ty) = split ty
458 split (UsageTy _ ty) = split ty
459 split _ = panic "splitMethodTy"
461 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
462 -- Split the type of a dictionary function
464 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
465 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
466 (tvs, theta, clas, tys) }}
470 %************************************************************************
472 \subsection{Predicate types}
474 %************************************************************************
476 "Predicates" are particular source types, namelyClassP or IParams
479 isPred :: SourceType -> Bool
480 isPred (ClassP _ _) = True
481 isPred (IParam _ _) = True
482 isPred (NType _ _) = False
484 isPredTy :: Type -> Bool
485 isPredTy (NoteTy _ ty) = isPredTy ty
486 isPredTy (UsageTy _ ty) = isPredTy ty
487 isPredTy (SourceTy sty) = isPred sty
490 tcSplitPredTy_maybe :: Type -> Maybe PredType
491 -- Returns Just for predicates only
492 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
493 tcSplitPredTy_maybe (UsageTy _ ty) = tcSplitPredTy_maybe ty
494 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
495 tcSplitPredTy_maybe other = Nothing
497 predTyUnique :: PredType -> Unique
498 predTyUnique (IParam n _) = getUnique (ipNameName n)
499 predTyUnique (ClassP clas tys) = getUnique clas
501 predHasFDs :: PredType -> Bool
502 -- True if the predicate has functional depenencies;
503 -- I.e. should participate in improvement
504 predHasFDs (IParam _ _) = True
505 predHasFDs (ClassP cls _) = classHasFDs cls
507 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
508 mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
509 mkPredName uniq loc (IParam ip ty) = mkLocalName uniq (getOccName (ipNameName ip)) loc
513 --------------------- Dictionary types ---------------------------------
516 mkClassPred clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
519 isClassPred :: SourceType -> Bool
520 isClassPred (ClassP clas tys) = True
521 isClassPred other = False
523 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
524 isTyVarClassPred other = False
526 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
527 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
528 getClassPredTys_maybe _ = Nothing
530 getClassPredTys :: PredType -> (Class, [Type])
531 getClassPredTys (ClassP clas tys) = (clas, tys)
533 mkDictTy :: Class -> [Type] -> Type
534 mkDictTy clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
535 mkPredTy (ClassP clas tys)
537 isDictTy :: Type -> Bool
538 isDictTy (SourceTy p) = isClassPred p
539 isDictTy (NoteTy _ ty) = isDictTy ty
540 isDictTy (UsageTy _ ty) = isDictTy ty
541 isDictTy other = False
544 --------------------- Implicit parameters ---------------------------------
547 isIPPred :: SourceType -> Bool
548 isIPPred (IParam _ _) = True
549 isIPPred other = False
551 inheritablePred :: PredType -> Bool
552 -- Can be inherited by a context. For example, consider
553 -- f x = let g y = (?v, y+x)
554 -- in (g 3 with ?v = 8,
556 -- The point is that g's type must be quantifed over ?v:
557 -- g :: (?v :: a) => a -> a
558 -- but it doesn't need to be quantified over the Num a dictionary
559 -- which can be free in g's rhs, and shared by both calls to g
560 inheritablePred (ClassP _ _) = True
561 inheritablePred other = False
565 %************************************************************************
567 \subsection{Comparison}
569 %************************************************************************
571 Comparison, taking note of newtypes, predicates, etc,
572 But ignoring usage types
575 tcEqType :: Type -> Type -> Bool
576 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
578 tcEqPred :: PredType -> PredType -> Bool
579 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
582 tcCmpType :: Type -> Type -> Ordering
583 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
585 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
587 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
589 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
592 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
593 -- The "env" maps type variables in ty1 to type variables in ty2
594 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
595 -- we in effect substitute tv2 for tv1 in t1 before continuing
597 -- Look through NoteTy and UsageTy
598 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
599 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
600 cmpTy env (UsageTy _ ty1) ty2 = cmpTy env ty1 ty2
601 cmpTy env ty1 (UsageTy _ ty2) = cmpTy env ty1 ty2
603 -- Deal with equal constructors
604 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
605 Just tv1a -> tv1a `compare` tv2
606 Nothing -> tv1 `compare` tv2
608 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
609 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
610 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
611 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
612 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
614 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
615 cmpTy env (AppTy _ _) (TyVarTy _) = GT
617 cmpTy env (FunTy _ _) (TyVarTy _) = GT
618 cmpTy env (FunTy _ _) (AppTy _ _) = GT
620 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
621 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
622 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
624 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
625 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
626 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
627 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
629 cmpTy env (SourceTy _) t2 = GT
635 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
636 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
637 -- Compare types as well as names for implicit parameters
638 -- This comparison is used exclusively (I think) for the
639 -- finite map built in TcSimplify
640 cmpSourceTy env (IParam _ _) sty = LT
642 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
643 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
644 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
646 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
647 cmpSourceTy env (NType _ _) sty = GT
650 PredTypes are used as a FM key in TcSimplify,
651 so we take the easy path and make them an instance of Ord
654 instance Eq SourceType where { (==) = tcEqPred }
655 instance Ord SourceType where { compare = tcCmpPred }
659 %************************************************************************
661 \subsection{Predicates}
663 %************************************************************************
665 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
667 f :: (?x::Int) => Int -> Int
670 isSigmaTy :: Type -> Bool
671 isSigmaTy (ForAllTy tyvar ty) = True
672 isSigmaTy (FunTy a b) = isPredTy a
673 isSigmaTy (NoteTy n ty) = isSigmaTy ty
674 isSigmaTy (UsageTy _ ty) = isSigmaTy ty
677 isOverloadedTy :: Type -> Bool
678 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
679 isOverloadedTy (FunTy a b) = isPredTy a
680 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
681 isOverloadedTy (UsageTy _ ty) = isOverloadedTy ty
682 isOverloadedTy _ = False
686 isFloatTy = is_tc floatTyConKey
687 isDoubleTy = is_tc doubleTyConKey
688 isForeignPtrTy = is_tc foreignPtrTyConKey
689 isIntegerTy = is_tc integerTyConKey
690 isIntTy = is_tc intTyConKey
691 isAddrTy = is_tc addrTyConKey
692 isBoolTy = is_tc boolTyConKey
693 isUnitTy = is_tc unitTyConKey
695 is_tc :: Unique -> Type -> Bool
696 -- Newtypes are opaque to this
697 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
698 Just (tc, _) -> uniq == getUnique tc
703 %************************************************************************
707 %************************************************************************
710 hoistForAllTys :: Type -> Type
711 -- Move all the foralls to the top
712 -- e.g. T -> forall a. a ==> forall a. T -> a
713 -- Careful: LOSES USAGE ANNOTATIONS!
715 = case hoist ty of { (tvs, body) -> mkForAllTys tvs body }
717 hoist :: Type -> ([TyVar], Type)
718 hoist ty = case tcSplitFunTys ty of { (args, res) ->
719 case tcSplitForAllTys res of {
720 ([], body) -> ([], ty) ;
721 (tvs1, body1) -> case hoist body1 of { (tvs2,body2) ->
722 (tvs1 ++ tvs2, mkFunTys args body2)
728 deNoteType :: Type -> Type
729 -- Remove synonyms, but not source types
730 deNoteType ty@(TyVarTy tyvar) = ty
731 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
732 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
733 deNoteType (NoteTy _ ty) = deNoteType ty
734 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
735 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
736 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
737 deNoteType (UsageTy u ty) = UsageTy u (deNoteType ty)
739 deNoteSourceType :: SourceType -> SourceType
740 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
741 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
742 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
745 Find the free names of a type, including the type constructors and classes it mentions
746 This is used in the front end of the compiler
749 namesOfType :: Type -> NameSet
750 namesOfType (TyVarTy tv) = unitNameSet (getName tv)
751 namesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
752 namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
753 namesOfType (NoteTy other_note ty2) = namesOfType ty2
754 namesOfType (SourceTy (IParam n ty)) = namesOfType ty
755 namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
756 namesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
757 namesOfType (FunTy arg res) = namesOfType arg `unionNameSets` namesOfType res
758 namesOfType (AppTy fun arg) = namesOfType fun `unionNameSets` namesOfType arg
759 namesOfType (ForAllTy tyvar ty) = namesOfType ty `delFromNameSet` getName tyvar
760 namesOfType (UsageTy u ty) = namesOfType u `unionNameSets` namesOfType ty
762 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
764 namesOfDFunHead :: Type -> NameSet
765 -- Find the free type constructors and classes
766 -- of the head of the dfun instance type
767 -- The 'dfun_head_type' is because of
768 -- instance Foo a => Baz T where ...
769 -- The decl is an orphan if Baz and T are both not locally defined,
770 -- even if Foo *is* locally defined
771 namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
772 (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
777 %************************************************************************
779 \subsection[TysWiredIn-ext-type]{External types}
781 %************************************************************************
783 The compiler's foreign function interface supports the passing of a
784 restricted set of types as arguments and results (the restricting factor
788 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
789 -- Checks for valid argument type for a 'foreign import'
790 isFFIArgumentTy dflags safety ty
791 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
793 isFFIExternalTy :: Type -> Bool
794 -- Types that are allowed as arguments of a 'foreign export'
795 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
797 isFFIImportResultTy :: DynFlags -> Type -> Bool
798 isFFIImportResultTy dflags ty
799 = checkRepTyCon (legalFIResultTyCon dflags) ty
801 isFFIExportResultTy :: Type -> Bool
802 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
804 isFFIDynArgumentTy :: Type -> Bool
805 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
806 -- or a newtype of either.
807 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
809 isFFIDynResultTy :: Type -> Bool
810 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
811 -- or a newtype of either.
812 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
814 isFFILabelTy :: Type -> Bool
815 -- The type of a foreign label must be Ptr, FunPtr, Addr,
816 -- or a newtype of either.
817 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
819 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
820 -- Look through newtypes
821 -- Non-recursive ones are transparent to splitTyConApp,
822 -- but recursive ones aren't; hence the splitNewType_maybe
823 checkRepTyCon check_tc ty
824 | Just ty' <- splitNewType_maybe ty = checkRepTyCon check_tc ty'
825 | Just (tc,_) <- splitTyConApp_maybe ty = check_tc tc
829 ----------------------------------------------
830 These chaps do the work; they are not exported
831 ----------------------------------------------
834 legalFEArgTyCon :: TyCon -> Bool
835 -- It's illegal to return foreign objects and (mutable)
836 -- bytearrays from a _ccall_ / foreign declaration
837 -- (or be passed them as arguments in foreign exported functions).
839 | getUnique tc `elem` [ foreignObjTyConKey, foreignPtrTyConKey,
840 byteArrayTyConKey, mutableByteArrayTyConKey ]
842 -- It's also illegal to make foreign exports that take unboxed
843 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
845 = boxedMarshalableTyCon tc
847 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
848 legalFIResultTyCon dflags tc
849 | getUnique tc `elem`
850 [ foreignObjTyConKey, foreignPtrTyConKey,
851 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
852 | tc == unitTyCon = True
853 | otherwise = marshalableTyCon dflags tc
855 legalFEResultTyCon :: TyCon -> Bool
856 legalFEResultTyCon tc
857 | getUnique tc `elem`
858 [ foreignObjTyConKey, foreignPtrTyConKey,
859 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
860 | tc == unitTyCon = True
861 | otherwise = boxedMarshalableTyCon tc
863 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
864 -- Checks validity of types going from Haskell -> external world
865 legalOutgoingTyCon dflags safety tc
866 | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
869 = marshalableTyCon dflags tc
871 marshalableTyCon dflags tc
872 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
873 || boxedMarshalableTyCon tc
875 boxedMarshalableTyCon tc
876 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
877 , int32TyConKey, int64TyConKey
878 , wordTyConKey, word8TyConKey, word16TyConKey
879 , word32TyConKey, word64TyConKey
880 , floatTyConKey, doubleTyConKey
881 , addrTyConKey, ptrTyConKey, funPtrTyConKey
882 , charTyConKey, foreignObjTyConKey
885 , byteArrayTyConKey, mutableByteArrayTyConKey
891 %************************************************************************
893 \subsection{Unification with an explicit substitution}
895 %************************************************************************
897 (allDistinctTyVars tys tvs) = True
899 all the types tys are type variables,
900 distinct from each other and from tvs.
902 This is useful when checking that unification hasn't unified signature
903 type variables. For example, if the type sig is
904 f :: forall a b. a -> b -> b
905 we want to check that 'a' and 'b' havn't
906 (a) been unified with a non-tyvar type
907 (b) been unified with each other (all distinct)
908 (c) been unified with a variable free in the environment
911 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
913 allDistinctTyVars [] acc
915 allDistinctTyVars (ty:tys) acc
916 = case tcGetTyVar_maybe ty of
917 Nothing -> False -- (a)
918 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
919 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
923 %************************************************************************
925 \subsection{Unification with an explicit substitution}
927 %************************************************************************
929 Unify types with an explicit substitution and no monad.
930 Ignore usage annotations.
934 = (TyVarSet, -- Set of template tyvars
935 TyVarSubstEnv) -- Not necessarily idempotent
937 unifyTysX :: TyVarSet -- Template tyvars
940 -> Maybe TyVarSubstEnv
941 unifyTysX tmpl_tyvars ty1 ty2
942 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
944 unifyExtendTysX :: TyVarSet -- Template tyvars
945 -> TyVarSubstEnv -- Substitution to start with
948 -> Maybe TyVarSubstEnv -- Extended substitution
949 unifyExtendTysX tmpl_tyvars subst ty1 ty2
950 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
952 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
953 -> Maybe TyVarSubstEnv
954 unifyTyListsX tmpl_tyvars tys1 tys2
955 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
960 -> (MySubst -> Maybe result)
964 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
965 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
967 -- Variables; go for uVar
968 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
971 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
972 | tyvar1 `elemVarSet` tmpls
973 = uVarX tyvar1 ty2 k subst
974 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
975 | tyvar2 `elemVarSet` tmpls
976 = uVarX tyvar2 ty1 k subst
979 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
980 | n1 == n2 = uTysX t1 t2 k subst
981 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
982 | c1 == c2 = uTyListsX tys1 tys2 k subst
983 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
984 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
986 -- Functions; just check the two parts
987 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
988 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
990 -- Type constructors must match
991 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
992 | (con1 == con2 && equalLength tys1 tys2)
993 = uTyListsX tys1 tys2 k subst
995 -- Applications need a bit of care!
996 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
997 -- NB: we've already dealt with type variables and Notes,
998 -- so if one type is an App the other one jolly well better be too
999 uTysX (AppTy s1 t1) ty2 k subst
1000 = case tcSplitAppTy_maybe ty2 of
1001 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1002 Nothing -> Nothing -- Fail
1004 uTysX ty1 (AppTy s2 t2) k subst
1005 = case tcSplitAppTy_maybe ty1 of
1006 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1007 Nothing -> Nothing -- Fail
1009 -- Not expecting for-alls in unification
1011 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
1012 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1016 uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
1017 uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
1019 -- Anything else fails
1020 uTysX ty1 ty2 k subst = Nothing
1023 uTyListsX [] [] k subst = k subst
1024 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1025 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1029 -- Invariant: tv1 is a unifiable variable
1030 uVarX tv1 ty2 k subst@(tmpls, env)
1031 = case lookupSubstEnv env tv1 of
1032 Just (DoneTy ty1) -> -- Already bound
1033 uTysX ty1 ty2 k subst
1035 Nothing -- Not already bound
1036 | typeKind ty2 `eqKind` tyVarKind tv1
1037 && occur_check_ok ty2
1038 -> -- No kind mismatch nor occur check
1039 UASSERT( not (isUTy ty2) )
1040 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1042 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1044 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1045 occur_check_ok_tv tv | tv1 == tv = False
1046 | otherwise = case lookupSubstEnv env tv of
1048 Just (DoneTy ty) -> occur_check_ok ty
1053 %************************************************************************
1055 \subsection{Matching on types}
1057 %************************************************************************
1059 Matching is a {\em unidirectional} process, matching a type against a
1060 template (which is just a type with type variables in it). The
1061 matcher assumes that there are no repeated type variables in the
1062 template, so that it simply returns a mapping of type variables to
1063 types. It also fails on nested foralls.
1065 @matchTys@ matches corresponding elements of a list of templates and
1066 types. It and @matchTy@ both ignore usage annotations, unlike the
1067 main function @match@.
1070 matchTy :: TyVarSet -- Template tyvars
1072 -> Type -- Proposed instance of template
1073 -> Maybe TyVarSubstEnv -- Matching substitution
1076 matchTys :: TyVarSet -- Template tyvars
1077 -> [Type] -- Templates
1078 -> [Type] -- Proposed instance of template
1079 -> Maybe (TyVarSubstEnv, -- Matching substitution
1080 [Type]) -- Left over instance types
1082 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1084 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1085 (\ (senv,tys) -> Just (senv,tys))
1089 @match@ is the main function. It takes a flag indicating whether
1090 usage annotations are to be respected.
1093 match :: Type -> Type -- Current match pair
1094 -> TyVarSet -- Template vars
1095 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1096 -> TyVarSubstEnv -- Current subst
1099 -- When matching against a type variable, see if the variable
1100 -- has already been bound. If so, check that what it's bound to
1101 -- is the same as ty; if not, bind it and carry on.
1103 match (TyVarTy v) ty tmpls k senv
1104 | v `elemVarSet` tmpls
1105 = -- v is a template variable
1106 case lookupSubstEnv senv v of
1107 Nothing -> UASSERT( not (isUTy ty) )
1108 k (extendSubstEnv senv v (DoneTy ty))
1109 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1110 | otherwise -> Nothing -- Fails
1113 = -- v is not a template variable; ty had better match
1114 -- Can't use (==) because types differ
1115 case tcGetTyVar_maybe ty of
1116 Just v' | v == v' -> k senv -- Success
1117 other -> Nothing -- Failure
1118 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1119 -- I guess the reason the Note-stripping case is *last* rather than first
1120 -- is to preserve type synonyms etc., so I'm not moving it to the
1121 -- top; but this means that (without the deNotetype) a type
1122 -- variable may not match the pattern (TyVarTy v') as one would
1123 -- expect, due to an intervening Note. KSW 2000-06.
1126 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1127 | n1 == n2 = match t1 t2 tmpls k senv
1128 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1129 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1130 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1131 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1133 -- Functions; just check the two parts
1134 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1135 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1137 match (AppTy fun1 arg1) ty2 tmpls k senv
1138 = case tcSplitAppTy_maybe ty2 of
1139 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1140 Nothing -> Nothing -- Fail
1142 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1143 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1145 -- Newtypes are opaque; other source types should not happen
1146 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1147 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1149 match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1150 match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1152 -- With type synonyms, we have to be careful for the exact
1153 -- same reasons as in the unifier. Please see the
1154 -- considerable commentary there before changing anything
1155 -- here! (WDP 95/05)
1156 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1157 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1160 match _ _ _ _ _ = Nothing
1162 match_list_exactly tys1 tys2 tmpls k senv
1163 = match_list tys1 tys2 tmpls k' senv
1165 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1166 | otherwise = Nothing -- Fail
1168 match_list [] tys2 tmpls k senv = k (senv, tys2)
1169 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1170 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1171 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv