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,
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, Type, SourceType(..), PredType, ThetaType,
67 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
68 mkForAllTy, mkForAllTys,
69 mkFunTy, mkFunTys, zipFunTys,
70 mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
71 mkTyVarTy, mkTyVarTys, mkTyConTy,
72 predTyUnique, mkClassPred,
73 isUnLiftedType, -- Source types are always lifted
74 isUnboxedTupleType, -- Ditto
75 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
76 tidyTyVar, tidyTyVars,
80 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
83 #include "HsVersions.h"
86 import {-# SOURCE #-} PprType( pprType )
89 import TypeRep ( Type(..), TyNote(..) ) -- friend
90 import Type -- Lots and lots
91 import TyCon ( TyCon, isPrimTyCon, tyConArity, isNewTyCon )
92 import Class ( classTyCon, classHasFDs, Class )
93 import Var ( TyVar, tyVarName, isTyVar, tyVarKind, mkTyVar )
98 import CmdLineOpts ( opt_DictsStrict )
99 import Name ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
100 mkLocalName, mkDerivedTyConOcc
102 import OccName ( OccName, mkDictOcc )
104 import PrelNames ( floatTyConKey, doubleTyConKey, foreignPtrTyConKey,
105 integerTyConKey, intTyConKey, addrTyConKey, boolTyConKey )
106 import Unique ( Unique, Uniquable(..), mkTupleTyConUnique )
107 import SrcLoc ( SrcLoc, noSrcLoc )
108 import Util ( nOfThem, cmpList, thenCmp )
109 import Maybes ( maybeToBool, expectJust )
110 import BasicTypes ( Boxity(..) )
115 %************************************************************************
117 \subsection{Tau, sigma and rho}
119 %************************************************************************
122 type SigmaType = Type
125 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
127 mkRhoTy :: [SourceType] -> Type -> Type
128 mkRhoTy theta ty = UASSERT2( not (isUTy ty), pprType ty )
129 foldr (\p r -> FunTy (mkUTyM (mkPredTy p)) (mkUTyM r)) ty theta
134 @isTauTy@ tests for nested for-alls.
137 isTauTy :: Type -> Bool
138 isTauTy (TyVarTy v) = True
139 isTauTy (TyConApp _ tys) = all isTauTy tys
140 isTauTy (AppTy a b) = isTauTy a && isTauTy b
141 isTauTy (FunTy a b) = isTauTy a && isTauTy b
142 isTauTy (SourceTy p) = isTauTy (sourceTypeRep p)
143 isTauTy (NoteTy _ ty) = isTauTy ty
144 isTauTy (UsageTy _ ty) = isTauTy ty
145 isTauTy other = False
149 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
150 -- construct a dictionary function name
151 getDFunTyKey (TyVarTy tv) = getOccName tv
152 getDFunTyKey (TyConApp tc _) = getOccName tc
153 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
154 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
155 getDFunTyKey (FunTy arg _) = getOccName funTyCon
156 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
157 getDFunTyKey (UsageTy _ t) = getDFunTyKey t
158 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
159 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
160 -- SourceTy shouldn't happen
164 %************************************************************************
166 \subsection{Expanding and splitting}
168 %************************************************************************
170 These tcSplit functions are like their non-Tc analogues, but
171 a) they do not look through newtypes
172 b) they do not look through PredTys
173 c) [future] they ignore usage-type annotations
175 However, they are non-monadic and do not follow through mutable type
176 variables. It's up to you to make sure this doesn't matter.
179 tcSplitForAllTys :: Type -> ([TyVar], Type)
180 tcSplitForAllTys ty = split ty ty []
182 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
183 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
184 split orig_ty (UsageTy _ ty) tvs = split orig_ty ty tvs
185 split orig_ty t tvs = (reverse tvs, orig_ty)
187 tcIsForAllTy (ForAllTy tv ty) = True
188 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
189 tcIsForAllTy (UsageTy n ty) = tcIsForAllTy ty
190 tcIsForAllTy t = False
192 tcSplitRhoTy :: Type -> ([PredType], Type)
193 tcSplitRhoTy ty = split ty ty []
195 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
196 Just p -> split res res (p:ts)
197 Nothing -> (reverse ts, orig_ty)
198 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
199 split orig_ty (UsageTy _ ty) ts = split orig_ty ty ts
200 split orig_ty ty ts = (reverse ts, orig_ty)
202 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
203 (tvs, rho) -> case tcSplitRhoTy rho of
204 (theta, tau) -> (tvs, theta, tau)
206 tcTyConAppTyCon :: Type -> TyCon
207 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
209 tcTyConAppArgs :: Type -> [Type]
210 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
212 tcSplitTyConApp :: Type -> (TyCon, [Type])
213 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
215 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
217 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
218 -- Newtypes are opaque, so they may be split
219 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
220 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [unUTy arg,unUTy res])
221 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
222 tcSplitTyConApp_maybe (UsageTy _ ty) = tcSplitTyConApp_maybe ty
223 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
224 -- However, predicates are not treated
225 -- as tycon applications by the type checker
226 tcSplitTyConApp_maybe other = Nothing
228 tcSplitFunTys :: Type -> ([Type], Type)
229 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
231 Just (arg,res) -> (arg:args, res')
233 (args,res') = tcSplitFunTys res
235 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
236 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
237 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
238 tcSplitFunTy_maybe (UsageTy _ ty) = tcSplitFunTy_maybe ty
239 tcSplitFunTy_maybe other = Nothing
241 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
242 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
245 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
246 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2)
247 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
248 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
249 tcSplitAppTy_maybe (UsageTy _ ty) = tcSplitAppTy_maybe ty
250 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
251 --- Don't forget that newtype!
252 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
253 tcSplitAppTy_maybe other = Nothing
255 tc_split_app tc [] = Nothing
256 tc_split_app tc tys = split tys []
258 split [ty2] acc = Just (TyConApp tc (reverse acc), ty2)
259 split (ty:tys) acc = split tys (ty:acc)
261 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
263 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
265 tcGetTyVar_maybe :: Type -> Maybe TyVar
266 tcGetTyVar_maybe (TyVarTy tv) = Just tv
267 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
268 tcGetTyVar_maybe ty@(UsageTy _ _) = pprPanic "tcGetTyVar_maybe: UTy:" (pprType ty)
269 tcGetTyVar_maybe other = Nothing
271 tcGetTyVar :: String -> Type -> TyVar
272 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
274 tcIsTyVarTy :: Type -> Bool
275 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
278 The type of a method for class C is always of the form:
279 Forall a1..an. C a1..an => sig_ty
280 where sig_ty is the type given by the method's signature, and thus in general
281 is a ForallTy. At the point that splitMethodTy is called, it is expected
282 that the outer Forall has already been stripped off. splitMethodTy then
283 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
287 tcSplitMethodTy :: Type -> (PredType, Type)
288 tcSplitMethodTy ty = split ty
290 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
292 Nothing -> panic "splitMethodTy"
293 split (NoteTy n ty) = split ty
294 split (UsageTy _ ty) = split ty
295 split _ = panic "splitMethodTy"
297 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
298 -- Split the type of a dictionary function
300 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
301 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
302 (tvs, theta, clas, tys) }}
306 %************************************************************************
308 \subsection{Predicate types}
310 %************************************************************************
312 "Predicates" are particular source types, namelyClassP or IParams
315 isPred :: SourceType -> Bool
316 isPred (ClassP _ _) = True
317 isPred (IParam _ _) = True
318 isPred (NType _ __) = False
320 isPredTy :: Type -> Bool
321 isPredTy (NoteTy _ ty) = isPredTy ty
322 isPredTy (UsageTy _ ty) = isPredTy ty
323 isPredTy (SourceTy sty) = isPred sty
326 tcSplitPredTy_maybe :: Type -> Maybe PredType
327 -- Returns Just for predicates only
328 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
329 tcSplitPredTy_maybe (UsageTy _ ty) = tcSplitPredTy_maybe ty
330 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
331 tcSplitPredTy_maybe other = Nothing
333 mkPredTy :: PredType -> Type
334 mkPredTy pred = SourceTy pred
336 mkPredTys :: ThetaType -> [Type]
337 mkPredTys preds = map SourceTy preds
339 predTyUnique :: PredType -> Unique
340 predTyUnique (IParam n _) = getUnique n
341 predTyUnique (ClassP clas tys) = getUnique clas
343 predHasFDs :: PredType -> Bool
344 -- True if the predicate has functional depenencies;
345 -- I.e. should participate in improvement
346 predHasFDs (IParam _ _) = True
347 predHasFDs (ClassP cls _) = classHasFDs cls
349 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
350 mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
351 mkPredName uniq loc (IParam name ty) = name
355 --------------------- Dictionary types ---------------------------------
358 mkClassPred clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
361 isClassPred :: SourceType -> Bool
362 isClassPred (ClassP clas tys) = True
363 isClassPred other = False
365 isTyVarClassPred (ClassP clas tys) = all isTyVarTy tys
366 isTyVarClassPred other = False
368 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
369 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
370 getClassPredTys_maybe _ = Nothing
372 getClassPredTys :: PredType -> (Class, [Type])
373 getClassPredTys (ClassP clas tys) = (clas, tys)
375 mkDictTy :: Class -> [Type] -> Type
376 mkDictTy clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
377 mkPredTy (ClassP clas tys)
379 isDictTy :: Type -> Bool
380 isDictTy (SourceTy p) = isClassPred p
381 isDictTy (NoteTy _ ty) = isDictTy ty
382 isDictTy (UsageTy _ ty) = isDictTy ty
383 isDictTy other = False
386 --------------------- Implicit parameters ---------------------------------
389 isIPPred :: SourceType -> Bool
390 isIPPred (IParam _ _) = True
391 isIPPred other = False
393 inheritablePred :: PredType -> Bool
394 -- Can be inherited by a context. For example, consider
395 -- f x = let g y = (?v, y+x)
396 -- in (g 3 with ?v = 8,
398 -- The point is that g's type must be quantifed over ?v:
399 -- g :: (?v :: a) => a -> a
400 -- but it doesn't need to be quantified over the Num a dictionary
401 -- which can be free in g's rhs, and shared by both calls to g
402 inheritablePred (ClassP _ _) = True
403 inheritablePred other = False
405 predMentionsIPs :: SourceType -> NameSet -> Bool
406 predMentionsIPs (IParam n _) ns = n `elemNameSet` ns
407 predMentionsIPs other ns = False
411 %************************************************************************
413 \subsection{Comparison}
415 %************************************************************************
417 Comparison, taking note of newtypes, predicates, etc,
418 But ignoring usage types
421 tcEqType :: Type -> Type -> Bool
422 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
424 tcEqPred :: PredType -> PredType -> Bool
425 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
428 tcCmpType :: Type -> Type -> Ordering
429 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
431 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
433 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
435 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
438 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
439 -- The "env" maps type variables in ty1 to type variables in ty2
440 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
441 -- we in effect substitute tv2 for tv1 in t1 before continuing
443 -- Look through NoteTy and UsageTy
444 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
445 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
446 cmpTy env (UsageTy _ ty1) ty2 = cmpTy env ty1 ty2
447 cmpTy env ty1 (UsageTy _ ty2) = cmpTy env ty1 ty2
449 -- Deal with equal constructors
450 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
451 Just tv1a -> tv1a `compare` tv2
452 Nothing -> tv1 `compare` tv2
454 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
455 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
456 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
457 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
458 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
460 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
461 cmpTy env (AppTy _ _) (TyVarTy _) = GT
463 cmpTy env (FunTy _ _) (TyVarTy _) = GT
464 cmpTy env (FunTy _ _) (AppTy _ _) = GT
466 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
467 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
468 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
470 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
471 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
472 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
473 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
475 cmpTy env (SourceTy _) t2 = GT
481 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
482 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
483 -- Compare types as well as names for implicit parameters
484 -- This comparison is used exclusively (I think) for the
485 -- finite map built in TcSimplify
486 cmpSourceTy env (IParam _ _) sty = LT
488 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
489 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
490 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
492 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
493 cmpSourceTy env (NType _ _) sty = GT
496 PredTypes are used as a FM key in TcSimplify,
497 so we take the easy path and make them an instance of Ord
500 instance Eq SourceType where { (==) = tcEqPred }
501 instance Ord SourceType where { compare = tcCmpPred }
505 %************************************************************************
507 \subsection{Predicates}
509 %************************************************************************
511 isQualifiedTy returns true of any qualified type. It doesn't *necessarily* have
513 f :: (?x::Int) => Int -> Int
516 isQualifiedTy :: Type -> Bool
517 isQualifiedTy (ForAllTy tyvar ty) = True
518 isQualifiedTy (FunTy a b) = isPredTy a
519 isQualifiedTy (NoteTy n ty) = isQualifiedTy ty
520 isQualifiedTy (UsageTy _ ty) = isQualifiedTy ty
521 isQualifiedTy _ = False
523 isOverloadedTy :: Type -> Bool
524 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
525 isOverloadedTy (FunTy a b) = isPredTy a
526 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
527 isOverloadedTy (UsageTy _ ty) = isOverloadedTy ty
528 isOverloadedTy _ = False
532 isFloatTy = is_tc floatTyConKey
533 isDoubleTy = is_tc doubleTyConKey
534 isForeignPtrTy = is_tc foreignPtrTyConKey
535 isIntegerTy = is_tc integerTyConKey
536 isIntTy = is_tc intTyConKey
537 isAddrTy = is_tc addrTyConKey
538 isBoolTy = is_tc boolTyConKey
539 isUnitTy = is_tc (mkTupleTyConUnique Boxed 0)
541 is_tc :: Unique -> Type -> Bool
542 -- Newtypes are opaque to this
543 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
544 Just (tc, _) -> uniq == getUnique tc
549 isPrimitiveType :: Type -> Bool
550 -- Returns types that are opaque to Haskell.
551 -- Most of these are unlifted, but now that we interact with .NET, we
552 -- may have primtive (foreign-imported) types that are lifted
553 isPrimitiveType ty = case splitTyConApp_maybe ty of
554 Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc )
559 @isStrictType@ computes whether an argument (or let RHS) should
560 be computed strictly or lazily, based only on its type
563 isStrictType :: Type -> Bool
565 | isUnLiftedType ty = True
566 | Just pred <- tcSplitPredTy_maybe ty = isStrictPred pred
569 isStrictPred (ClassP clas _) = opt_DictsStrict
570 && not (isNewTyCon (classTyCon clas))
571 isStrictPred pred = False
572 -- We may be strict in dictionary types, but only if it
573 -- has more than one component.
574 -- [Being strict in a single-component dictionary risks
575 -- poking the dictionary component, which is wrong.]
579 %************************************************************************
583 %************************************************************************
586 hoistForAllTys :: Type -> Type
587 -- Move all the foralls to the top
588 -- e.g. T -> forall a. a ==> forall a. T -> a
589 -- Careful: LOSES USAGE ANNOTATIONS!
591 = case hoist ty of { (tvs, body) -> mkForAllTys tvs body }
593 hoist :: Type -> ([TyVar], Type)
594 hoist ty = case tcSplitFunTys ty of { (args, res) ->
595 case tcSplitForAllTys res of {
596 ([], body) -> ([], ty) ;
597 (tvs1, body1) -> case hoist body1 of { (tvs2,body2) ->
598 (tvs1 ++ tvs2, mkFunTys args body2)
604 deNoteType :: Type -> Type
605 -- Remove synonyms, but not source types
606 deNoteType ty@(TyVarTy tyvar) = ty
607 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
608 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
609 deNoteType (NoteTy _ ty) = deNoteType ty
610 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
611 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
612 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
613 deNoteType (UsageTy u ty) = UsageTy u (deNoteType ty)
615 deNoteSourceType :: SourceType -> SourceType
616 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
617 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
618 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
621 Find the free names of a type, including the type constructors and classes it mentions
622 This is used in the front end of the compiler
625 namesOfType :: Type -> NameSet
626 namesOfType (TyVarTy tv) = unitNameSet (getName tv)
627 namesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
628 namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
629 namesOfType (NoteTy other_note ty2) = namesOfType ty2
630 namesOfType (SourceTy (IParam n ty)) = namesOfType ty
631 namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
632 namesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
633 namesOfType (FunTy arg res) = namesOfType arg `unionNameSets` namesOfType res
634 namesOfType (AppTy fun arg) = namesOfType fun `unionNameSets` namesOfType arg
635 namesOfType (ForAllTy tyvar ty) = namesOfType ty `delFromNameSet` getName tyvar
636 namesOfType (UsageTy u ty) = namesOfType u `unionNameSets` namesOfType ty
638 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
640 namesOfDFunHead :: Type -> NameSet
641 -- Find the free type constructors and classes
642 -- of the head of the dfun instance type
643 -- The 'dfun_head_type' is because of
644 -- instance Foo a => Baz T where ...
645 -- The decl is an orphan if Baz and T are both not locally defined,
646 -- even if Foo *is* locally defined
647 namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
648 (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
653 %************************************************************************
655 \subsection{Unification with an explicit substitution}
657 %************************************************************************
659 (allDistinctTyVars tys tvs) = True
661 all the types tys are type variables,
662 distinct from each other and from tvs.
664 This is useful when checking that unification hasn't unified signature
665 type variables. For example, if the type sig is
666 f :: forall a b. a -> b -> b
667 we want to check that 'a' and 'b' havn't
668 (a) been unified with a non-tyvar type
669 (b) been unified with each other (all distinct)
670 (c) been unified with a variable free in the environment
673 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
675 allDistinctTyVars [] acc
677 allDistinctTyVars (ty:tys) acc
678 = case tcGetTyVar_maybe ty of
679 Nothing -> False -- (a)
680 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
681 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
685 %************************************************************************
687 \subsection{Unification with an explicit substitution}
689 %************************************************************************
691 Unify types with an explicit substitution and no monad.
692 Ignore usage annotations.
696 = (TyVarSet, -- Set of template tyvars
697 TyVarSubstEnv) -- Not necessarily idempotent
699 unifyTysX :: TyVarSet -- Template tyvars
702 -> Maybe TyVarSubstEnv
703 unifyTysX tmpl_tyvars ty1 ty2
704 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
706 unifyExtendTysX :: TyVarSet -- Template tyvars
707 -> TyVarSubstEnv -- Substitution to start with
710 -> Maybe TyVarSubstEnv -- Extended substitution
711 unifyExtendTysX tmpl_tyvars subst ty1 ty2
712 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
714 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
715 -> Maybe TyVarSubstEnv
716 unifyTyListsX tmpl_tyvars tys1 tys2
717 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
722 -> (MySubst -> Maybe result)
726 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
727 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
729 -- Variables; go for uVar
730 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
733 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
734 | tyvar1 `elemVarSet` tmpls
735 = uVarX tyvar1 ty2 k subst
736 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
737 | tyvar2 `elemVarSet` tmpls
738 = uVarX tyvar2 ty1 k subst
740 -- Functions; just check the two parts
741 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
742 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
744 -- Type constructors must match
745 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
746 | (con1 == con2 && length tys1 == length tys2)
747 = uTyListsX tys1 tys2 k subst
749 -- Applications need a bit of care!
750 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
751 -- NB: we've already dealt with type variables and Notes,
752 -- so if one type is an App the other one jolly well better be too
753 uTysX (AppTy s1 t1) ty2 k subst
754 = case tcSplitAppTy_maybe ty2 of
755 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
756 Nothing -> Nothing -- Fail
758 uTysX ty1 (AppTy s2 t2) k subst
759 = case tcSplitAppTy_maybe ty1 of
760 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
761 Nothing -> Nothing -- Fail
763 -- Not expecting for-alls in unification
765 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
766 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
770 uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
771 uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
773 -- Anything else fails
774 uTysX ty1 ty2 k subst = Nothing
777 uTyListsX [] [] k subst = k subst
778 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
779 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
783 -- Invariant: tv1 is a unifiable variable
784 uVarX tv1 ty2 k subst@(tmpls, env)
785 = case lookupSubstEnv env tv1 of
786 Just (DoneTy ty1) -> -- Already bound
787 uTysX ty1 ty2 k subst
789 Nothing -- Not already bound
790 | typeKind ty2 `eqKind` tyVarKind tv1
791 && occur_check_ok ty2
792 -> -- No kind mismatch nor occur check
793 UASSERT( not (isUTy ty2) )
794 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
796 | otherwise -> Nothing -- Fail if kind mis-match or occur check
798 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
799 occur_check_ok_tv tv | tv1 == tv = False
800 | otherwise = case lookupSubstEnv env tv of
802 Just (DoneTy ty) -> occur_check_ok ty
807 %************************************************************************
809 \subsection{Matching on types}
811 %************************************************************************
813 Matching is a {\em unidirectional} process, matching a type against a
814 template (which is just a type with type variables in it). The
815 matcher assumes that there are no repeated type variables in the
816 template, so that it simply returns a mapping of type variables to
817 types. It also fails on nested foralls.
819 @matchTys@ matches corresponding elements of a list of templates and
820 types. It and @matchTy@ both ignore usage annotations, unlike the
821 main function @match@.
824 matchTy :: TyVarSet -- Template tyvars
826 -> Type -- Proposed instance of template
827 -> Maybe TyVarSubstEnv -- Matching substitution
830 matchTys :: TyVarSet -- Template tyvars
831 -> [Type] -- Templates
832 -> [Type] -- Proposed instance of template
833 -> Maybe (TyVarSubstEnv, -- Matching substitution
834 [Type]) -- Left over instance types
836 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
838 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
839 (\ (senv,tys) -> Just (senv,tys))
843 @match@ is the main function. It takes a flag indicating whether
844 usage annotations are to be respected.
847 match :: Type -> Type -- Current match pair
848 -> TyVarSet -- Template vars
849 -> (TyVarSubstEnv -> Maybe result) -- Continuation
850 -> TyVarSubstEnv -- Current subst
853 -- When matching against a type variable, see if the variable
854 -- has already been bound. If so, check that what it's bound to
855 -- is the same as ty; if not, bind it and carry on.
857 match (TyVarTy v) ty tmpls k senv
858 | v `elemVarSet` tmpls
859 = -- v is a template variable
860 case lookupSubstEnv senv v of
861 Nothing -> UASSERT( not (isUTy ty) )
862 k (extendSubstEnv senv v (DoneTy ty))
863 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
864 | otherwise -> Nothing -- Fails
867 = -- v is not a template variable; ty had better match
868 -- Can't use (==) because types differ
869 case tcGetTyVar_maybe ty of
870 Just v' | v == v' -> k senv -- Success
871 other -> Nothing -- Failure
872 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
873 -- I guess the reason the Note-stripping case is *last* rather than first
874 -- is to preserve type synonyms etc., so I'm not moving it to the
875 -- top; but this means that (without the deNotetype) a type
876 -- variable may not match the pattern (TyVarTy v') as one would
877 -- expect, due to an intervening Note. KSW 2000-06.
879 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
880 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
882 match (AppTy fun1 arg1) ty2 tmpls k senv
883 = case tcSplitAppTy_maybe ty2 of
884 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
885 Nothing -> Nothing -- Fail
887 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
888 | tc1 == tc2 = match_tc_app tys1 tys2 tmpls k senv
890 -- Newtypes are opaque; other source types should not happen
891 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
892 | tc1 == tc2 = match_tc_app tys1 tys2 tmpls k senv
894 match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
895 match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
897 -- With type synonyms, we have to be careful for the exact
898 -- same reasons as in the unifier. Please see the
899 -- considerable commentary there before changing anything
901 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
902 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
905 match _ _ _ _ _ = Nothing
907 match_tc_app tys1 tys2 tmpls k senv
908 = match_list tys1 tys2 tmpls k' senv
910 k' (senv', tys2') | null tys2' = k senv' -- Succeed
911 | otherwise = Nothing -- Fail
913 match_list [] tys2 tmpls k senv = k (senv, tys2)
914 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
915 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
916 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv