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 )
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 ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon,
159 charTyCon, listTyCon )
160 import BasicTypes ( IPName(..), ipNameName )
161 import Unique ( Unique, Uniquable(..) )
162 import SrcLoc ( SrcLoc )
163 import Util ( cmpList, thenCmp, equalLength, snocView )
164 import Maybes ( maybeToBool, expectJust )
169 %************************************************************************
173 %************************************************************************
176 data TyThing = AnId Id
181 instance NamedThing TyThing where
182 getName (AnId id) = getName id
183 getName (ATyCon tc) = getName tc
184 getName (AClass cl) = getName cl
185 getName (ADataCon dc) = getName dc
189 %************************************************************************
193 %************************************************************************
195 The type checker divides the generic Type world into the
196 following more structured beasts:
198 sigma ::= forall tyvars. phi
199 -- A sigma type is a qualified type
201 -- Note that even if 'tyvars' is empty, theta
202 -- may not be: e.g. (?x::Int) => Int
204 -- Note that 'sigma' is in prenex form:
205 -- all the foralls are at the front.
206 -- A 'phi' type has no foralls to the right of
214 -- A 'tau' type has no quantification anywhere
215 -- Note that the args of a type constructor must be taus
217 | tycon tau_1 .. tau_n
221 -- In all cases, a (saturated) type synonym application is legal,
222 -- provided it expands to the required form.
226 type SigmaType = Type
232 type TcTyVar = TyVar -- Might be a mutable tyvar
233 type TcTyVarSet = TyVarSet
235 type TcType = Type -- A TcType can have mutable type variables
236 -- Invariant on ForAllTy in TcTypes:
238 -- a cannot occur inside a MutTyVar in T; that is,
239 -- T is "flattened" before quantifying over a
241 type TcPredType = PredType
242 type TcThetaType = ThetaType
243 type TcSigmaType = TcType
244 type TcRhoType = TcType
245 type TcTauType = TcType
250 %************************************************************************
252 \subsection{TyVarDetails}
254 %************************************************************************
256 TyVarDetails gives extra info about type variables, used during type
257 checking. It's attached to mutable type variables only.
258 It's knot-tied back to Var.lhs. There is no reason in principle
259 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
263 = SigTv -- Introduced when instantiating a type signature,
264 -- prior to checking that the defn of a fn does
265 -- have the expected type. Should not be instantiated.
267 -- f :: forall a. a -> a
269 -- When checking e, with expected type (a->a), we
270 -- should not instantiate a
272 | ClsTv -- Scoped type variable introduced by a class decl
273 -- class C a where ...
275 | InstTv -- Ditto, but instance decl
277 | PatSigTv -- Scoped type variable, introduced by a pattern
281 | VanillaTv -- Everything else
283 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
284 isUserTyVar tv = case mutTyVarDetails tv of
288 isSkolemTyVar :: TcTyVar -> Bool
289 isSkolemTyVar tv = case mutTyVarDetails tv of
295 tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
298 = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
299 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
303 details SigTv = ptext SLIT("type signature")
304 details ClsTv = ptext SLIT("class declaration")
305 details InstTv = ptext SLIT("instance declaration")
306 details PatSigTv = ptext SLIT("pattern type signature")
307 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
311 %************************************************************************
313 \subsection{Tau, sigma and rho}
315 %************************************************************************
318 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
320 mkPhiTy :: [SourceType] -> Type -> Type
321 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
325 @isTauTy@ tests for nested for-alls.
328 isTauTy :: Type -> Bool
329 isTauTy (TyVarTy v) = True
330 isTauTy (TyConApp _ tys) = all isTauTy tys
331 isTauTy (AppTy a b) = isTauTy a && isTauTy b
332 isTauTy (FunTy a b) = isTauTy a && isTauTy b
333 isTauTy (SourceTy p) = True -- Don't look through source types
334 isTauTy (NoteTy _ ty) = isTauTy ty
335 isTauTy other = False
339 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
340 -- construct a dictionary function name
341 getDFunTyKey (TyVarTy tv) = getOccName tv
342 getDFunTyKey (TyConApp tc _) = getOccName tc
343 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
344 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
345 getDFunTyKey (FunTy arg _) = getOccName funTyCon
346 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
347 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
348 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
349 -- SourceTy shouldn't happen
353 %************************************************************************
355 \subsection{Expanding and splitting}
357 %************************************************************************
359 These tcSplit functions are like their non-Tc analogues, but
360 a) they do not look through newtypes
361 b) they do not look through PredTys
362 c) [future] they ignore usage-type annotations
364 However, they are non-monadic and do not follow through mutable type
365 variables. It's up to you to make sure this doesn't matter.
368 tcSplitForAllTys :: Type -> ([TyVar], Type)
369 tcSplitForAllTys ty = split ty ty []
371 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
372 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
373 split orig_ty t tvs = (reverse tvs, orig_ty)
375 tcIsForAllTy (ForAllTy tv ty) = True
376 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
377 tcIsForAllTy t = False
379 tcSplitPhiTy :: Type -> ([PredType], Type)
380 tcSplitPhiTy ty = split ty ty []
382 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
383 Just p -> split res res (p:ts)
384 Nothing -> (reverse ts, orig_ty)
385 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
386 split orig_ty ty ts = (reverse ts, orig_ty)
388 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
389 (tvs, rho) -> case tcSplitPhiTy rho of
390 (theta, tau) -> (tvs, theta, tau)
392 tcTyConAppTyCon :: Type -> TyCon
393 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
395 tcTyConAppArgs :: Type -> [Type]
396 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
398 tcSplitTyConApp :: Type -> (TyCon, [Type])
399 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
401 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
403 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
404 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
405 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
406 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
407 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
408 -- Newtypes are opaque, so they may be split
409 -- However, predicates are not treated
410 -- as tycon applications by the type checker
411 tcSplitTyConApp_maybe other = Nothing
413 tcSplitFunTys :: Type -> ([Type], Type)
414 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
416 Just (arg,res) -> (arg:args, res')
418 (args,res') = tcSplitFunTys res
420 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
421 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
422 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
423 tcSplitFunTy_maybe other = Nothing
425 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
426 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
429 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
430 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
431 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
432 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
433 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys --- Don't forget that newtype!
434 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
435 tcSplitAppTy_maybe other = Nothing
437 tc_split_app tc tys = case snocView tys of
438 Just (tys',ty') -> Just (TyConApp tc tys', ty')
441 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
443 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
445 tcSplitAppTys :: Type -> (Type, [Type])
449 go ty args = case tcSplitAppTy_maybe ty of
450 Just (ty', arg) -> go ty' (arg:args)
453 tcGetTyVar_maybe :: Type -> Maybe TyVar
454 tcGetTyVar_maybe (TyVarTy tv) = Just tv
455 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
456 tcGetTyVar_maybe other = Nothing
458 tcGetTyVar :: String -> Type -> TyVar
459 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
461 tcIsTyVarTy :: Type -> Bool
462 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
465 The type of a method for class C is always of the form:
466 Forall a1..an. C a1..an => sig_ty
467 where sig_ty is the type given by the method's signature, and thus in general
468 is a ForallTy. At the point that splitMethodTy is called, it is expected
469 that the outer Forall has already been stripped off. splitMethodTy then
470 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off.
473 tcSplitMethodTy :: Type -> (PredType, Type)
474 tcSplitMethodTy ty = split ty
476 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
478 Nothing -> panic "splitMethodTy"
479 split (NoteTy n ty) = split ty
480 split _ = panic "splitMethodTy"
482 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
483 -- Split the type of a dictionary function
485 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
486 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
487 (tvs, theta, clas, tys) }}
490 (allDistinctTyVars tys tvs) = True
492 all the types tys are type variables,
493 distinct from each other and from tvs.
495 This is useful when checking that unification hasn't unified signature
496 type variables. For example, if the type sig is
497 f :: forall a b. a -> b -> b
498 we want to check that 'a' and 'b' havn't
499 (a) been unified with a non-tyvar type
500 (b) been unified with each other (all distinct)
501 (c) been unified with a variable free in the environment
504 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
506 allDistinctTyVars [] acc
508 allDistinctTyVars (ty:tys) acc
509 = case tcGetTyVar_maybe ty of
510 Nothing -> False -- (a)
511 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
512 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
516 %************************************************************************
518 \subsection{Predicate types}
520 %************************************************************************
522 "Predicates" are particular source types, namelyClassP or IParams
525 isPred :: SourceType -> Bool
526 isPred (ClassP _ _) = True
527 isPred (IParam _ _) = True
528 isPred (NType _ _) = False
530 isPredTy :: Type -> Bool
531 isPredTy (NoteTy _ ty) = isPredTy ty
532 isPredTy (SourceTy sty) = isPred sty
535 tcSplitPredTy_maybe :: Type -> Maybe PredType
536 -- Returns Just for predicates only
537 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
538 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
539 tcSplitPredTy_maybe other = Nothing
541 predTyUnique :: PredType -> Unique
542 predTyUnique (IParam n _) = getUnique (ipNameName n)
543 predTyUnique (ClassP clas tys) = getUnique clas
545 predHasFDs :: PredType -> Bool
546 -- True if the predicate has functional depenencies;
547 -- I.e. should participate in improvement
548 predHasFDs (IParam _ _) = True
549 predHasFDs (ClassP cls _) = classHasFDs cls
551 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
552 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
553 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
557 --------------------- Dictionary types ---------------------------------
560 mkClassPred clas tys = ClassP clas tys
562 isClassPred :: SourceType -> Bool
563 isClassPred (ClassP clas tys) = True
564 isClassPred other = False
566 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
567 isTyVarClassPred other = False
569 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
570 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
571 getClassPredTys_maybe _ = Nothing
573 getClassPredTys :: PredType -> (Class, [Type])
574 getClassPredTys (ClassP clas tys) = (clas, tys)
576 mkDictTy :: Class -> [Type] -> Type
577 mkDictTy clas tys = mkPredTy (ClassP clas tys)
579 isDictTy :: Type -> Bool
580 isDictTy (SourceTy p) = isClassPred p
581 isDictTy (NoteTy _ ty) = isDictTy ty
582 isDictTy other = False
585 --------------------- Implicit parameters ---------------------------------
588 isIPPred :: SourceType -> Bool
589 isIPPred (IParam _ _) = True
590 isIPPred other = False
592 isInheritablePred :: PredType -> Bool
593 -- Can be inherited by a context. For example, consider
594 -- f x = let g y = (?v, y+x)
595 -- in (g 3 with ?v = 8,
597 -- The point is that g's type must be quantifed over ?v:
598 -- g :: (?v :: a) => a -> a
599 -- but it doesn't need to be quantified over the Num a dictionary
600 -- which can be free in g's rhs, and shared by both calls to g
601 isInheritablePred (ClassP _ _) = True
602 isInheritablePred other = False
604 isLinearPred :: TcPredType -> Bool
605 isLinearPred (IParam (Linear n) _) = True
606 isLinearPred other = False
610 %************************************************************************
612 \subsection{Comparison}
614 %************************************************************************
616 Comparison, taking note of newtypes, predicates, etc,
617 But ignoring usage types
620 tcEqType :: Type -> Type -> Bool
621 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
623 tcEqTypes :: [Type] -> [Type] -> Bool
624 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
626 tcEqPred :: PredType -> PredType -> Bool
627 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
630 tcCmpType :: Type -> Type -> Ordering
631 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
633 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
635 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
637 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
640 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
641 -- The "env" maps type variables in ty1 to type variables in ty2
642 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
643 -- we in effect substitute tv2 for tv1 in t1 before continuing
645 -- Look through NoteTy
646 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
647 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
649 -- Deal with equal constructors
650 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
651 Just tv1a -> tv1a `compare` tv2
652 Nothing -> tv1 `compare` tv2
654 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
655 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
656 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
657 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
658 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
660 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
661 cmpTy env (AppTy _ _) (TyVarTy _) = GT
663 cmpTy env (FunTy _ _) (TyVarTy _) = GT
664 cmpTy env (FunTy _ _) (AppTy _ _) = GT
666 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
667 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
668 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
670 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
671 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
672 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
673 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
675 cmpTy env (SourceTy _) t2 = GT
681 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
682 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
683 -- Compare types as well as names for implicit parameters
684 -- This comparison is used exclusively (I think) for the
685 -- finite map built in TcSimplify
686 cmpSourceTy env (IParam _ _) sty = LT
688 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
689 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
690 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
692 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
693 cmpSourceTy env (NType _ _) sty = GT
696 PredTypes are used as a FM key in TcSimplify,
697 so we take the easy path and make them an instance of Ord
700 instance Eq SourceType where { (==) = tcEqPred }
701 instance Ord SourceType where { compare = tcCmpPred }
705 %************************************************************************
707 \subsection{Predicates}
709 %************************************************************************
711 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
713 f :: (?x::Int) => Int -> Int
716 isSigmaTy :: Type -> Bool
717 isSigmaTy (ForAllTy tyvar ty) = True
718 isSigmaTy (FunTy a b) = isPredTy a
719 isSigmaTy (NoteTy n ty) = isSigmaTy ty
722 isOverloadedTy :: Type -> Bool
723 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
724 isOverloadedTy (FunTy a b) = isPredTy a
725 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
726 isOverloadedTy _ = False
730 isFloatTy = is_tc floatTyConKey
731 isDoubleTy = is_tc doubleTyConKey
732 isIntegerTy = is_tc integerTyConKey
733 isIntTy = is_tc intTyConKey
734 isAddrTy = is_tc addrTyConKey
735 isBoolTy = is_tc boolTyConKey
736 isUnitTy = is_tc unitTyConKey
738 is_tc :: Unique -> Type -> Bool
739 -- Newtypes are opaque to this
740 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
741 Just (tc, _) -> uniq == getUnique tc
746 %************************************************************************
750 %************************************************************************
753 deNoteType :: Type -> Type
754 -- Remove synonyms, but not source types
755 deNoteType ty@(TyVarTy tyvar) = ty
756 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
757 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
758 deNoteType (NoteTy _ ty) = deNoteType ty
759 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
760 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
761 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
763 deNoteSourceType :: SourceType -> SourceType
764 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
765 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
766 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
769 Find the free tycons and classes of a type. This is used in the front
773 tyClsNamesOfType :: Type -> NameSet
774 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
775 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
776 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
777 tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
778 tyClsNamesOfType (SourceTy (IParam n ty)) = tyClsNamesOfType ty
779 tyClsNamesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
780 tyClsNamesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` tyClsNamesOfTypes tys
781 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
782 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
783 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
785 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
787 tyClsNamesOfDFunHead :: Type -> NameSet
788 -- Find the free type constructors and classes
789 -- of the head of the dfun instance type
790 -- The 'dfun_head_type' is because of
791 -- instance Foo a => Baz T where ...
792 -- The decl is an orphan if Baz and T are both not locally defined,
793 -- even if Foo *is* locally defined
794 tyClsNamesOfDFunHead dfun_ty
795 = case tcSplitSigmaTy dfun_ty of
796 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
798 classNamesOfTheta :: ThetaType -> [Name]
799 -- Looks just for ClassP things; maybe it should check
800 classNamesOfTheta preds = [ getName c | ClassP c _ <- preds ]
804 %************************************************************************
806 \subsection[TysWiredIn-ext-type]{External types}
808 %************************************************************************
810 The compiler's foreign function interface supports the passing of a
811 restricted set of types as arguments and results (the restricting factor
815 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
816 -- Checks for valid argument type for a 'foreign import'
817 isFFIArgumentTy dflags safety ty
818 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
820 isFFIExternalTy :: Type -> Bool
821 -- Types that are allowed as arguments of a 'foreign export'
822 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
824 isFFIImportResultTy :: DynFlags -> Type -> Bool
825 isFFIImportResultTy dflags ty
826 = checkRepTyCon (legalFIResultTyCon dflags) ty
828 isFFIExportResultTy :: Type -> Bool
829 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
831 isFFIDynArgumentTy :: Type -> Bool
832 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
833 -- or a newtype of either.
834 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
836 isFFIDynResultTy :: Type -> Bool
837 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
838 -- or a newtype of either.
839 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
841 isFFILabelTy :: Type -> Bool
842 -- The type of a foreign label must be Ptr, FunPtr, Addr,
843 -- or a newtype of either.
844 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
846 isFFIDotnetTy :: DynFlags -> Type -> Bool
847 isFFIDotnetTy dflags ty
848 = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
849 (legalFIResultTyCon dflags tc ||
850 isFFIDotnetObjTy ty || isStringTy ty)) ty
852 -- Support String as an argument or result from a .NET FFI call.
854 case tcSplitTyConApp_maybe (repType ty) of
857 case tcSplitTyConApp_maybe (repType arg_ty) of
858 Just (cc,[]) -> cc == charTyCon
862 -- Support String as an argument or result from a .NET FFI call.
863 isFFIDotnetObjTy ty =
865 (_, t_ty) = tcSplitForAllTys ty
867 case tcSplitTyConApp_maybe (repType t_ty) of
868 Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
871 toDNType :: Type -> DNType
873 | isStringTy ty = DNString
874 | isFFIDotnetObjTy ty = DNObject
875 | Just (tc,argTys) <- tcSplitTyConApp_maybe ty =
876 case lookup (getUnique tc) dn_assoc of
879 | tc `hasKey` ioTyConKey -> toDNType (head argTys)
880 | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
882 dn_assoc :: [ (Unique, DNType) ]
883 dn_assoc = [ (unitTyConKey, DNUnit)
884 , (intTyConKey, DNInt)
885 , (int8TyConKey, DNInt8)
886 , (int16TyConKey, DNInt16)
887 , (int32TyConKey, DNInt32)
888 , (int64TyConKey, DNInt64)
889 , (wordTyConKey, DNInt)
890 , (word8TyConKey, DNWord8)
891 , (word16TyConKey, DNWord16)
892 , (word32TyConKey, DNWord32)
893 , (word64TyConKey, DNWord64)
894 , (floatTyConKey, DNFloat)
895 , (doubleTyConKey, DNDouble)
896 , (addrTyConKey, DNPtr)
897 , (ptrTyConKey, DNPtr)
898 , (funPtrTyConKey, DNPtr)
899 , (charTyConKey, DNChar)
900 , (boolTyConKey, DNBool)
903 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
904 -- Look through newtypes
905 -- Non-recursive ones are transparent to splitTyConApp,
906 -- but recursive ones aren't
907 checkRepTyCon check_tc ty
908 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
912 ----------------------------------------------
913 These chaps do the work; they are not exported
914 ----------------------------------------------
917 legalFEArgTyCon :: TyCon -> Bool
918 -- It's illegal to return foreign objects and (mutable)
919 -- bytearrays from a _ccall_ / foreign declaration
920 -- (or be passed them as arguments in foreign exported functions).
922 | isByteArrayLikeTyCon tc
924 -- It's also illegal to make foreign exports that take unboxed
925 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
927 = boxedMarshalableTyCon tc
929 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
930 legalFIResultTyCon dflags tc
931 | isByteArrayLikeTyCon tc = False
932 | tc == unitTyCon = True
933 | otherwise = marshalableTyCon dflags tc
935 legalFEResultTyCon :: TyCon -> Bool
936 legalFEResultTyCon tc
937 | isByteArrayLikeTyCon tc = False
938 | tc == unitTyCon = True
939 | otherwise = boxedMarshalableTyCon tc
941 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
942 -- Checks validity of types going from Haskell -> external world
943 legalOutgoingTyCon dflags safety tc
944 | playSafe safety && isByteArrayLikeTyCon tc
947 = marshalableTyCon dflags tc
949 marshalableTyCon dflags tc
950 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
951 || boxedMarshalableTyCon tc
953 boxedMarshalableTyCon tc
954 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
955 , int32TyConKey, int64TyConKey
956 , wordTyConKey, word8TyConKey, word16TyConKey
957 , word32TyConKey, word64TyConKey
958 , floatTyConKey, doubleTyConKey
959 , addrTyConKey, ptrTyConKey, funPtrTyConKey
962 , byteArrayTyConKey, mutableByteArrayTyConKey
966 isByteArrayLikeTyCon :: TyCon -> Bool
967 isByteArrayLikeTyCon tc =
968 getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
972 %************************************************************************
974 \subsection{Unification with an explicit substitution}
976 %************************************************************************
978 Unify types with an explicit substitution and no monad.
979 Ignore usage annotations.
983 = (TyVarSet, -- Set of template tyvars
984 TyVarSubstEnv) -- Not necessarily idempotent
986 unifyTysX :: TyVarSet -- Template tyvars
989 -> Maybe TyVarSubstEnv
990 unifyTysX tmpl_tyvars ty1 ty2
991 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
993 unifyExtendTysX :: TyVarSet -- Template tyvars
994 -> TyVarSubstEnv -- Substitution to start with
997 -> Maybe TyVarSubstEnv -- Extended substitution
998 unifyExtendTysX tmpl_tyvars subst ty1 ty2
999 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
1001 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
1002 -> Maybe TyVarSubstEnv
1003 unifyTyListsX tmpl_tyvars tys1 tys2
1004 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
1009 -> (MySubst -> Maybe result)
1013 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
1014 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
1016 -- Variables; go for uVar
1017 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
1020 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
1021 | tyvar1 `elemVarSet` tmpls
1022 = uVarX tyvar1 ty2 k subst
1023 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
1024 | tyvar2 `elemVarSet` tmpls
1025 = uVarX tyvar2 ty1 k subst
1028 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
1029 | n1 == n2 = uTysX t1 t2 k subst
1030 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
1031 | c1 == c2 = uTyListsX tys1 tys2 k subst
1032 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
1033 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
1035 -- Functions; just check the two parts
1036 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
1037 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
1039 -- Type constructors must match
1040 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
1041 | (con1 == con2 && equalLength tys1 tys2)
1042 = uTyListsX tys1 tys2 k subst
1044 -- Applications need a bit of care!
1045 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1046 -- NB: we've already dealt with type variables and Notes,
1047 -- so if one type is an App the other one jolly well better be too
1048 uTysX (AppTy s1 t1) ty2 k subst
1049 = case tcSplitAppTy_maybe ty2 of
1050 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1051 Nothing -> Nothing -- Fail
1053 uTysX ty1 (AppTy s2 t2) k subst
1054 = case tcSplitAppTy_maybe ty1 of
1055 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1056 Nothing -> Nothing -- Fail
1058 -- Not expecting for-alls in unification
1060 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
1061 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1064 -- Anything else fails
1065 uTysX ty1 ty2 k subst = Nothing
1068 uTyListsX [] [] k subst = k subst
1069 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1070 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1074 -- Invariant: tv1 is a unifiable variable
1075 uVarX tv1 ty2 k subst@(tmpls, env)
1076 = case lookupSubstEnv env tv1 of
1077 Just (DoneTy ty1) -> -- Already bound
1078 uTysX ty1 ty2 k subst
1080 Nothing -- Not already bound
1081 | typeKind ty2 `eqKind` tyVarKind tv1
1082 && occur_check_ok ty2
1083 -> -- No kind mismatch nor occur check
1084 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1086 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1088 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1089 occur_check_ok_tv tv | tv1 == tv = False
1090 | otherwise = case lookupSubstEnv env tv of
1092 Just (DoneTy ty) -> occur_check_ok ty
1097 %************************************************************************
1099 \subsection{Matching on types}
1101 %************************************************************************
1103 Matching is a {\em unidirectional} process, matching a type against a
1104 template (which is just a type with type variables in it). The
1105 matcher assumes that there are no repeated type variables in the
1106 template, so that it simply returns a mapping of type variables to
1107 types. It also fails on nested foralls.
1109 @matchTys@ matches corresponding elements of a list of templates and
1110 types. It and @matchTy@ both ignore usage annotations, unlike the
1111 main function @match@.
1114 matchTy :: TyVarSet -- Template tyvars
1116 -> Type -- Proposed instance of template
1117 -> Maybe TyVarSubstEnv -- Matching substitution
1120 matchTys :: TyVarSet -- Template tyvars
1121 -> [Type] -- Templates
1122 -> [Type] -- Proposed instance of template
1123 -> Maybe (TyVarSubstEnv, -- Matching substitution
1124 [Type]) -- Left over instance types
1126 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1128 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1129 (\ (senv,tys) -> Just (senv,tys))
1133 @match@ is the main function. It takes a flag indicating whether
1134 usage annotations are to be respected.
1137 match :: Type -> Type -- Current match pair
1138 -> TyVarSet -- Template vars
1139 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1140 -> TyVarSubstEnv -- Current subst
1143 -- When matching against a type variable, see if the variable
1144 -- has already been bound. If so, check that what it's bound to
1145 -- is the same as ty; if not, bind it and carry on.
1147 match (TyVarTy v) ty tmpls k senv
1148 | v `elemVarSet` tmpls
1149 = -- v is a template variable
1150 case lookupSubstEnv senv v of
1151 Nothing | typeKind ty `eqKind` tyVarKind v
1152 -- We do a kind check, just as in the uVarX above
1153 -- The kind check is needed to avoid bogus matches
1154 -- of (a b) with (c d), where the kinds don't match
1155 -- An occur check isn't needed when matching.
1156 -> k (extendSubstEnv senv v (DoneTy ty))
1158 | otherwise -> Nothing -- Fails
1160 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1161 | otherwise -> Nothing -- Fails
1164 = -- v is not a template variable; ty had better match
1165 -- Can't use (==) because types differ
1166 case tcGetTyVar_maybe ty of
1167 Just v' | v == v' -> k senv -- Success
1168 other -> Nothing -- Failure
1169 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1170 -- I guess the reason the Note-stripping case is *last* rather than first
1171 -- is to preserve type synonyms etc., so I'm not moving it to the
1172 -- top; but this means that (without the deNotetype) a type
1173 -- variable may not match the pattern (TyVarTy v') as one would
1174 -- expect, due to an intervening Note. KSW 2000-06.
1177 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1178 | n1 == n2 = match t1 t2 tmpls k senv
1179 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1180 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1181 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1182 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1184 -- Functions; just check the two parts
1185 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1186 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1188 match (AppTy fun1 arg1) ty2 tmpls k senv
1189 = case tcSplitAppTy_maybe ty2 of
1190 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1191 Nothing -> Nothing -- Fail
1193 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1194 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1196 -- Newtypes are opaque; other source types should not happen
1197 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1198 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1200 -- With type synonyms, we have to be careful for the exact
1201 -- same reasons as in the unifier. Please see the
1202 -- considerable commentary there before changing anything
1203 -- here! (WDP 95/05)
1204 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1205 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1208 match _ _ _ _ _ = Nothing
1210 match_list_exactly tys1 tys2 tmpls k senv
1211 = match_list tys1 tys2 tmpls k' senv
1213 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1214 | otherwise = Nothing -- Fail
1216 match_list [] tys2 tmpls k senv = k (senv, tys2)
1217 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1218 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1219 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv