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
78 isFFIDotnetTy, -- :: DynFlags -> Type -> Bool
79 isFFIDotnetObjTy, -- :: Type -> Bool
81 toDNType, -- :: Type -> DNType
83 ---------------------------------
84 -- Unifier and matcher
85 unifyTysX, unifyTyListsX, unifyExtendTysX,
86 matchTy, matchTys, match,
88 --------------------------------
89 -- Rexported from Type
90 Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
91 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
92 superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
93 isTypeKind, isAnyTypeKind,
95 Type, SourceType(..), PredType, ThetaType,
96 mkForAllTy, mkForAllTys,
97 mkFunTy, mkFunTys, zipFunTys,
98 mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
99 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
101 isUnLiftedType, -- Source types are always lifted
102 isUnboxedTupleType, -- Ditto
103 isPrimitiveType, isTyVarTy,
105 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
106 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
109 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
112 #include "HsVersions.h"
115 import {-# SOURCE #-} PprType( pprType )
116 -- PprType imports TcType so that it can print intelligently
119 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
121 import Type ( -- Re-exports
122 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
123 tyVarsOfTheta, Kind, Type, SourceType(..),
124 PredType, ThetaType, unliftedTypeKind,
125 liftedTypeKind, openTypeKind, mkArrowKind,
126 mkArrowKinds, mkForAllTy, mkForAllTys,
127 defaultKind, isTypeKind, isAnyTypeKind,
128 mkFunTy, mkFunTys, zipFunTys, isTyVarTy,
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,
138 tidyOpenTyVars, eqKind,
139 hasMoreBoxityInfo, liftedBoxity,
140 superBoxity, typeKind, superKind, repType
142 import DataCon ( DataCon )
143 import TyCon ( TyCon, isUnLiftedTyCon, tyConUnique )
144 import Class ( classHasFDs, Class )
145 import Var ( TyVar, Id, tyVarKind, isMutTyVar, mutTyVarDetails )
146 import ForeignCall ( Safety, playSafe
153 import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
154 import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
155 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 %************************************************************************
175 data TyThing = AnId Id
180 instance NamedThing TyThing where
181 getName (AnId id) = getName id
182 getName (ATyCon tc) = getName tc
183 getName (AClass cl) = getName cl
184 getName (ADataCon dc) = getName dc
188 %************************************************************************
192 %************************************************************************
194 The type checker divides the generic Type world into the
195 following more structured beasts:
197 sigma ::= forall tyvars. phi
198 -- A sigma type is a qualified type
200 -- Note that even if 'tyvars' is empty, theta
201 -- may not be: e.g. (?x::Int) => Int
203 -- Note that 'sigma' is in prenex form:
204 -- all the foralls are at the front.
205 -- A 'phi' type has no foralls to the right of
213 -- A 'tau' type has no quantification anywhere
214 -- Note that the args of a type constructor must be taus
216 | tycon tau_1 .. tau_n
220 -- In all cases, a (saturated) type synonym application is legal,
221 -- provided it expands to the required form.
225 type SigmaType = Type
231 type TcTyVar = TyVar -- Might be a mutable tyvar
232 type TcTyVarSet = TyVarSet
234 type TcType = Type -- A TcType can have mutable type variables
235 -- Invariant on ForAllTy in TcTypes:
237 -- a cannot occur inside a MutTyVar in T; that is,
238 -- T is "flattened" before quantifying over a
240 type TcPredType = PredType
241 type TcThetaType = ThetaType
242 type TcSigmaType = TcType
243 type TcRhoType = TcType
244 type TcTauType = TcType
249 %************************************************************************
251 \subsection{TyVarDetails}
253 %************************************************************************
255 TyVarDetails gives extra info about type variables, used during type
256 checking. It's attached to mutable type variables only.
257 It's knot-tied back to Var.lhs. There is no reason in principle
258 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
262 = SigTv -- Introduced when instantiating a type signature,
263 -- prior to checking that the defn of a fn does
264 -- have the expected type. Should not be instantiated.
266 -- f :: forall a. a -> a
268 -- When checking e, with expected type (a->a), we
269 -- should not instantiate a
271 | ClsTv -- Scoped type variable introduced by a class decl
272 -- class C a where ...
274 | InstTv -- Ditto, but instance decl
276 | PatSigTv -- Scoped type variable, introduced by a pattern
280 | VanillaTv -- Everything else
282 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
283 isUserTyVar tv = case mutTyVarDetails tv of
287 isSkolemTyVar :: TcTyVar -> Bool
288 isSkolemTyVar tv = case mutTyVarDetails tv of
294 tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
297 = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
298 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
302 details SigTv = ptext SLIT("type signature")
303 details ClsTv = ptext SLIT("class declaration")
304 details InstTv = ptext SLIT("instance declaration")
305 details PatSigTv = ptext SLIT("pattern type signature")
306 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
310 %************************************************************************
312 \subsection{Tau, sigma and rho}
314 %************************************************************************
317 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
319 mkPhiTy :: [SourceType] -> Type -> Type
320 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
324 @isTauTy@ tests for nested for-alls.
327 isTauTy :: Type -> Bool
328 isTauTy (TyVarTy v) = True
329 isTauTy (TyConApp _ tys) = all isTauTy tys
330 isTauTy (AppTy a b) = isTauTy a && isTauTy b
331 isTauTy (FunTy a b) = isTauTy a && isTauTy b
332 isTauTy (SourceTy p) = True -- Don't look through source types
333 isTauTy (NoteTy _ ty) = isTauTy ty
334 isTauTy other = False
338 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
339 -- construct a dictionary function name
340 getDFunTyKey (TyVarTy tv) = getOccName tv
341 getDFunTyKey (TyConApp tc _) = getOccName tc
342 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
343 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
344 getDFunTyKey (FunTy arg _) = getOccName funTyCon
345 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
346 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
347 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
348 -- SourceTy shouldn't happen
352 %************************************************************************
354 \subsection{Expanding and splitting}
356 %************************************************************************
358 These tcSplit functions are like their non-Tc analogues, but
359 a) they do not look through newtypes
360 b) they do not look through PredTys
361 c) [future] they ignore usage-type annotations
363 However, they are non-monadic and do not follow through mutable type
364 variables. It's up to you to make sure this doesn't matter.
367 tcSplitForAllTys :: Type -> ([TyVar], Type)
368 tcSplitForAllTys ty = split ty ty []
370 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
371 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
372 split orig_ty t tvs = (reverse tvs, orig_ty)
374 tcIsForAllTy (ForAllTy tv ty) = True
375 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
376 tcIsForAllTy t = False
378 tcSplitPhiTy :: Type -> ([PredType], Type)
379 tcSplitPhiTy ty = split ty ty []
381 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
382 Just p -> split res res (p:ts)
383 Nothing -> (reverse ts, orig_ty)
384 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
385 split orig_ty ty ts = (reverse ts, orig_ty)
387 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
388 (tvs, rho) -> case tcSplitPhiTy rho of
389 (theta, tau) -> (tvs, theta, tau)
391 tcTyConAppTyCon :: Type -> TyCon
392 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
394 tcTyConAppArgs :: Type -> [Type]
395 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
397 tcSplitTyConApp :: Type -> (TyCon, [Type])
398 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
400 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
402 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
403 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
404 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
405 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
406 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
407 -- Newtypes are opaque, so they may be split
408 -- However, predicates are not treated
409 -- as tycon applications by the type checker
410 tcSplitTyConApp_maybe other = Nothing
412 tcSplitFunTys :: Type -> ([Type], Type)
413 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
415 Just (arg,res) -> (arg:args, res')
417 (args,res') = tcSplitFunTys res
419 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
420 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
421 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
422 tcSplitFunTy_maybe other = Nothing
424 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
425 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
428 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
429 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
430 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
431 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
432 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys --- Don't forget that newtype!
433 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
434 tcSplitAppTy_maybe other = Nothing
436 tc_split_app tc tys = case snocView tys of
437 Just (tys',ty') -> Just (TyConApp tc tys', ty')
440 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
442 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
444 tcSplitAppTys :: Type -> (Type, [Type])
448 go ty args = case tcSplitAppTy_maybe ty of
449 Just (ty', arg) -> go ty' (arg:args)
452 tcGetTyVar_maybe :: Type -> Maybe TyVar
453 tcGetTyVar_maybe (TyVarTy tv) = Just tv
454 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
455 tcGetTyVar_maybe other = Nothing
457 tcGetTyVar :: String -> Type -> TyVar
458 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
460 tcIsTyVarTy :: Type -> Bool
461 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
464 The type of a method for class C is always of the form:
465 Forall a1..an. C a1..an => sig_ty
466 where sig_ty is the type given by the method's signature, and thus in general
467 is a ForallTy. At the point that splitMethodTy is called, it is expected
468 that the outer Forall has already been stripped off. splitMethodTy then
469 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off.
472 tcSplitMethodTy :: Type -> (PredType, Type)
473 tcSplitMethodTy ty = split ty
475 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
477 Nothing -> panic "splitMethodTy"
478 split (NoteTy n ty) = split ty
479 split _ = panic "splitMethodTy"
481 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
482 -- Split the type of a dictionary function
484 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
485 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
486 (tvs, theta, clas, tys) }}
489 (allDistinctTyVars tys tvs) = True
491 all the types tys are type variables,
492 distinct from each other and from tvs.
494 This is useful when checking that unification hasn't unified signature
495 type variables. For example, if the type sig is
496 f :: forall a b. a -> b -> b
497 we want to check that 'a' and 'b' havn't
498 (a) been unified with a non-tyvar type
499 (b) been unified with each other (all distinct)
500 (c) been unified with a variable free in the environment
503 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
505 allDistinctTyVars [] acc
507 allDistinctTyVars (ty:tys) acc
508 = case tcGetTyVar_maybe ty of
509 Nothing -> False -- (a)
510 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
511 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
515 %************************************************************************
517 \subsection{Predicate types}
519 %************************************************************************
521 "Predicates" are particular source types, namelyClassP or IParams
524 isPred :: SourceType -> Bool
525 isPred (ClassP _ _) = True
526 isPred (IParam _ _) = True
527 isPred (NType _ _) = False
529 isPredTy :: Type -> Bool
530 isPredTy (NoteTy _ ty) = isPredTy ty
531 isPredTy (SourceTy sty) = isPred sty
534 tcSplitPredTy_maybe :: Type -> Maybe PredType
535 -- Returns Just for predicates only
536 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
537 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
538 tcSplitPredTy_maybe other = Nothing
540 predTyUnique :: PredType -> Unique
541 predTyUnique (IParam n _) = getUnique (ipNameName n)
542 predTyUnique (ClassP clas tys) = getUnique clas
544 predHasFDs :: PredType -> Bool
545 -- True if the predicate has functional depenencies;
546 -- I.e. should participate in improvement
547 predHasFDs (IParam _ _) = True
548 predHasFDs (ClassP cls _) = classHasFDs cls
550 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
551 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
552 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
556 --------------------- Dictionary types ---------------------------------
559 mkClassPred clas tys = ClassP clas tys
561 isClassPred :: SourceType -> Bool
562 isClassPred (ClassP clas tys) = True
563 isClassPred other = False
565 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
566 isTyVarClassPred other = False
568 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
569 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
570 getClassPredTys_maybe _ = Nothing
572 getClassPredTys :: PredType -> (Class, [Type])
573 getClassPredTys (ClassP clas tys) = (clas, tys)
575 mkDictTy :: Class -> [Type] -> Type
576 mkDictTy clas tys = mkPredTy (ClassP clas tys)
578 isDictTy :: Type -> Bool
579 isDictTy (SourceTy p) = isClassPred p
580 isDictTy (NoteTy _ ty) = isDictTy ty
581 isDictTy other = False
584 --------------------- Implicit parameters ---------------------------------
587 isIPPred :: SourceType -> Bool
588 isIPPred (IParam _ _) = True
589 isIPPred other = False
591 isInheritablePred :: PredType -> Bool
592 -- Can be inherited by a context. For example, consider
593 -- f x = let g y = (?v, y+x)
594 -- in (g 3 with ?v = 8,
596 -- The point is that g's type must be quantifed over ?v:
597 -- g :: (?v :: a) => a -> a
598 -- but it doesn't need to be quantified over the Num a dictionary
599 -- which can be free in g's rhs, and shared by both calls to g
600 isInheritablePred (ClassP _ _) = True
601 isInheritablePred other = False
603 isLinearPred :: TcPredType -> Bool
604 isLinearPred (IParam (Linear n) _) = True
605 isLinearPred other = False
609 %************************************************************************
611 \subsection{Comparison}
613 %************************************************************************
615 Comparison, taking note of newtypes, predicates, etc,
616 But ignoring usage types
619 tcEqType :: Type -> Type -> Bool
620 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
622 tcEqTypes :: [Type] -> [Type] -> Bool
623 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
625 tcEqPred :: PredType -> PredType -> Bool
626 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
629 tcCmpType :: Type -> Type -> Ordering
630 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
632 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
634 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
636 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
639 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
640 -- The "env" maps type variables in ty1 to type variables in ty2
641 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
642 -- we in effect substitute tv2 for tv1 in t1 before continuing
644 -- Look through NoteTy
645 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
646 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
648 -- Deal with equal constructors
649 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
650 Just tv1a -> tv1a `compare` tv2
651 Nothing -> tv1 `compare` tv2
653 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
654 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
655 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
656 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
657 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
659 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
660 cmpTy env (AppTy _ _) (TyVarTy _) = GT
662 cmpTy env (FunTy _ _) (TyVarTy _) = GT
663 cmpTy env (FunTy _ _) (AppTy _ _) = GT
665 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
666 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
667 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
669 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
670 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
671 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
672 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
674 cmpTy env (SourceTy _) t2 = GT
680 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
681 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
682 -- Compare types as well as names for implicit parameters
683 -- This comparison is used exclusively (I think) for the
684 -- finite map built in TcSimplify
685 cmpSourceTy env (IParam _ _) sty = LT
687 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
688 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
689 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
691 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
692 cmpSourceTy env (NType _ _) sty = GT
695 PredTypes are used as a FM key in TcSimplify,
696 so we take the easy path and make them an instance of Ord
699 instance Eq SourceType where { (==) = tcEqPred }
700 instance Ord SourceType where { compare = tcCmpPred }
704 %************************************************************************
706 \subsection{Predicates}
708 %************************************************************************
710 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
712 f :: (?x::Int) => Int -> Int
715 isSigmaTy :: Type -> Bool
716 isSigmaTy (ForAllTy tyvar ty) = True
717 isSigmaTy (FunTy a b) = isPredTy a
718 isSigmaTy (NoteTy n ty) = isSigmaTy ty
721 isOverloadedTy :: Type -> Bool
722 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
723 isOverloadedTy (FunTy a b) = isPredTy a
724 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
725 isOverloadedTy _ = False
729 isFloatTy = is_tc floatTyConKey
730 isDoubleTy = is_tc doubleTyConKey
731 isIntegerTy = is_tc integerTyConKey
732 isIntTy = is_tc intTyConKey
733 isAddrTy = is_tc addrTyConKey
734 isBoolTy = is_tc boolTyConKey
735 isUnitTy = is_tc unitTyConKey
737 is_tc :: Unique -> Type -> Bool
738 -- Newtypes are opaque to this
739 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
740 Just (tc, _) -> uniq == getUnique tc
745 %************************************************************************
749 %************************************************************************
752 deNoteType :: Type -> Type
753 -- Remove synonyms, but not source types
754 deNoteType ty@(TyVarTy tyvar) = ty
755 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
756 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
757 deNoteType (NoteTy _ ty) = deNoteType ty
758 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
759 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
760 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
762 deNoteSourceType :: SourceType -> SourceType
763 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
764 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
765 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
768 Find the free tycons and classes of a type. This is used in the front
772 tyClsNamesOfType :: Type -> NameSet
773 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
774 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
775 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
776 tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
777 tyClsNamesOfType (SourceTy (IParam n ty)) = tyClsNamesOfType ty
778 tyClsNamesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
779 tyClsNamesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` tyClsNamesOfTypes tys
780 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
781 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
782 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
784 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
786 tyClsNamesOfDFunHead :: Type -> NameSet
787 -- Find the free type constructors and classes
788 -- of the head of the dfun instance type
789 -- The 'dfun_head_type' is because of
790 -- instance Foo a => Baz T where ...
791 -- The decl is an orphan if Baz and T are both not locally defined,
792 -- even if Foo *is* locally defined
793 tyClsNamesOfDFunHead dfun_ty
794 = case tcSplitSigmaTy dfun_ty of
795 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
797 classNamesOfTheta :: ThetaType -> [Name]
798 -- Looks just for ClassP things; maybe it should check
799 classNamesOfTheta preds = [ getName c | ClassP c _ <- preds ]
803 %************************************************************************
805 \subsection[TysWiredIn-ext-type]{External types}
807 %************************************************************************
809 The compiler's foreign function interface supports the passing of a
810 restricted set of types as arguments and results (the restricting factor
814 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
815 -- Checks for valid argument type for a 'foreign import'
816 isFFIArgumentTy dflags safety ty
817 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
819 isFFIExternalTy :: Type -> Bool
820 -- Types that are allowed as arguments of a 'foreign export'
821 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
823 isFFIImportResultTy :: DynFlags -> Type -> Bool
824 isFFIImportResultTy dflags ty
825 = checkRepTyCon (legalFIResultTyCon dflags) ty
827 isFFIExportResultTy :: Type -> Bool
828 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
830 isFFIDynArgumentTy :: Type -> Bool
831 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
832 -- or a newtype of either.
833 isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
835 isFFIDynResultTy :: Type -> Bool
836 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
837 -- or a newtype of either.
838 isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
840 isFFILabelTy :: Type -> Bool
841 -- The type of a foreign label must be Ptr, FunPtr, Addr,
842 -- or a newtype of either.
843 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
845 isFFIDotnetTy :: DynFlags -> Type -> Bool
846 isFFIDotnetTy dflags ty
847 = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
848 (legalFIResultTyCon dflags tc ||
849 isFFIDotnetObjTy ty || isStringTy ty)) ty
851 -- Support String as an argument or result from a .NET FFI call.
853 case tcSplitTyConApp_maybe (repType ty) of
856 case tcSplitTyConApp_maybe (repType arg_ty) of
857 Just (cc,[]) -> cc == charTyCon
861 -- Support String as an argument or result from a .NET FFI call.
862 isFFIDotnetObjTy ty =
864 (_, t_ty) = tcSplitForAllTys ty
866 case tcSplitTyConApp_maybe (repType t_ty) of
867 Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
870 toDNType :: Type -> DNType
872 | isStringTy ty = DNString
873 | isFFIDotnetObjTy ty = DNObject
874 | Just (tc,argTys) <- tcSplitTyConApp_maybe ty =
875 case lookup (getUnique tc) dn_assoc of
878 | tc `hasKey` ioTyConKey -> toDNType (head argTys)
879 | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
881 dn_assoc :: [ (Unique, DNType) ]
882 dn_assoc = [ (unitTyConKey, DNUnit)
883 , (intTyConKey, DNInt)
884 , (int8TyConKey, DNInt8)
885 , (int16TyConKey, DNInt16)
886 , (int32TyConKey, DNInt32)
887 , (int64TyConKey, DNInt64)
888 , (wordTyConKey, DNInt)
889 , (word8TyConKey, DNWord8)
890 , (word16TyConKey, DNWord16)
891 , (word32TyConKey, DNWord32)
892 , (word64TyConKey, DNWord64)
893 , (floatTyConKey, DNFloat)
894 , (doubleTyConKey, DNDouble)
895 , (addrTyConKey, DNPtr)
896 , (ptrTyConKey, DNPtr)
897 , (funPtrTyConKey, DNPtr)
898 , (charTyConKey, DNChar)
899 , (boolTyConKey, DNBool)
902 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
903 -- Look through newtypes
904 -- Non-recursive ones are transparent to splitTyConApp,
905 -- but recursive ones aren't
906 checkRepTyCon check_tc ty
907 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
910 checkRepTyConKey :: [Unique] -> Type -> Bool
911 -- Like checkRepTyCon, but just looks at the TyCon key
912 checkRepTyConKey keys
913 = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
916 ----------------------------------------------
917 These chaps do the work; they are not exported
918 ----------------------------------------------
921 legalFEArgTyCon :: TyCon -> Bool
922 -- It's illegal to return foreign objects and (mutable)
923 -- bytearrays from a _ccall_ / foreign declaration
924 -- (or be passed them as arguments in foreign exported functions).
926 | isByteArrayLikeTyCon tc
928 -- It's also illegal to make foreign exports that take unboxed
929 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
931 = boxedMarshalableTyCon tc
933 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
934 legalFIResultTyCon dflags tc
935 | isByteArrayLikeTyCon tc = False
936 | tc == unitTyCon = True
937 | otherwise = marshalableTyCon dflags tc
939 legalFEResultTyCon :: TyCon -> Bool
940 legalFEResultTyCon tc
941 | isByteArrayLikeTyCon tc = False
942 | tc == unitTyCon = True
943 | otherwise = boxedMarshalableTyCon tc
945 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
946 -- Checks validity of types going from Haskell -> external world
947 legalOutgoingTyCon dflags safety tc
948 | playSafe safety && isByteArrayLikeTyCon tc
951 = marshalableTyCon dflags tc
953 marshalableTyCon dflags tc
954 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
955 || boxedMarshalableTyCon tc
957 boxedMarshalableTyCon tc
958 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
959 , int32TyConKey, int64TyConKey
960 , wordTyConKey, word8TyConKey, word16TyConKey
961 , word32TyConKey, word64TyConKey
962 , floatTyConKey, doubleTyConKey
963 , addrTyConKey, ptrTyConKey, funPtrTyConKey
966 , byteArrayTyConKey, mutableByteArrayTyConKey
970 isByteArrayLikeTyCon :: TyCon -> Bool
971 isByteArrayLikeTyCon tc =
972 getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
976 %************************************************************************
978 \subsection{Unification with an explicit substitution}
980 %************************************************************************
982 Unify types with an explicit substitution and no monad.
983 Ignore usage annotations.
987 = (TyVarSet, -- Set of template tyvars
988 TyVarSubstEnv) -- Not necessarily idempotent
990 unifyTysX :: TyVarSet -- Template tyvars
993 -> Maybe TyVarSubstEnv
994 unifyTysX tmpl_tyvars ty1 ty2
995 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
997 unifyExtendTysX :: TyVarSet -- Template tyvars
998 -> TyVarSubstEnv -- Substitution to start with
1001 -> Maybe TyVarSubstEnv -- Extended substitution
1002 unifyExtendTysX tmpl_tyvars subst ty1 ty2
1003 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
1005 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
1006 -> Maybe TyVarSubstEnv
1007 unifyTyListsX tmpl_tyvars tys1 tys2
1008 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
1013 -> (MySubst -> Maybe result)
1017 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
1018 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
1020 -- Variables; go for uVar
1021 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
1024 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
1025 | tyvar1 `elemVarSet` tmpls
1026 = uVarX tyvar1 ty2 k subst
1027 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
1028 | tyvar2 `elemVarSet` tmpls
1029 = uVarX tyvar2 ty1 k subst
1032 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
1033 | n1 == n2 = uTysX t1 t2 k subst
1034 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
1035 | c1 == c2 = uTyListsX tys1 tys2 k subst
1036 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
1037 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
1039 -- Functions; just check the two parts
1040 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
1041 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
1043 -- Type constructors must match
1044 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
1045 | (con1 == con2 && equalLength tys1 tys2)
1046 = uTyListsX tys1 tys2 k subst
1048 -- Applications need a bit of care!
1049 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1050 -- NB: we've already dealt with type variables and Notes,
1051 -- so if one type is an App the other one jolly well better be too
1052 uTysX (AppTy s1 t1) ty2 k subst
1053 = case tcSplitAppTy_maybe ty2 of
1054 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1055 Nothing -> Nothing -- Fail
1057 uTysX ty1 (AppTy s2 t2) k subst
1058 = case tcSplitAppTy_maybe ty1 of
1059 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1060 Nothing -> Nothing -- Fail
1062 -- Not expecting for-alls in unification
1064 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
1065 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1068 -- Anything else fails
1069 uTysX ty1 ty2 k subst = Nothing
1072 uTyListsX [] [] k subst = k subst
1073 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1074 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1078 -- Invariant: tv1 is a unifiable variable
1079 uVarX tv1 ty2 k subst@(tmpls, env)
1080 = case lookupSubstEnv env tv1 of
1081 Just (DoneTy ty1) -> -- Already bound
1082 uTysX ty1 ty2 k subst
1084 Nothing -- Not already bound
1085 | typeKind ty2 `eqKind` tyVarKind tv1
1086 && occur_check_ok ty2
1087 -> -- No kind mismatch nor occur check
1088 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1090 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1092 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1093 occur_check_ok_tv tv | tv1 == tv = False
1094 | otherwise = case lookupSubstEnv env tv of
1096 Just (DoneTy ty) -> occur_check_ok ty
1101 %************************************************************************
1103 \subsection{Matching on types}
1105 %************************************************************************
1107 Matching is a {\em unidirectional} process, matching a type against a
1108 template (which is just a type with type variables in it). The
1109 matcher assumes that there are no repeated type variables in the
1110 template, so that it simply returns a mapping of type variables to
1111 types. It also fails on nested foralls.
1113 @matchTys@ matches corresponding elements of a list of templates and
1114 types. It and @matchTy@ both ignore usage annotations, unlike the
1115 main function @match@.
1118 matchTy :: TyVarSet -- Template tyvars
1120 -> Type -- Proposed instance of template
1121 -> Maybe TyVarSubstEnv -- Matching substitution
1124 matchTys :: TyVarSet -- Template tyvars
1125 -> [Type] -- Templates
1126 -> [Type] -- Proposed instance of template
1127 -> Maybe (TyVarSubstEnv, -- Matching substitution
1128 [Type]) -- Left over instance types
1130 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1132 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1133 (\ (senv,tys) -> Just (senv,tys))
1137 @match@ is the main function. It takes a flag indicating whether
1138 usage annotations are to be respected.
1141 match :: Type -> Type -- Current match pair
1142 -> TyVarSet -- Template vars
1143 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1144 -> TyVarSubstEnv -- Current subst
1147 -- When matching against a type variable, see if the variable
1148 -- has already been bound. If so, check that what it's bound to
1149 -- is the same as ty; if not, bind it and carry on.
1151 match (TyVarTy v) ty tmpls k senv
1152 | v `elemVarSet` tmpls
1153 = -- v is a template variable
1154 case lookupSubstEnv senv v of
1155 Nothing | typeKind ty `eqKind` tyVarKind v
1156 -- We do a kind check, just as in the uVarX above
1157 -- The kind check is needed to avoid bogus matches
1158 -- of (a b) with (c d), where the kinds don't match
1159 -- An occur check isn't needed when matching.
1160 -> k (extendSubstEnv senv v (DoneTy ty))
1162 | otherwise -> Nothing -- Fails
1164 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1165 | otherwise -> Nothing -- Fails
1168 = -- v is not a template variable; ty had better match
1169 -- Can't use (==) because types differ
1170 case tcGetTyVar_maybe ty of
1171 Just v' | v == v' -> k senv -- Success
1172 other -> Nothing -- Failure
1173 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1174 -- I guess the reason the Note-stripping case is *last* rather than first
1175 -- is to preserve type synonyms etc., so I'm not moving it to the
1176 -- top; but this means that (without the deNotetype) a type
1177 -- variable may not match the pattern (TyVarTy v') as one would
1178 -- expect, due to an intervening Note. KSW 2000-06.
1181 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1182 | n1 == n2 = match t1 t2 tmpls k senv
1183 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1184 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1185 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1186 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1188 -- Functions; just check the two parts
1189 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1190 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1192 match (AppTy fun1 arg1) ty2 tmpls k senv
1193 = case tcSplitAppTy_maybe ty2 of
1194 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1195 Nothing -> Nothing -- Fail
1197 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1198 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1200 -- Newtypes are opaque; other source types should not happen
1201 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1202 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1204 -- With type synonyms, we have to be careful for the exact
1205 -- same reasons as in the unifier. Please see the
1206 -- considerable commentary there before changing anything
1207 -- here! (WDP 95/05)
1208 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1209 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1212 match _ _ _ _ _ = Nothing
1214 match_list_exactly tys1 tys2 tmpls k senv
1215 = match_list tys1 tys2 tmpls k' senv
1217 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1218 | otherwise = Nothing -- Fail
1220 match_list [] tys2 tmpls k senv = k (senv, tys2)
1221 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1222 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1223 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv