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 TauType, RhoType, SigmaType,
22 --------------------------------
26 --------------------------------
28 -- These are important because they do not look through newtypes
29 tcSplitForAllTys, tcSplitRhoTy,
30 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
31 tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
32 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitSigmaTy,
33 tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
35 ---------------------------------
37 -- Again, newtypes are opaque
38 tcEqType, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
39 isQualifiedTy, isOverloadedTy,
40 isDoubleTy, isFloatTy, isIntTy,
41 isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy,
42 isTauTy, tcIsTyVarTy, tcIsForAllTy,
44 ---------------------------------
45 -- Misc type manipulators
46 hoistForAllTys, deNoteType,
47 namesOfType, namesOfDFunHead,
50 ---------------------------------
52 PredType, getClassPredTys_maybe, getClassPredTys,
53 isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
54 mkDictTy, tcSplitPredTy_maybe, predTyUnique,
55 isDictTy, tcSplitDFunTy, predTyUnique,
56 mkClassPred, predMentionsIPs, inheritablePred, isIPPred, mkPredName,
58 ---------------------------------
59 -- Foreign import and export
60 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
61 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
62 isFFIExportResultTy, -- :: Type -> Bool
63 isFFIExternalTy, -- :: Type -> Bool
64 isFFIDynArgumentTy, -- :: Type -> Bool
65 isFFIDynResultTy, -- :: Type -> Bool
66 isFFILabelTy, -- :: Type -> Bool
68 ---------------------------------
69 -- Unifier and matcher
70 unifyTysX, unifyTyListsX, unifyExtendTysX,
72 matchTy, matchTys, match,
74 --------------------------------
75 -- Rexported from Type
76 Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
77 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
78 superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
81 Type, SourceType(..), PredType, ThetaType,
82 mkForAllTy, mkForAllTys,
83 mkFunTy, mkFunTys, zipFunTys,
84 mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
85 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
87 isUnLiftedType, -- Source types are always lifted
88 isUnboxedTupleType, -- Ditto
91 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
92 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
93 typeKind, eqKind, eqUsage,
95 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
98 #include "HsVersions.h"
101 import {-# SOURCE #-} PprType( pprType )
104 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
105 import Type ( mkUTyM, unUTy ) -- Used locally
107 import Type ( -- Re-exports
108 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
109 Kind, Type, TauType, SourceType(..), PredType, ThetaType,
110 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
111 mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
112 mkFunTy, mkFunTys, zipFunTys,
113 mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
114 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
115 isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
116 splitNewType_maybe, splitTyConApp_maybe,
117 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
118 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
119 hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
121 import TyCon ( TyCon, isUnLiftedTyCon )
122 import Class ( classHasFDs, Class )
123 import Var ( TyVar, tyVarKind )
124 import ForeignCall ( Safety, playSafe )
129 import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
130 import Name ( Name, NamedThing(..), mkLocalName )
131 import OccName ( OccName, mkDictOcc )
133 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
134 import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
135 import Unique ( Unique, Uniquable(..) )
136 import SrcLoc ( SrcLoc )
137 import Util ( cmpList, thenCmp )
138 import Maybes ( maybeToBool, expectJust )
143 %************************************************************************
145 \subsection{Tau, sigma and rho}
147 %************************************************************************
150 type SigmaType = Type
153 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
155 mkRhoTy :: [SourceType] -> Type -> Type
156 mkRhoTy theta ty = UASSERT2( not (isUTy ty), pprType ty )
157 foldr (\p r -> FunTy (mkUTyM (mkPredTy p)) (mkUTyM r)) ty theta
162 @isTauTy@ tests for nested for-alls.
165 isTauTy :: Type -> Bool
166 isTauTy (TyVarTy v) = True
167 isTauTy (TyConApp _ tys) = all isTauTy tys
168 isTauTy (AppTy a b) = isTauTy a && isTauTy b
169 isTauTy (FunTy a b) = isTauTy a && isTauTy b
170 isTauTy (SourceTy p) = True -- Don't look through source types
171 isTauTy (NoteTy _ ty) = isTauTy ty
172 isTauTy (UsageTy _ ty) = isTauTy ty
173 isTauTy other = False
177 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
178 -- construct a dictionary function name
179 getDFunTyKey (TyVarTy tv) = getOccName tv
180 getDFunTyKey (TyConApp tc _) = getOccName tc
181 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
182 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
183 getDFunTyKey (FunTy arg _) = getOccName funTyCon
184 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
185 getDFunTyKey (UsageTy _ t) = getDFunTyKey t
186 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
187 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
188 -- SourceTy shouldn't happen
192 %************************************************************************
194 \subsection{Expanding and splitting}
196 %************************************************************************
198 These tcSplit functions are like their non-Tc analogues, but
199 a) they do not look through newtypes
200 b) they do not look through PredTys
201 c) [future] they ignore usage-type annotations
203 However, they are non-monadic and do not follow through mutable type
204 variables. It's up to you to make sure this doesn't matter.
207 tcSplitForAllTys :: Type -> ([TyVar], Type)
208 tcSplitForAllTys ty = split ty ty []
210 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
211 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
212 split orig_ty (UsageTy _ ty) tvs = split orig_ty ty tvs
213 split orig_ty t tvs = (reverse tvs, orig_ty)
215 tcIsForAllTy (ForAllTy tv ty) = True
216 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
217 tcIsForAllTy (UsageTy n ty) = tcIsForAllTy ty
218 tcIsForAllTy t = False
220 tcSplitRhoTy :: Type -> ([PredType], Type)
221 tcSplitRhoTy ty = split ty ty []
223 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
224 Just p -> split res res (p:ts)
225 Nothing -> (reverse ts, orig_ty)
226 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
227 split orig_ty (UsageTy _ ty) ts = split orig_ty ty ts
228 split orig_ty ty ts = (reverse ts, orig_ty)
230 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
231 (tvs, rho) -> case tcSplitRhoTy rho of
232 (theta, tau) -> (tvs, theta, tau)
234 tcTyConAppTyCon :: Type -> TyCon
235 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
237 tcTyConAppArgs :: Type -> [Type]
238 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
240 tcSplitTyConApp :: Type -> (TyCon, [Type])
241 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
243 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
245 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
246 -- Newtypes are opaque, so they may be split
247 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
248 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [unUTy arg,unUTy res])
249 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
250 tcSplitTyConApp_maybe (UsageTy _ ty) = tcSplitTyConApp_maybe ty
251 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
252 -- However, predicates are not treated
253 -- as tycon applications by the type checker
254 tcSplitTyConApp_maybe other = Nothing
256 tcSplitFunTys :: Type -> ([Type], Type)
257 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
259 Just (arg,res) -> (arg:args, res')
261 (args,res') = tcSplitFunTys res
263 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
264 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
265 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
266 tcSplitFunTy_maybe (UsageTy _ ty) = tcSplitFunTy_maybe ty
267 tcSplitFunTy_maybe other = Nothing
269 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
270 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
273 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
274 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2)
275 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
276 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
277 tcSplitAppTy_maybe (UsageTy _ ty) = tcSplitAppTy_maybe ty
278 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
279 --- Don't forget that newtype!
280 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
281 tcSplitAppTy_maybe other = Nothing
283 tc_split_app tc [] = Nothing
284 tc_split_app tc tys = split tys []
286 split [ty2] acc = Just (TyConApp tc (reverse acc), ty2)
287 split (ty:tys) acc = split tys (ty:acc)
289 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
291 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
293 tcGetTyVar_maybe :: Type -> Maybe TyVar
294 tcGetTyVar_maybe (TyVarTy tv) = Just tv
295 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
296 tcGetTyVar_maybe ty@(UsageTy _ _) = pprPanic "tcGetTyVar_maybe: UTy:" (pprType ty)
297 tcGetTyVar_maybe other = Nothing
299 tcGetTyVar :: String -> Type -> TyVar
300 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
302 tcIsTyVarTy :: Type -> Bool
303 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
306 The type of a method for class C is always of the form:
307 Forall a1..an. C a1..an => sig_ty
308 where sig_ty is the type given by the method's signature, and thus in general
309 is a ForallTy. At the point that splitMethodTy is called, it is expected
310 that the outer Forall has already been stripped off. splitMethodTy then
311 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
315 tcSplitMethodTy :: Type -> (PredType, Type)
316 tcSplitMethodTy ty = split ty
318 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
320 Nothing -> panic "splitMethodTy"
321 split (NoteTy n ty) = split ty
322 split (UsageTy _ ty) = split ty
323 split _ = panic "splitMethodTy"
325 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
326 -- Split the type of a dictionary function
328 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
329 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
330 (tvs, theta, clas, tys) }}
334 %************************************************************************
336 \subsection{Predicate types}
338 %************************************************************************
340 "Predicates" are particular source types, namelyClassP or IParams
343 isPred :: SourceType -> Bool
344 isPred (ClassP _ _) = True
345 isPred (IParam _ _) = True
346 isPred (NType _ __) = False
348 isPredTy :: Type -> Bool
349 isPredTy (NoteTy _ ty) = isPredTy ty
350 isPredTy (UsageTy _ ty) = isPredTy ty
351 isPredTy (SourceTy sty) = isPred sty
354 tcSplitPredTy_maybe :: Type -> Maybe PredType
355 -- Returns Just for predicates only
356 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
357 tcSplitPredTy_maybe (UsageTy _ ty) = tcSplitPredTy_maybe ty
358 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
359 tcSplitPredTy_maybe other = Nothing
361 predTyUnique :: PredType -> Unique
362 predTyUnique (IParam n _) = getUnique n
363 predTyUnique (ClassP clas tys) = getUnique clas
365 predHasFDs :: PredType -> Bool
366 -- True if the predicate has functional depenencies;
367 -- I.e. should participate in improvement
368 predHasFDs (IParam _ _) = True
369 predHasFDs (ClassP cls _) = classHasFDs cls
371 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
372 mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
373 mkPredName uniq loc (IParam name ty) = name
377 --------------------- Dictionary types ---------------------------------
380 mkClassPred clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
383 isClassPred :: SourceType -> Bool
384 isClassPred (ClassP clas tys) = True
385 isClassPred other = False
387 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
388 isTyVarClassPred other = False
390 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
391 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
392 getClassPredTys_maybe _ = Nothing
394 getClassPredTys :: PredType -> (Class, [Type])
395 getClassPredTys (ClassP clas tys) = (clas, tys)
397 mkDictTy :: Class -> [Type] -> Type
398 mkDictTy clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
399 mkPredTy (ClassP clas tys)
401 isDictTy :: Type -> Bool
402 isDictTy (SourceTy p) = isClassPred p
403 isDictTy (NoteTy _ ty) = isDictTy ty
404 isDictTy (UsageTy _ ty) = isDictTy ty
405 isDictTy other = False
408 --------------------- Implicit parameters ---------------------------------
411 isIPPred :: SourceType -> Bool
412 isIPPred (IParam _ _) = True
413 isIPPred other = False
415 inheritablePred :: PredType -> Bool
416 -- Can be inherited by a context. For example, consider
417 -- f x = let g y = (?v, y+x)
418 -- in (g 3 with ?v = 8,
420 -- The point is that g's type must be quantifed over ?v:
421 -- g :: (?v :: a) => a -> a
422 -- but it doesn't need to be quantified over the Num a dictionary
423 -- which can be free in g's rhs, and shared by both calls to g
424 inheritablePred (ClassP _ _) = True
425 inheritablePred other = False
427 predMentionsIPs :: SourceType -> NameSet -> Bool
428 predMentionsIPs (IParam n _) ns = n `elemNameSet` ns
429 predMentionsIPs other ns = False
433 %************************************************************************
435 \subsection{Comparison}
437 %************************************************************************
439 Comparison, taking note of newtypes, predicates, etc,
440 But ignoring usage types
443 tcEqType :: Type -> Type -> Bool
444 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
446 tcEqPred :: PredType -> PredType -> Bool
447 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
450 tcCmpType :: Type -> Type -> Ordering
451 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
453 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
455 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
457 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
460 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
461 -- The "env" maps type variables in ty1 to type variables in ty2
462 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
463 -- we in effect substitute tv2 for tv1 in t1 before continuing
465 -- Look through NoteTy and UsageTy
466 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
467 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
468 cmpTy env (UsageTy _ ty1) ty2 = cmpTy env ty1 ty2
469 cmpTy env ty1 (UsageTy _ ty2) = cmpTy env ty1 ty2
471 -- Deal with equal constructors
472 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
473 Just tv1a -> tv1a `compare` tv2
474 Nothing -> tv1 `compare` tv2
476 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
477 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
478 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
479 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
480 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
482 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
483 cmpTy env (AppTy _ _) (TyVarTy _) = GT
485 cmpTy env (FunTy _ _) (TyVarTy _) = GT
486 cmpTy env (FunTy _ _) (AppTy _ _) = GT
488 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
489 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
490 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
492 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
493 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
494 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
495 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
497 cmpTy env (SourceTy _) t2 = GT
503 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
504 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
505 -- Compare types as well as names for implicit parameters
506 -- This comparison is used exclusively (I think) for the
507 -- finite map built in TcSimplify
508 cmpSourceTy env (IParam _ _) sty = LT
510 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
511 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
512 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
514 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
515 cmpSourceTy env (NType _ _) sty = GT
518 PredTypes are used as a FM key in TcSimplify,
519 so we take the easy path and make them an instance of Ord
522 instance Eq SourceType where { (==) = tcEqPred }
523 instance Ord SourceType where { compare = tcCmpPred }
527 %************************************************************************
529 \subsection{Predicates}
531 %************************************************************************
533 isQualifiedTy returns true of any qualified type. It doesn't *necessarily* have
535 f :: (?x::Int) => Int -> Int
538 isQualifiedTy :: Type -> Bool
539 isQualifiedTy (ForAllTy tyvar ty) = True
540 isQualifiedTy (FunTy a b) = isPredTy a
541 isQualifiedTy (NoteTy n ty) = isQualifiedTy ty
542 isQualifiedTy (UsageTy _ ty) = isQualifiedTy ty
543 isQualifiedTy _ = False
545 isOverloadedTy :: Type -> Bool
546 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
547 isOverloadedTy (FunTy a b) = isPredTy a
548 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
549 isOverloadedTy (UsageTy _ ty) = isOverloadedTy ty
550 isOverloadedTy _ = False
554 isFloatTy = is_tc floatTyConKey
555 isDoubleTy = is_tc doubleTyConKey
556 isForeignPtrTy = is_tc foreignPtrTyConKey
557 isIntegerTy = is_tc integerTyConKey
558 isIntTy = is_tc intTyConKey
559 isAddrTy = is_tc addrTyConKey
560 isBoolTy = is_tc boolTyConKey
561 isUnitTy = is_tc unitTyConKey
563 is_tc :: Unique -> Type -> Bool
564 -- Newtypes are opaque to this
565 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
566 Just (tc, _) -> uniq == getUnique tc
571 %************************************************************************
575 %************************************************************************
578 hoistForAllTys :: Type -> Type
579 -- Move all the foralls to the top
580 -- e.g. T -> forall a. a ==> forall a. T -> a
581 -- Careful: LOSES USAGE ANNOTATIONS!
583 = case hoist ty of { (tvs, body) -> mkForAllTys tvs body }
585 hoist :: Type -> ([TyVar], Type)
586 hoist ty = case tcSplitFunTys ty of { (args, res) ->
587 case tcSplitForAllTys res of {
588 ([], body) -> ([], ty) ;
589 (tvs1, body1) -> case hoist body1 of { (tvs2,body2) ->
590 (tvs1 ++ tvs2, mkFunTys args body2)
596 deNoteType :: Type -> Type
597 -- Remove synonyms, but not source types
598 deNoteType ty@(TyVarTy tyvar) = ty
599 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
600 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
601 deNoteType (NoteTy _ ty) = deNoteType ty
602 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
603 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
604 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
605 deNoteType (UsageTy u ty) = UsageTy u (deNoteType ty)
607 deNoteSourceType :: SourceType -> SourceType
608 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
609 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
610 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
613 Find the free names of a type, including the type constructors and classes it mentions
614 This is used in the front end of the compiler
617 namesOfType :: Type -> NameSet
618 namesOfType (TyVarTy tv) = unitNameSet (getName tv)
619 namesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
620 namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
621 namesOfType (NoteTy other_note ty2) = namesOfType ty2
622 namesOfType (SourceTy (IParam n ty)) = namesOfType ty
623 namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
624 namesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
625 namesOfType (FunTy arg res) = namesOfType arg `unionNameSets` namesOfType res
626 namesOfType (AppTy fun arg) = namesOfType fun `unionNameSets` namesOfType arg
627 namesOfType (ForAllTy tyvar ty) = namesOfType ty `delFromNameSet` getName tyvar
628 namesOfType (UsageTy u ty) = namesOfType u `unionNameSets` namesOfType ty
630 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
632 namesOfDFunHead :: Type -> NameSet
633 -- Find the free type constructors and classes
634 -- of the head of the dfun instance type
635 -- The 'dfun_head_type' is because of
636 -- instance Foo a => Baz T where ...
637 -- The decl is an orphan if Baz and T are both not locally defined,
638 -- even if Foo *is* locally defined
639 namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
640 (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
645 %************************************************************************
647 \subsection[TysWiredIn-ext-type]{External types}
649 %************************************************************************
651 The compiler's foreign function interface supports the passing of a
652 restricted set of types as arguments and results (the restricting factor
656 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
657 -- Checks for valid argument type for a 'foreign import'
658 isFFIArgumentTy dflags safety ty
659 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
661 isFFIExternalTy :: Type -> Bool
662 -- Types that are allowed as arguments of a 'foreign export'
663 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
665 isFFIImportResultTy :: DynFlags -> Type -> Bool
666 isFFIImportResultTy dflags ty
667 = checkRepTyCon (legalFIResultTyCon dflags) ty
669 isFFIExportResultTy :: Type -> Bool
670 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
672 isFFIDynArgumentTy :: Type -> Bool
673 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
674 -- or a newtype of either.
675 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
677 isFFIDynResultTy :: Type -> Bool
678 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
679 -- or a newtype of either.
680 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
682 isFFILabelTy :: Type -> Bool
683 -- The type of a foreign label must be Ptr, FunPtr, Addr,
684 -- or a newtype of either.
685 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
687 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
688 -- Look through newtypes
689 -- Non-recursive ones are transparent to splitTyConApp,
690 -- but recursive ones aren't; hence the splitNewType_maybe
691 checkRepTyCon check_tc ty
692 | Just ty' <- splitNewType_maybe ty = checkRepTyCon check_tc ty'
693 | Just (tc,_) <- splitTyConApp_maybe ty = check_tc tc
697 ----------------------------------------------
698 These chaps do the work; they are not exported
699 ----------------------------------------------
702 legalFEArgTyCon :: TyCon -> Bool
703 -- It's illegal to return foreign objects and (mutable)
704 -- bytearrays from a _ccall_ / foreign declaration
705 -- (or be passed them as arguments in foreign exported functions).
707 | getUnique tc `elem` [ foreignObjTyConKey, foreignPtrTyConKey,
708 byteArrayTyConKey, mutableByteArrayTyConKey ]
710 -- It's also illegal to make foreign exports that take unboxed
711 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
713 = boxedMarshalableTyCon tc
715 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
716 legalFIResultTyCon dflags tc
717 | getUnique tc `elem`
718 [ foreignObjTyConKey, foreignPtrTyConKey,
719 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
720 | tc == unitTyCon = True
721 | otherwise = marshalableTyCon dflags tc
723 legalFEResultTyCon :: TyCon -> Bool
724 legalFEResultTyCon tc
725 | getUnique tc `elem`
726 [ foreignObjTyConKey, foreignPtrTyConKey,
727 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
728 | tc == unitTyCon = True
729 | otherwise = boxedMarshalableTyCon tc
731 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
732 -- Checks validity of types going from Haskell -> external world
733 legalOutgoingTyCon dflags safety tc
734 | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
737 = marshalableTyCon dflags tc
739 marshalableTyCon dflags tc
740 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
741 || boxedMarshalableTyCon tc
743 boxedMarshalableTyCon tc
744 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
745 , int32TyConKey, int64TyConKey
746 , wordTyConKey, word8TyConKey, word16TyConKey
747 , word32TyConKey, word64TyConKey
748 , floatTyConKey, doubleTyConKey
749 , addrTyConKey, ptrTyConKey, funPtrTyConKey
750 , charTyConKey, foreignObjTyConKey
753 , byteArrayTyConKey, mutableByteArrayTyConKey
759 %************************************************************************
761 \subsection{Unification with an explicit substitution}
763 %************************************************************************
765 (allDistinctTyVars tys tvs) = True
767 all the types tys are type variables,
768 distinct from each other and from tvs.
770 This is useful when checking that unification hasn't unified signature
771 type variables. For example, if the type sig is
772 f :: forall a b. a -> b -> b
773 we want to check that 'a' and 'b' havn't
774 (a) been unified with a non-tyvar type
775 (b) been unified with each other (all distinct)
776 (c) been unified with a variable free in the environment
779 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
781 allDistinctTyVars [] acc
783 allDistinctTyVars (ty:tys) acc
784 = case tcGetTyVar_maybe ty of
785 Nothing -> False -- (a)
786 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
787 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
791 %************************************************************************
793 \subsection{Unification with an explicit substitution}
795 %************************************************************************
797 Unify types with an explicit substitution and no monad.
798 Ignore usage annotations.
802 = (TyVarSet, -- Set of template tyvars
803 TyVarSubstEnv) -- Not necessarily idempotent
805 unifyTysX :: TyVarSet -- Template tyvars
808 -> Maybe TyVarSubstEnv
809 unifyTysX tmpl_tyvars ty1 ty2
810 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
812 unifyExtendTysX :: TyVarSet -- Template tyvars
813 -> TyVarSubstEnv -- Substitution to start with
816 -> Maybe TyVarSubstEnv -- Extended substitution
817 unifyExtendTysX tmpl_tyvars subst ty1 ty2
818 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
820 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
821 -> Maybe TyVarSubstEnv
822 unifyTyListsX tmpl_tyvars tys1 tys2
823 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
828 -> (MySubst -> Maybe result)
832 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
833 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
835 -- Variables; go for uVar
836 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
839 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
840 | tyvar1 `elemVarSet` tmpls
841 = uVarX tyvar1 ty2 k subst
842 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
843 | tyvar2 `elemVarSet` tmpls
844 = uVarX tyvar2 ty1 k subst
847 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
848 | n1 == n2 = uTysX t1 t2 k subst
849 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
850 | c1 == c2 = uTyListsX tys1 tys2 k subst
851 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
852 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
854 -- Functions; just check the two parts
855 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
856 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
858 -- Type constructors must match
859 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
860 | (con1 == con2 && length tys1 == length tys2)
861 = uTyListsX tys1 tys2 k subst
863 -- Applications need a bit of care!
864 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
865 -- NB: we've already dealt with type variables and Notes,
866 -- so if one type is an App the other one jolly well better be too
867 uTysX (AppTy s1 t1) ty2 k subst
868 = case tcSplitAppTy_maybe ty2 of
869 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
870 Nothing -> Nothing -- Fail
872 uTysX ty1 (AppTy s2 t2) k subst
873 = case tcSplitAppTy_maybe ty1 of
874 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
875 Nothing -> Nothing -- Fail
877 -- Not expecting for-alls in unification
879 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
880 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
884 uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
885 uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
887 -- Anything else fails
888 uTysX ty1 ty2 k subst = Nothing
891 uTyListsX [] [] k subst = k subst
892 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
893 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
897 -- Invariant: tv1 is a unifiable variable
898 uVarX tv1 ty2 k subst@(tmpls, env)
899 = case lookupSubstEnv env tv1 of
900 Just (DoneTy ty1) -> -- Already bound
901 uTysX ty1 ty2 k subst
903 Nothing -- Not already bound
904 | typeKind ty2 `eqKind` tyVarKind tv1
905 && occur_check_ok ty2
906 -> -- No kind mismatch nor occur check
907 UASSERT( not (isUTy ty2) )
908 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
910 | otherwise -> Nothing -- Fail if kind mis-match or occur check
912 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
913 occur_check_ok_tv tv | tv1 == tv = False
914 | otherwise = case lookupSubstEnv env tv of
916 Just (DoneTy ty) -> occur_check_ok ty
921 %************************************************************************
923 \subsection{Matching on types}
925 %************************************************************************
927 Matching is a {\em unidirectional} process, matching a type against a
928 template (which is just a type with type variables in it). The
929 matcher assumes that there are no repeated type variables in the
930 template, so that it simply returns a mapping of type variables to
931 types. It also fails on nested foralls.
933 @matchTys@ matches corresponding elements of a list of templates and
934 types. It and @matchTy@ both ignore usage annotations, unlike the
935 main function @match@.
938 matchTy :: TyVarSet -- Template tyvars
940 -> Type -- Proposed instance of template
941 -> Maybe TyVarSubstEnv -- Matching substitution
944 matchTys :: TyVarSet -- Template tyvars
945 -> [Type] -- Templates
946 -> [Type] -- Proposed instance of template
947 -> Maybe (TyVarSubstEnv, -- Matching substitution
948 [Type]) -- Left over instance types
950 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
952 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
953 (\ (senv,tys) -> Just (senv,tys))
957 @match@ is the main function. It takes a flag indicating whether
958 usage annotations are to be respected.
961 match :: Type -> Type -- Current match pair
962 -> TyVarSet -- Template vars
963 -> (TyVarSubstEnv -> Maybe result) -- Continuation
964 -> TyVarSubstEnv -- Current subst
967 -- When matching against a type variable, see if the variable
968 -- has already been bound. If so, check that what it's bound to
969 -- is the same as ty; if not, bind it and carry on.
971 match (TyVarTy v) ty tmpls k senv
972 | v `elemVarSet` tmpls
973 = -- v is a template variable
974 case lookupSubstEnv senv v of
975 Nothing -> UASSERT( not (isUTy ty) )
976 k (extendSubstEnv senv v (DoneTy ty))
977 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
978 | otherwise -> Nothing -- Fails
981 = -- v is not a template variable; ty had better match
982 -- Can't use (==) because types differ
983 case tcGetTyVar_maybe ty of
984 Just v' | v == v' -> k senv -- Success
985 other -> Nothing -- Failure
986 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
987 -- I guess the reason the Note-stripping case is *last* rather than first
988 -- is to preserve type synonyms etc., so I'm not moving it to the
989 -- top; but this means that (without the deNotetype) a type
990 -- variable may not match the pattern (TyVarTy v') as one would
991 -- expect, due to an intervening Note. KSW 2000-06.
994 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
995 | n1 == n2 = match t1 t2 tmpls k senv
996 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
997 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
998 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
999 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1001 -- Functions; just check the two parts
1002 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1003 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1005 match (AppTy fun1 arg1) ty2 tmpls k senv
1006 = case tcSplitAppTy_maybe ty2 of
1007 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1008 Nothing -> Nothing -- Fail
1010 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1011 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1013 -- Newtypes are opaque; other source types should not happen
1014 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1015 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1017 match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1018 match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1020 -- With type synonyms, we have to be careful for the exact
1021 -- same reasons as in the unifier. Please see the
1022 -- considerable commentary there before changing anything
1023 -- here! (WDP 95/05)
1024 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1025 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1028 match _ _ _ _ _ = Nothing
1030 match_list_exactly tys1 tys2 tmpls k senv
1031 = match_list tys1 tys2 tmpls k' senv
1033 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1034 | otherwise = Nothing -- Fail
1036 match_list [] tys2 tmpls k senv = k (senv, tys2)
1037 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1038 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1039 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv