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,
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 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 = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
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 = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
834 isFFILabelTy :: Type -> Bool
835 -- The type of a foreign label must be Ptr, FunPtr, Addr,
836 -- or a newtype of either.
837 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
839 isFFIDotnetTy :: DynFlags -> Type -> Bool
840 isFFIDotnetTy dflags ty
841 = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
842 (legalFIResultTyCon dflags tc ||
843 isFFIDotnetObjTy ty || isStringTy ty)) ty
845 -- Support String as an argument or result from a .NET FFI call.
847 case tcSplitTyConApp_maybe (repType ty) of
850 case tcSplitTyConApp_maybe (repType arg_ty) of
851 Just (cc,[]) -> cc == charTyCon
855 -- Support String as an argument or result from a .NET FFI call.
856 isFFIDotnetObjTy ty =
858 (_, t_ty) = tcSplitForAllTys ty
860 case tcSplitTyConApp_maybe (repType t_ty) of
861 Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
864 toDNType :: Type -> DNType
866 | isStringTy ty = DNString
867 | isFFIDotnetObjTy ty = DNObject
868 | Just (tc,argTys) <- tcSplitTyConApp_maybe ty =
869 case lookup (getUnique tc) dn_assoc of
872 | tc `hasKey` ioTyConKey -> toDNType (head argTys)
873 | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
875 dn_assoc :: [ (Unique, DNType) ]
876 dn_assoc = [ (unitTyConKey, DNUnit)
877 , (intTyConKey, DNInt)
878 , (int8TyConKey, DNInt8)
879 , (int16TyConKey, DNInt16)
880 , (int32TyConKey, DNInt32)
881 , (int64TyConKey, DNInt64)
882 , (wordTyConKey, DNInt)
883 , (word8TyConKey, DNWord8)
884 , (word16TyConKey, DNWord16)
885 , (word32TyConKey, DNWord32)
886 , (word64TyConKey, DNWord64)
887 , (floatTyConKey, DNFloat)
888 , (doubleTyConKey, DNDouble)
889 , (addrTyConKey, DNPtr)
890 , (ptrTyConKey, DNPtr)
891 , (funPtrTyConKey, DNPtr)
892 , (charTyConKey, DNChar)
893 , (boolTyConKey, DNBool)
896 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
897 -- Look through newtypes
898 -- Non-recursive ones are transparent to splitTyConApp,
899 -- but recursive ones aren't
900 checkRepTyCon check_tc ty
901 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
904 checkRepTyConKey :: [Unique] -> Type -> Bool
905 -- Like checkRepTyCon, but just looks at the TyCon key
906 checkRepTyConKey keys
907 = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
910 ----------------------------------------------
911 These chaps do the work; they are not exported
912 ----------------------------------------------
915 legalFEArgTyCon :: TyCon -> Bool
916 -- It's illegal to return foreign objects and (mutable)
917 -- bytearrays from a _ccall_ / foreign declaration
918 -- (or be passed them as arguments in foreign exported functions).
920 | isByteArrayLikeTyCon tc
922 -- It's also illegal to make foreign exports that take unboxed
923 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
925 = boxedMarshalableTyCon tc
927 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
928 legalFIResultTyCon dflags tc
929 | isByteArrayLikeTyCon tc = False
930 | tc == unitTyCon = True
931 | otherwise = marshalableTyCon dflags tc
933 legalFEResultTyCon :: TyCon -> Bool
934 legalFEResultTyCon tc
935 | isByteArrayLikeTyCon tc = False
936 | tc == unitTyCon = True
937 | otherwise = boxedMarshalableTyCon tc
939 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
940 -- Checks validity of types going from Haskell -> external world
941 legalOutgoingTyCon dflags safety tc
942 | playSafe safety && isByteArrayLikeTyCon tc
945 = marshalableTyCon dflags tc
947 marshalableTyCon dflags tc
948 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
949 || boxedMarshalableTyCon tc
951 boxedMarshalableTyCon tc
952 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
953 , int32TyConKey, int64TyConKey
954 , wordTyConKey, word8TyConKey, word16TyConKey
955 , word32TyConKey, word64TyConKey
956 , floatTyConKey, doubleTyConKey
957 , addrTyConKey, ptrTyConKey, funPtrTyConKey
960 , byteArrayTyConKey, mutableByteArrayTyConKey
964 isByteArrayLikeTyCon :: TyCon -> Bool
965 isByteArrayLikeTyCon tc =
966 getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
970 %************************************************************************
972 \subsection{Unification with an explicit substitution}
974 %************************************************************************
976 Unify types with an explicit substitution and no monad.
977 Ignore usage annotations.
981 = (TyVarSet, -- Set of template tyvars
982 TyVarSubstEnv) -- Not necessarily idempotent
984 unifyTysX :: TyVarSet -- Template tyvars
987 -> Maybe TyVarSubstEnv
988 unifyTysX tmpl_tyvars ty1 ty2
989 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
991 unifyExtendTysX :: TyVarSet -- Template tyvars
992 -> TyVarSubstEnv -- Substitution to start with
995 -> Maybe TyVarSubstEnv -- Extended substitution
996 unifyExtendTysX tmpl_tyvars subst ty1 ty2
997 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
999 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
1000 -> Maybe TyVarSubstEnv
1001 unifyTyListsX tmpl_tyvars tys1 tys2
1002 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
1007 -> (MySubst -> Maybe result)
1011 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
1012 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
1014 -- Variables; go for uVar
1015 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
1018 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
1019 | tyvar1 `elemVarSet` tmpls
1020 = uVarX tyvar1 ty2 k subst
1021 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
1022 | tyvar2 `elemVarSet` tmpls
1023 = uVarX tyvar2 ty1 k subst
1026 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
1027 | n1 == n2 = uTysX t1 t2 k subst
1028 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
1029 | c1 == c2 = uTyListsX tys1 tys2 k subst
1030 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
1031 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
1033 -- Functions; just check the two parts
1034 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
1035 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
1037 -- Type constructors must match
1038 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
1039 | (con1 == con2 && equalLength tys1 tys2)
1040 = uTyListsX tys1 tys2 k subst
1042 -- Applications need a bit of care!
1043 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1044 -- NB: we've already dealt with type variables and Notes,
1045 -- so if one type is an App the other one jolly well better be too
1046 uTysX (AppTy s1 t1) ty2 k subst
1047 = case tcSplitAppTy_maybe ty2 of
1048 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1049 Nothing -> Nothing -- Fail
1051 uTysX ty1 (AppTy s2 t2) k subst
1052 = case tcSplitAppTy_maybe ty1 of
1053 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1054 Nothing -> Nothing -- Fail
1056 -- Not expecting for-alls in unification
1058 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
1059 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1062 -- Anything else fails
1063 uTysX ty1 ty2 k subst = Nothing
1066 uTyListsX [] [] k subst = k subst
1067 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1068 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1072 -- Invariant: tv1 is a unifiable variable
1073 uVarX tv1 ty2 k subst@(tmpls, env)
1074 = case lookupSubstEnv env tv1 of
1075 Just (DoneTy ty1) -> -- Already bound
1076 uTysX ty1 ty2 k subst
1078 Nothing -- Not already bound
1079 | typeKind ty2 `eqKind` tyVarKind tv1
1080 && occur_check_ok ty2
1081 -> -- No kind mismatch nor occur check
1082 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1084 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1086 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1087 occur_check_ok_tv tv | tv1 == tv = False
1088 | otherwise = case lookupSubstEnv env tv of
1090 Just (DoneTy ty) -> occur_check_ok ty
1095 %************************************************************************
1097 \subsection{Matching on types}
1099 %************************************************************************
1101 Matching is a {\em unidirectional} process, matching a type against a
1102 template (which is just a type with type variables in it). The
1103 matcher assumes that there are no repeated type variables in the
1104 template, so that it simply returns a mapping of type variables to
1105 types. It also fails on nested foralls.
1107 @matchTys@ matches corresponding elements of a list of templates and
1108 types. It and @matchTy@ both ignore usage annotations, unlike the
1109 main function @match@.
1112 matchTy :: TyVarSet -- Template tyvars
1114 -> Type -- Proposed instance of template
1115 -> Maybe TyVarSubstEnv -- Matching substitution
1118 matchTys :: TyVarSet -- Template tyvars
1119 -> [Type] -- Templates
1120 -> [Type] -- Proposed instance of template
1121 -> Maybe (TyVarSubstEnv, -- Matching substitution
1122 [Type]) -- Left over instance types
1124 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1126 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1127 (\ (senv,tys) -> Just (senv,tys))
1131 @match@ is the main function. It takes a flag indicating whether
1132 usage annotations are to be respected.
1135 match :: Type -> Type -- Current match pair
1136 -> TyVarSet -- Template vars
1137 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1138 -> TyVarSubstEnv -- Current subst
1141 -- When matching against a type variable, see if the variable
1142 -- has already been bound. If so, check that what it's bound to
1143 -- is the same as ty; if not, bind it and carry on.
1145 match (TyVarTy v) ty tmpls k senv
1146 | v `elemVarSet` tmpls
1147 = -- v is a template variable
1148 case lookupSubstEnv senv v of
1149 Nothing | typeKind ty `eqKind` tyVarKind v
1150 -- We do a kind check, just as in the uVarX above
1151 -- The kind check is needed to avoid bogus matches
1152 -- of (a b) with (c d), where the kinds don't match
1153 -- An occur check isn't needed when matching.
1154 -> k (extendSubstEnv senv v (DoneTy ty))
1156 | otherwise -> Nothing -- Fails
1158 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1159 | otherwise -> Nothing -- Fails
1162 = -- v is not a template variable; ty had better match
1163 -- Can't use (==) because types differ
1164 case tcGetTyVar_maybe ty of
1165 Just v' | v == v' -> k senv -- Success
1166 other -> Nothing -- Failure
1167 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1168 -- I guess the reason the Note-stripping case is *last* rather than first
1169 -- is to preserve type synonyms etc., so I'm not moving it to the
1170 -- top; but this means that (without the deNotetype) a type
1171 -- variable may not match the pattern (TyVarTy v') as one would
1172 -- expect, due to an intervening Note. KSW 2000-06.
1175 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1176 | n1 == n2 = match t1 t2 tmpls k senv
1177 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1178 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1179 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1180 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1182 -- Functions; just check the two parts
1183 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1184 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1186 match (AppTy fun1 arg1) ty2 tmpls k senv
1187 = case tcSplitAppTy_maybe ty2 of
1188 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1189 Nothing -> Nothing -- Fail
1191 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1192 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1194 -- Newtypes are opaque; other source types should not happen
1195 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1196 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1198 -- With type synonyms, we have to be careful for the exact
1199 -- same reasons as in the unifier. Please see the
1200 -- considerable commentary there before changing anything
1201 -- here! (WDP 95/05)
1202 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1203 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1206 match _ _ _ _ _ = Nothing
1208 match_list_exactly tys1 tys2 tmpls k senv
1209 = match_list tys1 tys2 tmpls k' senv
1211 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1212 | otherwise = Nothing -- Fail
1214 match_list [] tys2 tmpls k senv = k (senv, tys2)
1215 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1216 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1217 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv