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,
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,
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 = SigTv -- Introduced when instantiating a type signature,
257 -- prior to checking that the defn of a fn does
258 -- have the expected type. Should not be instantiated.
260 -- f :: forall a. a -> a
262 -- When checking e, with expected type (a->a), we
263 -- should not instantiate a
265 | ClsTv -- Scoped type variable introduced by a class decl
266 -- class C a where ...
268 | InstTv -- Ditto, but instance decl
270 | PatSigTv -- Scoped type variable, introduced by a pattern
274 | VanillaTv -- Everything else
276 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
277 isUserTyVar tv = case mutTyVarDetails tv of
281 isSkolemTyVar :: TcTyVar -> Bool
282 isSkolemTyVar tv = case mutTyVarDetails tv of
288 tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
291 = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
292 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
296 details SigTv = ptext SLIT("type signature")
297 details ClsTv = ptext SLIT("class declaration")
298 details InstTv = ptext SLIT("instance declaration")
299 details PatSigTv = ptext SLIT("pattern type signature")
300 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
304 %************************************************************************
306 \subsection{Tau, sigma and rho}
308 %************************************************************************
311 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
313 mkPhiTy :: [SourceType] -> Type -> Type
314 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
318 @isTauTy@ tests for nested for-alls.
321 isTauTy :: Type -> Bool
322 isTauTy (TyVarTy v) = True
323 isTauTy (TyConApp _ tys) = all isTauTy tys
324 isTauTy (AppTy a b) = isTauTy a && isTauTy b
325 isTauTy (FunTy a b) = isTauTy a && isTauTy b
326 isTauTy (SourceTy p) = True -- Don't look through source types
327 isTauTy (NoteTy _ ty) = isTauTy ty
328 isTauTy other = False
332 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
333 -- construct a dictionary function name
334 getDFunTyKey (TyVarTy tv) = getOccName tv
335 getDFunTyKey (TyConApp tc _) = getOccName tc
336 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
337 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
338 getDFunTyKey (FunTy arg _) = getOccName funTyCon
339 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
340 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
341 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
342 -- SourceTy shouldn't happen
346 %************************************************************************
348 \subsection{Expanding and splitting}
350 %************************************************************************
352 These tcSplit functions are like their non-Tc analogues, but
353 a) they do not look through newtypes
354 b) they do not look through PredTys
355 c) [future] they ignore usage-type annotations
357 However, they are non-monadic and do not follow through mutable type
358 variables. It's up to you to make sure this doesn't matter.
361 tcSplitForAllTys :: Type -> ([TyVar], Type)
362 tcSplitForAllTys ty = split ty ty []
364 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
365 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
366 split orig_ty t tvs = (reverse tvs, orig_ty)
368 tcIsForAllTy (ForAllTy tv ty) = True
369 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
370 tcIsForAllTy t = False
372 tcSplitPhiTy :: Type -> ([PredType], Type)
373 tcSplitPhiTy ty = split ty ty []
375 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
376 Just p -> split res res (p:ts)
377 Nothing -> (reverse ts, orig_ty)
378 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
379 split orig_ty ty ts = (reverse ts, orig_ty)
381 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
382 (tvs, rho) -> case tcSplitPhiTy rho of
383 (theta, tau) -> (tvs, theta, tau)
385 tcTyConAppTyCon :: Type -> TyCon
386 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
388 tcTyConAppArgs :: Type -> [Type]
389 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
391 tcSplitTyConApp :: Type -> (TyCon, [Type])
392 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
394 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
396 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
397 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
398 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
399 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
400 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
401 -- Newtypes are opaque, so they may be split
402 -- However, predicates are not treated
403 -- as tycon applications by the type checker
404 tcSplitTyConApp_maybe other = Nothing
406 tcSplitFunTys :: Type -> ([Type], Type)
407 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
409 Just (arg,res) -> (arg:args, res')
411 (args,res') = tcSplitFunTys res
413 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
414 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
415 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
416 tcSplitFunTy_maybe other = Nothing
418 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
419 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
422 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
423 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
424 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
425 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
426 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys --- Don't forget that newtype!
427 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
428 tcSplitAppTy_maybe other = Nothing
430 tc_split_app tc tys = case snocView tys of
431 Just (tys',ty') -> Just (TyConApp tc tys', ty')
434 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
436 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
438 tcSplitAppTys :: Type -> (Type, [Type])
442 go ty args = case tcSplitAppTy_maybe ty of
443 Just (ty', arg) -> go ty' (arg:args)
446 tcGetTyVar_maybe :: Type -> Maybe TyVar
447 tcGetTyVar_maybe (TyVarTy tv) = Just tv
448 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
449 tcGetTyVar_maybe other = Nothing
451 tcGetTyVar :: String -> Type -> TyVar
452 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
454 tcIsTyVarTy :: Type -> Bool
455 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
458 The type of a method for class C is always of the form:
459 Forall a1..an. C a1..an => sig_ty
460 where sig_ty is the type given by the method's signature, and thus in general
461 is a ForallTy. At the point that splitMethodTy is called, it is expected
462 that the outer Forall has already been stripped off. splitMethodTy then
463 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off.
466 tcSplitMethodTy :: Type -> (PredType, Type)
467 tcSplitMethodTy ty = split ty
469 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
471 Nothing -> panic "splitMethodTy"
472 split (NoteTy n ty) = split ty
473 split _ = panic "splitMethodTy"
475 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
476 -- Split the type of a dictionary function
478 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
479 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
480 (tvs, theta, clas, tys) }}
483 (allDistinctTyVars tys tvs) = True
485 all the types tys are type variables,
486 distinct from each other and from tvs.
488 This is useful when checking that unification hasn't unified signature
489 type variables. For example, if the type sig is
490 f :: forall a b. a -> b -> b
491 we want to check that 'a' and 'b' havn't
492 (a) been unified with a non-tyvar type
493 (b) been unified with each other (all distinct)
494 (c) been unified with a variable free in the environment
497 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
499 allDistinctTyVars [] acc
501 allDistinctTyVars (ty:tys) acc
502 = case tcGetTyVar_maybe ty of
503 Nothing -> False -- (a)
504 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
505 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
509 %************************************************************************
511 \subsection{Predicate types}
513 %************************************************************************
515 "Predicates" are particular source types, namelyClassP or IParams
518 isPred :: SourceType -> Bool
519 isPred (ClassP _ _) = True
520 isPred (IParam _ _) = True
521 isPred (NType _ _) = False
523 isPredTy :: Type -> Bool
524 isPredTy (NoteTy _ ty) = isPredTy ty
525 isPredTy (SourceTy sty) = isPred sty
528 tcSplitPredTy_maybe :: Type -> Maybe PredType
529 -- Returns Just for predicates only
530 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
531 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
532 tcSplitPredTy_maybe other = Nothing
534 predTyUnique :: PredType -> Unique
535 predTyUnique (IParam n _) = getUnique (ipNameName n)
536 predTyUnique (ClassP clas tys) = getUnique clas
538 predHasFDs :: PredType -> Bool
539 -- True if the predicate has functional depenencies;
540 -- I.e. should participate in improvement
541 predHasFDs (IParam _ _) = True
542 predHasFDs (ClassP cls _) = classHasFDs cls
544 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
545 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
546 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
550 --------------------- Dictionary types ---------------------------------
553 mkClassPred clas tys = ClassP clas tys
555 isClassPred :: SourceType -> Bool
556 isClassPred (ClassP clas tys) = True
557 isClassPred other = False
559 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
560 isTyVarClassPred other = False
562 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
563 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
564 getClassPredTys_maybe _ = Nothing
566 getClassPredTys :: PredType -> (Class, [Type])
567 getClassPredTys (ClassP clas tys) = (clas, tys)
569 mkDictTy :: Class -> [Type] -> Type
570 mkDictTy clas tys = mkPredTy (ClassP clas tys)
572 isDictTy :: Type -> Bool
573 isDictTy (SourceTy p) = isClassPred p
574 isDictTy (NoteTy _ ty) = isDictTy ty
575 isDictTy other = False
578 --------------------- Implicit parameters ---------------------------------
581 isIPPred :: SourceType -> Bool
582 isIPPred (IParam _ _) = True
583 isIPPred other = False
585 isInheritablePred :: PredType -> Bool
586 -- Can be inherited by a context. For example, consider
587 -- f x = let g y = (?v, y+x)
588 -- in (g 3 with ?v = 8,
590 -- The point is that g's type must be quantifed over ?v:
591 -- g :: (?v :: a) => a -> a
592 -- but it doesn't need to be quantified over the Num a dictionary
593 -- which can be free in g's rhs, and shared by both calls to g
594 isInheritablePred (ClassP _ _) = True
595 isInheritablePred other = False
597 isLinearPred :: TcPredType -> Bool
598 isLinearPred (IParam (Linear n) _) = True
599 isLinearPred other = False
603 %************************************************************************
605 \subsection{Comparison}
607 %************************************************************************
609 Comparison, taking note of newtypes, predicates, etc,
610 But ignoring usage types
613 tcEqType :: Type -> Type -> Bool
614 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
616 tcEqTypes :: [Type] -> [Type] -> Bool
617 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
619 tcEqPred :: PredType -> PredType -> Bool
620 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
623 tcCmpType :: Type -> Type -> Ordering
624 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
626 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
628 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
630 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
633 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
634 -- The "env" maps type variables in ty1 to type variables in ty2
635 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
636 -- we in effect substitute tv2 for tv1 in t1 before continuing
638 -- Look through NoteTy
639 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
640 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
642 -- Deal with equal constructors
643 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
644 Just tv1a -> tv1a `compare` tv2
645 Nothing -> tv1 `compare` tv2
647 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
648 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
649 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
650 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
651 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
653 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
654 cmpTy env (AppTy _ _) (TyVarTy _) = GT
656 cmpTy env (FunTy _ _) (TyVarTy _) = GT
657 cmpTy env (FunTy _ _) (AppTy _ _) = GT
659 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
660 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
661 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
663 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
664 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
665 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
666 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
668 cmpTy env (SourceTy _) t2 = GT
674 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
675 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
676 -- Compare types as well as names for implicit parameters
677 -- This comparison is used exclusively (I think) for the
678 -- finite map built in TcSimplify
679 cmpSourceTy env (IParam _ _) sty = LT
681 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
682 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
683 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
685 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
686 cmpSourceTy env (NType _ _) sty = GT
689 PredTypes are used as a FM key in TcSimplify,
690 so we take the easy path and make them an instance of Ord
693 instance Eq SourceType where { (==) = tcEqPred }
694 instance Ord SourceType where { compare = tcCmpPred }
698 %************************************************************************
700 \subsection{Predicates}
702 %************************************************************************
704 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
706 f :: (?x::Int) => Int -> Int
709 isSigmaTy :: Type -> Bool
710 isSigmaTy (ForAllTy tyvar ty) = True
711 isSigmaTy (FunTy a b) = isPredTy a
712 isSigmaTy (NoteTy n ty) = isSigmaTy ty
715 isOverloadedTy :: Type -> Bool
716 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
717 isOverloadedTy (FunTy a b) = isPredTy a
718 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
719 isOverloadedTy _ = False
723 isFloatTy = is_tc floatTyConKey
724 isDoubleTy = is_tc doubleTyConKey
725 isIntegerTy = is_tc integerTyConKey
726 isIntTy = is_tc intTyConKey
727 isAddrTy = is_tc addrTyConKey
728 isBoolTy = is_tc boolTyConKey
729 isUnitTy = is_tc unitTyConKey
731 is_tc :: Unique -> Type -> Bool
732 -- Newtypes are opaque to this
733 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
734 Just (tc, _) -> uniq == getUnique tc
739 %************************************************************************
743 %************************************************************************
746 deNoteType :: Type -> Type
747 -- Remove synonyms, but not source types
748 deNoteType ty@(TyVarTy tyvar) = ty
749 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
750 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
751 deNoteType (NoteTy _ ty) = deNoteType ty
752 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
753 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
754 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
756 deNoteSourceType :: SourceType -> SourceType
757 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
758 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
759 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
762 Find the free tycons and classes of a type. This is used in the front
766 tyClsNamesOfType :: Type -> NameSet
767 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
768 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
769 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
770 tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
771 tyClsNamesOfType (SourceTy (IParam n ty)) = tyClsNamesOfType ty
772 tyClsNamesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
773 tyClsNamesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` tyClsNamesOfTypes tys
774 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
775 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
776 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
778 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
780 tyClsNamesOfDFunHead :: Type -> NameSet
781 -- Find the free type constructors and classes
782 -- of the head of the dfun instance type
783 -- The 'dfun_head_type' is because of
784 -- instance Foo a => Baz T where ...
785 -- The decl is an orphan if Baz and T are both not locally defined,
786 -- even if Foo *is* locally defined
787 tyClsNamesOfDFunHead dfun_ty
788 = case tcSplitSigmaTy dfun_ty of
789 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
791 classNamesOfTheta :: ThetaType -> [Name]
792 -- Looks just for ClassP things; maybe it should check
793 classNamesOfTheta preds = [ getName c | ClassP c _ <- preds ]
797 %************************************************************************
799 \subsection[TysWiredIn-ext-type]{External types}
801 %************************************************************************
803 The compiler's foreign function interface supports the passing of a
804 restricted set of types as arguments and results (the restricting factor
808 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
809 -- Checks for valid argument type for a 'foreign import'
810 isFFIArgumentTy dflags safety ty
811 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
813 isFFIExternalTy :: Type -> Bool
814 -- Types that are allowed as arguments of a 'foreign export'
815 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
817 isFFIImportResultTy :: DynFlags -> Type -> Bool
818 isFFIImportResultTy dflags ty
819 = checkRepTyCon (legalFIResultTyCon dflags) ty
821 isFFIExportResultTy :: Type -> Bool
822 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
824 isFFIDynArgumentTy :: Type -> Bool
825 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
826 -- or a newtype of either.
827 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
829 isFFIDynResultTy :: Type -> Bool
830 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
831 -- or a newtype of either.
832 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
834 isFFILabelTy :: Type -> Bool
835 -- The type of a foreign label must be Ptr, FunPtr, Addr,
836 -- or a newtype of either.
837 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
839 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
840 -- Look through newtypes
841 -- Non-recursive ones are transparent to splitTyConApp,
842 -- but recursive ones aren't
843 checkRepTyCon check_tc ty
844 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
848 ----------------------------------------------
849 These chaps do the work; they are not exported
850 ----------------------------------------------
853 legalFEArgTyCon :: TyCon -> Bool
854 -- It's illegal to return foreign objects and (mutable)
855 -- bytearrays from a _ccall_ / foreign declaration
856 -- (or be passed them as arguments in foreign exported functions).
858 | getUnique tc `elem` [ byteArrayTyConKey, mutableByteArrayTyConKey ]
860 -- It's also illegal to make foreign exports that take unboxed
861 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
863 = boxedMarshalableTyCon tc
865 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
866 legalFIResultTyCon dflags tc
867 | getUnique tc `elem`
868 [ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
869 | tc == unitTyCon = True
870 | otherwise = marshalableTyCon dflags tc
872 legalFEResultTyCon :: TyCon -> Bool
873 legalFEResultTyCon tc
874 | getUnique tc `elem`
875 [ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
876 | tc == unitTyCon = True
877 | otherwise = boxedMarshalableTyCon tc
879 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
880 -- Checks validity of types going from Haskell -> external world
881 legalOutgoingTyCon dflags safety tc
882 | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
885 = marshalableTyCon dflags tc
887 marshalableTyCon dflags tc
888 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
889 || boxedMarshalableTyCon tc
891 boxedMarshalableTyCon tc
892 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
893 , int32TyConKey, int64TyConKey
894 , wordTyConKey, word8TyConKey, word16TyConKey
895 , word32TyConKey, word64TyConKey
896 , floatTyConKey, doubleTyConKey
897 , addrTyConKey, ptrTyConKey, funPtrTyConKey
900 , byteArrayTyConKey, mutableByteArrayTyConKey
906 %************************************************************************
908 \subsection{Unification with an explicit substitution}
910 %************************************************************************
912 Unify types with an explicit substitution and no monad.
913 Ignore usage annotations.
917 = (TyVarSet, -- Set of template tyvars
918 TyVarSubstEnv) -- Not necessarily idempotent
920 unifyTysX :: TyVarSet -- Template tyvars
923 -> Maybe TyVarSubstEnv
924 unifyTysX tmpl_tyvars ty1 ty2
925 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
927 unifyExtendTysX :: TyVarSet -- Template tyvars
928 -> TyVarSubstEnv -- Substitution to start with
931 -> Maybe TyVarSubstEnv -- Extended substitution
932 unifyExtendTysX tmpl_tyvars subst ty1 ty2
933 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
935 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
936 -> Maybe TyVarSubstEnv
937 unifyTyListsX tmpl_tyvars tys1 tys2
938 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
943 -> (MySubst -> Maybe result)
947 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
948 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
950 -- Variables; go for uVar
951 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
954 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
955 | tyvar1 `elemVarSet` tmpls
956 = uVarX tyvar1 ty2 k subst
957 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
958 | tyvar2 `elemVarSet` tmpls
959 = uVarX tyvar2 ty1 k subst
962 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
963 | n1 == n2 = uTysX t1 t2 k subst
964 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
965 | c1 == c2 = uTyListsX tys1 tys2 k subst
966 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
967 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
969 -- Functions; just check the two parts
970 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
971 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
973 -- Type constructors must match
974 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
975 | (con1 == con2 && equalLength tys1 tys2)
976 = uTyListsX tys1 tys2 k subst
978 -- Applications need a bit of care!
979 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
980 -- NB: we've already dealt with type variables and Notes,
981 -- so if one type is an App the other one jolly well better be too
982 uTysX (AppTy s1 t1) ty2 k subst
983 = case tcSplitAppTy_maybe ty2 of
984 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
985 Nothing -> Nothing -- Fail
987 uTysX ty1 (AppTy s2 t2) k subst
988 = case tcSplitAppTy_maybe ty1 of
989 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
990 Nothing -> Nothing -- Fail
992 -- Not expecting for-alls in unification
994 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
995 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
998 -- Anything else fails
999 uTysX ty1 ty2 k subst = Nothing
1002 uTyListsX [] [] k subst = k subst
1003 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1004 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1008 -- Invariant: tv1 is a unifiable variable
1009 uVarX tv1 ty2 k subst@(tmpls, env)
1010 = case lookupSubstEnv env tv1 of
1011 Just (DoneTy ty1) -> -- Already bound
1012 uTysX ty1 ty2 k subst
1014 Nothing -- Not already bound
1015 | typeKind ty2 `eqKind` tyVarKind tv1
1016 && occur_check_ok ty2
1017 -> -- No kind mismatch nor occur check
1018 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1020 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1022 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1023 occur_check_ok_tv tv | tv1 == tv = False
1024 | otherwise = case lookupSubstEnv env tv of
1026 Just (DoneTy ty) -> occur_check_ok ty
1031 %************************************************************************
1033 \subsection{Matching on types}
1035 %************************************************************************
1037 Matching is a {\em unidirectional} process, matching a type against a
1038 template (which is just a type with type variables in it). The
1039 matcher assumes that there are no repeated type variables in the
1040 template, so that it simply returns a mapping of type variables to
1041 types. It also fails on nested foralls.
1043 @matchTys@ matches corresponding elements of a list of templates and
1044 types. It and @matchTy@ both ignore usage annotations, unlike the
1045 main function @match@.
1048 matchTy :: TyVarSet -- Template tyvars
1050 -> Type -- Proposed instance of template
1051 -> Maybe TyVarSubstEnv -- Matching substitution
1054 matchTys :: TyVarSet -- Template tyvars
1055 -> [Type] -- Templates
1056 -> [Type] -- Proposed instance of template
1057 -> Maybe (TyVarSubstEnv, -- Matching substitution
1058 [Type]) -- Left over instance types
1060 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1062 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1063 (\ (senv,tys) -> Just (senv,tys))
1067 @match@ is the main function. It takes a flag indicating whether
1068 usage annotations are to be respected.
1071 match :: Type -> Type -- Current match pair
1072 -> TyVarSet -- Template vars
1073 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1074 -> TyVarSubstEnv -- Current subst
1077 -- When matching against a type variable, see if the variable
1078 -- has already been bound. If so, check that what it's bound to
1079 -- is the same as ty; if not, bind it and carry on.
1081 match (TyVarTy v) ty tmpls k senv
1082 | v `elemVarSet` tmpls
1083 = -- v is a template variable
1084 case lookupSubstEnv senv v of
1085 Nothing | typeKind ty `eqKind` tyVarKind v
1086 -- We do a kind check, just as in the uVarX above
1087 -- The kind check is needed to avoid bogus matches
1088 -- of (a b) with (c d), where the kinds don't match
1089 -- An occur check isn't needed when matching.
1090 -> k (extendSubstEnv senv v (DoneTy ty))
1092 | otherwise -> Nothing -- Fails
1094 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1095 | otherwise -> Nothing -- Fails
1098 = -- v is not a template variable; ty had better match
1099 -- Can't use (==) because types differ
1100 case tcGetTyVar_maybe ty of
1101 Just v' | v == v' -> k senv -- Success
1102 other -> Nothing -- Failure
1103 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1104 -- I guess the reason the Note-stripping case is *last* rather than first
1105 -- is to preserve type synonyms etc., so I'm not moving it to the
1106 -- top; but this means that (without the deNotetype) a type
1107 -- variable may not match the pattern (TyVarTy v') as one would
1108 -- expect, due to an intervening Note. KSW 2000-06.
1111 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1112 | n1 == n2 = match t1 t2 tmpls k senv
1113 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1114 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1115 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1116 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1118 -- Functions; just check the two parts
1119 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1120 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1122 match (AppTy fun1 arg1) ty2 tmpls k senv
1123 = case tcSplitAppTy_maybe ty2 of
1124 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1125 Nothing -> Nothing -- Fail
1127 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1128 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1130 -- Newtypes are opaque; other source types should not happen
1131 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1132 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1134 -- With type synonyms, we have to be careful for the exact
1135 -- same reasons as in the unifier. Please see the
1136 -- considerable commentary there before changing anything
1137 -- here! (WDP 95/05)
1138 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1139 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1142 match _ _ _ _ _ = Nothing
1144 match_list_exactly tys1 tys2 tmpls k senv
1145 = match_list tys1 tys2 tmpls k' senv
1147 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1148 | otherwise = Nothing -- Fail
1150 match_list [] tys2 tmpls k senv = k (senv, tys2)
1151 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1152 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1153 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv