2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcType]{Types used in the typechecker}
6 This module provides the Type interface for front-end parts of the
9 * treat "source types" as opaque:
10 newtypes, and predicates are meaningful.
11 * look through usage types
13 The "tc" prefix is for "typechechecker", because the type checker
14 is the principal client.
18 --------------------------------
20 TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
21 TcTyVar, TcTyVarSet, TcKind,
23 --------------------------------
25 TyVarDetails(..), isUserTyVar, isSkolemTyVar,
28 --------------------------------
32 --------------------------------
34 -- These are important because they do not look through newtypes
35 tcSplitForAllTys, tcSplitPhiTy,
36 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
37 tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
38 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, 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,
48 isTauTy, tcIsTyVarTy, tcIsForAllTy,
51 ---------------------------------
52 -- Misc type manipulators
53 deNoteType, classesOfTheta,
54 tyClsNamesOfType, tyClsNamesOfDFunHead,
57 ---------------------------------
59 getClassPredTys_maybe, getClassPredTys,
60 isClassPred, isTyVarClassPred,
61 mkDictTy, tcSplitPredTy_maybe,
62 isPredTy, 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
74 isFFIDotnetTy, -- :: DynFlags -> Type -> Bool
75 isFFIDotnetObjTy, -- :: Type -> Bool
77 toDNType, -- :: Type -> DNType
79 ---------------------------------
80 -- Unifier and matcher
81 unifyTysX, unifyTyListsX, unifyExtendTysX,
82 matchTy, matchTys, match,
84 --------------------------------
85 -- Rexported from Type
86 Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
87 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
88 superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
89 isTypeKind, isAnyTypeKind, typeCon,
91 Type, PredType(..), ThetaType,
92 mkForAllTy, mkForAllTys,
93 mkFunTy, mkFunTys, zipFunTys,
94 mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
95 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
97 isUnLiftedType, -- Source types are always lifted
98 isUnboxedTupleType, -- Ditto
101 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
102 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
105 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
107 pprKind, pprParendKind,
108 pprType, pprParendType,
109 pprPred, pprTheta, pprThetaArrow, pprClassPred
113 #include "HsVersions.h"
116 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
118 import Type ( -- Re-exports
119 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
120 tyVarsOfTheta, Kind, Type, PredType(..),
121 ThetaType, unliftedTypeKind, typeCon,
122 liftedTypeKind, openTypeKind, mkArrowKind,
123 mkArrowKinds, mkForAllTy, mkForAllTys,
124 defaultKind, isTypeKind, isAnyTypeKind,
125 mkFunTy, mkFunTys, zipFunTys,
126 mkTyConApp, mkGenTyConApp, mkAppTy,
127 mkAppTys, mkSynTy, applyTy, applyTys,
128 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
129 mkPredTys, isUnLiftedType,
130 isUnboxedTupleType, isPrimitiveType,
132 tidyTopType, tidyType, tidyPred, tidyTypes,
133 tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
134 tidyTyVarBndr, tidyOpenTyVar,
135 tidyOpenTyVars, eqKind,
136 hasMoreBoxityInfo, liftedBoxity,
137 superBoxity, typeKind, superKind, repType,
138 pprKind, pprParendKind,
139 pprType, pprParendType,
140 pprPred, pprTheta, pprThetaArrow, pprClassPred
142 import TyCon ( TyCon, isUnLiftedTyCon, tyConUnique )
143 import Class ( Class )
144 import Var ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
145 import ForeignCall ( Safety, playSafe
152 import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
153 import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
155 import OccName ( OccName, mkDictOcc )
156 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
157 import TysWiredIn ( unitTyCon, charTyCon, listTyCon )
158 import BasicTypes ( IPName(..), ipNameName )
159 import Unique ( Unique, Uniquable(..) )
160 import SrcLoc ( SrcLoc )
161 import Util ( cmpList, thenCmp, equalLength, snocView )
162 import Maybes ( maybeToBool, expectJust )
167 %************************************************************************
171 %************************************************************************
173 The type checker divides the generic Type world into the
174 following more structured beasts:
176 sigma ::= forall tyvars. phi
177 -- A sigma type is a qualified type
179 -- Note that even if 'tyvars' is empty, theta
180 -- may not be: e.g. (?x::Int) => Int
182 -- Note that 'sigma' is in prenex form:
183 -- all the foralls are at the front.
184 -- A 'phi' type has no foralls to the right of
192 -- A 'tau' type has no quantification anywhere
193 -- Note that the args of a type constructor must be taus
195 | tycon tau_1 .. tau_n
199 -- In all cases, a (saturated) type synonym application is legal,
200 -- provided it expands to the required form.
203 type TcTyVar = TyVar -- Might be a mutable tyvar
204 type TcTyVarSet = TyVarSet
206 type TcType = Type -- A TcType can have mutable type variables
207 -- Invariant on ForAllTy in TcTypes:
209 -- a cannot occur inside a MutTyVar in T; that is,
210 -- T is "flattened" before quantifying over a
212 type TcPredType = PredType
213 type TcThetaType = ThetaType
214 type TcSigmaType = TcType
215 type TcRhoType = TcType
216 type TcTauType = TcType
221 %************************************************************************
223 \subsection{TyVarDetails}
225 %************************************************************************
227 TyVarDetails gives extra info about type variables, used during type
228 checking. It's attached to mutable type variables only.
229 It's knot-tied back to Var.lhs. There is no reason in principle
230 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
234 = SigTv -- Introduced when instantiating a type signature,
235 -- prior to checking that the defn of a fn does
236 -- have the expected type. Should not be instantiated.
238 -- f :: forall a. a -> a
240 -- When checking e, with expected type (a->a), we
241 -- should not instantiate a
243 | ClsTv -- Scoped type variable introduced by a class decl
244 -- class C a where ...
246 | InstTv -- Ditto, but instance decl
248 | PatSigTv -- Scoped type variable, introduced by a pattern
252 | VanillaTv -- Everything else
254 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
255 isUserTyVar tv = case mutTyVarDetails tv of
259 isSkolemTyVar :: TcTyVar -> Bool
260 isSkolemTyVar tv = 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 VanillaTv = ptext SLIT("//vanilla//") -- Ditto
282 %************************************************************************
284 \subsection{Tau, sigma and rho}
286 %************************************************************************
289 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
291 mkPhiTy :: [PredType] -> Type -> Type
292 mkPhiTy 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 (NewTcApp _ tys) = all isTauTy tys
302 isTauTy (AppTy a b) = isTauTy a && isTauTy b
303 isTauTy (FunTy a b) = isTauTy a && isTauTy b
304 isTauTy (PredTy p) = True -- Don't look through source types
305 isTauTy (NoteTy _ ty) = isTauTy ty
306 isTauTy other = False
310 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
311 -- construct a dictionary function name
312 getDFunTyKey (TyVarTy tv) = getOccName tv
313 getDFunTyKey (TyConApp tc _) = getOccName tc
314 getDFunTyKey (NewTcApp 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 ty = pprPanic "getDFunTyKey" (pprType ty)
320 -- PredTy shouldn't happen
324 %************************************************************************
326 \subsection{Expanding and splitting}
328 %************************************************************************
330 These tcSplit functions are like their non-Tc analogues, but
331 a) they do not look through newtypes
332 b) they do not look through PredTys
333 c) [future] they ignore usage-type annotations
335 However, they are non-monadic and do not follow through mutable type
336 variables. It's up to you to make sure this doesn't matter.
339 tcSplitForAllTys :: Type -> ([TyVar], Type)
340 tcSplitForAllTys ty = split ty ty []
342 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
343 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
344 split orig_ty t tvs = (reverse tvs, orig_ty)
346 tcIsForAllTy (ForAllTy tv ty) = True
347 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
348 tcIsForAllTy t = False
350 tcSplitPhiTy :: Type -> ([PredType], Type)
351 tcSplitPhiTy ty = split ty ty []
353 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
354 Just p -> split res res (p:ts)
355 Nothing -> (reverse ts, orig_ty)
356 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
357 split orig_ty ty ts = (reverse ts, orig_ty)
359 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
360 (tvs, rho) -> case tcSplitPhiTy rho of
361 (theta, tau) -> (tvs, theta, tau)
363 tcTyConAppTyCon :: Type -> TyCon
364 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
366 tcTyConAppArgs :: Type -> [Type]
367 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
369 tcSplitTyConApp :: Type -> (TyCon, [Type])
370 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
372 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
374 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
375 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
376 tcSplitTyConApp_maybe (NewTcApp 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 -- Newtypes are opaque, so they may be split
380 -- However, predicates are not treated
381 -- as tycon applications by the type checker
382 tcSplitTyConApp_maybe other = Nothing
384 tcSplitFunTys :: Type -> ([Type], Type)
385 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
387 Just (arg,res) -> (arg:args, res')
389 (args,res') = tcSplitFunTys res
391 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
392 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
393 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
394 tcSplitFunTy_maybe other = Nothing
396 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
397 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
400 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
401 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
402 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
403 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
404 tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
405 Just (tys', ty') -> Just (TyConApp tc tys', ty')
407 tcSplitAppTy_maybe (NewTcApp tc tys) = case snocView tys of
408 Just (tys', ty') -> Just (NewTcApp tc tys', ty')
410 tcSplitAppTy_maybe other = Nothing
412 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
414 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
416 tcSplitAppTys :: Type -> (Type, [Type])
420 go ty args = case tcSplitAppTy_maybe ty of
421 Just (ty', arg) -> go ty' (arg:args)
424 tcGetTyVar_maybe :: Type -> Maybe TyVar
425 tcGetTyVar_maybe (TyVarTy tv) = Just tv
426 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
427 tcGetTyVar_maybe other = Nothing
429 tcGetTyVar :: String -> Type -> TyVar
430 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
432 tcIsTyVarTy :: Type -> Bool
433 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
436 The type of a method for class C is always of the form:
437 Forall a1..an. C a1..an => sig_ty
438 where sig_ty is the type given by the method's signature, and thus in general
439 is a ForallTy. At the point that splitMethodTy is called, it is expected
440 that the outer Forall has already been stripped off. splitMethodTy then
441 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off.
444 tcSplitMethodTy :: Type -> (PredType, Type)
445 tcSplitMethodTy ty = split ty
447 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
449 Nothing -> panic "splitMethodTy"
450 split (NoteTy n ty) = split ty
451 split _ = panic "splitMethodTy"
453 tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
454 -- Split the type of a dictionary function
456 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
457 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
458 (tvs, theta, clas, tys) }}
461 (allDistinctTyVars tys tvs) = True
463 all the types tys are type variables,
464 distinct from each other and from tvs.
466 This is useful when checking that unification hasn't unified signature
467 type variables. For example, if the type sig is
468 f :: forall a b. a -> b -> b
469 we want to check that 'a' and 'b' havn't
470 (a) been unified with a non-tyvar type
471 (b) been unified with each other (all distinct)
472 (c) been unified with a variable free in the environment
475 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
477 allDistinctTyVars [] acc
479 allDistinctTyVars (ty:tys) acc
480 = case tcGetTyVar_maybe ty of
481 Nothing -> False -- (a)
482 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
483 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
487 %************************************************************************
489 \subsection{Predicate types}
491 %************************************************************************
494 tcSplitPredTy_maybe :: Type -> Maybe PredType
495 -- Returns Just for predicates only
496 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
497 tcSplitPredTy_maybe (PredTy p) = Just p
498 tcSplitPredTy_maybe other = Nothing
500 predTyUnique :: PredType -> Unique
501 predTyUnique (IParam n _) = getUnique (ipNameName n)
502 predTyUnique (ClassP clas tys) = getUnique clas
504 mkPredName :: Unique -> SrcLoc -> PredType -> Name
505 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
506 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
510 --------------------- Dictionary types ---------------------------------
513 mkClassPred clas tys = ClassP clas tys
515 isClassPred :: PredType -> Bool
516 isClassPred (ClassP clas tys) = True
517 isClassPred other = False
519 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
520 isTyVarClassPred other = False
522 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
523 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
524 getClassPredTys_maybe _ = Nothing
526 getClassPredTys :: PredType -> (Class, [Type])
527 getClassPredTys (ClassP clas tys) = (clas, tys)
529 mkDictTy :: Class -> [Type] -> Type
530 mkDictTy clas tys = mkPredTy (ClassP clas tys)
532 isDictTy :: Type -> Bool
533 isDictTy (PredTy p) = isClassPred p
534 isDictTy (NoteTy _ ty) = isDictTy ty
535 isDictTy other = False
538 --------------------- Implicit parameters ---------------------------------
541 isIPPred :: PredType -> Bool
542 isIPPred (IParam _ _) = True
543 isIPPred other = False
545 isInheritablePred :: PredType -> Bool
546 -- Can be inherited by a context. For example, consider
547 -- f x = let g y = (?v, y+x)
548 -- in (g 3 with ?v = 8,
550 -- The point is that g's type must be quantifed over ?v:
551 -- g :: (?v :: a) => a -> a
552 -- but it doesn't need to be quantified over the Num a dictionary
553 -- which can be free in g's rhs, and shared by both calls to g
554 isInheritablePred (ClassP _ _) = True
555 isInheritablePred other = False
557 isLinearPred :: TcPredType -> Bool
558 isLinearPred (IParam (Linear n) _) = True
559 isLinearPred other = False
563 %************************************************************************
565 \subsection{Comparison}
567 %************************************************************************
569 Comparison, taking note of newtypes, predicates, etc,
572 tcEqType :: Type -> Type -> Bool
573 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
575 tcEqTypes :: [Type] -> [Type] -> Bool
576 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` 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 = cmpPredTy 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
598 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
599 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
601 -- Deal with equal constructors
602 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
603 Just tv1a -> tv1a `compare` tv2
604 Nothing -> tv1 `compare` tv2
606 cmpTy env (PredTy p1) (PredTy p2) = cmpPredTy env p1 p2
607 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
608 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
609 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
610 cmpTy env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
611 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
613 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < NewTcApp < ForAllTy < PredTy
614 cmpTy env (AppTy _ _) (TyVarTy _) = GT
616 cmpTy env (FunTy _ _) (TyVarTy _) = GT
617 cmpTy env (FunTy _ _) (AppTy _ _) = GT
619 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
620 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
621 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
623 cmpTy env (NewTcApp _ _) (TyVarTy _) = GT
624 cmpTy env (NewTcApp _ _) (AppTy _ _) = GT
625 cmpTy env (NewTcApp _ _) (FunTy _ _) = GT
626 cmpTy env (NewTcApp _ _) (TyConApp _ _) = GT
628 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
629 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
630 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
631 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
632 cmpTy env (ForAllTy _ _) (NewTcApp _ _) = GT
634 cmpTy env (PredTy _) t2 = GT
640 cmpPredTy :: TyVarEnv TyVar -> PredType -> PredType -> Ordering
641 cmpPredTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
642 -- Compare types as well as names for implicit parameters
643 -- This comparison is used exclusively (I think) for the
644 -- finite map built in TcSimplify
645 cmpPredTy env (IParam _ _) (ClassP _ _) = LT
646 cmpPredTy env (ClassP _ _) (IParam _ _) = GT
647 cmpPredTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
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 PredType where { (==) = tcEqPred }
655 instance Ord PredType 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
676 isOverloadedTy :: Type -> Bool
677 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
678 isOverloadedTy (FunTy a b) = isPredTy a
679 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
680 isOverloadedTy _ = False
682 isPredTy :: Type -> Bool -- Belongs in TcType because it does
683 -- not look through newtypes, or predtypes (of course)
684 isPredTy (NoteTy _ ty) = isPredTy ty
685 isPredTy (PredTy sty) = True
690 isFloatTy = is_tc floatTyConKey
691 isDoubleTy = is_tc doubleTyConKey
692 isIntegerTy = is_tc integerTyConKey
693 isIntTy = is_tc intTyConKey
694 isAddrTy = is_tc addrTyConKey
695 isBoolTy = is_tc boolTyConKey
696 isUnitTy = is_tc unitTyConKey
698 is_tc :: Unique -> Type -> Bool
699 -- Newtypes are opaque to this
700 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
701 Just (tc, _) -> uniq == getUnique tc
706 %************************************************************************
710 %************************************************************************
713 deNoteType :: Type -> Type
714 -- Remove synonyms, but not predicate types
715 deNoteType ty@(TyVarTy tyvar) = ty
716 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
717 deNoteType (NewTcApp tycon tys) = NewTcApp tycon (map deNoteType tys)
718 deNoteType (PredTy p) = PredTy (deNotePredType p)
719 deNoteType (NoteTy _ ty) = deNoteType ty
720 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
721 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
722 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
724 deNotePredType :: PredType -> PredType
725 deNotePredType (ClassP c tys) = ClassP c (map deNoteType tys)
726 deNotePredType (IParam n ty) = IParam n (deNoteType ty)
729 Find the free tycons and classes of a type. This is used in the front
733 tyClsNamesOfType :: Type -> NameSet
734 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
735 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
736 tyClsNamesOfType (NewTcApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
737 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
738 tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
739 tyClsNamesOfType (PredTy (IParam n ty)) = tyClsNamesOfType ty
740 tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
741 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
742 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
743 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
745 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
747 tyClsNamesOfDFunHead :: Type -> NameSet
748 -- Find the free type constructors and classes
749 -- of the head of the dfun instance type
750 -- The 'dfun_head_type' is because of
751 -- instance Foo a => Baz T where ...
752 -- The decl is an orphan if Baz and T are both not locally defined,
753 -- even if Foo *is* locally defined
754 tyClsNamesOfDFunHead dfun_ty
755 = case tcSplitSigmaTy dfun_ty of
756 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
758 classesOfTheta :: ThetaType -> [Class]
759 -- Looks just for ClassP things; maybe it should check
760 classesOfTheta preds = [ c | ClassP c _ <- preds ]
764 %************************************************************************
766 \subsection[TysWiredIn-ext-type]{External types}
768 %************************************************************************
770 The compiler's foreign function interface supports the passing of a
771 restricted set of types as arguments and results (the restricting factor
775 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
776 -- Checks for valid argument type for a 'foreign import'
777 isFFIArgumentTy dflags safety ty
778 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
780 isFFIExternalTy :: Type -> Bool
781 -- Types that are allowed as arguments of a 'foreign export'
782 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
784 isFFIImportResultTy :: DynFlags -> Type -> Bool
785 isFFIImportResultTy dflags ty
786 = checkRepTyCon (legalFIResultTyCon dflags) ty
788 isFFIExportResultTy :: Type -> Bool
789 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
791 isFFIDynArgumentTy :: Type -> Bool
792 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
793 -- or a newtype of either.
794 isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
796 isFFIDynResultTy :: Type -> Bool
797 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
798 -- or a newtype of either.
799 isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
801 isFFILabelTy :: Type -> Bool
802 -- The type of a foreign label must be Ptr, FunPtr, Addr,
803 -- or a newtype of either.
804 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
806 isFFIDotnetTy :: DynFlags -> Type -> Bool
807 isFFIDotnetTy dflags ty
808 = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
809 (legalFIResultTyCon dflags tc ||
810 isFFIDotnetObjTy ty || isStringTy ty)) ty
812 -- Support String as an argument or result from a .NET FFI call.
814 case tcSplitTyConApp_maybe (repType ty) of
817 case tcSplitTyConApp_maybe (repType arg_ty) of
818 Just (cc,[]) -> cc == charTyCon
822 -- Support String as an argument or result from a .NET FFI call.
823 isFFIDotnetObjTy ty =
825 (_, t_ty) = tcSplitForAllTys ty
827 case tcSplitTyConApp_maybe (repType t_ty) of
828 Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
831 toDNType :: Type -> DNType
833 | isStringTy ty = DNString
834 | isFFIDotnetObjTy ty = DNObject
835 | Just (tc,argTys) <- tcSplitTyConApp_maybe ty =
836 case lookup (getUnique tc) dn_assoc of
839 | tc `hasKey` ioTyConKey -> toDNType (head argTys)
840 | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
842 dn_assoc :: [ (Unique, DNType) ]
843 dn_assoc = [ (unitTyConKey, DNUnit)
844 , (intTyConKey, DNInt)
845 , (int8TyConKey, DNInt8)
846 , (int16TyConKey, DNInt16)
847 , (int32TyConKey, DNInt32)
848 , (int64TyConKey, DNInt64)
849 , (wordTyConKey, DNInt)
850 , (word8TyConKey, DNWord8)
851 , (word16TyConKey, DNWord16)
852 , (word32TyConKey, DNWord32)
853 , (word64TyConKey, DNWord64)
854 , (floatTyConKey, DNFloat)
855 , (doubleTyConKey, DNDouble)
856 , (addrTyConKey, DNPtr)
857 , (ptrTyConKey, DNPtr)
858 , (funPtrTyConKey, DNPtr)
859 , (charTyConKey, DNChar)
860 , (boolTyConKey, DNBool)
863 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
864 -- Look through newtypes
865 -- Non-recursive ones are transparent to splitTyConApp,
866 -- but recursive ones aren't
867 checkRepTyCon check_tc ty
868 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
871 checkRepTyConKey :: [Unique] -> Type -> Bool
872 -- Like checkRepTyCon, but just looks at the TyCon key
873 checkRepTyConKey keys
874 = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
877 ----------------------------------------------
878 These chaps do the work; they are not exported
879 ----------------------------------------------
882 legalFEArgTyCon :: TyCon -> Bool
883 -- It's illegal to return foreign objects and (mutable)
884 -- bytearrays from a _ccall_ / foreign declaration
885 -- (or be passed them as arguments in foreign exported functions).
887 | isByteArrayLikeTyCon tc
889 -- It's also illegal to make foreign exports that take unboxed
890 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
892 = boxedMarshalableTyCon tc
894 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
895 legalFIResultTyCon dflags tc
896 | isByteArrayLikeTyCon tc = False
897 | tc == unitTyCon = True
898 | otherwise = marshalableTyCon dflags tc
900 legalFEResultTyCon :: TyCon -> Bool
901 legalFEResultTyCon tc
902 | isByteArrayLikeTyCon tc = False
903 | tc == unitTyCon = True
904 | otherwise = boxedMarshalableTyCon tc
906 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
907 -- Checks validity of types going from Haskell -> external world
908 legalOutgoingTyCon dflags safety tc
909 | playSafe safety && isByteArrayLikeTyCon tc
912 = marshalableTyCon dflags tc
914 marshalableTyCon dflags tc
915 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
916 || boxedMarshalableTyCon tc
918 boxedMarshalableTyCon tc
919 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
920 , int32TyConKey, int64TyConKey
921 , wordTyConKey, word8TyConKey, word16TyConKey
922 , word32TyConKey, word64TyConKey
923 , floatTyConKey, doubleTyConKey
924 , addrTyConKey, ptrTyConKey, funPtrTyConKey
927 , byteArrayTyConKey, mutableByteArrayTyConKey
931 isByteArrayLikeTyCon :: TyCon -> Bool
932 isByteArrayLikeTyCon tc =
933 getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
937 %************************************************************************
939 \subsection{Unification with an explicit substitution}
941 %************************************************************************
943 Unify types with an explicit substitution and no monad.
944 Ignore usage annotations.
948 = (TyVarSet, -- Set of template tyvars
949 TyVarSubstEnv) -- Not necessarily idempotent
951 unifyTysX :: TyVarSet -- Template tyvars
954 -> Maybe TyVarSubstEnv
955 unifyTysX tmpl_tyvars ty1 ty2
956 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
958 unifyExtendTysX :: TyVarSet -- Template tyvars
959 -> TyVarSubstEnv -- Substitution to start with
962 -> Maybe TyVarSubstEnv -- Extended substitution
963 unifyExtendTysX tmpl_tyvars subst ty1 ty2
964 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
966 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
967 -> Maybe TyVarSubstEnv
968 unifyTyListsX tmpl_tyvars tys1 tys2
969 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
974 -> (MySubst -> Maybe result)
978 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
979 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
981 -- Variables; go for uVar
982 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
985 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
986 | tyvar1 `elemVarSet` tmpls
987 = uVarX tyvar1 ty2 k subst
988 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
989 | tyvar2 `elemVarSet` tmpls
990 = uVarX tyvar2 ty1 k subst
993 uTysX (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) k subst
994 | n1 == n2 = uTysX t1 t2 k subst
995 uTysX (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) k subst
996 | c1 == c2 = uTyListsX tys1 tys2 k subst
998 -- Functions; just check the two parts
999 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
1000 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
1002 -- Type constructors must match
1003 uTysX (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) k subst
1004 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
1005 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
1006 | (con1 == con2 && equalLength tys1 tys2)
1007 = uTyListsX tys1 tys2 k subst
1009 -- Applications need a bit of care!
1010 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1011 -- NB: we've already dealt with type variables and Notes,
1012 -- so if one type is an App the other one jolly well better be too
1013 uTysX (AppTy s1 t1) ty2 k subst
1014 = case tcSplitAppTy_maybe ty2 of
1015 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1016 Nothing -> Nothing -- Fail
1018 uTysX ty1 (AppTy s2 t2) k subst
1019 = case tcSplitAppTy_maybe ty1 of
1020 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1021 Nothing -> Nothing -- Fail
1023 -- Not expecting for-alls in unification
1025 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
1026 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1029 -- Anything else fails
1030 uTysX ty1 ty2 k subst = Nothing
1033 uTyListsX [] [] k subst = k subst
1034 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1035 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1039 -- Invariant: tv1 is a unifiable variable
1040 uVarX tv1 ty2 k subst@(tmpls, env)
1041 = case lookupSubstEnv env tv1 of
1042 Just (DoneTy ty1) -> -- Already bound
1043 uTysX ty1 ty2 k subst
1045 Nothing -- Not already bound
1046 | typeKind ty2 `eqKind` tyVarKind tv1
1047 && occur_check_ok ty2
1048 -> -- No kind mismatch nor occur check
1049 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1051 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1053 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1054 occur_check_ok_tv tv | tv1 == tv = False
1055 | otherwise = case lookupSubstEnv env tv of
1057 Just (DoneTy ty) -> occur_check_ok ty
1062 %************************************************************************
1064 \subsection{Matching on types}
1066 %************************************************************************
1068 Matching is a {\em unidirectional} process, matching a type against a
1069 template (which is just a type with type variables in it). The
1070 matcher assumes that there are no repeated type variables in the
1071 template, so that it simply returns a mapping of type variables to
1072 types. It also fails on nested foralls.
1074 @matchTys@ matches corresponding elements of a list of templates and
1075 types. It and @matchTy@ both ignore usage annotations, unlike the
1076 main function @match@.
1079 matchTy :: TyVarSet -- Template tyvars
1081 -> Type -- Proposed instance of template
1082 -> Maybe TyVarSubstEnv -- Matching substitution
1085 matchTys :: TyVarSet -- Template tyvars
1086 -> [Type] -- Templates
1087 -> [Type] -- Proposed instance of template
1088 -> Maybe (TyVarSubstEnv, -- Matching substitution
1089 [Type]) -- Left over instance types
1091 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1093 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1094 (\ (senv,tys) -> Just (senv,tys))
1098 @match@ is the main function. It takes a flag indicating whether
1099 usage annotations are to be respected.
1102 match :: Type -> Type -- Current match pair
1103 -> TyVarSet -- Template vars
1104 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1105 -> TyVarSubstEnv -- Current subst
1108 -- When matching against a type variable, see if the variable
1109 -- has already been bound. If so, check that what it's bound to
1110 -- is the same as ty; if not, bind it and carry on.
1112 match (TyVarTy v) ty tmpls k senv
1113 | v `elemVarSet` tmpls
1114 = -- v is a template variable
1115 case lookupSubstEnv senv v of
1116 Nothing | typeKind ty `eqKind` tyVarKind v
1117 -- We do a kind check, just as in the uVarX above
1118 -- The kind check is needed to avoid bogus matches
1119 -- of (a b) with (c d), where the kinds don't match
1120 -- An occur check isn't needed when matching.
1121 -> k (extendSubstEnv senv v (DoneTy ty))
1123 | otherwise -> Nothing -- Fails
1125 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1126 | otherwise -> Nothing -- Fails
1129 = -- v is not a template variable; ty had better match
1130 -- Can't use (==) because types differ
1131 case tcGetTyVar_maybe ty of
1132 Just v' | v == v' -> k senv -- Success
1133 other -> Nothing -- Failure
1134 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1135 -- I guess the reason the Note-stripping case is *last* rather than first
1136 -- is to preserve type synonyms etc., so I'm not moving it to the
1137 -- top; but this means that (without the deNotetype) a type
1138 -- variable may not match the pattern (TyVarTy v') as one would
1139 -- expect, due to an intervening Note. KSW 2000-06.
1142 match (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) tmpls k senv
1143 | n1 == n2 = match t1 t2 tmpls k senv
1144 match (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) tmpls k senv
1145 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1147 -- Functions; just check the two parts
1148 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1149 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1151 match (AppTy fun1 arg1) ty2 tmpls k senv
1152 = case tcSplitAppTy_maybe ty2 of
1153 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1154 Nothing -> Nothing -- Fail
1156 -- Newtypes are opaque; predicate types should not happen
1157 match (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) tmpls k senv
1158 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1159 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1160 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1162 -- With type synonyms, we have to be careful for the exact
1163 -- same reasons as in the unifier. Please see the
1164 -- considerable commentary there before changing anything
1165 -- here! (WDP 95/05)
1166 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1167 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1170 match _ _ _ _ _ = Nothing
1172 match_list_exactly tys1 tys2 tmpls k senv
1173 = match_list tys1 tys2 tmpls k' senv
1175 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1176 | otherwise = Nothing -- Fail
1178 match_list [] tys2 tmpls k senv = k (senv, tys2)
1179 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1180 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1181 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv