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 TcType, TcTauType, TcPredType, TcThetaType, TcRhoType,
21 TcTyVar, TcTyVarSet, TcKind,
23 --------------------------------
25 TyVarDetails(..), isUserTyVar, isSkolemTyVar,
27 --------------------------------
31 --------------------------------
33 -- These are important because they do not look through newtypes
34 tcSplitForAllTys, tcSplitRhoTy,
35 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
36 tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
37 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitSigmaTy,
38 tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
40 ---------------------------------
42 -- Again, newtypes are opaque
43 tcEqType, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
44 isQualifiedTy, isOverloadedTy,
45 isDoubleTy, isFloatTy, isIntTy,
46 isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy,
47 isTauTy, tcIsTyVarTy, tcIsForAllTy,
49 ---------------------------------
50 -- Misc type manipulators
51 hoistForAllTys, deNoteType,
52 namesOfType, namesOfDFunHead,
55 ---------------------------------
57 PredType, getClassPredTys_maybe, getClassPredTys,
58 isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
59 mkDictTy, tcSplitPredTy_maybe, predTyUnique,
60 isDictTy, tcSplitDFunTy, predTyUnique,
61 mkClassPred, inheritablePred, isIPPred, mkPredName,
63 ---------------------------------
64 -- Foreign import and export
65 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
66 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
67 isFFIExportResultTy, -- :: Type -> Bool
68 isFFIExternalTy, -- :: Type -> Bool
69 isFFIDynArgumentTy, -- :: Type -> Bool
70 isFFIDynResultTy, -- :: Type -> Bool
71 isFFILabelTy, -- :: Type -> Bool
73 ---------------------------------
74 -- Unifier and matcher
75 unifyTysX, unifyTyListsX, unifyExtendTysX,
77 matchTy, matchTys, match,
79 --------------------------------
80 -- Rexported from Type
81 Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
82 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
83 superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
86 Type, SourceType(..), PredType, ThetaType,
87 mkForAllTy, mkForAllTys,
88 mkFunTy, mkFunTys, zipFunTys,
89 mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
90 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
92 isUnLiftedType, -- Source types are always lifted
93 isUnboxedTupleType, -- Ditto
96 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
97 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
98 typeKind, eqKind, eqUsage,
100 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
103 #include "HsVersions.h"
106 import {-# SOURCE #-} PprType( pprType )
109 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
110 import Type ( mkUTyM, unUTy ) -- Used locally
112 import Type ( -- Re-exports
113 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
114 Kind, Type, TauType, SourceType(..), PredType, ThetaType,
115 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
116 mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
117 mkFunTy, mkFunTys, zipFunTys,
118 mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
119 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
120 isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
121 splitNewType_maybe, splitTyConApp_maybe,
122 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
123 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
124 hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
126 import TyCon ( TyCon, isUnLiftedTyCon )
127 import Class ( classHasFDs, Class )
128 import Var ( TyVar, tyVarKind )
129 import ForeignCall ( Safety, playSafe )
134 import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
135 import Name ( Name, NamedThing(..), mkLocalName )
136 import OccName ( OccName, mkDictOcc )
138 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
139 import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
140 import Unique ( Unique, Uniquable(..) )
141 import SrcLoc ( SrcLoc )
142 import Util ( cmpList, thenCmp, equalLength )
143 import Maybes ( maybeToBool, expectJust )
148 %************************************************************************
152 %************************************************************************
155 type TcTyVar = TyVar -- Might be a mutable tyvar
156 type TcTyVarSet = TyVarSet
158 type TcType = Type -- A TcType can have mutable type variables
159 -- Invariant on ForAllTy in TcTypes:
161 -- a cannot occur inside a MutTyVar in T; that is,
162 -- T is "flattened" before quantifying over a
164 type TcPredType = PredType
165 type TcThetaType = ThetaType
166 type TcRhoType = Type
167 type TcTauType = TauType
172 %************************************************************************
174 \subsection{TyVarDetails}
176 %************************************************************************
178 TyVarDetails gives extra info about type variables, used during type
179 checking. It's attached to mutable type variables only.
180 It's knot-tied back to Var.lhs. There is no reason in principle
181 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
185 = SigTv -- Introduced when instantiating a type signature,
186 -- prior to checking that the defn of a fn does
187 -- have the expected type. Should not be instantiated.
189 -- f :: forall a. a -> a
191 -- When checking e, with expected type (a->a), we
192 -- should not instantiate a
194 | ClsTv -- Scoped type variable introduced by a class decl
195 -- class C a where ...
197 | InstTv -- Ditto, but instance decl
199 | PatSigTv -- Scoped type variable, introduced by a pattern
203 | VanillaTv -- Everything else
205 isUserTyVar :: TyVarDetails -> Bool -- Avoid unifying these if possible
206 isUserTyVar VanillaTv = False
207 isUserTyVar other = True
209 isSkolemTyVar :: TyVarDetails -> Bool
210 isSkolemTyVar SigTv = True
211 isSkolemTyVar other = False
213 instance Outputable TyVarDetails where
214 ppr SigTv = ptext SLIT("type signature")
215 ppr ClsTv = ptext SLIT("class declaration")
216 ppr InstTv = ptext SLIT("instance declaration")
217 ppr PatSigTv = ptext SLIT("pattern type signature")
218 ppr VanillaTv = ptext SLIT("???")
222 %************************************************************************
224 \subsection{Tau, sigma and rho}
226 %************************************************************************
229 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
231 mkRhoTy :: [SourceType] -> Type -> Type
232 mkRhoTy theta ty = UASSERT2( not (isUTy ty), pprType ty )
233 foldr (\p r -> FunTy (mkUTyM (mkPredTy p)) (mkUTyM r)) ty theta
238 @isTauTy@ tests for nested for-alls.
241 isTauTy :: Type -> Bool
242 isTauTy (TyVarTy v) = True
243 isTauTy (TyConApp _ tys) = all isTauTy tys
244 isTauTy (AppTy a b) = isTauTy a && isTauTy b
245 isTauTy (FunTy a b) = isTauTy a && isTauTy b
246 isTauTy (SourceTy p) = True -- Don't look through source types
247 isTauTy (NoteTy _ ty) = isTauTy ty
248 isTauTy (UsageTy _ ty) = isTauTy ty
249 isTauTy other = False
253 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
254 -- construct a dictionary function name
255 getDFunTyKey (TyVarTy tv) = getOccName tv
256 getDFunTyKey (TyConApp tc _) = getOccName tc
257 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
258 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
259 getDFunTyKey (FunTy arg _) = getOccName funTyCon
260 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
261 getDFunTyKey (UsageTy _ t) = getDFunTyKey t
262 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
263 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
264 -- SourceTy shouldn't happen
268 %************************************************************************
270 \subsection{Expanding and splitting}
272 %************************************************************************
274 These tcSplit functions are like their non-Tc analogues, but
275 a) they do not look through newtypes
276 b) they do not look through PredTys
277 c) [future] they ignore usage-type annotations
279 However, they are non-monadic and do not follow through mutable type
280 variables. It's up to you to make sure this doesn't matter.
283 tcSplitForAllTys :: Type -> ([TyVar], Type)
284 tcSplitForAllTys ty = split ty ty []
286 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
287 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
288 split orig_ty (UsageTy _ ty) tvs = split orig_ty ty tvs
289 split orig_ty t tvs = (reverse tvs, orig_ty)
291 tcIsForAllTy (ForAllTy tv ty) = True
292 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
293 tcIsForAllTy (UsageTy n ty) = tcIsForAllTy ty
294 tcIsForAllTy t = False
296 tcSplitRhoTy :: Type -> ([PredType], Type)
297 tcSplitRhoTy ty = split ty ty []
299 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
300 Just p -> split res res (p:ts)
301 Nothing -> (reverse ts, orig_ty)
302 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
303 split orig_ty (UsageTy _ ty) ts = split orig_ty ty ts
304 split orig_ty ty ts = (reverse ts, orig_ty)
306 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
307 (tvs, rho) -> case tcSplitRhoTy rho of
308 (theta, tau) -> (tvs, theta, tau)
310 tcTyConAppTyCon :: Type -> TyCon
311 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
313 tcTyConAppArgs :: Type -> [Type]
314 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
316 tcSplitTyConApp :: Type -> (TyCon, [Type])
317 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
319 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
321 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
322 -- Newtypes are opaque, so they may be split
323 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
324 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [unUTy arg,unUTy res])
325 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
326 tcSplitTyConApp_maybe (UsageTy _ ty) = tcSplitTyConApp_maybe ty
327 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
328 -- However, predicates are not treated
329 -- as tycon applications by the type checker
330 tcSplitTyConApp_maybe other = Nothing
332 tcSplitFunTys :: Type -> ([Type], Type)
333 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
335 Just (arg,res) -> (arg:args, res')
337 (args,res') = tcSplitFunTys res
339 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
340 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
341 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
342 tcSplitFunTy_maybe (UsageTy _ ty) = tcSplitFunTy_maybe ty
343 tcSplitFunTy_maybe other = Nothing
345 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
346 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
349 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
350 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2)
351 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
352 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
353 tcSplitAppTy_maybe (UsageTy _ ty) = tcSplitAppTy_maybe ty
354 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
355 --- Don't forget that newtype!
356 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
357 tcSplitAppTy_maybe other = Nothing
359 tc_split_app tc [] = Nothing
360 tc_split_app tc tys = split tys []
362 split [ty2] acc = Just (TyConApp tc (reverse acc), ty2)
363 split (ty:tys) acc = split tys (ty:acc)
365 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
367 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
369 tcGetTyVar_maybe :: Type -> Maybe TyVar
370 tcGetTyVar_maybe (TyVarTy tv) = Just tv
371 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
372 tcGetTyVar_maybe ty@(UsageTy _ _) = pprPanic "tcGetTyVar_maybe: UTy:" (pprType ty)
373 tcGetTyVar_maybe other = Nothing
375 tcGetTyVar :: String -> Type -> TyVar
376 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
378 tcIsTyVarTy :: Type -> Bool
379 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
382 The type of a method for class C is always of the form:
383 Forall a1..an. C a1..an => sig_ty
384 where sig_ty is the type given by the method's signature, and thus in general
385 is a ForallTy. At the point that splitMethodTy is called, it is expected
386 that the outer Forall has already been stripped off. splitMethodTy then
387 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
391 tcSplitMethodTy :: Type -> (PredType, Type)
392 tcSplitMethodTy ty = split ty
394 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
396 Nothing -> panic "splitMethodTy"
397 split (NoteTy n ty) = split ty
398 split (UsageTy _ ty) = split ty
399 split _ = panic "splitMethodTy"
401 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
402 -- Split the type of a dictionary function
404 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
405 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
406 (tvs, theta, clas, tys) }}
410 %************************************************************************
412 \subsection{Predicate types}
414 %************************************************************************
416 "Predicates" are particular source types, namelyClassP or IParams
419 isPred :: SourceType -> Bool
420 isPred (ClassP _ _) = True
421 isPred (IParam _ _) = True
422 isPred (NType _ __) = False
424 isPredTy :: Type -> Bool
425 isPredTy (NoteTy _ ty) = isPredTy ty
426 isPredTy (UsageTy _ ty) = isPredTy ty
427 isPredTy (SourceTy sty) = isPred sty
430 tcSplitPredTy_maybe :: Type -> Maybe PredType
431 -- Returns Just for predicates only
432 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
433 tcSplitPredTy_maybe (UsageTy _ ty) = tcSplitPredTy_maybe ty
434 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
435 tcSplitPredTy_maybe other = Nothing
437 predTyUnique :: PredType -> Unique
438 predTyUnique (IParam n _) = getUnique n
439 predTyUnique (ClassP clas tys) = getUnique clas
441 predHasFDs :: PredType -> Bool
442 -- True if the predicate has functional depenencies;
443 -- I.e. should participate in improvement
444 predHasFDs (IParam _ _) = True
445 predHasFDs (ClassP cls _) = classHasFDs cls
447 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
448 mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
449 mkPredName uniq loc (IParam name ty) = name
453 --------------------- Dictionary types ---------------------------------
456 mkClassPred clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
459 isClassPred :: SourceType -> Bool
460 isClassPred (ClassP clas tys) = True
461 isClassPred other = False
463 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
464 isTyVarClassPred other = False
466 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
467 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
468 getClassPredTys_maybe _ = Nothing
470 getClassPredTys :: PredType -> (Class, [Type])
471 getClassPredTys (ClassP clas tys) = (clas, tys)
473 mkDictTy :: Class -> [Type] -> Type
474 mkDictTy clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
475 mkPredTy (ClassP clas tys)
477 isDictTy :: Type -> Bool
478 isDictTy (SourceTy p) = isClassPred p
479 isDictTy (NoteTy _ ty) = isDictTy ty
480 isDictTy (UsageTy _ ty) = isDictTy ty
481 isDictTy other = False
484 --------------------- Implicit parameters ---------------------------------
487 isIPPred :: SourceType -> Bool
488 isIPPred (IParam _ _) = True
489 isIPPred other = False
491 inheritablePred :: PredType -> Bool
492 -- Can be inherited by a context. For example, consider
493 -- f x = let g y = (?v, y+x)
494 -- in (g 3 with ?v = 8,
496 -- The point is that g's type must be quantifed over ?v:
497 -- g :: (?v :: a) => a -> a
498 -- but it doesn't need to be quantified over the Num a dictionary
499 -- which can be free in g's rhs, and shared by both calls to g
500 inheritablePred (ClassP _ _) = True
501 inheritablePred other = False
505 %************************************************************************
507 \subsection{Comparison}
509 %************************************************************************
511 Comparison, taking note of newtypes, predicates, etc,
512 But ignoring usage types
515 tcEqType :: Type -> Type -> Bool
516 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
518 tcEqPred :: PredType -> PredType -> Bool
519 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
522 tcCmpType :: Type -> Type -> Ordering
523 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
525 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
527 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
529 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
532 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
533 -- The "env" maps type variables in ty1 to type variables in ty2
534 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
535 -- we in effect substitute tv2 for tv1 in t1 before continuing
537 -- Look through NoteTy and UsageTy
538 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
539 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
540 cmpTy env (UsageTy _ ty1) ty2 = cmpTy env ty1 ty2
541 cmpTy env ty1 (UsageTy _ ty2) = cmpTy env ty1 ty2
543 -- Deal with equal constructors
544 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
545 Just tv1a -> tv1a `compare` tv2
546 Nothing -> tv1 `compare` tv2
548 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
549 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
550 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
551 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
552 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
554 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
555 cmpTy env (AppTy _ _) (TyVarTy _) = GT
557 cmpTy env (FunTy _ _) (TyVarTy _) = GT
558 cmpTy env (FunTy _ _) (AppTy _ _) = GT
560 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
561 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
562 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
564 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
565 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
566 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
567 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
569 cmpTy env (SourceTy _) t2 = GT
575 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
576 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
577 -- Compare types as well as names for implicit parameters
578 -- This comparison is used exclusively (I think) for the
579 -- finite map built in TcSimplify
580 cmpSourceTy env (IParam _ _) sty = LT
582 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
583 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
584 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
586 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
587 cmpSourceTy env (NType _ _) sty = GT
590 PredTypes are used as a FM key in TcSimplify,
591 so we take the easy path and make them an instance of Ord
594 instance Eq SourceType where { (==) = tcEqPred }
595 instance Ord SourceType where { compare = tcCmpPred }
599 %************************************************************************
601 \subsection{Predicates}
603 %************************************************************************
605 isQualifiedTy returns true of any qualified type. It doesn't *necessarily* have
607 f :: (?x::Int) => Int -> Int
610 isQualifiedTy :: Type -> Bool
611 isQualifiedTy (ForAllTy tyvar ty) = True
612 isQualifiedTy (FunTy a b) = isPredTy a
613 isQualifiedTy (NoteTy n ty) = isQualifiedTy ty
614 isQualifiedTy (UsageTy _ ty) = isQualifiedTy ty
615 isQualifiedTy _ = False
617 isOverloadedTy :: Type -> Bool
618 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
619 isOverloadedTy (FunTy a b) = isPredTy a
620 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
621 isOverloadedTy (UsageTy _ ty) = isOverloadedTy ty
622 isOverloadedTy _ = False
626 isFloatTy = is_tc floatTyConKey
627 isDoubleTy = is_tc doubleTyConKey
628 isForeignPtrTy = is_tc foreignPtrTyConKey
629 isIntegerTy = is_tc integerTyConKey
630 isIntTy = is_tc intTyConKey
631 isAddrTy = is_tc addrTyConKey
632 isBoolTy = is_tc boolTyConKey
633 isUnitTy = is_tc unitTyConKey
635 is_tc :: Unique -> Type -> Bool
636 -- Newtypes are opaque to this
637 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
638 Just (tc, _) -> uniq == getUnique tc
643 %************************************************************************
647 %************************************************************************
650 hoistForAllTys :: Type -> Type
651 -- Move all the foralls to the top
652 -- e.g. T -> forall a. a ==> forall a. T -> a
653 -- Careful: LOSES USAGE ANNOTATIONS!
655 = case hoist ty of { (tvs, body) -> mkForAllTys tvs body }
657 hoist :: Type -> ([TyVar], Type)
658 hoist ty = case tcSplitFunTys ty of { (args, res) ->
659 case tcSplitForAllTys res of {
660 ([], body) -> ([], ty) ;
661 (tvs1, body1) -> case hoist body1 of { (tvs2,body2) ->
662 (tvs1 ++ tvs2, mkFunTys args body2)
668 deNoteType :: Type -> Type
669 -- Remove synonyms, but not source types
670 deNoteType ty@(TyVarTy tyvar) = ty
671 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
672 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
673 deNoteType (NoteTy _ ty) = deNoteType ty
674 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
675 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
676 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
677 deNoteType (UsageTy u ty) = UsageTy u (deNoteType ty)
679 deNoteSourceType :: SourceType -> SourceType
680 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
681 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
682 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
685 Find the free names of a type, including the type constructors and classes it mentions
686 This is used in the front end of the compiler
689 namesOfType :: Type -> NameSet
690 namesOfType (TyVarTy tv) = unitNameSet (getName tv)
691 namesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
692 namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
693 namesOfType (NoteTy other_note ty2) = namesOfType ty2
694 namesOfType (SourceTy (IParam n ty)) = namesOfType ty
695 namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
696 namesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
697 namesOfType (FunTy arg res) = namesOfType arg `unionNameSets` namesOfType res
698 namesOfType (AppTy fun arg) = namesOfType fun `unionNameSets` namesOfType arg
699 namesOfType (ForAllTy tyvar ty) = namesOfType ty `delFromNameSet` getName tyvar
700 namesOfType (UsageTy u ty) = namesOfType u `unionNameSets` namesOfType ty
702 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
704 namesOfDFunHead :: Type -> NameSet
705 -- Find the free type constructors and classes
706 -- of the head of the dfun instance type
707 -- The 'dfun_head_type' is because of
708 -- instance Foo a => Baz T where ...
709 -- The decl is an orphan if Baz and T are both not locally defined,
710 -- even if Foo *is* locally defined
711 namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
712 (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
717 %************************************************************************
719 \subsection[TysWiredIn-ext-type]{External types}
721 %************************************************************************
723 The compiler's foreign function interface supports the passing of a
724 restricted set of types as arguments and results (the restricting factor
728 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
729 -- Checks for valid argument type for a 'foreign import'
730 isFFIArgumentTy dflags safety ty
731 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
733 isFFIExternalTy :: Type -> Bool
734 -- Types that are allowed as arguments of a 'foreign export'
735 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
737 isFFIImportResultTy :: DynFlags -> Type -> Bool
738 isFFIImportResultTy dflags ty
739 = checkRepTyCon (legalFIResultTyCon dflags) ty
741 isFFIExportResultTy :: Type -> Bool
742 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
744 isFFIDynArgumentTy :: Type -> Bool
745 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
746 -- or a newtype of either.
747 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
749 isFFIDynResultTy :: Type -> Bool
750 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
751 -- or a newtype of either.
752 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
754 isFFILabelTy :: Type -> Bool
755 -- The type of a foreign label must be Ptr, FunPtr, Addr,
756 -- or a newtype of either.
757 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
759 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
760 -- Look through newtypes
761 -- Non-recursive ones are transparent to splitTyConApp,
762 -- but recursive ones aren't; hence the splitNewType_maybe
763 checkRepTyCon check_tc ty
764 | Just ty' <- splitNewType_maybe ty = checkRepTyCon check_tc ty'
765 | Just (tc,_) <- splitTyConApp_maybe ty = check_tc tc
769 ----------------------------------------------
770 These chaps do the work; they are not exported
771 ----------------------------------------------
774 legalFEArgTyCon :: TyCon -> Bool
775 -- It's illegal to return foreign objects and (mutable)
776 -- bytearrays from a _ccall_ / foreign declaration
777 -- (or be passed them as arguments in foreign exported functions).
779 | getUnique tc `elem` [ foreignObjTyConKey, foreignPtrTyConKey,
780 byteArrayTyConKey, mutableByteArrayTyConKey ]
782 -- It's also illegal to make foreign exports that take unboxed
783 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
785 = boxedMarshalableTyCon tc
787 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
788 legalFIResultTyCon dflags tc
789 | getUnique tc `elem`
790 [ foreignObjTyConKey, foreignPtrTyConKey,
791 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
792 | tc == unitTyCon = True
793 | otherwise = marshalableTyCon dflags tc
795 legalFEResultTyCon :: TyCon -> Bool
796 legalFEResultTyCon tc
797 | getUnique tc `elem`
798 [ foreignObjTyConKey, foreignPtrTyConKey,
799 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
800 | tc == unitTyCon = True
801 | otherwise = boxedMarshalableTyCon tc
803 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
804 -- Checks validity of types going from Haskell -> external world
805 legalOutgoingTyCon dflags safety tc
806 | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
809 = marshalableTyCon dflags tc
811 marshalableTyCon dflags tc
812 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
813 || boxedMarshalableTyCon tc
815 boxedMarshalableTyCon tc
816 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
817 , int32TyConKey, int64TyConKey
818 , wordTyConKey, word8TyConKey, word16TyConKey
819 , word32TyConKey, word64TyConKey
820 , floatTyConKey, doubleTyConKey
821 , addrTyConKey, ptrTyConKey, funPtrTyConKey
822 , charTyConKey, foreignObjTyConKey
825 , byteArrayTyConKey, mutableByteArrayTyConKey
831 %************************************************************************
833 \subsection{Unification with an explicit substitution}
835 %************************************************************************
837 (allDistinctTyVars tys tvs) = True
839 all the types tys are type variables,
840 distinct from each other and from tvs.
842 This is useful when checking that unification hasn't unified signature
843 type variables. For example, if the type sig is
844 f :: forall a b. a -> b -> b
845 we want to check that 'a' and 'b' havn't
846 (a) been unified with a non-tyvar type
847 (b) been unified with each other (all distinct)
848 (c) been unified with a variable free in the environment
851 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
853 allDistinctTyVars [] acc
855 allDistinctTyVars (ty:tys) acc
856 = case tcGetTyVar_maybe ty of
857 Nothing -> False -- (a)
858 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
859 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
863 %************************************************************************
865 \subsection{Unification with an explicit substitution}
867 %************************************************************************
869 Unify types with an explicit substitution and no monad.
870 Ignore usage annotations.
874 = (TyVarSet, -- Set of template tyvars
875 TyVarSubstEnv) -- Not necessarily idempotent
877 unifyTysX :: TyVarSet -- Template tyvars
880 -> Maybe TyVarSubstEnv
881 unifyTysX tmpl_tyvars ty1 ty2
882 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
884 unifyExtendTysX :: TyVarSet -- Template tyvars
885 -> TyVarSubstEnv -- Substitution to start with
888 -> Maybe TyVarSubstEnv -- Extended substitution
889 unifyExtendTysX tmpl_tyvars subst ty1 ty2
890 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
892 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
893 -> Maybe TyVarSubstEnv
894 unifyTyListsX tmpl_tyvars tys1 tys2
895 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
900 -> (MySubst -> Maybe result)
904 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
905 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
907 -- Variables; go for uVar
908 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
911 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
912 | tyvar1 `elemVarSet` tmpls
913 = uVarX tyvar1 ty2 k subst
914 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
915 | tyvar2 `elemVarSet` tmpls
916 = uVarX tyvar2 ty1 k subst
919 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
920 | n1 == n2 = uTysX t1 t2 k subst
921 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
922 | c1 == c2 = uTyListsX tys1 tys2 k subst
923 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
924 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
926 -- Functions; just check the two parts
927 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
928 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
930 -- Type constructors must match
931 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
932 | (con1 == con2 && equalLength tys1 tys2)
933 = uTyListsX tys1 tys2 k subst
935 -- Applications need a bit of care!
936 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
937 -- NB: we've already dealt with type variables and Notes,
938 -- so if one type is an App the other one jolly well better be too
939 uTysX (AppTy s1 t1) ty2 k subst
940 = case tcSplitAppTy_maybe ty2 of
941 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
942 Nothing -> Nothing -- Fail
944 uTysX ty1 (AppTy s2 t2) k subst
945 = case tcSplitAppTy_maybe ty1 of
946 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
947 Nothing -> Nothing -- Fail
949 -- Not expecting for-alls in unification
951 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
952 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
956 uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
957 uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
959 -- Anything else fails
960 uTysX ty1 ty2 k subst = Nothing
963 uTyListsX [] [] k subst = k subst
964 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
965 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
969 -- Invariant: tv1 is a unifiable variable
970 uVarX tv1 ty2 k subst@(tmpls, env)
971 = case lookupSubstEnv env tv1 of
972 Just (DoneTy ty1) -> -- Already bound
973 uTysX ty1 ty2 k subst
975 Nothing -- Not already bound
976 | typeKind ty2 `eqKind` tyVarKind tv1
977 && occur_check_ok ty2
978 -> -- No kind mismatch nor occur check
979 UASSERT( not (isUTy ty2) )
980 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
982 | otherwise -> Nothing -- Fail if kind mis-match or occur check
984 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
985 occur_check_ok_tv tv | tv1 == tv = False
986 | otherwise = case lookupSubstEnv env tv of
988 Just (DoneTy ty) -> occur_check_ok ty
993 %************************************************************************
995 \subsection{Matching on types}
997 %************************************************************************
999 Matching is a {\em unidirectional} process, matching a type against a
1000 template (which is just a type with type variables in it). The
1001 matcher assumes that there are no repeated type variables in the
1002 template, so that it simply returns a mapping of type variables to
1003 types. It also fails on nested foralls.
1005 @matchTys@ matches corresponding elements of a list of templates and
1006 types. It and @matchTy@ both ignore usage annotations, unlike the
1007 main function @match@.
1010 matchTy :: TyVarSet -- Template tyvars
1012 -> Type -- Proposed instance of template
1013 -> Maybe TyVarSubstEnv -- Matching substitution
1016 matchTys :: TyVarSet -- Template tyvars
1017 -> [Type] -- Templates
1018 -> [Type] -- Proposed instance of template
1019 -> Maybe (TyVarSubstEnv, -- Matching substitution
1020 [Type]) -- Left over instance types
1022 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1024 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1025 (\ (senv,tys) -> Just (senv,tys))
1029 @match@ is the main function. It takes a flag indicating whether
1030 usage annotations are to be respected.
1033 match :: Type -> Type -- Current match pair
1034 -> TyVarSet -- Template vars
1035 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1036 -> TyVarSubstEnv -- Current subst
1039 -- When matching against a type variable, see if the variable
1040 -- has already been bound. If so, check that what it's bound to
1041 -- is the same as ty; if not, bind it and carry on.
1043 match (TyVarTy v) ty tmpls k senv
1044 | v `elemVarSet` tmpls
1045 = -- v is a template variable
1046 case lookupSubstEnv senv v of
1047 Nothing -> UASSERT( not (isUTy ty) )
1048 k (extendSubstEnv senv v (DoneTy ty))
1049 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1050 | otherwise -> Nothing -- Fails
1053 = -- v is not a template variable; ty had better match
1054 -- Can't use (==) because types differ
1055 case tcGetTyVar_maybe ty of
1056 Just v' | v == v' -> k senv -- Success
1057 other -> Nothing -- Failure
1058 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1059 -- I guess the reason the Note-stripping case is *last* rather than first
1060 -- is to preserve type synonyms etc., so I'm not moving it to the
1061 -- top; but this means that (without the deNotetype) a type
1062 -- variable may not match the pattern (TyVarTy v') as one would
1063 -- expect, due to an intervening Note. KSW 2000-06.
1066 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1067 | n1 == n2 = match t1 t2 tmpls k senv
1068 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1069 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1070 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1071 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1073 -- Functions; just check the two parts
1074 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1075 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1077 match (AppTy fun1 arg1) ty2 tmpls k senv
1078 = case tcSplitAppTy_maybe ty2 of
1079 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1080 Nothing -> Nothing -- Fail
1082 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1083 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1085 -- Newtypes are opaque; other source types should not happen
1086 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1087 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1089 match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1090 match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1092 -- With type synonyms, we have to be careful for the exact
1093 -- same reasons as in the unifier. Please see the
1094 -- considerable commentary there before changing anything
1095 -- here! (WDP 95/05)
1096 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1097 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1100 match _ _ _ _ _ = Nothing
1102 match_list_exactly tys1 tys2 tmpls k senv
1103 = match_list tys1 tys2 tmpls k' senv
1105 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1106 | otherwise = Nothing -- Fail
1108 match_list [] tys2 tmpls k senv = k (senv, tys2)
1109 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1110 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1111 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv