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 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
89 isArgTypeKind, isSubKind, defaultKind,
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,
122 liftedTypeKind, openTypeKind, mkArrowKind,
123 isLiftedTypeKind, isUnliftedTypeKind,
125 mkArrowKinds, mkForAllTy, mkForAllTys,
126 defaultKind, isArgTypeKind, isOpenTypeKind,
127 mkFunTy, mkFunTys, zipFunTys,
128 mkTyConApp, mkGenTyConApp, mkAppTy,
129 mkAppTys, mkSynTy, applyTy, applyTys,
130 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
131 mkPredTys, isUnLiftedType,
132 isUnboxedTupleType, isPrimitiveType,
134 tidyTopType, tidyType, tidyPred, tidyTypes,
135 tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
136 tidyTyVarBndr, tidyOpenTyVar,
140 pprKind, pprParendKind,
141 pprType, pprParendType,
142 pprPred, pprTheta, pprThetaArrow, pprClassPred
144 import TyCon ( TyCon, isUnLiftedTyCon, tyConUnique )
145 import Class ( Class )
146 import Var ( TyVar, tyVarKind, tcTyVarDetails )
147 import ForeignCall ( Safety, playSafe, DNType(..) )
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 TcType = Type -- A TcType can have mutable type variables
204 -- Invariant on ForAllTy in TcTypes:
206 -- a cannot occur inside a MutTyVar in T; that is,
207 -- T is "flattened" before quantifying over a
209 type TcPredType = PredType
210 type TcThetaType = ThetaType
211 type TcSigmaType = TcType
212 type TcRhoType = TcType
213 type TcTauType = TcType
219 %************************************************************************
221 \subsection{TyVarDetails}
223 %************************************************************************
225 TyVarDetails gives extra info about type variables, used during type
226 checking. It's attached to mutable type variables only.
227 It's knot-tied back to Var.lhs. There is no reason in principle
228 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
231 type TcTyVar = TyVar -- Used only during type inference
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.
237 -- f :: forall a. a -> a
239 -- When checking e, with expected type (a->a), we
240 -- should not instantiate a
242 | ClsTv -- Scoped type variable introduced by a class decl
243 -- class C a where ...
245 | InstTv -- Ditto, but instance decl
247 | PatSigTv -- Scoped type variable, introduced by a pattern
248 -- type signature \ x::a -> e
250 | VanillaTv -- Everything else
252 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
253 isUserTyVar tv = case tcTyVarDetails tv of
257 isSkolemTyVar :: TcTyVar -> Bool
258 isSkolemTyVar tv = case tcTyVarDetails tv of
264 tyVarBindingInfo :: TcTyVar -> SDoc -- Used in checkSigTyVars
266 = sep [ptext SLIT("is bound by the") <+> details (tcTyVarDetails tv),
267 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
269 details SigTv = ptext SLIT("type signature")
270 details ClsTv = ptext SLIT("class declaration")
271 details InstTv = ptext SLIT("instance declaration")
272 details PatSigTv = ptext SLIT("pattern type signature")
273 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
277 type TcTyVarSet = TyVarSet
280 %************************************************************************
282 \subsection{Tau, sigma and rho}
284 %************************************************************************
287 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
289 mkPhiTy :: [PredType] -> Type -> Type
290 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
293 @isTauTy@ tests for nested for-alls.
296 isTauTy :: Type -> Bool
297 isTauTy (TyVarTy v) = True
298 isTauTy (TyConApp _ tys) = all isTauTy tys
299 isTauTy (NewTcApp _ tys) = all isTauTy tys
300 isTauTy (AppTy a b) = isTauTy a && isTauTy b
301 isTauTy (FunTy a b) = isTauTy a && isTauTy b
302 isTauTy (PredTy p) = True -- Don't look through source types
303 isTauTy (NoteTy _ ty) = isTauTy ty
304 isTauTy other = False
308 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
309 -- construct a dictionary function name
310 getDFunTyKey (TyVarTy tv) = getOccName tv
311 getDFunTyKey (TyConApp tc _) = getOccName tc
312 getDFunTyKey (NewTcApp 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 ty = pprPanic "getDFunTyKey" (pprType ty)
318 -- PredTy shouldn't happen
322 %************************************************************************
324 \subsection{Expanding and splitting}
326 %************************************************************************
328 These tcSplit functions are like their non-Tc analogues, but
329 a) they do not look through newtypes
330 b) they do not look through PredTys
331 c) [future] they ignore usage-type annotations
333 However, they are non-monadic and do not follow through mutable type
334 variables. It's up to you to make sure this doesn't matter.
337 tcSplitForAllTys :: Type -> ([TyVar], Type)
338 tcSplitForAllTys ty = split ty ty []
340 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
341 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
342 split orig_ty t tvs = (reverse tvs, orig_ty)
344 tcIsForAllTy (ForAllTy tv ty) = True
345 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
346 tcIsForAllTy t = False
348 tcSplitPhiTy :: Type -> ([PredType], Type)
349 tcSplitPhiTy ty = split ty ty []
351 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
352 Just p -> split res res (p:ts)
353 Nothing -> (reverse ts, orig_ty)
354 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
355 split orig_ty ty ts = (reverse ts, orig_ty)
357 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
358 (tvs, rho) -> case tcSplitPhiTy rho of
359 (theta, tau) -> (tvs, theta, tau)
361 tcTyConAppTyCon :: Type -> TyCon
362 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
364 tcTyConAppArgs :: Type -> [Type]
365 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
367 tcSplitTyConApp :: Type -> (TyCon, [Type])
368 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
370 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
372 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
373 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
374 tcSplitTyConApp_maybe (NewTcApp tc tys) = Just (tc, tys)
375 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
376 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
377 -- Newtypes are opaque, so they may be split
378 -- However, predicates are not treated
379 -- as tycon applications by the type checker
380 tcSplitTyConApp_maybe other = Nothing
382 tcSplitFunTys :: Type -> ([Type], Type)
383 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
385 Just (arg,res) -> (arg:args, res')
387 (args,res') = tcSplitFunTys res
389 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
390 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
391 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
392 tcSplitFunTy_maybe other = Nothing
394 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
395 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
398 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
399 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
400 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
401 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
402 tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
403 Just (tys', ty') -> Just (TyConApp tc tys', ty')
405 tcSplitAppTy_maybe (NewTcApp tc tys) = case snocView tys of
406 Just (tys', ty') -> Just (NewTcApp tc tys', ty')
408 tcSplitAppTy_maybe other = Nothing
410 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
412 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
414 tcSplitAppTys :: Type -> (Type, [Type])
418 go ty args = case tcSplitAppTy_maybe ty of
419 Just (ty', arg) -> go ty' (arg:args)
422 tcGetTyVar_maybe :: Type -> Maybe TyVar
423 tcGetTyVar_maybe (TyVarTy tv) = Just tv
424 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
425 tcGetTyVar_maybe other = Nothing
427 tcGetTyVar :: String -> Type -> TyVar
428 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
430 tcIsTyVarTy :: Type -> Bool
431 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
434 The type of a method for class C is always of the form:
435 Forall a1..an. C a1..an => sig_ty
436 where sig_ty is the type given by the method's signature, and thus in general
437 is a ForallTy. At the point that splitMethodTy is called, it is expected
438 that the outer Forall has already been stripped off. splitMethodTy then
439 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off.
442 tcSplitMethodTy :: Type -> (PredType, Type)
443 tcSplitMethodTy ty = split ty
445 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
447 Nothing -> panic "splitMethodTy"
448 split (NoteTy n ty) = split ty
449 split _ = panic "splitMethodTy"
451 tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
452 -- Split the type of a dictionary function
454 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
455 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
456 (tvs, theta, clas, tys) }}
459 (allDistinctTyVars tys tvs) = True
461 all the types tys are type variables,
462 distinct from each other and from tvs.
464 This is useful when checking that unification hasn't unified signature
465 type variables. For example, if the type sig is
466 f :: forall a b. a -> b -> b
467 we want to check that 'a' and 'b' havn't
468 (a) been unified with a non-tyvar type
469 (b) been unified with each other (all distinct)
470 (c) been unified with a variable free in the environment
473 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
475 allDistinctTyVars [] acc
477 allDistinctTyVars (ty:tys) acc
478 = case tcGetTyVar_maybe ty of
479 Nothing -> False -- (a)
480 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
481 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
485 %************************************************************************
487 \subsection{Predicate types}
489 %************************************************************************
492 tcSplitPredTy_maybe :: Type -> Maybe PredType
493 -- Returns Just for predicates only
494 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
495 tcSplitPredTy_maybe (PredTy p) = Just p
496 tcSplitPredTy_maybe other = Nothing
498 predTyUnique :: PredType -> Unique
499 predTyUnique (IParam n _) = getUnique (ipNameName n)
500 predTyUnique (ClassP clas tys) = getUnique clas
502 mkPredName :: Unique -> SrcLoc -> PredType -> Name
503 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
504 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
508 --------------------- Dictionary types ---------------------------------
511 mkClassPred clas tys = ClassP clas tys
513 isClassPred :: PredType -> Bool
514 isClassPred (ClassP clas tys) = True
515 isClassPred other = False
517 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
518 isTyVarClassPred other = False
520 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
521 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
522 getClassPredTys_maybe _ = Nothing
524 getClassPredTys :: PredType -> (Class, [Type])
525 getClassPredTys (ClassP clas tys) = (clas, tys)
527 mkDictTy :: Class -> [Type] -> Type
528 mkDictTy clas tys = mkPredTy (ClassP clas tys)
530 isDictTy :: Type -> Bool
531 isDictTy (PredTy p) = isClassPred p
532 isDictTy (NoteTy _ ty) = isDictTy ty
533 isDictTy other = False
536 --------------------- Implicit parameters ---------------------------------
539 isIPPred :: PredType -> Bool
540 isIPPred (IParam _ _) = True
541 isIPPred other = False
543 isInheritablePred :: PredType -> Bool
544 -- Can be inherited by a context. For example, consider
545 -- f x = let g y = (?v, y+x)
546 -- in (g 3 with ?v = 8,
548 -- The point is that g's type must be quantifed over ?v:
549 -- g :: (?v :: a) => a -> a
550 -- but it doesn't need to be quantified over the Num a dictionary
551 -- which can be free in g's rhs, and shared by both calls to g
552 isInheritablePred (ClassP _ _) = True
553 isInheritablePred other = False
555 isLinearPred :: TcPredType -> Bool
556 isLinearPred (IParam (Linear n) _) = True
557 isLinearPred other = False
561 %************************************************************************
563 \subsection{Comparison}
565 %************************************************************************
567 Comparison, taking note of newtypes, predicates, etc,
570 tcEqType :: Type -> Type -> Bool
571 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
573 tcEqTypes :: [Type] -> [Type] -> Bool
574 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
576 tcEqPred :: PredType -> PredType -> Bool
577 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
580 tcCmpType :: Type -> Type -> Ordering
581 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
583 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
585 tcCmpPred p1 p2 = cmpPredTy emptyVarEnv p1 p2
587 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
590 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
591 -- The "env" maps type variables in ty1 to type variables in ty2
592 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
593 -- we in effect substitute tv2 for tv1 in t1 before continuing
595 -- Look through NoteTy
596 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
597 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
599 -- Deal with equal constructors
600 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
601 Just tv1a -> tv1a `compare` tv2
602 Nothing -> tv1 `compare` tv2
604 cmpTy env (PredTy p1) (PredTy p2) = cmpPredTy env p1 p2
605 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
606 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
607 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
608 cmpTy env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
609 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
611 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < NewTcApp < ForAllTy < PredTy
612 cmpTy env (AppTy _ _) (TyVarTy _) = GT
614 cmpTy env (FunTy _ _) (TyVarTy _) = GT
615 cmpTy env (FunTy _ _) (AppTy _ _) = GT
617 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
618 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
619 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
621 cmpTy env (NewTcApp _ _) (TyVarTy _) = GT
622 cmpTy env (NewTcApp _ _) (AppTy _ _) = GT
623 cmpTy env (NewTcApp _ _) (FunTy _ _) = GT
624 cmpTy env (NewTcApp _ _) (TyConApp _ _) = GT
626 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
627 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
628 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
629 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
630 cmpTy env (ForAllTy _ _) (NewTcApp _ _) = GT
632 cmpTy env (PredTy _) t2 = GT
638 cmpPredTy :: TyVarEnv TyVar -> PredType -> PredType -> Ordering
639 cmpPredTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
640 -- Compare types as well as names for implicit parameters
641 -- This comparison is used exclusively (I think) for the
642 -- finite map built in TcSimplify
643 cmpPredTy env (IParam _ _) (ClassP _ _) = LT
644 cmpPredTy env (ClassP _ _) (IParam _ _) = GT
645 cmpPredTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
648 PredTypes are used as a FM key in TcSimplify,
649 so we take the easy path and make them an instance of Ord
652 instance Eq PredType where { (==) = tcEqPred }
653 instance Ord PredType where { compare = tcCmpPred }
657 %************************************************************************
659 \subsection{Predicates}
661 %************************************************************************
663 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
665 f :: (?x::Int) => Int -> Int
668 isSigmaTy :: Type -> Bool
669 isSigmaTy (ForAllTy tyvar ty) = True
670 isSigmaTy (FunTy a b) = isPredTy a
671 isSigmaTy (NoteTy n ty) = isSigmaTy ty
674 isOverloadedTy :: Type -> Bool
675 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
676 isOverloadedTy (FunTy a b) = isPredTy a
677 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
678 isOverloadedTy _ = False
680 isPredTy :: Type -> Bool -- Belongs in TcType because it does
681 -- not look through newtypes, or predtypes (of course)
682 isPredTy (NoteTy _ ty) = isPredTy ty
683 isPredTy (PredTy sty) = True
688 isFloatTy = is_tc floatTyConKey
689 isDoubleTy = is_tc doubleTyConKey
690 isIntegerTy = is_tc integerTyConKey
691 isIntTy = is_tc intTyConKey
692 isAddrTy = is_tc addrTyConKey
693 isBoolTy = is_tc boolTyConKey
694 isUnitTy = is_tc unitTyConKey
696 is_tc :: Unique -> Type -> Bool
697 -- Newtypes are opaque to this
698 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
699 Just (tc, _) -> uniq == getUnique tc
704 %************************************************************************
708 %************************************************************************
711 deNoteType :: Type -> Type
712 -- Remove synonyms, but not predicate types
713 deNoteType ty@(TyVarTy tyvar) = ty
714 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
715 deNoteType (NewTcApp tycon tys) = NewTcApp tycon (map deNoteType tys)
716 deNoteType (PredTy p) = PredTy (deNotePredType p)
717 deNoteType (NoteTy _ ty) = deNoteType ty
718 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
719 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
720 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
722 deNotePredType :: PredType -> PredType
723 deNotePredType (ClassP c tys) = ClassP c (map deNoteType tys)
724 deNotePredType (IParam n ty) = IParam n (deNoteType ty)
727 Find the free tycons and classes of a type. This is used in the front
731 tyClsNamesOfType :: Type -> NameSet
732 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
733 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
734 tyClsNamesOfType (NewTcApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
735 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
736 tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
737 tyClsNamesOfType (PredTy (IParam n ty)) = tyClsNamesOfType ty
738 tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
739 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
740 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
741 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
743 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
745 tyClsNamesOfDFunHead :: Type -> NameSet
746 -- Find the free type constructors and classes
747 -- of the head of the dfun instance type
748 -- The 'dfun_head_type' is because of
749 -- instance Foo a => Baz T where ...
750 -- The decl is an orphan if Baz and T are both not locally defined,
751 -- even if Foo *is* locally defined
752 tyClsNamesOfDFunHead dfun_ty
753 = case tcSplitSigmaTy dfun_ty of
754 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
756 classesOfTheta :: ThetaType -> [Class]
757 -- Looks just for ClassP things; maybe it should check
758 classesOfTheta preds = [ c | ClassP c _ <- preds ]
762 %************************************************************************
764 \subsection[TysWiredIn-ext-type]{External types}
766 %************************************************************************
768 The compiler's foreign function interface supports the passing of a
769 restricted set of types as arguments and results (the restricting factor
773 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
774 -- Checks for valid argument type for a 'foreign import'
775 isFFIArgumentTy dflags safety ty
776 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
778 isFFIExternalTy :: Type -> Bool
779 -- Types that are allowed as arguments of a 'foreign export'
780 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
782 isFFIImportResultTy :: DynFlags -> Type -> Bool
783 isFFIImportResultTy dflags ty
784 = checkRepTyCon (legalFIResultTyCon dflags) ty
786 isFFIExportResultTy :: Type -> Bool
787 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
789 isFFIDynArgumentTy :: Type -> Bool
790 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
791 -- or a newtype of either.
792 isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
794 isFFIDynResultTy :: Type -> Bool
795 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
796 -- or a newtype of either.
797 isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
799 isFFILabelTy :: Type -> Bool
800 -- The type of a foreign label must be Ptr, FunPtr, Addr,
801 -- or a newtype of either.
802 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
804 isFFIDotnetTy :: DynFlags -> Type -> Bool
805 isFFIDotnetTy dflags ty
806 = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
807 (legalFIResultTyCon dflags tc ||
808 isFFIDotnetObjTy ty || isStringTy ty)) ty
810 -- Support String as an argument or result from a .NET FFI call.
812 case tcSplitTyConApp_maybe (repType ty) of
815 case tcSplitTyConApp_maybe (repType arg_ty) of
816 Just (cc,[]) -> cc == charTyCon
820 -- Support String as an argument or result from a .NET FFI call.
821 isFFIDotnetObjTy ty =
823 (_, t_ty) = tcSplitForAllTys ty
825 case tcSplitTyConApp_maybe (repType t_ty) of
826 Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
829 toDNType :: Type -> DNType
831 | isStringTy ty = DNString
832 | isFFIDotnetObjTy ty = DNObject
833 | Just (tc,argTys) <- tcSplitTyConApp_maybe ty =
834 case lookup (getUnique tc) dn_assoc of
837 | tc `hasKey` ioTyConKey -> toDNType (head argTys)
838 | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
840 dn_assoc :: [ (Unique, DNType) ]
841 dn_assoc = [ (unitTyConKey, DNUnit)
842 , (intTyConKey, DNInt)
843 , (int8TyConKey, DNInt8)
844 , (int16TyConKey, DNInt16)
845 , (int32TyConKey, DNInt32)
846 , (int64TyConKey, DNInt64)
847 , (wordTyConKey, DNInt)
848 , (word8TyConKey, DNWord8)
849 , (word16TyConKey, DNWord16)
850 , (word32TyConKey, DNWord32)
851 , (word64TyConKey, DNWord64)
852 , (floatTyConKey, DNFloat)
853 , (doubleTyConKey, DNDouble)
854 , (addrTyConKey, DNPtr)
855 , (ptrTyConKey, DNPtr)
856 , (funPtrTyConKey, DNPtr)
857 , (charTyConKey, DNChar)
858 , (boolTyConKey, DNBool)
861 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
862 -- Look through newtypes
863 -- Non-recursive ones are transparent to splitTyConApp,
864 -- but recursive ones aren't
865 checkRepTyCon check_tc ty
866 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
869 checkRepTyConKey :: [Unique] -> Type -> Bool
870 -- Like checkRepTyCon, but just looks at the TyCon key
871 checkRepTyConKey keys
872 = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
875 ----------------------------------------------
876 These chaps do the work; they are not exported
877 ----------------------------------------------
880 legalFEArgTyCon :: TyCon -> Bool
881 -- It's illegal to return foreign objects and (mutable)
882 -- bytearrays from a _ccall_ / foreign declaration
883 -- (or be passed them as arguments in foreign exported functions).
885 | isByteArrayLikeTyCon tc
887 -- It's also illegal to make foreign exports that take unboxed
888 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
890 = boxedMarshalableTyCon tc
892 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
893 legalFIResultTyCon dflags tc
894 | isByteArrayLikeTyCon tc = False
895 | tc == unitTyCon = True
896 | otherwise = marshalableTyCon dflags tc
898 legalFEResultTyCon :: TyCon -> Bool
899 legalFEResultTyCon tc
900 | isByteArrayLikeTyCon tc = False
901 | tc == unitTyCon = True
902 | otherwise = boxedMarshalableTyCon tc
904 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
905 -- Checks validity of types going from Haskell -> external world
906 legalOutgoingTyCon dflags safety tc
907 | playSafe safety && isByteArrayLikeTyCon tc
910 = marshalableTyCon dflags tc
912 marshalableTyCon dflags tc
913 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
914 || boxedMarshalableTyCon tc
916 boxedMarshalableTyCon tc
917 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
918 , int32TyConKey, int64TyConKey
919 , wordTyConKey, word8TyConKey, word16TyConKey
920 , word32TyConKey, word64TyConKey
921 , floatTyConKey, doubleTyConKey
922 , addrTyConKey, ptrTyConKey, funPtrTyConKey
925 , byteArrayTyConKey, mutableByteArrayTyConKey
929 isByteArrayLikeTyCon :: TyCon -> Bool
930 isByteArrayLikeTyCon tc =
931 getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
935 %************************************************************************
937 \subsection{Unification with an explicit substitution}
939 %************************************************************************
941 Unify types with an explicit substitution and no monad.
942 Ignore usage annotations.
946 = (TyVarSet, -- Set of template tyvars
947 TyVarSubstEnv) -- Not necessarily idempotent
949 unifyTysX :: TyVarSet -- Template tyvars
952 -> Maybe TyVarSubstEnv
953 unifyTysX tmpl_tyvars ty1 ty2
954 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
956 unifyExtendTysX :: TyVarSet -- Template tyvars
957 -> TyVarSubstEnv -- Substitution to start with
960 -> Maybe TyVarSubstEnv -- Extended substitution
961 unifyExtendTysX tmpl_tyvars subst ty1 ty2
962 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
964 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
965 -> Maybe TyVarSubstEnv
966 unifyTyListsX tmpl_tyvars tys1 tys2
967 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
972 -> (MySubst -> Maybe result)
976 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
977 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
979 -- Variables; go for uVar
980 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
983 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
984 | tyvar1 `elemVarSet` tmpls
985 = uVarX tyvar1 ty2 k subst
986 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
987 | tyvar2 `elemVarSet` tmpls
988 = uVarX tyvar2 ty1 k subst
991 uTysX (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) k subst
992 | n1 == n2 = uTysX t1 t2 k subst
993 uTysX (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) k subst
994 | c1 == c2 = uTyListsX tys1 tys2 k subst
996 -- Functions; just check the two parts
997 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
998 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
1000 -- Type constructors must match
1001 uTysX (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) k subst
1002 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
1003 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
1004 | (con1 == con2 && equalLength tys1 tys2)
1005 = uTyListsX tys1 tys2 k subst
1007 -- Applications need a bit of care!
1008 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1009 -- NB: we've already dealt with type variables and Notes,
1010 -- so if one type is an App the other one jolly well better be too
1011 uTysX (AppTy s1 t1) ty2 k subst
1012 = case tcSplitAppTy_maybe ty2 of
1013 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1014 Nothing -> Nothing -- Fail
1016 uTysX ty1 (AppTy s2 t2) k subst
1017 = case tcSplitAppTy_maybe ty1 of
1018 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1019 Nothing -> Nothing -- Fail
1021 -- Not expecting for-alls in unification
1023 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
1024 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1027 -- Anything else fails
1028 uTysX ty1 ty2 k subst = Nothing
1031 uTyListsX [] [] k subst = k subst
1032 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1033 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1037 -- Invariant: tv1 is a unifiable variable
1038 uVarX tv1 ty2 k subst@(tmpls, env)
1039 = case lookupSubstEnv env tv1 of
1040 Just (DoneTy ty1) -> -- Already bound
1041 uTysX ty1 ty2 k subst
1043 Nothing -- Not already bound
1044 | typeKind ty2 == tyVarKind tv1
1045 && occur_check_ok ty2
1046 -> -- No kind mismatch nor occur check
1047 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1049 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1051 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1052 occur_check_ok_tv tv | tv1 == tv = False
1053 | otherwise = case lookupSubstEnv env tv of
1055 Just (DoneTy ty) -> occur_check_ok ty
1060 %************************************************************************
1062 \subsection{Matching on types}
1064 %************************************************************************
1066 Matching is a {\em unidirectional} process, matching a type against a
1067 template (which is just a type with type variables in it). The
1068 matcher assumes that there are no repeated type variables in the
1069 template, so that it simply returns a mapping of type variables to
1070 types. It also fails on nested foralls.
1072 @matchTys@ matches corresponding elements of a list of templates and
1073 types. It and @matchTy@ both ignore usage annotations, unlike the
1074 main function @match@.
1077 matchTy :: TyVarSet -- Template tyvars
1079 -> Type -- Proposed instance of template
1080 -> Maybe TyVarSubstEnv -- Matching substitution
1083 matchTys :: TyVarSet -- Template tyvars
1084 -> [Type] -- Templates
1085 -> [Type] -- Proposed instance of template
1086 -> Maybe (TyVarSubstEnv, -- Matching substitution
1087 [Type]) -- Left over instance types
1089 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1091 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1092 (\ (senv,tys) -> Just (senv,tys))
1096 @match@ is the main function. It takes a flag indicating whether
1097 usage annotations are to be respected.
1100 match :: Type -> Type -- Current match pair
1101 -> TyVarSet -- Template vars
1102 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1103 -> TyVarSubstEnv -- Current subst
1106 -- When matching against a type variable, see if the variable
1107 -- has already been bound. If so, check that what it's bound to
1108 -- is the same as ty; if not, bind it and carry on.
1110 match (TyVarTy v) ty tmpls k senv
1111 | v `elemVarSet` tmpls
1112 = -- v is a template variable
1113 case lookupSubstEnv senv v of
1114 Nothing | typeKind ty == tyVarKind v
1115 -- We do a kind check, just as in the uVarX above
1116 -- The kind check is needed to avoid bogus matches
1117 -- of (a b) with (c d), where the kinds don't match
1118 -- An occur check isn't needed when matching.
1119 -> k (extendSubstEnv senv v (DoneTy ty))
1121 | otherwise -> Nothing -- Fails
1123 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1124 | otherwise -> Nothing -- Fails
1127 = -- v is not a template variable; ty had better match
1128 -- Can't use (==) because types differ
1129 case tcGetTyVar_maybe ty of
1130 Just v' | v == v' -> k senv -- Success
1131 other -> Nothing -- Failure
1132 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1133 -- I guess the reason the Note-stripping case is *last* rather than first
1134 -- is to preserve type synonyms etc., so I'm not moving it to the
1135 -- top; but this means that (without the deNotetype) a type
1136 -- variable may not match the pattern (TyVarTy v') as one would
1137 -- expect, due to an intervening Note. KSW 2000-06.
1140 match (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) tmpls k senv
1141 | n1 == n2 = match t1 t2 tmpls k senv
1142 match (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) tmpls k senv
1143 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1145 -- Functions; just check the two parts
1146 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1147 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1149 match (AppTy fun1 arg1) ty2 tmpls k senv
1150 = case tcSplitAppTy_maybe ty2 of
1151 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1152 Nothing -> Nothing -- Fail
1154 -- Newtypes are opaque; predicate types should not happen
1155 match (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) tmpls k senv
1156 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1157 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1158 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1160 -- With type synonyms, we have to be careful for the exact
1161 -- same reasons as in the unifier. Please see the
1162 -- considerable commentary there before changing anything
1163 -- here! (WDP 95/05)
1164 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1165 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1168 match _ _ _ _ _ = Nothing
1170 match_list_exactly tys1 tys2 tmpls k senv
1171 = match_list tys1 tys2 tmpls k' senv
1173 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1174 | otherwise = Nothing -- Fail
1176 match_list [] tys2 tmpls k senv = k (senv, tys2)
1177 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1178 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1179 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv