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 TyThing(..), -- instance NamedThing
22 --------------------------------
24 TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
25 TcTyVar, TcTyVarSet, TcKind,
27 --------------------------------
29 TyVarDetails(..), isUserTyVar, isSkolemTyVar, isHoleTyVar,
32 --------------------------------
36 --------------------------------
38 -- These are important because they do not look through newtypes
39 tcSplitForAllTys, tcSplitPhiTy,
40 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
41 tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
42 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
43 tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
45 ---------------------------------
47 -- Again, newtypes are opaque
48 tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
49 isSigmaTy, isOverloadedTy,
50 isDoubleTy, isFloatTy, isIntTy,
51 isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
52 isTauTy, tcIsTyVarTy, tcIsForAllTy,
55 ---------------------------------
56 -- Misc type manipulators
57 deNoteType, classNamesOfTheta,
58 tyClsNamesOfType, tyClsNamesOfDFunHead,
61 ---------------------------------
63 getClassPredTys_maybe, getClassPredTys,
64 isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
65 mkDictTy, tcSplitPredTy_maybe,
66 isDictTy, tcSplitDFunTy, predTyUnique,
67 mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
69 ---------------------------------
70 -- Foreign import and export
71 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
72 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
73 isFFIExportResultTy, -- :: Type -> Bool
74 isFFIExternalTy, -- :: Type -> Bool
75 isFFIDynArgumentTy, -- :: Type -> Bool
76 isFFIDynResultTy, -- :: Type -> Bool
77 isFFILabelTy, -- :: Type -> Bool
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,
91 Type, SourceType(..), 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
99 isPrimitiveType, isTyVarTy,
101 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
102 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
105 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
108 #include "HsVersions.h"
111 import {-# SOURCE #-} PprType( pprType )
112 -- PprType imports TcType so that it can print intelligently
115 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
117 import Type ( -- Re-exports
118 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
119 tyVarsOfTheta, Kind, Type, SourceType(..),
120 PredType, ThetaType, unliftedTypeKind,
121 liftedTypeKind, openTypeKind, mkArrowKind,
122 mkArrowKinds, mkForAllTy, mkForAllTys,
123 defaultKind, isTypeKind, isAnyTypeKind,
124 mkFunTy, mkFunTys, zipFunTys, isTyVarTy,
125 mkTyConApp, mkGenTyConApp, mkAppTy,
126 mkAppTys, mkSynTy, applyTy, applyTys,
127 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
128 mkPredTys, isUnLiftedType,
129 isUnboxedTupleType, isPrimitiveType,
130 splitNewType_maybe, splitTyConApp_maybe,
131 tidyTopType, tidyType, tidyPred, tidyTypes,
132 tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
133 tidyTyVarBndr, tidyOpenTyVar,
134 tidyOpenTyVars, eqKind,
135 hasMoreBoxityInfo, liftedBoxity,
136 superBoxity, typeKind, superKind, repType
138 import DataCon ( DataCon )
139 import TyCon ( TyCon, isUnLiftedTyCon )
140 import Class ( classHasFDs, Class )
141 import Var ( TyVar, Id, tyVarKind, isMutTyVar, mutTyVarDetails )
142 import ForeignCall ( Safety, playSafe )
147 import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
148 import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
149 import OccName ( OccName, mkDictOcc )
151 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
152 import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
153 import BasicTypes ( IPName(..), ipNameName )
154 import Unique ( Unique, Uniquable(..) )
155 import SrcLoc ( SrcLoc )
156 import Util ( cmpList, thenCmp, equalLength, snocView )
157 import Maybes ( maybeToBool, expectJust )
162 %************************************************************************
166 %************************************************************************
169 data TyThing = AnId Id
174 instance NamedThing TyThing where
175 getName (AnId id) = getName id
176 getName (ATyCon tc) = getName tc
177 getName (AClass cl) = getName cl
178 getName (ADataCon dc) = getName dc
182 %************************************************************************
186 %************************************************************************
188 The type checker divides the generic Type world into the
189 following more structured beasts:
191 sigma ::= forall tyvars. phi
192 -- A sigma type is a qualified type
194 -- Note that even if 'tyvars' is empty, theta
195 -- may not be: e.g. (?x::Int) => Int
197 -- Note that 'sigma' is in prenex form:
198 -- all the foralls are at the front.
199 -- A 'phi' type has no foralls to the right of
207 -- A 'tau' type has no quantification anywhere
208 -- Note that the args of a type constructor must be taus
210 | tycon tau_1 .. tau_n
214 -- In all cases, a (saturated) type synonym application is legal,
215 -- provided it expands to the required form.
219 type SigmaType = Type
225 type TcTyVar = TyVar -- Might be a mutable tyvar
226 type TcTyVarSet = TyVarSet
228 type TcType = Type -- A TcType can have mutable type variables
229 -- Invariant on ForAllTy in TcTypes:
231 -- a cannot occur inside a MutTyVar in T; that is,
232 -- T is "flattened" before quantifying over a
234 type TcPredType = PredType
235 type TcThetaType = ThetaType
236 type TcSigmaType = TcType
237 type TcRhoType = TcType
238 type TcTauType = TcType
243 %************************************************************************
245 \subsection{TyVarDetails}
247 %************************************************************************
249 TyVarDetails gives extra info about type variables, used during type
250 checking. It's attached to mutable type variables only.
251 It's knot-tied back to Var.lhs. There is no reason in principle
252 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
256 = HoleTv -- Used *only* by the type checker when passing in a type
257 -- variable that should be side-effected to the result type.
258 -- Always has kind openTypeKind.
259 -- Never appears in types
261 | SigTv -- Introduced when instantiating a type signature,
262 -- prior to checking that the defn of a fn does
263 -- have the expected type. Should not be instantiated.
265 -- f :: forall a. a -> a
267 -- When checking e, with expected type (a->a), we
268 -- should not instantiate a
270 | ClsTv -- Scoped type variable introduced by a class decl
271 -- class C a where ...
273 | InstTv -- Ditto, but instance decl
275 | PatSigTv -- Scoped type variable, introduced by a pattern
279 | VanillaTv -- Everything else
281 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
282 isUserTyVar tv = case mutTyVarDetails tv of
286 isSkolemTyVar :: TcTyVar -> Bool
287 isSkolemTyVar tv = case mutTyVarDetails tv of
293 isHoleTyVar :: TcTyVar -> Bool
294 -- NB: the hole might be filled in by now, and this
295 -- function does not check for that
296 isHoleTyVar tv = ASSERT( isMutTyVar tv )
297 case mutTyVarDetails tv of
301 tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
304 = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
305 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
309 details SigTv = ptext SLIT("type signature")
310 details ClsTv = ptext SLIT("class declaration")
311 details InstTv = ptext SLIT("instance declaration")
312 details PatSigTv = ptext SLIT("pattern type signature")
313 details HoleTv = ptext SLIT("//hole//") -- Should not happen
314 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
318 %************************************************************************
320 \subsection{Tau, sigma and rho}
322 %************************************************************************
325 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
327 mkPhiTy :: [SourceType] -> Type -> Type
328 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
332 @isTauTy@ tests for nested for-alls.
335 isTauTy :: Type -> Bool
336 isTauTy (TyVarTy v) = True
337 isTauTy (TyConApp _ tys) = all isTauTy tys
338 isTauTy (AppTy a b) = isTauTy a && isTauTy b
339 isTauTy (FunTy a b) = isTauTy a && isTauTy b
340 isTauTy (SourceTy p) = True -- Don't look through source types
341 isTauTy (NoteTy _ ty) = isTauTy ty
342 isTauTy other = False
346 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
347 -- construct a dictionary function name
348 getDFunTyKey (TyVarTy tv) = getOccName tv
349 getDFunTyKey (TyConApp tc _) = getOccName tc
350 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
351 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
352 getDFunTyKey (FunTy arg _) = getOccName funTyCon
353 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
354 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
355 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
356 -- SourceTy shouldn't happen
360 %************************************************************************
362 \subsection{Expanding and splitting}
364 %************************************************************************
366 These tcSplit functions are like their non-Tc analogues, but
367 a) they do not look through newtypes
368 b) they do not look through PredTys
369 c) [future] they ignore usage-type annotations
371 However, they are non-monadic and do not follow through mutable type
372 variables. It's up to you to make sure this doesn't matter.
375 tcSplitForAllTys :: Type -> ([TyVar], Type)
376 tcSplitForAllTys ty = split ty ty []
378 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
379 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
380 split orig_ty t tvs = (reverse tvs, orig_ty)
382 tcIsForAllTy (ForAllTy tv ty) = True
383 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
384 tcIsForAllTy t = False
386 tcSplitPhiTy :: Type -> ([PredType], Type)
387 tcSplitPhiTy ty = split ty ty []
389 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
390 Just p -> split res res (p:ts)
391 Nothing -> (reverse ts, orig_ty)
392 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
393 split orig_ty ty ts = (reverse ts, orig_ty)
395 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
396 (tvs, rho) -> case tcSplitPhiTy rho of
397 (theta, tau) -> (tvs, theta, tau)
399 tcTyConAppTyCon :: Type -> TyCon
400 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
402 tcTyConAppArgs :: Type -> [Type]
403 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
405 tcSplitTyConApp :: Type -> (TyCon, [Type])
406 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
408 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
410 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
411 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
412 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
413 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
414 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
415 -- Newtypes are opaque, so they may be split
416 -- However, predicates are not treated
417 -- as tycon applications by the type checker
418 tcSplitTyConApp_maybe other = Nothing
420 tcSplitFunTys :: Type -> ([Type], Type)
421 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
423 Just (arg,res) -> (arg:args, res')
425 (args,res') = tcSplitFunTys res
427 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
428 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
429 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
430 tcSplitFunTy_maybe other = Nothing
432 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
433 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
436 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
437 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
438 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
439 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
440 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys --- Don't forget that newtype!
441 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
442 tcSplitAppTy_maybe other = Nothing
444 tc_split_app tc tys = case snocView tys of
445 Just (tys',ty') -> Just (TyConApp tc tys', ty')
448 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
450 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
452 tcSplitAppTys :: Type -> (Type, [Type])
456 go ty args = case tcSplitAppTy_maybe ty of
457 Just (ty', arg) -> go ty' (arg:args)
460 tcGetTyVar_maybe :: Type -> Maybe TyVar
461 tcGetTyVar_maybe (TyVarTy tv) = Just tv
462 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
463 tcGetTyVar_maybe other = Nothing
465 tcGetTyVar :: String -> Type -> TyVar
466 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
468 tcIsTyVarTy :: Type -> Bool
469 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
472 The type of a method for class C is always of the form:
473 Forall a1..an. C a1..an => sig_ty
474 where sig_ty is the type given by the method's signature, and thus in general
475 is a ForallTy. At the point that splitMethodTy is called, it is expected
476 that the outer Forall has already been stripped off. splitMethodTy then
477 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off.
480 tcSplitMethodTy :: Type -> (PredType, Type)
481 tcSplitMethodTy ty = split ty
483 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
485 Nothing -> panic "splitMethodTy"
486 split (NoteTy n ty) = split ty
487 split _ = panic "splitMethodTy"
489 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
490 -- Split the type of a dictionary function
492 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
493 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
494 (tvs, theta, clas, tys) }}
497 (allDistinctTyVars tys tvs) = True
499 all the types tys are type variables,
500 distinct from each other and from tvs.
502 This is useful when checking that unification hasn't unified signature
503 type variables. For example, if the type sig is
504 f :: forall a b. a -> b -> b
505 we want to check that 'a' and 'b' havn't
506 (a) been unified with a non-tyvar type
507 (b) been unified with each other (all distinct)
508 (c) been unified with a variable free in the environment
511 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
513 allDistinctTyVars [] acc
515 allDistinctTyVars (ty:tys) acc
516 = case tcGetTyVar_maybe ty of
517 Nothing -> False -- (a)
518 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
519 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
523 %************************************************************************
525 \subsection{Predicate types}
527 %************************************************************************
529 "Predicates" are particular source types, namelyClassP or IParams
532 isPred :: SourceType -> Bool
533 isPred (ClassP _ _) = True
534 isPred (IParam _ _) = True
535 isPred (NType _ _) = False
537 isPredTy :: Type -> Bool
538 isPredTy (NoteTy _ ty) = isPredTy ty
539 isPredTy (SourceTy sty) = isPred sty
542 tcSplitPredTy_maybe :: Type -> Maybe PredType
543 -- Returns Just for predicates only
544 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
545 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
546 tcSplitPredTy_maybe other = Nothing
548 predTyUnique :: PredType -> Unique
549 predTyUnique (IParam n _) = getUnique (ipNameName n)
550 predTyUnique (ClassP clas tys) = getUnique clas
552 predHasFDs :: PredType -> Bool
553 -- True if the predicate has functional depenencies;
554 -- I.e. should participate in improvement
555 predHasFDs (IParam _ _) = True
556 predHasFDs (ClassP cls _) = classHasFDs cls
558 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
559 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
560 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
564 --------------------- Dictionary types ---------------------------------
567 mkClassPred clas tys = ClassP clas tys
569 isClassPred :: SourceType -> Bool
570 isClassPred (ClassP clas tys) = True
571 isClassPred other = False
573 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
574 isTyVarClassPred other = False
576 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
577 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
578 getClassPredTys_maybe _ = Nothing
580 getClassPredTys :: PredType -> (Class, [Type])
581 getClassPredTys (ClassP clas tys) = (clas, tys)
583 mkDictTy :: Class -> [Type] -> Type
584 mkDictTy clas tys = mkPredTy (ClassP clas tys)
586 isDictTy :: Type -> Bool
587 isDictTy (SourceTy p) = isClassPred p
588 isDictTy (NoteTy _ ty) = isDictTy ty
589 isDictTy other = False
592 --------------------- Implicit parameters ---------------------------------
595 isIPPred :: SourceType -> Bool
596 isIPPred (IParam _ _) = True
597 isIPPred other = False
599 isInheritablePred :: PredType -> Bool
600 -- Can be inherited by a context. For example, consider
601 -- f x = let g y = (?v, y+x)
602 -- in (g 3 with ?v = 8,
604 -- The point is that g's type must be quantifed over ?v:
605 -- g :: (?v :: a) => a -> a
606 -- but it doesn't need to be quantified over the Num a dictionary
607 -- which can be free in g's rhs, and shared by both calls to g
608 isInheritablePred (ClassP _ _) = True
609 isInheritablePred other = False
611 isLinearPred :: TcPredType -> Bool
612 isLinearPred (IParam (Linear n) _) = True
613 isLinearPred other = False
617 %************************************************************************
619 \subsection{Comparison}
621 %************************************************************************
623 Comparison, taking note of newtypes, predicates, etc,
624 But ignoring usage types
627 tcEqType :: Type -> Type -> Bool
628 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
630 tcEqTypes :: [Type] -> [Type] -> Bool
631 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
633 tcEqPred :: PredType -> PredType -> Bool
634 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
637 tcCmpType :: Type -> Type -> Ordering
638 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
640 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
642 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
644 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
647 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
648 -- The "env" maps type variables in ty1 to type variables in ty2
649 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
650 -- we in effect substitute tv2 for tv1 in t1 before continuing
652 -- Look through NoteTy
653 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
654 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
656 -- Deal with equal constructors
657 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
658 Just tv1a -> tv1a `compare` tv2
659 Nothing -> tv1 `compare` tv2
661 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
662 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
663 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
664 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
665 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
667 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
668 cmpTy env (AppTy _ _) (TyVarTy _) = GT
670 cmpTy env (FunTy _ _) (TyVarTy _) = GT
671 cmpTy env (FunTy _ _) (AppTy _ _) = GT
673 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
674 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
675 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
677 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
678 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
679 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
680 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
682 cmpTy env (SourceTy _) t2 = GT
688 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
689 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
690 -- Compare types as well as names for implicit parameters
691 -- This comparison is used exclusively (I think) for the
692 -- finite map built in TcSimplify
693 cmpSourceTy env (IParam _ _) sty = LT
695 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
696 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
697 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
699 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
700 cmpSourceTy env (NType _ _) sty = GT
703 PredTypes are used as a FM key in TcSimplify,
704 so we take the easy path and make them an instance of Ord
707 instance Eq SourceType where { (==) = tcEqPred }
708 instance Ord SourceType where { compare = tcCmpPred }
712 %************************************************************************
714 \subsection{Predicates}
716 %************************************************************************
718 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
720 f :: (?x::Int) => Int -> Int
723 isSigmaTy :: Type -> Bool
724 isSigmaTy (ForAllTy tyvar ty) = True
725 isSigmaTy (FunTy a b) = isPredTy a
726 isSigmaTy (NoteTy n ty) = isSigmaTy ty
729 isOverloadedTy :: Type -> Bool
730 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
731 isOverloadedTy (FunTy a b) = isPredTy a
732 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
733 isOverloadedTy _ = False
737 isFloatTy = is_tc floatTyConKey
738 isDoubleTy = is_tc doubleTyConKey
739 isIntegerTy = is_tc integerTyConKey
740 isIntTy = is_tc intTyConKey
741 isAddrTy = is_tc addrTyConKey
742 isBoolTy = is_tc boolTyConKey
743 isUnitTy = is_tc unitTyConKey
745 is_tc :: Unique -> Type -> Bool
746 -- Newtypes are opaque to this
747 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
748 Just (tc, _) -> uniq == getUnique tc
753 %************************************************************************
757 %************************************************************************
760 deNoteType :: Type -> Type
761 -- Remove synonyms, but not source types
762 deNoteType ty@(TyVarTy tyvar) = ty
763 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
764 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
765 deNoteType (NoteTy _ ty) = deNoteType ty
766 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
767 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
768 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
770 deNoteSourceType :: SourceType -> SourceType
771 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
772 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
773 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
776 Find the free tycons and classes of a type. This is used in the front
780 tyClsNamesOfType :: Type -> NameSet
781 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
782 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
783 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
784 tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
785 tyClsNamesOfType (SourceTy (IParam n ty)) = tyClsNamesOfType ty
786 tyClsNamesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
787 tyClsNamesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` tyClsNamesOfTypes tys
788 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
789 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
790 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
792 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
794 tyClsNamesOfDFunHead :: Type -> NameSet
795 -- Find the free type constructors and classes
796 -- of the head of the dfun instance type
797 -- The 'dfun_head_type' is because of
798 -- instance Foo a => Baz T where ...
799 -- The decl is an orphan if Baz and T are both not locally defined,
800 -- even if Foo *is* locally defined
801 tyClsNamesOfDFunHead dfun_ty
802 = case tcSplitSigmaTy dfun_ty of
803 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
805 classNamesOfTheta :: ThetaType -> [Name]
806 -- Looks just for ClassP things; maybe it should check
807 classNamesOfTheta preds = [ getName c | ClassP c _ <- preds ]
811 %************************************************************************
813 \subsection[TysWiredIn-ext-type]{External types}
815 %************************************************************************
817 The compiler's foreign function interface supports the passing of a
818 restricted set of types as arguments and results (the restricting factor
822 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
823 -- Checks for valid argument type for a 'foreign import'
824 isFFIArgumentTy dflags safety ty
825 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
827 isFFIExternalTy :: Type -> Bool
828 -- Types that are allowed as arguments of a 'foreign export'
829 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
831 isFFIImportResultTy :: DynFlags -> Type -> Bool
832 isFFIImportResultTy dflags ty
833 = checkRepTyCon (legalFIResultTyCon dflags) ty
835 isFFIExportResultTy :: Type -> Bool
836 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
838 isFFIDynArgumentTy :: Type -> Bool
839 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
840 -- or a newtype of either.
841 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
843 isFFIDynResultTy :: Type -> Bool
844 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
845 -- or a newtype of either.
846 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
848 isFFILabelTy :: Type -> Bool
849 -- The type of a foreign label must be Ptr, FunPtr, Addr,
850 -- or a newtype of either.
851 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
853 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
854 -- Look through newtypes
855 -- Non-recursive ones are transparent to splitTyConApp,
856 -- but recursive ones aren't; hence the splitNewType_maybe
857 checkRepTyCon check_tc ty
858 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
862 ----------------------------------------------
863 These chaps do the work; they are not exported
864 ----------------------------------------------
867 legalFEArgTyCon :: TyCon -> Bool
868 -- It's illegal to return foreign objects and (mutable)
869 -- bytearrays from a _ccall_ / foreign declaration
870 -- (or be passed them as arguments in foreign exported functions).
872 | getUnique tc `elem` [ byteArrayTyConKey, mutableByteArrayTyConKey ]
874 -- It's also illegal to make foreign exports that take unboxed
875 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
877 = boxedMarshalableTyCon tc
879 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
880 legalFIResultTyCon dflags tc
881 | getUnique tc `elem`
882 [ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
883 | tc == unitTyCon = True
884 | otherwise = marshalableTyCon dflags tc
886 legalFEResultTyCon :: TyCon -> Bool
887 legalFEResultTyCon tc
888 | getUnique tc `elem`
889 [ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
890 | tc == unitTyCon = True
891 | otherwise = boxedMarshalableTyCon tc
893 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
894 -- Checks validity of types going from Haskell -> external world
895 legalOutgoingTyCon dflags safety tc
896 | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
899 = marshalableTyCon dflags tc
901 marshalableTyCon dflags tc
902 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
903 || boxedMarshalableTyCon tc
905 boxedMarshalableTyCon tc
906 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
907 , int32TyConKey, int64TyConKey
908 , wordTyConKey, word8TyConKey, word16TyConKey
909 , word32TyConKey, word64TyConKey
910 , floatTyConKey, doubleTyConKey
911 , addrTyConKey, ptrTyConKey, funPtrTyConKey
914 , byteArrayTyConKey, mutableByteArrayTyConKey
920 %************************************************************************
922 \subsection{Unification with an explicit substitution}
924 %************************************************************************
926 Unify types with an explicit substitution and no monad.
927 Ignore usage annotations.
931 = (TyVarSet, -- Set of template tyvars
932 TyVarSubstEnv) -- Not necessarily idempotent
934 unifyTysX :: TyVarSet -- Template tyvars
937 -> Maybe TyVarSubstEnv
938 unifyTysX tmpl_tyvars ty1 ty2
939 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
941 unifyExtendTysX :: TyVarSet -- Template tyvars
942 -> TyVarSubstEnv -- Substitution to start with
945 -> Maybe TyVarSubstEnv -- Extended substitution
946 unifyExtendTysX tmpl_tyvars subst ty1 ty2
947 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
949 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
950 -> Maybe TyVarSubstEnv
951 unifyTyListsX tmpl_tyvars tys1 tys2
952 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
957 -> (MySubst -> Maybe result)
961 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
962 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
964 -- Variables; go for uVar
965 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
968 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
969 | tyvar1 `elemVarSet` tmpls
970 = uVarX tyvar1 ty2 k subst
971 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
972 | tyvar2 `elemVarSet` tmpls
973 = uVarX tyvar2 ty1 k subst
976 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
977 | n1 == n2 = uTysX t1 t2 k subst
978 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
979 | c1 == c2 = uTyListsX tys1 tys2 k subst
980 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
981 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
983 -- Functions; just check the two parts
984 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
985 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
987 -- Type constructors must match
988 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
989 | (con1 == con2 && equalLength tys1 tys2)
990 = uTyListsX tys1 tys2 k subst
992 -- Applications need a bit of care!
993 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
994 -- NB: we've already dealt with type variables and Notes,
995 -- so if one type is an App the other one jolly well better be too
996 uTysX (AppTy s1 t1) ty2 k subst
997 = case tcSplitAppTy_maybe ty2 of
998 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
999 Nothing -> Nothing -- Fail
1001 uTysX ty1 (AppTy s2 t2) k subst
1002 = case tcSplitAppTy_maybe ty1 of
1003 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1004 Nothing -> Nothing -- Fail
1006 -- Not expecting for-alls in unification
1008 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
1009 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1012 -- Anything else fails
1013 uTysX ty1 ty2 k subst = Nothing
1016 uTyListsX [] [] k subst = k subst
1017 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1018 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1022 -- Invariant: tv1 is a unifiable variable
1023 uVarX tv1 ty2 k subst@(tmpls, env)
1024 = case lookupSubstEnv env tv1 of
1025 Just (DoneTy ty1) -> -- Already bound
1026 uTysX ty1 ty2 k subst
1028 Nothing -- Not already bound
1029 | typeKind ty2 `eqKind` tyVarKind tv1
1030 && occur_check_ok ty2
1031 -> -- No kind mismatch nor occur check
1032 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1034 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1036 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1037 occur_check_ok_tv tv | tv1 == tv = False
1038 | otherwise = case lookupSubstEnv env tv of
1040 Just (DoneTy ty) -> occur_check_ok ty
1045 %************************************************************************
1047 \subsection{Matching on types}
1049 %************************************************************************
1051 Matching is a {\em unidirectional} process, matching a type against a
1052 template (which is just a type with type variables in it). The
1053 matcher assumes that there are no repeated type variables in the
1054 template, so that it simply returns a mapping of type variables to
1055 types. It also fails on nested foralls.
1057 @matchTys@ matches corresponding elements of a list of templates and
1058 types. It and @matchTy@ both ignore usage annotations, unlike the
1059 main function @match@.
1062 matchTy :: TyVarSet -- Template tyvars
1064 -> Type -- Proposed instance of template
1065 -> Maybe TyVarSubstEnv -- Matching substitution
1068 matchTys :: TyVarSet -- Template tyvars
1069 -> [Type] -- Templates
1070 -> [Type] -- Proposed instance of template
1071 -> Maybe (TyVarSubstEnv, -- Matching substitution
1072 [Type]) -- Left over instance types
1074 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1076 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1077 (\ (senv,tys) -> Just (senv,tys))
1081 @match@ is the main function. It takes a flag indicating whether
1082 usage annotations are to be respected.
1085 match :: Type -> Type -- Current match pair
1086 -> TyVarSet -- Template vars
1087 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1088 -> TyVarSubstEnv -- Current subst
1091 -- When matching against a type variable, see if the variable
1092 -- has already been bound. If so, check that what it's bound to
1093 -- is the same as ty; if not, bind it and carry on.
1095 match (TyVarTy v) ty tmpls k senv
1096 | v `elemVarSet` tmpls
1097 = -- v is a template variable
1098 case lookupSubstEnv senv v of
1099 Nothing | typeKind ty `eqKind` tyVarKind v
1100 -- We do a kind check, just as in the uVarX above
1101 -- The kind check is needed to avoid bogus matches
1102 -- of (a b) with (c d), where the kinds don't match
1103 -- An occur check isn't needed when matching.
1104 -> k (extendSubstEnv senv v (DoneTy ty))
1106 | otherwise -> Nothing -- Fails
1108 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1109 | otherwise -> Nothing -- Fails
1112 = -- v is not a template variable; ty had better match
1113 -- Can't use (==) because types differ
1114 case tcGetTyVar_maybe ty of
1115 Just v' | v == v' -> k senv -- Success
1116 other -> Nothing -- Failure
1117 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1118 -- I guess the reason the Note-stripping case is *last* rather than first
1119 -- is to preserve type synonyms etc., so I'm not moving it to the
1120 -- top; but this means that (without the deNotetype) a type
1121 -- variable may not match the pattern (TyVarTy v') as one would
1122 -- expect, due to an intervening Note. KSW 2000-06.
1125 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1126 | n1 == n2 = match t1 t2 tmpls k senv
1127 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1128 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1129 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1130 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1132 -- Functions; just check the two parts
1133 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1134 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1136 match (AppTy fun1 arg1) ty2 tmpls k senv
1137 = case tcSplitAppTy_maybe ty2 of
1138 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1139 Nothing -> Nothing -- Fail
1141 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1142 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1144 -- Newtypes are opaque; other source types should not happen
1145 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1146 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1148 -- With type synonyms, we have to be careful for the exact
1149 -- same reasons as in the unifier. Please see the
1150 -- considerable commentary there before changing anything
1151 -- here! (WDP 95/05)
1152 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1153 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1156 match _ _ _ _ _ = Nothing
1158 match_list_exactly tys1 tys2 tmpls k senv
1159 = match_list tys1 tys2 tmpls k' senv
1161 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1162 | otherwise = Nothing -- Fail
1164 match_list [] tys2 tmpls k senv = k (senv, tys2)
1165 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1166 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1167 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv