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,
70 Type, SourceType(..), PredType, ThetaType,
71 mkForAllTy, mkForAllTys,
72 mkFunTy, mkFunTys, zipFunTys,
73 mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
74 mkTyVarTy, mkTyVarTys, mkTyConTy,
76 isUnLiftedType, -- Source types are always lifted
77 isUnboxedTupleType, -- Ditto
79 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
80 tidyTyVar, tidyTyVars,
81 typeKind, eqKind, eqUsage,
83 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
86 #include "HsVersions.h"
89 import {-# SOURCE #-} PprType( pprType )
92 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
93 import Type ( mkUTyM, unUTy ) -- Used locally
95 import Type ( -- Re-exports
96 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
97 Kind, Type, TauType, SourceType(..), PredType, ThetaType,
98 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
99 mkForAllTy, mkForAllTys, defaultKind,
100 mkFunTy, mkFunTys, zipFunTys,
101 mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
102 mkTyVarTy, mkTyVarTys, mkTyConTy,
103 isUnLiftedType, isUnboxedTupleType,
104 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
105 tidyTyVar, tidyTyVars, eqKind, eqUsage,
106 hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
108 import TyCon ( TyCon, isPrimTyCon, tyConArity, isNewTyCon )
109 import Class ( classTyCon, classHasFDs, Class )
110 import Var ( TyVar, tyVarKind )
115 import CmdLineOpts ( opt_DictsStrict )
116 import Name ( Name, NamedThing(..), mkLocalName )
117 import OccName ( OccName, mkDictOcc )
119 import PrelNames ( floatTyConKey, doubleTyConKey, foreignPtrTyConKey,
120 integerTyConKey, intTyConKey, addrTyConKey, boolTyConKey )
121 import Unique ( Unique, Uniquable(..), mkTupleTyConUnique )
122 import SrcLoc ( SrcLoc )
123 import Util ( cmpList, thenCmp )
124 import Maybes ( maybeToBool, expectJust )
125 import BasicTypes ( Boxity(..) )
130 %************************************************************************
132 \subsection{Tau, sigma and rho}
134 %************************************************************************
137 type SigmaType = Type
140 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
142 mkRhoTy :: [SourceType] -> Type -> Type
143 mkRhoTy theta ty = UASSERT2( not (isUTy ty), pprType ty )
144 foldr (\p r -> FunTy (mkUTyM (mkPredTy p)) (mkUTyM r)) ty theta
149 @isTauTy@ tests for nested for-alls.
152 isTauTy :: Type -> Bool
153 isTauTy (TyVarTy v) = True
154 isTauTy (TyConApp _ tys) = all isTauTy tys
155 isTauTy (AppTy a b) = isTauTy a && isTauTy b
156 isTauTy (FunTy a b) = isTauTy a && isTauTy b
157 isTauTy (SourceTy p) = True -- Don't look through source types
158 isTauTy (NoteTy _ ty) = isTauTy ty
159 isTauTy (UsageTy _ ty) = isTauTy ty
160 isTauTy other = False
164 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
165 -- construct a dictionary function name
166 getDFunTyKey (TyVarTy tv) = getOccName tv
167 getDFunTyKey (TyConApp tc _) = getOccName tc
168 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
169 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
170 getDFunTyKey (FunTy arg _) = getOccName funTyCon
171 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
172 getDFunTyKey (UsageTy _ t) = getDFunTyKey t
173 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
174 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
175 -- SourceTy shouldn't happen
179 %************************************************************************
181 \subsection{Expanding and splitting}
183 %************************************************************************
185 These tcSplit functions are like their non-Tc analogues, but
186 a) they do not look through newtypes
187 b) they do not look through PredTys
188 c) [future] they ignore usage-type annotations
190 However, they are non-monadic and do not follow through mutable type
191 variables. It's up to you to make sure this doesn't matter.
194 tcSplitForAllTys :: Type -> ([TyVar], Type)
195 tcSplitForAllTys ty = split ty ty []
197 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
198 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
199 split orig_ty (UsageTy _ ty) tvs = split orig_ty ty tvs
200 split orig_ty t tvs = (reverse tvs, orig_ty)
202 tcIsForAllTy (ForAllTy tv ty) = True
203 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
204 tcIsForAllTy (UsageTy n ty) = tcIsForAllTy ty
205 tcIsForAllTy t = False
207 tcSplitRhoTy :: Type -> ([PredType], Type)
208 tcSplitRhoTy ty = split ty ty []
210 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
211 Just p -> split res res (p:ts)
212 Nothing -> (reverse ts, orig_ty)
213 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
214 split orig_ty (UsageTy _ ty) ts = split orig_ty ty ts
215 split orig_ty ty ts = (reverse ts, orig_ty)
217 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
218 (tvs, rho) -> case tcSplitRhoTy rho of
219 (theta, tau) -> (tvs, theta, tau)
221 tcTyConAppTyCon :: Type -> TyCon
222 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
224 tcTyConAppArgs :: Type -> [Type]
225 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
227 tcSplitTyConApp :: Type -> (TyCon, [Type])
228 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
230 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
232 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
233 -- Newtypes are opaque, so they may be split
234 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
235 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [unUTy arg,unUTy res])
236 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
237 tcSplitTyConApp_maybe (UsageTy _ ty) = tcSplitTyConApp_maybe ty
238 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
239 -- However, predicates are not treated
240 -- as tycon applications by the type checker
241 tcSplitTyConApp_maybe other = Nothing
243 tcSplitFunTys :: Type -> ([Type], Type)
244 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
246 Just (arg,res) -> (arg:args, res')
248 (args,res') = tcSplitFunTys res
250 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
251 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
252 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
253 tcSplitFunTy_maybe (UsageTy _ ty) = tcSplitFunTy_maybe ty
254 tcSplitFunTy_maybe other = Nothing
256 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
257 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
260 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
261 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2)
262 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
263 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
264 tcSplitAppTy_maybe (UsageTy _ ty) = tcSplitAppTy_maybe ty
265 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
266 --- Don't forget that newtype!
267 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
268 tcSplitAppTy_maybe other = Nothing
270 tc_split_app tc [] = Nothing
271 tc_split_app tc tys = split tys []
273 split [ty2] acc = Just (TyConApp tc (reverse acc), ty2)
274 split (ty:tys) acc = split tys (ty:acc)
276 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
278 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
280 tcGetTyVar_maybe :: Type -> Maybe TyVar
281 tcGetTyVar_maybe (TyVarTy tv) = Just tv
282 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
283 tcGetTyVar_maybe ty@(UsageTy _ _) = pprPanic "tcGetTyVar_maybe: UTy:" (pprType ty)
284 tcGetTyVar_maybe other = Nothing
286 tcGetTyVar :: String -> Type -> TyVar
287 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
289 tcIsTyVarTy :: Type -> Bool
290 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
293 The type of a method for class C is always of the form:
294 Forall a1..an. C a1..an => sig_ty
295 where sig_ty is the type given by the method's signature, and thus in general
296 is a ForallTy. At the point that splitMethodTy is called, it is expected
297 that the outer Forall has already been stripped off. splitMethodTy then
298 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
302 tcSplitMethodTy :: Type -> (PredType, Type)
303 tcSplitMethodTy ty = split ty
305 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
307 Nothing -> panic "splitMethodTy"
308 split (NoteTy n ty) = split ty
309 split (UsageTy _ ty) = split ty
310 split _ = panic "splitMethodTy"
312 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
313 -- Split the type of a dictionary function
315 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
316 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
317 (tvs, theta, clas, tys) }}
321 %************************************************************************
323 \subsection{Predicate types}
325 %************************************************************************
327 "Predicates" are particular source types, namelyClassP or IParams
330 isPred :: SourceType -> Bool
331 isPred (ClassP _ _) = True
332 isPred (IParam _ _) = True
333 isPred (NType _ __) = False
335 isPredTy :: Type -> Bool
336 isPredTy (NoteTy _ ty) = isPredTy ty
337 isPredTy (UsageTy _ ty) = isPredTy ty
338 isPredTy (SourceTy sty) = isPred sty
341 tcSplitPredTy_maybe :: Type -> Maybe PredType
342 -- Returns Just for predicates only
343 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
344 tcSplitPredTy_maybe (UsageTy _ ty) = tcSplitPredTy_maybe ty
345 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
346 tcSplitPredTy_maybe other = Nothing
348 mkPredTy :: PredType -> Type
349 mkPredTy pred = SourceTy pred
351 mkPredTys :: ThetaType -> [Type]
352 mkPredTys preds = map SourceTy preds
354 predTyUnique :: PredType -> Unique
355 predTyUnique (IParam n _) = getUnique n
356 predTyUnique (ClassP clas tys) = getUnique clas
358 predHasFDs :: PredType -> Bool
359 -- True if the predicate has functional depenencies;
360 -- I.e. should participate in improvement
361 predHasFDs (IParam _ _) = True
362 predHasFDs (ClassP cls _) = classHasFDs cls
364 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
365 mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
366 mkPredName uniq loc (IParam name ty) = name
370 --------------------- Dictionary types ---------------------------------
373 mkClassPred clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
376 isClassPred :: SourceType -> Bool
377 isClassPred (ClassP clas tys) = True
378 isClassPred other = False
380 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
381 isTyVarClassPred other = False
383 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
384 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
385 getClassPredTys_maybe _ = Nothing
387 getClassPredTys :: PredType -> (Class, [Type])
388 getClassPredTys (ClassP clas tys) = (clas, tys)
390 mkDictTy :: Class -> [Type] -> Type
391 mkDictTy clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
392 mkPredTy (ClassP clas tys)
394 isDictTy :: Type -> Bool
395 isDictTy (SourceTy p) = isClassPred p
396 isDictTy (NoteTy _ ty) = isDictTy ty
397 isDictTy (UsageTy _ ty) = isDictTy ty
398 isDictTy other = False
401 --------------------- Implicit parameters ---------------------------------
404 isIPPred :: SourceType -> Bool
405 isIPPred (IParam _ _) = True
406 isIPPred other = False
408 inheritablePred :: PredType -> Bool
409 -- Can be inherited by a context. For example, consider
410 -- f x = let g y = (?v, y+x)
411 -- in (g 3 with ?v = 8,
413 -- The point is that g's type must be quantifed over ?v:
414 -- g :: (?v :: a) => a -> a
415 -- but it doesn't need to be quantified over the Num a dictionary
416 -- which can be free in g's rhs, and shared by both calls to g
417 inheritablePred (ClassP _ _) = True
418 inheritablePred other = False
420 predMentionsIPs :: SourceType -> NameSet -> Bool
421 predMentionsIPs (IParam n _) ns = n `elemNameSet` ns
422 predMentionsIPs other ns = False
426 %************************************************************************
428 \subsection{Comparison}
430 %************************************************************************
432 Comparison, taking note of newtypes, predicates, etc,
433 But ignoring usage types
436 tcEqType :: Type -> Type -> Bool
437 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
439 tcEqPred :: PredType -> PredType -> Bool
440 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
443 tcCmpType :: Type -> Type -> Ordering
444 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
446 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
448 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
450 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
453 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
454 -- The "env" maps type variables in ty1 to type variables in ty2
455 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
456 -- we in effect substitute tv2 for tv1 in t1 before continuing
458 -- Look through NoteTy and UsageTy
459 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
460 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
461 cmpTy env (UsageTy _ ty1) ty2 = cmpTy env ty1 ty2
462 cmpTy env ty1 (UsageTy _ ty2) = cmpTy env ty1 ty2
464 -- Deal with equal constructors
465 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
466 Just tv1a -> tv1a `compare` tv2
467 Nothing -> tv1 `compare` tv2
469 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
470 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
471 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
472 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
473 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
475 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
476 cmpTy env (AppTy _ _) (TyVarTy _) = GT
478 cmpTy env (FunTy _ _) (TyVarTy _) = GT
479 cmpTy env (FunTy _ _) (AppTy _ _) = GT
481 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
482 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
483 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
485 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
486 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
487 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
488 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
490 cmpTy env (SourceTy _) t2 = GT
496 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
497 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
498 -- Compare types as well as names for implicit parameters
499 -- This comparison is used exclusively (I think) for the
500 -- finite map built in TcSimplify
501 cmpSourceTy env (IParam _ _) sty = LT
503 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
504 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
505 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
507 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
508 cmpSourceTy env (NType _ _) sty = GT
511 PredTypes are used as a FM key in TcSimplify,
512 so we take the easy path and make them an instance of Ord
515 instance Eq SourceType where { (==) = tcEqPred }
516 instance Ord SourceType where { compare = tcCmpPred }
520 %************************************************************************
522 \subsection{Predicates}
524 %************************************************************************
526 isQualifiedTy returns true of any qualified type. It doesn't *necessarily* have
528 f :: (?x::Int) => Int -> Int
531 isQualifiedTy :: Type -> Bool
532 isQualifiedTy (ForAllTy tyvar ty) = True
533 isQualifiedTy (FunTy a b) = isPredTy a
534 isQualifiedTy (NoteTy n ty) = isQualifiedTy ty
535 isQualifiedTy (UsageTy _ ty) = isQualifiedTy ty
536 isQualifiedTy _ = False
538 isOverloadedTy :: Type -> Bool
539 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
540 isOverloadedTy (FunTy a b) = isPredTy a
541 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
542 isOverloadedTy (UsageTy _ ty) = isOverloadedTy ty
543 isOverloadedTy _ = False
547 isFloatTy = is_tc floatTyConKey
548 isDoubleTy = is_tc doubleTyConKey
549 isForeignPtrTy = is_tc foreignPtrTyConKey
550 isIntegerTy = is_tc integerTyConKey
551 isIntTy = is_tc intTyConKey
552 isAddrTy = is_tc addrTyConKey
553 isBoolTy = is_tc boolTyConKey
554 isUnitTy = is_tc (mkTupleTyConUnique Boxed 0)
556 is_tc :: Unique -> Type -> Bool
557 -- Newtypes are opaque to this
558 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
559 Just (tc, _) -> uniq == getUnique tc
564 isPrimitiveType :: Type -> Bool
565 -- Returns types that are opaque to Haskell.
566 -- Most of these are unlifted, but now that we interact with .NET, we
567 -- may have primtive (foreign-imported) types that are lifted
568 isPrimitiveType ty = case tcSplitTyConApp_maybe ty of
569 Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc )
574 @isStrictType@ computes whether an argument (or let RHS) should
575 be computed strictly or lazily, based only on its type
578 isStrictType :: Type -> Bool
580 | isUnLiftedType ty = True
581 | Just pred <- tcSplitPredTy_maybe ty = isStrictPred pred
584 isStrictPred (ClassP clas _) = opt_DictsStrict
585 && not (isNewTyCon (classTyCon clas))
586 isStrictPred pred = False
587 -- We may be strict in dictionary types, but only if it
588 -- has more than one component.
589 -- [Being strict in a single-component dictionary risks
590 -- poking the dictionary component, which is wrong.]
594 %************************************************************************
598 %************************************************************************
601 hoistForAllTys :: Type -> Type
602 -- Move all the foralls to the top
603 -- e.g. T -> forall a. a ==> forall a. T -> a
604 -- Careful: LOSES USAGE ANNOTATIONS!
606 = case hoist ty of { (tvs, body) -> mkForAllTys tvs body }
608 hoist :: Type -> ([TyVar], Type)
609 hoist ty = case tcSplitFunTys ty of { (args, res) ->
610 case tcSplitForAllTys res of {
611 ([], body) -> ([], ty) ;
612 (tvs1, body1) -> case hoist body1 of { (tvs2,body2) ->
613 (tvs1 ++ tvs2, mkFunTys args body2)
619 deNoteType :: Type -> Type
620 -- Remove synonyms, but not source types
621 deNoteType ty@(TyVarTy tyvar) = ty
622 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
623 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
624 deNoteType (NoteTy _ ty) = deNoteType ty
625 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
626 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
627 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
628 deNoteType (UsageTy u ty) = UsageTy u (deNoteType ty)
630 deNoteSourceType :: SourceType -> SourceType
631 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
632 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
633 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
636 Find the free names of a type, including the type constructors and classes it mentions
637 This is used in the front end of the compiler
640 namesOfType :: Type -> NameSet
641 namesOfType (TyVarTy tv) = unitNameSet (getName tv)
642 namesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
643 namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
644 namesOfType (NoteTy other_note ty2) = namesOfType ty2
645 namesOfType (SourceTy (IParam n ty)) = namesOfType ty
646 namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
647 namesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
648 namesOfType (FunTy arg res) = namesOfType arg `unionNameSets` namesOfType res
649 namesOfType (AppTy fun arg) = namesOfType fun `unionNameSets` namesOfType arg
650 namesOfType (ForAllTy tyvar ty) = namesOfType ty `delFromNameSet` getName tyvar
651 namesOfType (UsageTy u ty) = namesOfType u `unionNameSets` namesOfType ty
653 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
655 namesOfDFunHead :: Type -> NameSet
656 -- Find the free type constructors and classes
657 -- of the head of the dfun instance type
658 -- The 'dfun_head_type' is because of
659 -- instance Foo a => Baz T where ...
660 -- The decl is an orphan if Baz and T are both not locally defined,
661 -- even if Foo *is* locally defined
662 namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
663 (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
668 %************************************************************************
670 \subsection{Unification with an explicit substitution}
672 %************************************************************************
674 (allDistinctTyVars tys tvs) = True
676 all the types tys are type variables,
677 distinct from each other and from tvs.
679 This is useful when checking that unification hasn't unified signature
680 type variables. For example, if the type sig is
681 f :: forall a b. a -> b -> b
682 we want to check that 'a' and 'b' havn't
683 (a) been unified with a non-tyvar type
684 (b) been unified with each other (all distinct)
685 (c) been unified with a variable free in the environment
688 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
690 allDistinctTyVars [] acc
692 allDistinctTyVars (ty:tys) acc
693 = case tcGetTyVar_maybe ty of
694 Nothing -> False -- (a)
695 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
696 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
700 %************************************************************************
702 \subsection{Unification with an explicit substitution}
704 %************************************************************************
706 Unify types with an explicit substitution and no monad.
707 Ignore usage annotations.
711 = (TyVarSet, -- Set of template tyvars
712 TyVarSubstEnv) -- Not necessarily idempotent
714 unifyTysX :: TyVarSet -- Template tyvars
717 -> Maybe TyVarSubstEnv
718 unifyTysX tmpl_tyvars ty1 ty2
719 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
721 unifyExtendTysX :: TyVarSet -- Template tyvars
722 -> TyVarSubstEnv -- Substitution to start with
725 -> Maybe TyVarSubstEnv -- Extended substitution
726 unifyExtendTysX tmpl_tyvars subst ty1 ty2
727 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
729 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
730 -> Maybe TyVarSubstEnv
731 unifyTyListsX tmpl_tyvars tys1 tys2
732 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
737 -> (MySubst -> Maybe result)
741 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
742 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
744 -- Variables; go for uVar
745 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
748 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
749 | tyvar1 `elemVarSet` tmpls
750 = uVarX tyvar1 ty2 k subst
751 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
752 | tyvar2 `elemVarSet` tmpls
753 = uVarX tyvar2 ty1 k subst
756 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
757 | n1 == n2 = uTysX t1 t2 k subst
758 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
759 | c1 == c2 = uTyListsX tys1 tys2 k subst
760 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
761 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
763 -- Functions; just check the two parts
764 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
765 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
767 -- Type constructors must match
768 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
769 | (con1 == con2 && length tys1 == length tys2)
770 = uTyListsX tys1 tys2 k subst
772 -- Applications need a bit of care!
773 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
774 -- NB: we've already dealt with type variables and Notes,
775 -- so if one type is an App the other one jolly well better be too
776 uTysX (AppTy s1 t1) ty2 k subst
777 = case tcSplitAppTy_maybe ty2 of
778 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
779 Nothing -> Nothing -- Fail
781 uTysX ty1 (AppTy s2 t2) k subst
782 = case tcSplitAppTy_maybe ty1 of
783 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
784 Nothing -> Nothing -- Fail
786 -- Not expecting for-alls in unification
788 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
789 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
793 uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
794 uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
796 -- Anything else fails
797 uTysX ty1 ty2 k subst = Nothing
800 uTyListsX [] [] k subst = k subst
801 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
802 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
806 -- Invariant: tv1 is a unifiable variable
807 uVarX tv1 ty2 k subst@(tmpls, env)
808 = case lookupSubstEnv env tv1 of
809 Just (DoneTy ty1) -> -- Already bound
810 uTysX ty1 ty2 k subst
812 Nothing -- Not already bound
813 | typeKind ty2 `eqKind` tyVarKind tv1
814 && occur_check_ok ty2
815 -> -- No kind mismatch nor occur check
816 UASSERT( not (isUTy ty2) )
817 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
819 | otherwise -> Nothing -- Fail if kind mis-match or occur check
821 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
822 occur_check_ok_tv tv | tv1 == tv = False
823 | otherwise = case lookupSubstEnv env tv of
825 Just (DoneTy ty) -> occur_check_ok ty
830 %************************************************************************
832 \subsection{Matching on types}
834 %************************************************************************
836 Matching is a {\em unidirectional} process, matching a type against a
837 template (which is just a type with type variables in it). The
838 matcher assumes that there are no repeated type variables in the
839 template, so that it simply returns a mapping of type variables to
840 types. It also fails on nested foralls.
842 @matchTys@ matches corresponding elements of a list of templates and
843 types. It and @matchTy@ both ignore usage annotations, unlike the
844 main function @match@.
847 matchTy :: TyVarSet -- Template tyvars
849 -> Type -- Proposed instance of template
850 -> Maybe TyVarSubstEnv -- Matching substitution
853 matchTys :: TyVarSet -- Template tyvars
854 -> [Type] -- Templates
855 -> [Type] -- Proposed instance of template
856 -> Maybe (TyVarSubstEnv, -- Matching substitution
857 [Type]) -- Left over instance types
859 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
861 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
862 (\ (senv,tys) -> Just (senv,tys))
866 @match@ is the main function. It takes a flag indicating whether
867 usage annotations are to be respected.
870 match :: Type -> Type -- Current match pair
871 -> TyVarSet -- Template vars
872 -> (TyVarSubstEnv -> Maybe result) -- Continuation
873 -> TyVarSubstEnv -- Current subst
876 -- When matching against a type variable, see if the variable
877 -- has already been bound. If so, check that what it's bound to
878 -- is the same as ty; if not, bind it and carry on.
880 match (TyVarTy v) ty tmpls k senv
881 | v `elemVarSet` tmpls
882 = -- v is a template variable
883 case lookupSubstEnv senv v of
884 Nothing -> UASSERT( not (isUTy ty) )
885 k (extendSubstEnv senv v (DoneTy ty))
886 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
887 | otherwise -> Nothing -- Fails
890 = -- v is not a template variable; ty had better match
891 -- Can't use (==) because types differ
892 case tcGetTyVar_maybe ty of
893 Just v' | v == v' -> k senv -- Success
894 other -> Nothing -- Failure
895 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
896 -- I guess the reason the Note-stripping case is *last* rather than first
897 -- is to preserve type synonyms etc., so I'm not moving it to the
898 -- top; but this means that (without the deNotetype) a type
899 -- variable may not match the pattern (TyVarTy v') as one would
900 -- expect, due to an intervening Note. KSW 2000-06.
903 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
904 | n1 == n2 = match t1 t2 tmpls k senv
905 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
906 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
907 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
908 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
910 -- Functions; just check the two parts
911 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
912 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
914 match (AppTy fun1 arg1) ty2 tmpls k senv
915 = case tcSplitAppTy_maybe ty2 of
916 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
917 Nothing -> Nothing -- Fail
919 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
920 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
922 -- Newtypes are opaque; other source types should not happen
923 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
924 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
926 match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
927 match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
929 -- With type synonyms, we have to be careful for the exact
930 -- same reasons as in the unifier. Please see the
931 -- considerable commentary there before changing anything
933 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
934 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
937 match _ _ _ _ _ = Nothing
939 match_list_exactly tys1 tys2 tmpls k senv
940 = match_list tys1 tys2 tmpls k' senv
942 k' (senv', tys2') | null tys2' = k senv' -- Succeed
943 | otherwise = Nothing -- Fail
945 match_list [] tys2 tmpls k senv = k (senv, tys2)
946 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
947 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
948 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv