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, isStrictType, isStrictPred,
40 isDoubleTy, isFloatTy, isIntTy,
41 isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy, isPrimitiveType,
42 isTauTy, tcIsTyVarTy, tcIsForAllTy,
44 ---------------------------------
45 -- Misc type manipulators
46 hoistForAllTys, deNoteType,
47 namesOfType, namesOfDFunHead,
50 ---------------------------------
52 PredType, mkPredTy, mkPredTys, 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 -- Unifier and matcher
60 unifyTysX, unifyTyListsX, unifyExtendTysX,
62 matchTy, matchTys, match,
64 --------------------------------
65 -- Rexported from Type
66 Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
67 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
68 superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
71 Type, SourceType(..), PredType, ThetaType,
72 mkForAllTy, mkForAllTys,
73 mkFunTy, mkFunTys, zipFunTys,
74 mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
75 mkTyVarTy, mkTyVarTys, mkTyConTy,
77 isUnLiftedType, -- Source types are always lifted
78 isUnboxedTupleType, -- Ditto
80 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
81 tidyTyVar, tidyTyVars,
82 typeKind, eqKind, eqUsage,
84 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
87 #include "HsVersions.h"
90 import {-# SOURCE #-} PprType( pprType )
93 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
94 import Type ( mkUTyM, unUTy ) -- Used locally
96 import Type ( -- Re-exports
97 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
98 Kind, Type, TauType, SourceType(..), PredType, ThetaType,
99 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
100 mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
101 mkFunTy, mkFunTys, zipFunTys,
102 mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
103 mkTyVarTy, mkTyVarTys, mkTyConTy,
104 isUnLiftedType, isUnboxedTupleType,
105 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
106 tidyTyVar, tidyTyVars, eqKind, eqUsage,
107 hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
109 import TyCon ( TyCon, isPrimTyCon, tyConArity, isNewTyCon )
110 import Class ( classTyCon, classHasFDs, Class )
111 import Var ( TyVar, tyVarKind )
116 import CmdLineOpts ( opt_DictsStrict )
117 import Name ( Name, NamedThing(..), mkLocalName )
118 import OccName ( OccName, mkDictOcc )
120 import PrelNames ( floatTyConKey, doubleTyConKey, foreignPtrTyConKey,
121 integerTyConKey, intTyConKey, addrTyConKey, boolTyConKey )
122 import Unique ( Unique, Uniquable(..), mkTupleTyConUnique )
123 import SrcLoc ( SrcLoc )
124 import Util ( cmpList, thenCmp )
125 import Maybes ( maybeToBool, expectJust )
126 import BasicTypes ( Boxity(..) )
131 %************************************************************************
133 \subsection{Tau, sigma and rho}
135 %************************************************************************
138 type SigmaType = Type
141 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
143 mkRhoTy :: [SourceType] -> Type -> Type
144 mkRhoTy theta ty = UASSERT2( not (isUTy ty), pprType ty )
145 foldr (\p r -> FunTy (mkUTyM (mkPredTy p)) (mkUTyM r)) ty theta
150 @isTauTy@ tests for nested for-alls.
153 isTauTy :: Type -> Bool
154 isTauTy (TyVarTy v) = True
155 isTauTy (TyConApp _ tys) = all isTauTy tys
156 isTauTy (AppTy a b) = isTauTy a && isTauTy b
157 isTauTy (FunTy a b) = isTauTy a && isTauTy b
158 isTauTy (SourceTy p) = True -- Don't look through source types
159 isTauTy (NoteTy _ ty) = isTauTy ty
160 isTauTy (UsageTy _ ty) = isTauTy ty
161 isTauTy other = False
165 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
166 -- construct a dictionary function name
167 getDFunTyKey (TyVarTy tv) = getOccName tv
168 getDFunTyKey (TyConApp tc _) = getOccName tc
169 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
170 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
171 getDFunTyKey (FunTy arg _) = getOccName funTyCon
172 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
173 getDFunTyKey (UsageTy _ t) = getDFunTyKey t
174 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
175 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
176 -- SourceTy shouldn't happen
180 %************************************************************************
182 \subsection{Expanding and splitting}
184 %************************************************************************
186 These tcSplit functions are like their non-Tc analogues, but
187 a) they do not look through newtypes
188 b) they do not look through PredTys
189 c) [future] they ignore usage-type annotations
191 However, they are non-monadic and do not follow through mutable type
192 variables. It's up to you to make sure this doesn't matter.
195 tcSplitForAllTys :: Type -> ([TyVar], Type)
196 tcSplitForAllTys ty = split ty ty []
198 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
199 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
200 split orig_ty (UsageTy _ ty) tvs = split orig_ty ty tvs
201 split orig_ty t tvs = (reverse tvs, orig_ty)
203 tcIsForAllTy (ForAllTy tv ty) = True
204 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
205 tcIsForAllTy (UsageTy n ty) = tcIsForAllTy ty
206 tcIsForAllTy t = False
208 tcSplitRhoTy :: Type -> ([PredType], Type)
209 tcSplitRhoTy ty = split ty ty []
211 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
212 Just p -> split res res (p:ts)
213 Nothing -> (reverse ts, orig_ty)
214 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
215 split orig_ty (UsageTy _ ty) ts = split orig_ty ty ts
216 split orig_ty ty ts = (reverse ts, orig_ty)
218 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
219 (tvs, rho) -> case tcSplitRhoTy rho of
220 (theta, tau) -> (tvs, theta, tau)
222 tcTyConAppTyCon :: Type -> TyCon
223 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
225 tcTyConAppArgs :: Type -> [Type]
226 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
228 tcSplitTyConApp :: Type -> (TyCon, [Type])
229 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
231 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
233 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
234 -- Newtypes are opaque, so they may be split
235 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
236 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [unUTy arg,unUTy res])
237 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
238 tcSplitTyConApp_maybe (UsageTy _ ty) = tcSplitTyConApp_maybe ty
239 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
240 -- However, predicates are not treated
241 -- as tycon applications by the type checker
242 tcSplitTyConApp_maybe other = Nothing
244 tcSplitFunTys :: Type -> ([Type], Type)
245 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
247 Just (arg,res) -> (arg:args, res')
249 (args,res') = tcSplitFunTys res
251 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
252 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
253 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
254 tcSplitFunTy_maybe (UsageTy _ ty) = tcSplitFunTy_maybe ty
255 tcSplitFunTy_maybe other = Nothing
257 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
258 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
261 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
262 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2)
263 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
264 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
265 tcSplitAppTy_maybe (UsageTy _ ty) = tcSplitAppTy_maybe ty
266 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
267 --- Don't forget that newtype!
268 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
269 tcSplitAppTy_maybe other = Nothing
271 tc_split_app tc [] = Nothing
272 tc_split_app tc tys = split tys []
274 split [ty2] acc = Just (TyConApp tc (reverse acc), ty2)
275 split (ty:tys) acc = split tys (ty:acc)
277 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
279 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
281 tcGetTyVar_maybe :: Type -> Maybe TyVar
282 tcGetTyVar_maybe (TyVarTy tv) = Just tv
283 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
284 tcGetTyVar_maybe ty@(UsageTy _ _) = pprPanic "tcGetTyVar_maybe: UTy:" (pprType ty)
285 tcGetTyVar_maybe other = Nothing
287 tcGetTyVar :: String -> Type -> TyVar
288 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
290 tcIsTyVarTy :: Type -> Bool
291 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
294 The type of a method for class C is always of the form:
295 Forall a1..an. C a1..an => sig_ty
296 where sig_ty is the type given by the method's signature, and thus in general
297 is a ForallTy. At the point that splitMethodTy is called, it is expected
298 that the outer Forall has already been stripped off. splitMethodTy then
299 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
303 tcSplitMethodTy :: Type -> (PredType, Type)
304 tcSplitMethodTy ty = split ty
306 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
308 Nothing -> panic "splitMethodTy"
309 split (NoteTy n ty) = split ty
310 split (UsageTy _ ty) = split ty
311 split _ = panic "splitMethodTy"
313 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
314 -- Split the type of a dictionary function
316 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
317 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
318 (tvs, theta, clas, tys) }}
322 %************************************************************************
324 \subsection{Predicate types}
326 %************************************************************************
328 "Predicates" are particular source types, namelyClassP or IParams
331 isPred :: SourceType -> Bool
332 isPred (ClassP _ _) = True
333 isPred (IParam _ _) = True
334 isPred (NType _ __) = False
336 isPredTy :: Type -> Bool
337 isPredTy (NoteTy _ ty) = isPredTy ty
338 isPredTy (UsageTy _ ty) = isPredTy ty
339 isPredTy (SourceTy sty) = isPred sty
342 tcSplitPredTy_maybe :: Type -> Maybe PredType
343 -- Returns Just for predicates only
344 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
345 tcSplitPredTy_maybe (UsageTy _ ty) = tcSplitPredTy_maybe ty
346 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
347 tcSplitPredTy_maybe other = Nothing
349 mkPredTy :: PredType -> Type
350 mkPredTy pred = SourceTy pred
352 mkPredTys :: ThetaType -> [Type]
353 mkPredTys preds = map SourceTy preds
355 predTyUnique :: PredType -> Unique
356 predTyUnique (IParam n _) = getUnique n
357 predTyUnique (ClassP clas tys) = getUnique clas
359 predHasFDs :: PredType -> Bool
360 -- True if the predicate has functional depenencies;
361 -- I.e. should participate in improvement
362 predHasFDs (IParam _ _) = True
363 predHasFDs (ClassP cls _) = classHasFDs cls
365 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
366 mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
367 mkPredName uniq loc (IParam name ty) = name
371 --------------------- Dictionary types ---------------------------------
374 mkClassPred clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
377 isClassPred :: SourceType -> Bool
378 isClassPred (ClassP clas tys) = True
379 isClassPred other = False
381 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
382 isTyVarClassPred other = False
384 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
385 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
386 getClassPredTys_maybe _ = Nothing
388 getClassPredTys :: PredType -> (Class, [Type])
389 getClassPredTys (ClassP clas tys) = (clas, tys)
391 mkDictTy :: Class -> [Type] -> Type
392 mkDictTy clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
393 mkPredTy (ClassP clas tys)
395 isDictTy :: Type -> Bool
396 isDictTy (SourceTy p) = isClassPred p
397 isDictTy (NoteTy _ ty) = isDictTy ty
398 isDictTy (UsageTy _ ty) = isDictTy ty
399 isDictTy other = False
402 --------------------- Implicit parameters ---------------------------------
405 isIPPred :: SourceType -> Bool
406 isIPPred (IParam _ _) = True
407 isIPPred other = False
409 inheritablePred :: PredType -> Bool
410 -- Can be inherited by a context. For example, consider
411 -- f x = let g y = (?v, y+x)
412 -- in (g 3 with ?v = 8,
414 -- The point is that g's type must be quantifed over ?v:
415 -- g :: (?v :: a) => a -> a
416 -- but it doesn't need to be quantified over the Num a dictionary
417 -- which can be free in g's rhs, and shared by both calls to g
418 inheritablePred (ClassP _ _) = True
419 inheritablePred other = False
421 predMentionsIPs :: SourceType -> NameSet -> Bool
422 predMentionsIPs (IParam n _) ns = n `elemNameSet` ns
423 predMentionsIPs other ns = False
427 %************************************************************************
429 \subsection{Comparison}
431 %************************************************************************
433 Comparison, taking note of newtypes, predicates, etc,
434 But ignoring usage types
437 tcEqType :: Type -> Type -> Bool
438 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
440 tcEqPred :: PredType -> PredType -> Bool
441 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
444 tcCmpType :: Type -> Type -> Ordering
445 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
447 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
449 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
451 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
454 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
455 -- The "env" maps type variables in ty1 to type variables in ty2
456 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
457 -- we in effect substitute tv2 for tv1 in t1 before continuing
459 -- Look through NoteTy and UsageTy
460 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
461 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
462 cmpTy env (UsageTy _ ty1) ty2 = cmpTy env ty1 ty2
463 cmpTy env ty1 (UsageTy _ ty2) = cmpTy env ty1 ty2
465 -- Deal with equal constructors
466 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
467 Just tv1a -> tv1a `compare` tv2
468 Nothing -> tv1 `compare` tv2
470 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
471 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
472 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
473 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
474 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
476 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
477 cmpTy env (AppTy _ _) (TyVarTy _) = GT
479 cmpTy env (FunTy _ _) (TyVarTy _) = GT
480 cmpTy env (FunTy _ _) (AppTy _ _) = GT
482 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
483 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
484 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
486 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
487 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
488 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
489 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
491 cmpTy env (SourceTy _) t2 = GT
497 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
498 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
499 -- Compare types as well as names for implicit parameters
500 -- This comparison is used exclusively (I think) for the
501 -- finite map built in TcSimplify
502 cmpSourceTy env (IParam _ _) sty = LT
504 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
505 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
506 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
508 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
509 cmpSourceTy env (NType _ _) sty = GT
512 PredTypes are used as a FM key in TcSimplify,
513 so we take the easy path and make them an instance of Ord
516 instance Eq SourceType where { (==) = tcEqPred }
517 instance Ord SourceType where { compare = tcCmpPred }
521 %************************************************************************
523 \subsection{Predicates}
525 %************************************************************************
527 isQualifiedTy returns true of any qualified type. It doesn't *necessarily* have
529 f :: (?x::Int) => Int -> Int
532 isQualifiedTy :: Type -> Bool
533 isQualifiedTy (ForAllTy tyvar ty) = True
534 isQualifiedTy (FunTy a b) = isPredTy a
535 isQualifiedTy (NoteTy n ty) = isQualifiedTy ty
536 isQualifiedTy (UsageTy _ ty) = isQualifiedTy ty
537 isQualifiedTy _ = False
539 isOverloadedTy :: Type -> Bool
540 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
541 isOverloadedTy (FunTy a b) = isPredTy a
542 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
543 isOverloadedTy (UsageTy _ ty) = isOverloadedTy ty
544 isOverloadedTy _ = False
548 isFloatTy = is_tc floatTyConKey
549 isDoubleTy = is_tc doubleTyConKey
550 isForeignPtrTy = is_tc foreignPtrTyConKey
551 isIntegerTy = is_tc integerTyConKey
552 isIntTy = is_tc intTyConKey
553 isAddrTy = is_tc addrTyConKey
554 isBoolTy = is_tc boolTyConKey
555 isUnitTy = is_tc (mkTupleTyConUnique Boxed 0)
557 is_tc :: Unique -> Type -> Bool
558 -- Newtypes are opaque to this
559 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
560 Just (tc, _) -> uniq == getUnique tc
565 isPrimitiveType :: Type -> Bool
566 -- Returns types that are opaque to Haskell.
567 -- Most of these are unlifted, but now that we interact with .NET, we
568 -- may have primtive (foreign-imported) types that are lifted
569 isPrimitiveType ty = case tcSplitTyConApp_maybe ty of
570 Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc )
575 @isStrictType@ computes whether an argument (or let RHS) should
576 be computed strictly or lazily, based only on its type
579 isStrictType :: Type -> Bool
581 | isUnLiftedType ty = True
582 | Just pred <- tcSplitPredTy_maybe ty = isStrictPred pred
585 isStrictPred (ClassP clas _) = opt_DictsStrict
586 && not (isNewTyCon (classTyCon clas))
587 isStrictPred pred = False
588 -- We may be strict in dictionary types, but only if it
589 -- has more than one component.
590 -- [Being strict in a single-component dictionary risks
591 -- poking the dictionary component, which is wrong.]
595 %************************************************************************
599 %************************************************************************
602 hoistForAllTys :: Type -> Type
603 -- Move all the foralls to the top
604 -- e.g. T -> forall a. a ==> forall a. T -> a
605 -- Careful: LOSES USAGE ANNOTATIONS!
607 = case hoist ty of { (tvs, body) -> mkForAllTys tvs body }
609 hoist :: Type -> ([TyVar], Type)
610 hoist ty = case tcSplitFunTys ty of { (args, res) ->
611 case tcSplitForAllTys res of {
612 ([], body) -> ([], ty) ;
613 (tvs1, body1) -> case hoist body1 of { (tvs2,body2) ->
614 (tvs1 ++ tvs2, mkFunTys args body2)
620 deNoteType :: Type -> Type
621 -- Remove synonyms, but not source types
622 deNoteType ty@(TyVarTy tyvar) = ty
623 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
624 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
625 deNoteType (NoteTy _ ty) = deNoteType ty
626 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
627 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
628 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
629 deNoteType (UsageTy u ty) = UsageTy u (deNoteType ty)
631 deNoteSourceType :: SourceType -> SourceType
632 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
633 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
634 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
637 Find the free names of a type, including the type constructors and classes it mentions
638 This is used in the front end of the compiler
641 namesOfType :: Type -> NameSet
642 namesOfType (TyVarTy tv) = unitNameSet (getName tv)
643 namesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
644 namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
645 namesOfType (NoteTy other_note ty2) = namesOfType ty2
646 namesOfType (SourceTy (IParam n ty)) = namesOfType ty
647 namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
648 namesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
649 namesOfType (FunTy arg res) = namesOfType arg `unionNameSets` namesOfType res
650 namesOfType (AppTy fun arg) = namesOfType fun `unionNameSets` namesOfType arg
651 namesOfType (ForAllTy tyvar ty) = namesOfType ty `delFromNameSet` getName tyvar
652 namesOfType (UsageTy u ty) = namesOfType u `unionNameSets` namesOfType ty
654 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
656 namesOfDFunHead :: Type -> NameSet
657 -- Find the free type constructors and classes
658 -- of the head of the dfun instance type
659 -- The 'dfun_head_type' is because of
660 -- instance Foo a => Baz T where ...
661 -- The decl is an orphan if Baz and T are both not locally defined,
662 -- even if Foo *is* locally defined
663 namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
664 (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
669 %************************************************************************
671 \subsection{Unification with an explicit substitution}
673 %************************************************************************
675 (allDistinctTyVars tys tvs) = True
677 all the types tys are type variables,
678 distinct from each other and from tvs.
680 This is useful when checking that unification hasn't unified signature
681 type variables. For example, if the type sig is
682 f :: forall a b. a -> b -> b
683 we want to check that 'a' and 'b' havn't
684 (a) been unified with a non-tyvar type
685 (b) been unified with each other (all distinct)
686 (c) been unified with a variable free in the environment
689 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
691 allDistinctTyVars [] acc
693 allDistinctTyVars (ty:tys) acc
694 = case tcGetTyVar_maybe ty of
695 Nothing -> False -- (a)
696 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
697 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
701 %************************************************************************
703 \subsection{Unification with an explicit substitution}
705 %************************************************************************
707 Unify types with an explicit substitution and no monad.
708 Ignore usage annotations.
712 = (TyVarSet, -- Set of template tyvars
713 TyVarSubstEnv) -- Not necessarily idempotent
715 unifyTysX :: TyVarSet -- Template tyvars
718 -> Maybe TyVarSubstEnv
719 unifyTysX tmpl_tyvars ty1 ty2
720 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
722 unifyExtendTysX :: TyVarSet -- Template tyvars
723 -> TyVarSubstEnv -- Substitution to start with
726 -> Maybe TyVarSubstEnv -- Extended substitution
727 unifyExtendTysX tmpl_tyvars subst ty1 ty2
728 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
730 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
731 -> Maybe TyVarSubstEnv
732 unifyTyListsX tmpl_tyvars tys1 tys2
733 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
738 -> (MySubst -> Maybe result)
742 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
743 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
745 -- Variables; go for uVar
746 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
749 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
750 | tyvar1 `elemVarSet` tmpls
751 = uVarX tyvar1 ty2 k subst
752 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
753 | tyvar2 `elemVarSet` tmpls
754 = uVarX tyvar2 ty1 k subst
757 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
758 | n1 == n2 = uTysX t1 t2 k subst
759 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
760 | c1 == c2 = uTyListsX tys1 tys2 k subst
761 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
762 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
764 -- Functions; just check the two parts
765 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
766 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
768 -- Type constructors must match
769 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
770 | (con1 == con2 && length tys1 == length tys2)
771 = uTyListsX tys1 tys2 k subst
773 -- Applications need a bit of care!
774 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
775 -- NB: we've already dealt with type variables and Notes,
776 -- so if one type is an App the other one jolly well better be too
777 uTysX (AppTy s1 t1) ty2 k subst
778 = case tcSplitAppTy_maybe ty2 of
779 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
780 Nothing -> Nothing -- Fail
782 uTysX ty1 (AppTy s2 t2) k subst
783 = case tcSplitAppTy_maybe ty1 of
784 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
785 Nothing -> Nothing -- Fail
787 -- Not expecting for-alls in unification
789 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
790 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
794 uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
795 uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
797 -- Anything else fails
798 uTysX ty1 ty2 k subst = Nothing
801 uTyListsX [] [] k subst = k subst
802 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
803 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
807 -- Invariant: tv1 is a unifiable variable
808 uVarX tv1 ty2 k subst@(tmpls, env)
809 = case lookupSubstEnv env tv1 of
810 Just (DoneTy ty1) -> -- Already bound
811 uTysX ty1 ty2 k subst
813 Nothing -- Not already bound
814 | typeKind ty2 `eqKind` tyVarKind tv1
815 && occur_check_ok ty2
816 -> -- No kind mismatch nor occur check
817 UASSERT( not (isUTy ty2) )
818 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
820 | otherwise -> Nothing -- Fail if kind mis-match or occur check
822 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
823 occur_check_ok_tv tv | tv1 == tv = False
824 | otherwise = case lookupSubstEnv env tv of
826 Just (DoneTy ty) -> occur_check_ok ty
831 %************************************************************************
833 \subsection{Matching on types}
835 %************************************************************************
837 Matching is a {\em unidirectional} process, matching a type against a
838 template (which is just a type with type variables in it). The
839 matcher assumes that there are no repeated type variables in the
840 template, so that it simply returns a mapping of type variables to
841 types. It also fails on nested foralls.
843 @matchTys@ matches corresponding elements of a list of templates and
844 types. It and @matchTy@ both ignore usage annotations, unlike the
845 main function @match@.
848 matchTy :: TyVarSet -- Template tyvars
850 -> Type -- Proposed instance of template
851 -> Maybe TyVarSubstEnv -- Matching substitution
854 matchTys :: TyVarSet -- Template tyvars
855 -> [Type] -- Templates
856 -> [Type] -- Proposed instance of template
857 -> Maybe (TyVarSubstEnv, -- Matching substitution
858 [Type]) -- Left over instance types
860 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
862 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
863 (\ (senv,tys) -> Just (senv,tys))
867 @match@ is the main function. It takes a flag indicating whether
868 usage annotations are to be respected.
871 match :: Type -> Type -- Current match pair
872 -> TyVarSet -- Template vars
873 -> (TyVarSubstEnv -> Maybe result) -- Continuation
874 -> TyVarSubstEnv -- Current subst
877 -- When matching against a type variable, see if the variable
878 -- has already been bound. If so, check that what it's bound to
879 -- is the same as ty; if not, bind it and carry on.
881 match (TyVarTy v) ty tmpls k senv
882 | v `elemVarSet` tmpls
883 = -- v is a template variable
884 case lookupSubstEnv senv v of
885 Nothing -> UASSERT( not (isUTy ty) )
886 k (extendSubstEnv senv v (DoneTy ty))
887 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
888 | otherwise -> Nothing -- Fails
891 = -- v is not a template variable; ty had better match
892 -- Can't use (==) because types differ
893 case tcGetTyVar_maybe ty of
894 Just v' | v == v' -> k senv -- Success
895 other -> Nothing -- Failure
896 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
897 -- I guess the reason the Note-stripping case is *last* rather than first
898 -- is to preserve type synonyms etc., so I'm not moving it to the
899 -- top; but this means that (without the deNotetype) a type
900 -- variable may not match the pattern (TyVarTy v') as one would
901 -- expect, due to an intervening Note. KSW 2000-06.
904 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
905 | n1 == n2 = match t1 t2 tmpls k senv
906 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
907 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
908 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
909 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
911 -- Functions; just check the two parts
912 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
913 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
915 match (AppTy fun1 arg1) ty2 tmpls k senv
916 = case tcSplitAppTy_maybe ty2 of
917 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
918 Nothing -> Nothing -- Fail
920 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
921 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
923 -- Newtypes are opaque; other source types should not happen
924 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
925 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
927 match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
928 match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
930 -- With type synonyms, we have to be careful for the exact
931 -- same reasons as in the unifier. Please see the
932 -- considerable commentary there before changing anything
934 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
935 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
938 match _ _ _ _ _ = Nothing
940 match_list_exactly tys1 tys2 tmpls k senv
941 = match_list tys1 tys2 tmpls k' senv
943 k' (senv', tys2') | null tys2' = k senv' -- Succeed
944 | otherwise = Nothing -- Fail
946 match_list [] tys2 tmpls k senv = k (senv, tys2)
947 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
948 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
949 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv