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
76 isFFITy, -- :: Type -> Bool
78 toDNType, -- :: Type -> DNType
80 ---------------------------------
81 -- Unifier and matcher
82 unifyTysX, unifyTyListsX, unifyExtendTysX,
83 matchTy, matchTys, match,
85 --------------------------------
86 -- Rexported from Type
87 Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
88 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
89 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
90 isArgTypeKind, isSubKind, defaultKind,
92 Type, PredType(..), ThetaType,
93 mkForAllTy, mkForAllTys,
94 mkFunTy, mkFunTys, zipFunTys,
95 mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
96 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
98 isUnLiftedType, -- Source types are always lifted
99 isUnboxedTupleType, -- Ditto
102 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
103 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
106 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
108 pprKind, pprParendKind,
109 pprType, pprParendType,
110 pprPred, pprTheta, pprThetaArrow, pprClassPred
114 #include "HsVersions.h"
117 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
119 import Type ( -- Re-exports
120 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
121 tyVarsOfTheta, Kind, Type, PredType(..),
122 ThetaType, unliftedTypeKind,
123 liftedTypeKind, openTypeKind, mkArrowKind,
124 isLiftedTypeKind, isUnliftedTypeKind,
126 mkArrowKinds, mkForAllTy, mkForAllTys,
127 defaultKind, isArgTypeKind, isOpenTypeKind,
128 mkFunTy, mkFunTys, zipFunTys,
129 mkTyConApp, mkGenTyConApp, mkAppTy,
130 mkAppTys, mkSynTy, applyTy, applyTys,
131 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
132 mkPredTys, isUnLiftedType,
133 isUnboxedTupleType, isPrimitiveType,
135 tidyTopType, tidyType, tidyPred, tidyTypes,
136 tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
137 tidyTyVarBndr, tidyOpenTyVar,
141 pprKind, pprParendKind,
142 pprType, pprParendType,
143 pprPred, pprTheta, pprThetaArrow, pprClassPred
145 import TyCon ( TyCon, isUnLiftedTyCon, tyConUnique )
146 import Class ( Class )
147 import Var ( TyVar, tyVarKind, tcTyVarDetails )
148 import ForeignCall ( Safety, playSafe, DNType(..) )
153 import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
154 import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
156 import OccName ( OccName, mkDictOcc )
157 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
158 import TysWiredIn ( unitTyCon, charTyCon, listTyCon )
159 import BasicTypes ( IPName(..), ipNameName )
160 import Unique ( Unique, Uniquable(..) )
161 import SrcLoc ( SrcLoc )
162 import Util ( cmpList, thenCmp, equalLength, snocView )
163 import Maybes ( maybeToBool, expectJust )
168 %************************************************************************
172 %************************************************************************
174 The type checker divides the generic Type world into the
175 following more structured beasts:
177 sigma ::= forall tyvars. phi
178 -- A sigma type is a qualified type
180 -- Note that even if 'tyvars' is empty, theta
181 -- may not be: e.g. (?x::Int) => Int
183 -- Note that 'sigma' is in prenex form:
184 -- all the foralls are at the front.
185 -- A 'phi' type has no foralls to the right of
193 -- A 'tau' type has no quantification anywhere
194 -- Note that the args of a type constructor must be taus
196 | tycon tau_1 .. tau_n
200 -- In all cases, a (saturated) type synonym application is legal,
201 -- provided it expands to the required form.
204 type TcType = Type -- A TcType can have mutable type variables
205 -- Invariant on ForAllTy in TcTypes:
207 -- a cannot occur inside a MutTyVar in T; that is,
208 -- T is "flattened" before quantifying over a
210 type TcPredType = PredType
211 type TcThetaType = ThetaType
212 type TcSigmaType = TcType
213 type TcRhoType = TcType
214 type TcTauType = TcType
220 %************************************************************************
222 \subsection{TyVarDetails}
224 %************************************************************************
226 TyVarDetails gives extra info about type variables, used during type
227 checking. It's attached to mutable type variables only.
228 It's knot-tied back to Var.lhs. There is no reason in principle
229 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
232 type TcTyVar = TyVar -- Used only during type inference
235 = SigTv -- Introduced when instantiating a type signature,
236 -- prior to checking that the defn of a fn does
237 -- 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
249 -- type signature \ x::a -> e
251 | VanillaTv -- Everything else
253 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
254 isUserTyVar tv = case tcTyVarDetails tv of
258 isSkolemTyVar :: TcTyVar -> Bool
259 isSkolemTyVar tv = case tcTyVarDetails tv of
265 tyVarBindingInfo :: TcTyVar -> SDoc -- Used in checkSigTyVars
267 = sep [ptext SLIT("is bound by the") <+> details (tcTyVarDetails tv),
268 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
270 details SigTv = ptext SLIT("type signature")
271 details ClsTv = ptext SLIT("class declaration")
272 details InstTv = ptext SLIT("instance declaration")
273 details PatSigTv = ptext SLIT("pattern type signature")
274 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
278 type TcTyVarSet = TyVarSet
281 %************************************************************************
283 \subsection{Tau, sigma and rho}
285 %************************************************************************
288 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
290 mkPhiTy :: [PredType] -> Type -> Type
291 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
294 @isTauTy@ tests for nested for-alls.
297 isTauTy :: Type -> Bool
298 isTauTy (TyVarTy v) = True
299 isTauTy (TyConApp _ tys) = all isTauTy tys
300 isTauTy (NewTcApp _ tys) = all isTauTy tys
301 isTauTy (AppTy a b) = isTauTy a && isTauTy b
302 isTauTy (FunTy a b) = isTauTy a && isTauTy b
303 isTauTy (PredTy p) = True -- Don't look through source types
304 isTauTy (NoteTy _ ty) = isTauTy ty
305 isTauTy other = False
309 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
310 -- construct a dictionary function name
311 getDFunTyKey (TyVarTy tv) = getOccName tv
312 getDFunTyKey (TyConApp tc _) = getOccName tc
313 getDFunTyKey (NewTcApp tc _) = getOccName tc
314 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
315 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
316 getDFunTyKey (FunTy arg _) = getOccName funTyCon
317 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
318 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
319 -- PredTy shouldn't happen
323 %************************************************************************
325 \subsection{Expanding and splitting}
327 %************************************************************************
329 These tcSplit functions are like their non-Tc analogues, but
330 a) they do not look through newtypes
331 b) they do not look through PredTys
332 c) [future] they ignore usage-type annotations
334 However, they are non-monadic and do not follow through mutable type
335 variables. It's up to you to make sure this doesn't matter.
338 tcSplitForAllTys :: Type -> ([TyVar], Type)
339 tcSplitForAllTys ty = split ty ty []
341 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
342 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
343 split orig_ty t tvs = (reverse tvs, orig_ty)
345 tcIsForAllTy (ForAllTy tv ty) = True
346 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
347 tcIsForAllTy t = False
349 tcSplitPhiTy :: Type -> ([PredType], Type)
350 tcSplitPhiTy ty = split ty ty []
352 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
353 Just p -> split res res (p:ts)
354 Nothing -> (reverse ts, orig_ty)
355 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
356 split orig_ty ty ts = (reverse ts, orig_ty)
358 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
359 (tvs, rho) -> case tcSplitPhiTy rho of
360 (theta, tau) -> (tvs, theta, tau)
362 tcTyConAppTyCon :: Type -> TyCon
363 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
365 tcTyConAppArgs :: Type -> [Type]
366 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
368 tcSplitTyConApp :: Type -> (TyCon, [Type])
369 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
371 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
373 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
374 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
375 tcSplitTyConApp_maybe (NewTcApp tc tys) = Just (tc, tys)
376 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
377 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
378 -- Newtypes are opaque, so they may be split
379 -- However, predicates are not treated
380 -- as tycon applications by the type checker
381 tcSplitTyConApp_maybe other = Nothing
383 tcSplitFunTys :: Type -> ([Type], Type)
384 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
386 Just (arg,res) -> (arg:args, res')
388 (args,res') = tcSplitFunTys res
390 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
391 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
392 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
393 tcSplitFunTy_maybe other = Nothing
395 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
396 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
399 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
400 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
401 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
402 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
403 tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
404 Just (tys', ty') -> Just (TyConApp tc tys', ty')
406 tcSplitAppTy_maybe (NewTcApp tc tys) = case snocView tys of
407 Just (tys', ty') -> Just (NewTcApp tc tys', ty')
409 tcSplitAppTy_maybe other = Nothing
411 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
413 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
415 tcSplitAppTys :: Type -> (Type, [Type])
419 go ty args = case tcSplitAppTy_maybe ty of
420 Just (ty', arg) -> go ty' (arg:args)
423 tcGetTyVar_maybe :: Type -> Maybe TyVar
424 tcGetTyVar_maybe (TyVarTy tv) = Just tv
425 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
426 tcGetTyVar_maybe other = Nothing
428 tcGetTyVar :: String -> Type -> TyVar
429 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
431 tcIsTyVarTy :: Type -> Bool
432 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
435 The type of a method for class C is always of the form:
436 Forall a1..an. C a1..an => sig_ty
437 where sig_ty is the type given by the method's signature, and thus in general
438 is a ForallTy. At the point that splitMethodTy is called, it is expected
439 that the outer Forall has already been stripped off. splitMethodTy then
440 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off.
443 tcSplitMethodTy :: Type -> (PredType, Type)
444 tcSplitMethodTy ty = split ty
446 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
448 Nothing -> panic "splitMethodTy"
449 split (NoteTy n ty) = split ty
450 split _ = panic "splitMethodTy"
452 tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
453 -- Split the type of a dictionary function
455 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
456 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
457 (tvs, theta, clas, tys) }}
460 (allDistinctTyVars tys tvs) = True
462 all the types tys are type variables,
463 distinct from each other and from tvs.
465 This is useful when checking that unification hasn't unified signature
466 type variables. For example, if the type sig is
467 f :: forall a b. a -> b -> b
468 we want to check that 'a' and 'b' havn't
469 (a) been unified with a non-tyvar type
470 (b) been unified with each other (all distinct)
471 (c) been unified with a variable free in the environment
474 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
476 allDistinctTyVars [] acc
478 allDistinctTyVars (ty:tys) acc
479 = case tcGetTyVar_maybe ty of
480 Nothing -> False -- (a)
481 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
482 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
486 %************************************************************************
488 \subsection{Predicate types}
490 %************************************************************************
493 tcSplitPredTy_maybe :: Type -> Maybe PredType
494 -- Returns Just for predicates only
495 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
496 tcSplitPredTy_maybe (PredTy p) = Just p
497 tcSplitPredTy_maybe other = Nothing
499 predTyUnique :: PredType -> Unique
500 predTyUnique (IParam n _) = getUnique (ipNameName n)
501 predTyUnique (ClassP clas tys) = getUnique clas
503 mkPredName :: Unique -> SrcLoc -> PredType -> Name
504 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
505 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
509 --------------------- Dictionary types ---------------------------------
512 mkClassPred clas tys = ClassP clas tys
514 isClassPred :: PredType -> Bool
515 isClassPred (ClassP clas tys) = True
516 isClassPred other = False
518 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
519 isTyVarClassPred other = False
521 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
522 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
523 getClassPredTys_maybe _ = Nothing
525 getClassPredTys :: PredType -> (Class, [Type])
526 getClassPredTys (ClassP clas tys) = (clas, tys)
528 mkDictTy :: Class -> [Type] -> Type
529 mkDictTy clas tys = mkPredTy (ClassP clas tys)
531 isDictTy :: Type -> Bool
532 isDictTy (PredTy p) = isClassPred p
533 isDictTy (NoteTy _ ty) = isDictTy ty
534 isDictTy other = False
537 --------------------- Implicit parameters ---------------------------------
540 isIPPred :: PredType -> Bool
541 isIPPred (IParam _ _) = True
542 isIPPred other = False
544 isInheritablePred :: PredType -> Bool
545 -- Can be inherited by a context. For example, consider
546 -- f x = let g y = (?v, y+x)
547 -- in (g 3 with ?v = 8,
549 -- The point is that g's type must be quantifed over ?v:
550 -- g :: (?v :: a) => a -> a
551 -- but it doesn't need to be quantified over the Num a dictionary
552 -- which can be free in g's rhs, and shared by both calls to g
553 isInheritablePred (ClassP _ _) = True
554 isInheritablePred other = False
556 isLinearPred :: TcPredType -> Bool
557 isLinearPred (IParam (Linear n) _) = True
558 isLinearPred other = False
562 %************************************************************************
564 \subsection{Comparison}
566 %************************************************************************
568 Comparison, taking note of newtypes, predicates, etc,
571 tcEqType :: Type -> Type -> Bool
572 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
574 tcEqTypes :: [Type] -> [Type] -> Bool
575 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
577 tcEqPred :: PredType -> PredType -> Bool
578 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
581 tcCmpType :: Type -> Type -> Ordering
582 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
584 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
586 tcCmpPred p1 p2 = cmpPredTy emptyVarEnv p1 p2
588 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
591 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
592 -- The "env" maps type variables in ty1 to type variables in ty2
593 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
594 -- we in effect substitute tv2 for tv1 in t1 before continuing
596 -- Look through NoteTy
597 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
598 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
600 -- Deal with equal constructors
601 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
602 Just tv1a -> tv1a `compare` tv2
603 Nothing -> tv1 `compare` tv2
605 cmpTy env (PredTy p1) (PredTy p2) = cmpPredTy env p1 p2
606 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
607 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
608 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
609 cmpTy env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
610 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
612 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < NewTcApp < ForAllTy < PredTy
613 cmpTy env (AppTy _ _) (TyVarTy _) = GT
615 cmpTy env (FunTy _ _) (TyVarTy _) = GT
616 cmpTy env (FunTy _ _) (AppTy _ _) = GT
618 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
619 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
620 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
622 cmpTy env (NewTcApp _ _) (TyVarTy _) = GT
623 cmpTy env (NewTcApp _ _) (AppTy _ _) = GT
624 cmpTy env (NewTcApp _ _) (FunTy _ _) = GT
625 cmpTy env (NewTcApp _ _) (TyConApp _ _) = GT
627 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
628 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
629 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
630 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
631 cmpTy env (ForAllTy _ _) (NewTcApp _ _) = GT
633 cmpTy env (PredTy _) t2 = GT
639 cmpPredTy :: TyVarEnv TyVar -> PredType -> PredType -> Ordering
640 cmpPredTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
641 -- Compare types as well as names for implicit parameters
642 -- This comparison is used exclusively (I think) for the
643 -- finite map built in TcSimplify
644 cmpPredTy env (IParam _ _) (ClassP _ _) = LT
645 cmpPredTy env (ClassP _ _) (IParam _ _) = GT
646 cmpPredTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
649 PredTypes are used as a FM key in TcSimplify,
650 so we take the easy path and make them an instance of Ord
653 instance Eq PredType where { (==) = tcEqPred }
654 instance Ord PredType where { compare = tcCmpPred }
658 %************************************************************************
660 \subsection{Predicates}
662 %************************************************************************
664 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
666 f :: (?x::Int) => Int -> Int
669 isSigmaTy :: Type -> Bool
670 isSigmaTy (ForAllTy tyvar ty) = True
671 isSigmaTy (FunTy a b) = isPredTy a
672 isSigmaTy (NoteTy n ty) = isSigmaTy ty
675 isOverloadedTy :: Type -> Bool
676 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
677 isOverloadedTy (FunTy a b) = isPredTy a
678 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
679 isOverloadedTy _ = False
681 isPredTy :: Type -> Bool -- Belongs in TcType because it does
682 -- not look through newtypes, or predtypes (of course)
683 isPredTy (NoteTy _ ty) = isPredTy ty
684 isPredTy (PredTy sty) = True
689 isFloatTy = is_tc floatTyConKey
690 isDoubleTy = is_tc doubleTyConKey
691 isIntegerTy = is_tc integerTyConKey
692 isIntTy = is_tc intTyConKey
693 isAddrTy = is_tc addrTyConKey
694 isBoolTy = is_tc boolTyConKey
695 isUnitTy = is_tc unitTyConKey
697 is_tc :: Unique -> Type -> Bool
698 -- Newtypes are opaque to this
699 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
700 Just (tc, _) -> uniq == getUnique tc
705 %************************************************************************
709 %************************************************************************
712 deNoteType :: Type -> Type
713 -- Remove synonyms, but not predicate types
714 deNoteType ty@(TyVarTy tyvar) = ty
715 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
716 deNoteType (NewTcApp tycon tys) = NewTcApp tycon (map deNoteType tys)
717 deNoteType (PredTy p) = PredTy (deNotePredType p)
718 deNoteType (NoteTy _ ty) = deNoteType ty
719 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
720 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
721 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
723 deNotePredType :: PredType -> PredType
724 deNotePredType (ClassP c tys) = ClassP c (map deNoteType tys)
725 deNotePredType (IParam n ty) = IParam n (deNoteType ty)
728 Find the free tycons and classes of a type. This is used in the front
732 tyClsNamesOfType :: Type -> NameSet
733 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
734 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
735 tyClsNamesOfType (NewTcApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
736 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
737 tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
738 tyClsNamesOfType (PredTy (IParam n ty)) = tyClsNamesOfType ty
739 tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
740 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
741 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
742 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
744 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
746 tyClsNamesOfDFunHead :: Type -> NameSet
747 -- Find the free type constructors and classes
748 -- of the head of the dfun instance type
749 -- The 'dfun_head_type' is because of
750 -- instance Foo a => Baz T where ...
751 -- The decl is an orphan if Baz and T are both not locally defined,
752 -- even if Foo *is* locally defined
753 tyClsNamesOfDFunHead dfun_ty
754 = case tcSplitSigmaTy dfun_ty of
755 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
757 classesOfTheta :: ThetaType -> [Class]
758 -- Looks just for ClassP things; maybe it should check
759 classesOfTheta preds = [ c | ClassP c _ <- preds ]
763 %************************************************************************
765 \subsection[TysWiredIn-ext-type]{External types}
767 %************************************************************************
769 The compiler's foreign function interface supports the passing of a
770 restricted set of types as arguments and results (the restricting factor
774 isFFITy :: Type -> Bool
775 -- True for any TyCon that can possibly be an arg or result of an FFI call
776 isFFITy ty = checkRepTyCon legalFFITyCon ty
778 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
779 -- Checks for valid argument type for a 'foreign import'
780 isFFIArgumentTy dflags safety ty
781 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
783 isFFIExternalTy :: Type -> Bool
784 -- Types that are allowed as arguments of a 'foreign export'
785 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
787 isFFIImportResultTy :: DynFlags -> Type -> Bool
788 isFFIImportResultTy dflags ty
789 = checkRepTyCon (legalFIResultTyCon dflags) ty
791 isFFIExportResultTy :: Type -> Bool
792 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
794 isFFIDynArgumentTy :: Type -> Bool
795 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
796 -- or a newtype of either.
797 isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
799 isFFIDynResultTy :: Type -> Bool
800 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
801 -- or a newtype of either.
802 isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
804 isFFILabelTy :: Type -> Bool
805 -- The type of a foreign label must be Ptr, FunPtr, Addr,
806 -- or a newtype of either.
807 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
809 isFFIDotnetTy :: DynFlags -> Type -> Bool
810 isFFIDotnetTy dflags ty
811 = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
812 (legalFIResultTyCon dflags tc ||
813 isFFIDotnetObjTy ty || isStringTy ty)) ty
815 -- Support String as an argument or result from a .NET FFI call.
817 case tcSplitTyConApp_maybe (repType ty) of
820 case tcSplitTyConApp_maybe (repType arg_ty) of
821 Just (cc,[]) -> cc == charTyCon
825 -- Support String as an argument or result from a .NET FFI call.
826 isFFIDotnetObjTy ty =
828 (_, t_ty) = tcSplitForAllTys ty
830 case tcSplitTyConApp_maybe (repType t_ty) of
831 Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
834 toDNType :: Type -> DNType
836 | isStringTy ty = DNString
837 | isFFIDotnetObjTy ty = DNObject
838 | Just (tc,argTys) <- tcSplitTyConApp_maybe ty =
839 case lookup (getUnique tc) dn_assoc of
842 | tc `hasKey` ioTyConKey -> toDNType (head argTys)
843 | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
845 dn_assoc :: [ (Unique, DNType) ]
846 dn_assoc = [ (unitTyConKey, DNUnit)
847 , (intTyConKey, DNInt)
848 , (int8TyConKey, DNInt8)
849 , (int16TyConKey, DNInt16)
850 , (int32TyConKey, DNInt32)
851 , (int64TyConKey, DNInt64)
852 , (wordTyConKey, DNInt)
853 , (word8TyConKey, DNWord8)
854 , (word16TyConKey, DNWord16)
855 , (word32TyConKey, DNWord32)
856 , (word64TyConKey, DNWord64)
857 , (floatTyConKey, DNFloat)
858 , (doubleTyConKey, DNDouble)
859 , (addrTyConKey, DNPtr)
860 , (ptrTyConKey, DNPtr)
861 , (funPtrTyConKey, DNPtr)
862 , (charTyConKey, DNChar)
863 , (boolTyConKey, DNBool)
866 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
867 -- Look through newtypes
868 -- Non-recursive ones are transparent to splitTyConApp,
869 -- but recursive ones aren't. Manuel had:
870 -- newtype T = MkT (Ptr T)
871 -- and wanted it to work...
872 checkRepTyCon check_tc ty
873 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
876 checkRepTyConKey :: [Unique] -> Type -> Bool
877 -- Like checkRepTyCon, but just looks at the TyCon key
878 checkRepTyConKey keys
879 = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
882 ----------------------------------------------
883 These chaps do the work; they are not exported
884 ----------------------------------------------
887 legalFEArgTyCon :: TyCon -> Bool
888 -- It's illegal to return foreign objects and (mutable)
889 -- bytearrays from a _ccall_ / foreign declaration
890 -- (or be passed them as arguments in foreign exported functions).
892 | isByteArrayLikeTyCon tc
894 -- It's also illegal to make foreign exports that take unboxed
895 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
897 = boxedMarshalableTyCon tc
899 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
900 legalFIResultTyCon dflags tc
901 | isByteArrayLikeTyCon tc = False
902 | tc == unitTyCon = True
903 | otherwise = marshalableTyCon dflags tc
905 legalFEResultTyCon :: TyCon -> Bool
906 legalFEResultTyCon tc
907 | isByteArrayLikeTyCon tc = False
908 | tc == unitTyCon = True
909 | otherwise = boxedMarshalableTyCon tc
911 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
912 -- Checks validity of types going from Haskell -> external world
913 legalOutgoingTyCon dflags safety tc
914 | playSafe safety && isByteArrayLikeTyCon tc
917 = marshalableTyCon dflags tc
919 legalFFITyCon :: TyCon -> Bool
920 -- True for any TyCon that can possibly be an arg or result of an FFI call
922 = isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon
924 marshalableTyCon dflags tc
925 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
926 || boxedMarshalableTyCon tc
928 boxedMarshalableTyCon tc
929 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
930 , int32TyConKey, int64TyConKey
931 , wordTyConKey, word8TyConKey, word16TyConKey
932 , word32TyConKey, word64TyConKey
933 , floatTyConKey, doubleTyConKey
934 , addrTyConKey, ptrTyConKey, funPtrTyConKey
937 , byteArrayTyConKey, mutableByteArrayTyConKey
941 isByteArrayLikeTyCon :: TyCon -> Bool
942 isByteArrayLikeTyCon tc =
943 getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
947 %************************************************************************
949 \subsection{Unification with an explicit substitution}
951 %************************************************************************
953 Unify types with an explicit substitution and no monad.
954 Ignore usage annotations.
958 = (TyVarSet, -- Set of template tyvars
959 TyVarSubstEnv) -- Not necessarily idempotent
961 unifyTysX :: TyVarSet -- Template tyvars
964 -> Maybe TyVarSubstEnv
965 unifyTysX tmpl_tyvars ty1 ty2
966 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
968 unifyExtendTysX :: TyVarSet -- Template tyvars
969 -> TyVarSubstEnv -- Substitution to start with
972 -> Maybe TyVarSubstEnv -- Extended substitution
973 unifyExtendTysX tmpl_tyvars subst ty1 ty2
974 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
976 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
977 -> Maybe TyVarSubstEnv
978 unifyTyListsX tmpl_tyvars tys1 tys2
979 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
984 -> (MySubst -> Maybe result)
988 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
989 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
991 -- Variables; go for uVar
992 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
995 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
996 | tyvar1 `elemVarSet` tmpls
997 = uVarX tyvar1 ty2 k subst
998 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
999 | tyvar2 `elemVarSet` tmpls
1000 = uVarX tyvar2 ty1 k subst
1003 uTysX (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) k subst
1004 | n1 == n2 = uTysX t1 t2 k subst
1005 uTysX (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) k subst
1006 | c1 == c2 = uTyListsX tys1 tys2 k subst
1008 -- Functions; just check the two parts
1009 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
1010 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
1012 -- Type constructors must match
1013 uTysX (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) k subst
1014 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
1015 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
1016 | (con1 == con2 && equalLength tys1 tys2)
1017 = uTyListsX tys1 tys2 k subst
1019 -- Applications need a bit of care!
1020 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1021 -- NB: we've already dealt with type variables and Notes,
1022 -- so if one type is an App the other one jolly well better be too
1023 uTysX (AppTy s1 t1) ty2 k subst
1024 = case tcSplitAppTy_maybe ty2 of
1025 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1026 Nothing -> Nothing -- Fail
1028 uTysX ty1 (AppTy s2 t2) k subst
1029 = case tcSplitAppTy_maybe ty1 of
1030 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1031 Nothing -> Nothing -- Fail
1033 -- Not expecting for-alls in unification
1035 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
1036 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1039 -- Anything else fails
1040 uTysX ty1 ty2 k subst = Nothing
1043 uTyListsX [] [] k subst = k subst
1044 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1045 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1049 -- Invariant: tv1 is a unifiable variable
1050 uVarX tv1 ty2 k subst@(tmpls, env)
1051 = case lookupSubstEnv env tv1 of
1052 Just (DoneTy ty1) -> -- Already bound
1053 uTysX ty1 ty2 k subst
1055 Nothing -- Not already bound
1056 | typeKind ty2 == tyVarKind tv1
1057 && occur_check_ok ty2
1058 -> -- No kind mismatch nor occur check
1059 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1061 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1063 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1064 occur_check_ok_tv tv | tv1 == tv = False
1065 | otherwise = case lookupSubstEnv env tv of
1067 Just (DoneTy ty) -> occur_check_ok ty
1072 %************************************************************************
1074 \subsection{Matching on types}
1076 %************************************************************************
1078 Matching is a {\em unidirectional} process, matching a type against a
1079 template (which is just a type with type variables in it). The
1080 matcher assumes that there are no repeated type variables in the
1081 template, so that it simply returns a mapping of type variables to
1082 types. It also fails on nested foralls.
1084 @matchTys@ matches corresponding elements of a list of templates and
1085 types. It and @matchTy@ both ignore usage annotations, unlike the
1086 main function @match@.
1089 matchTy :: TyVarSet -- Template tyvars
1091 -> Type -- Proposed instance of template
1092 -> Maybe TyVarSubstEnv -- Matching substitution
1095 matchTys :: TyVarSet -- Template tyvars
1096 -> [Type] -- Templates
1097 -> [Type] -- Proposed instance of template
1098 -> Maybe (TyVarSubstEnv, -- Matching substitution
1099 [Type]) -- Left over instance types
1101 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1103 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1104 (\ (senv,tys) -> Just (senv,tys))
1108 @match@ is the main function. It takes a flag indicating whether
1109 usage annotations are to be respected.
1112 match :: Type -> Type -- Current match pair
1113 -> TyVarSet -- Template vars
1114 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1115 -> TyVarSubstEnv -- Current subst
1118 -- When matching against a type variable, see if the variable
1119 -- has already been bound. If so, check that what it's bound to
1120 -- is the same as ty; if not, bind it and carry on.
1122 match (TyVarTy v) ty tmpls k senv
1123 | v `elemVarSet` tmpls
1124 = -- v is a template variable
1125 case lookupSubstEnv senv v of
1126 Nothing | typeKind ty `isSubKind` tyVarKind v
1127 -- We do a kind check, just as in the uVarX above
1128 -- The kind check is needed to avoid bogus matches
1129 -- of (a b) with (c d), where the kinds don't match
1130 -- An occur check isn't needed when matching.
1131 -> k (extendSubstEnv senv v (DoneTy ty))
1133 | otherwise -> Nothing -- Fails
1135 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1136 | otherwise -> Nothing -- Fails
1139 = -- v is not a template variable; ty had better match
1140 -- Can't use (==) because types differ
1141 case tcGetTyVar_maybe ty of
1142 Just v' | v == v' -> k senv -- Success
1143 other -> Nothing -- Failure
1144 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1145 -- I guess the reason the Note-stripping case is *last* rather than first
1146 -- is to preserve type synonyms etc., so I'm not moving it to the
1147 -- top; but this means that (without the deNotetype) a type
1148 -- variable may not match the pattern (TyVarTy v') as one would
1149 -- expect, due to an intervening Note. KSW 2000-06.
1152 match (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) tmpls k senv
1153 | n1 == n2 = match t1 t2 tmpls k senv
1154 match (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) tmpls k senv
1155 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1157 -- Functions; just check the two parts
1158 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1159 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1161 -- If the template is an application, try to make the
1162 -- thing we are matching look like an application
1163 match (AppTy fun1 arg1) ty2 tmpls k senv
1164 = case tcSplitAppTy_maybe ty2 of
1165 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1166 Nothing -> Nothing -- Fail
1168 -- Newtypes are opaque; predicate types should not happen
1169 match (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) tmpls k senv
1170 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1171 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1172 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1174 -- With type synonyms, we have to be careful for the exact
1175 -- same reasons as in the unifier. Please see the
1176 -- considerable commentary there before changing anything
1177 -- here! (WDP 95/05)
1178 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1179 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1182 match _ _ _ _ _ = Nothing
1184 match_list_exactly tys1 tys2 tmpls k senv
1185 = match_list tys1 tys2 tmpls k' senv
1187 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1188 | otherwise = Nothing -- Fail
1190 match_list [] tys2 tmpls k senv = k (senv, tys2)
1191 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1192 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1193 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv