2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcType]{Types used in the typechecker}
6 This module provides the Type interface for front-end parts of the
9 * treat "source types" as opaque:
10 newtypes, and predicates are meaningful.
11 * look through usage types
13 The "tc" prefix is for "typechechecker", because the type checker
14 is the principal client.
18 --------------------------------
20 TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
21 TcTyVar, TcTyVarSet, TcKind,
23 --------------------------------
25 TyVarDetails(..), isUserTyVar, isSkolemTyVar, isHoleTyVar,
28 --------------------------------
32 --------------------------------
34 -- These are important because they do not look through newtypes
35 tcSplitForAllTys, tcSplitPhiTy,
36 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
37 tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
38 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
39 tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
41 ---------------------------------
43 -- Again, newtypes are opaque
44 tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
45 isSigmaTy, isOverloadedTy,
46 isDoubleTy, isFloatTy, isIntTy,
47 isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
48 isTauTy, tcIsTyVarTy, tcIsForAllTy,
51 ---------------------------------
52 -- Misc type manipulators
53 deNoteType, classNamesOfTheta,
54 tyClsNamesOfType, tyClsNamesOfDFunHead,
57 ---------------------------------
59 getClassPredTys_maybe, getClassPredTys,
60 isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
61 mkDictTy, tcSplitPredTy_maybe,
62 isDictTy, tcSplitDFunTy, predTyUnique,
63 mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
65 ---------------------------------
66 -- Foreign import and export
67 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
68 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
69 isFFIExportResultTy, -- :: Type -> Bool
70 isFFIExternalTy, -- :: Type -> Bool
71 isFFIDynArgumentTy, -- :: Type -> Bool
72 isFFIDynResultTy, -- :: Type -> Bool
73 isFFILabelTy, -- :: Type -> Bool
75 ---------------------------------
76 -- Unifier and matcher
77 unifyTysX, unifyTyListsX, unifyExtendTysX,
78 matchTy, matchTys, match,
80 --------------------------------
81 -- Rexported from Type
82 Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
83 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
84 superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
85 isTypeKind, isAnyTypeKind,
87 Type, SourceType(..), PredType, ThetaType,
88 mkForAllTy, mkForAllTys,
89 mkFunTy, mkFunTys, zipFunTys,
90 mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
91 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
93 isUnLiftedType, -- Source types are always lifted
94 isUnboxedTupleType, -- Ditto
95 isPrimitiveType, isTyVarTy,
97 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
98 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
99 typeKind, eqKind, eqUsage,
101 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
104 #include "HsVersions.h"
107 import {-# SOURCE #-} PprType( pprType )
108 -- PprType imports TcType so that it can print intelligently
111 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
113 import Type ( -- Re-exports
114 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
115 Kind, Type, SourceType(..), PredType, ThetaType,
116 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
117 mkForAllTy, mkForAllTys, defaultKind, isTypeKind, isAnyTypeKind,
118 mkFunTy, mkFunTys, zipFunTys, isTyVarTy,
119 mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
120 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
121 isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
122 splitNewType_maybe, splitTyConApp_maybe,
123 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
124 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
125 hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
127 import TyCon ( TyCon, isUnLiftedTyCon )
128 import Class ( classHasFDs, Class )
129 import Var ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
130 import ForeignCall ( Safety, playSafe )
135 import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
136 import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
137 import OccName ( OccName, mkDictOcc )
139 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
140 import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
141 import BasicTypes ( IPName(..), ipNameName )
142 import Unique ( Unique, Uniquable(..) )
143 import SrcLoc ( SrcLoc )
144 import Util ( cmpList, thenCmp, equalLength, snocView )
145 import Maybes ( maybeToBool, expectJust )
150 %************************************************************************
154 %************************************************************************
156 The type checker divides the generic Type world into the
157 following more structured beasts:
159 sigma ::= forall tyvars. phi
160 -- A sigma type is a qualified type
162 -- Note that even if 'tyvars' is empty, theta
163 -- may not be: e.g. (?x::Int) => Int
165 -- Note that 'sigma' is in prenex form:
166 -- all the foralls are at the front.
167 -- A 'phi' type has no foralls to the right of
175 -- A 'tau' type has no quantification anywhere
176 -- Note that the args of a type constructor must be taus
178 | tycon tau_1 .. tau_n
182 -- In all cases, a (saturated) type synonym application is legal,
183 -- provided it expands to the required form.
187 type SigmaType = Type
193 type TcTyVar = TyVar -- Might be a mutable tyvar
194 type TcTyVarSet = TyVarSet
196 type TcType = Type -- A TcType can have mutable type variables
197 -- Invariant on ForAllTy in TcTypes:
199 -- a cannot occur inside a MutTyVar in T; that is,
200 -- T is "flattened" before quantifying over a
202 type TcPredType = PredType
203 type TcThetaType = ThetaType
204 type TcSigmaType = TcType
205 type TcRhoType = TcType
206 type TcTauType = TcType
211 %************************************************************************
213 \subsection{TyVarDetails}
215 %************************************************************************
217 TyVarDetails gives extra info about type variables, used during type
218 checking. It's attached to mutable type variables only.
219 It's knot-tied back to Var.lhs. There is no reason in principle
220 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
224 = HoleTv -- Used *only* by the type checker when passing in a type
225 -- variable that should be side-effected to the result type.
226 -- Always has kind openTypeKind.
227 -- Never appears in types
229 | SigTv -- Introduced when instantiating a type signature,
230 -- prior to checking that the defn of a fn does
231 -- have the expected type. Should not be instantiated.
233 -- f :: forall a. a -> a
235 -- When checking e, with expected type (a->a), we
236 -- should not instantiate a
238 | ClsTv -- Scoped type variable introduced by a class decl
239 -- class C a where ...
241 | InstTv -- Ditto, but instance decl
243 | PatSigTv -- Scoped type variable, introduced by a pattern
247 | VanillaTv -- Everything else
249 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
250 isUserTyVar tv = case mutTyVarDetails tv of
254 isSkolemTyVar :: TcTyVar -> Bool
255 isSkolemTyVar tv = case mutTyVarDetails tv of
261 isHoleTyVar :: TcTyVar -> Bool
262 -- NB: the hole might be filled in by now, and this
263 -- function does not check for that
264 isHoleTyVar tv = ASSERT( isMutTyVar tv )
265 case mutTyVarDetails tv of
269 tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
272 = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
273 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
277 details SigTv = ptext SLIT("type signature")
278 details ClsTv = ptext SLIT("class declaration")
279 details InstTv = ptext SLIT("instance declaration")
280 details PatSigTv = ptext SLIT("pattern type signature")
281 details HoleTv = ptext SLIT("//hole//") -- Should not happen
282 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
286 %************************************************************************
288 \subsection{Tau, sigma and rho}
290 %************************************************************************
293 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
295 mkPhiTy :: [SourceType] -> Type -> Type
296 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
300 @isTauTy@ tests for nested for-alls.
303 isTauTy :: Type -> Bool
304 isTauTy (TyVarTy v) = True
305 isTauTy (TyConApp _ tys) = all isTauTy tys
306 isTauTy (AppTy a b) = isTauTy a && isTauTy b
307 isTauTy (FunTy a b) = isTauTy a && isTauTy b
308 isTauTy (SourceTy p) = True -- Don't look through source types
309 isTauTy (NoteTy _ ty) = isTauTy ty
310 isTauTy other = False
314 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
315 -- construct a dictionary function name
316 getDFunTyKey (TyVarTy tv) = getOccName tv
317 getDFunTyKey (TyConApp tc _) = getOccName tc
318 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
319 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
320 getDFunTyKey (FunTy arg _) = getOccName funTyCon
321 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
322 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
323 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
324 -- SourceTy shouldn't happen
328 %************************************************************************
330 \subsection{Expanding and splitting}
332 %************************************************************************
334 These tcSplit functions are like their non-Tc analogues, but
335 a) they do not look through newtypes
336 b) they do not look through PredTys
337 c) [future] they ignore usage-type annotations
339 However, they are non-monadic and do not follow through mutable type
340 variables. It's up to you to make sure this doesn't matter.
343 tcSplitForAllTys :: Type -> ([TyVar], Type)
344 tcSplitForAllTys ty = split ty ty []
346 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
347 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
348 split orig_ty t tvs = (reverse tvs, orig_ty)
350 tcIsForAllTy (ForAllTy tv ty) = True
351 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
352 tcIsForAllTy t = False
354 tcSplitPhiTy :: Type -> ([PredType], Type)
355 tcSplitPhiTy ty = split ty ty []
357 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
358 Just p -> split res res (p:ts)
359 Nothing -> (reverse ts, orig_ty)
360 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
361 split orig_ty ty ts = (reverse ts, orig_ty)
363 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
364 (tvs, rho) -> case tcSplitPhiTy rho of
365 (theta, tau) -> (tvs, theta, tau)
367 tcTyConAppTyCon :: Type -> TyCon
368 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
370 tcTyConAppArgs :: Type -> [Type]
371 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
373 tcSplitTyConApp :: Type -> (TyCon, [Type])
374 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
376 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
378 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
379 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
380 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
381 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
382 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
383 -- Newtypes are opaque, so they may be split
384 -- However, predicates are not treated
385 -- as tycon applications by the type checker
386 tcSplitTyConApp_maybe other = Nothing
388 tcSplitFunTys :: Type -> ([Type], Type)
389 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
391 Just (arg,res) -> (arg:args, res')
393 (args,res') = tcSplitFunTys res
395 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
396 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
397 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
398 tcSplitFunTy_maybe other = Nothing
400 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
401 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
404 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
405 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
406 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
407 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
408 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys --- Don't forget that newtype!
409 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
410 tcSplitAppTy_maybe other = Nothing
412 tc_split_app tc tys = case snocView tys of
413 Just (tys',ty') -> Just (TyConApp tc tys', ty')
416 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
418 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
420 tcSplitAppTys :: Type -> (Type, [Type])
424 go ty args = case tcSplitAppTy_maybe ty of
425 Just (ty', arg) -> go ty' (arg:args)
428 tcGetTyVar_maybe :: Type -> Maybe TyVar
429 tcGetTyVar_maybe (TyVarTy tv) = Just tv
430 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
431 tcGetTyVar_maybe other = Nothing
433 tcGetTyVar :: String -> Type -> TyVar
434 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
436 tcIsTyVarTy :: Type -> Bool
437 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
440 The type of a method for class C is always of the form:
441 Forall a1..an. C a1..an => sig_ty
442 where sig_ty is the type given by the method's signature, and thus in general
443 is a ForallTy. At the point that splitMethodTy is called, it is expected
444 that the outer Forall has already been stripped off. splitMethodTy then
445 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
449 tcSplitMethodTy :: Type -> (PredType, Type)
450 tcSplitMethodTy ty = split ty
452 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
454 Nothing -> panic "splitMethodTy"
455 split (NoteTy n ty) = split ty
456 split _ = panic "splitMethodTy"
458 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
459 -- Split the type of a dictionary function
461 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
462 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
463 (tvs, theta, clas, tys) }}
466 (allDistinctTyVars tys tvs) = True
468 all the types tys are type variables,
469 distinct from each other and from tvs.
471 This is useful when checking that unification hasn't unified signature
472 type variables. For example, if the type sig is
473 f :: forall a b. a -> b -> b
474 we want to check that 'a' and 'b' havn't
475 (a) been unified with a non-tyvar type
476 (b) been unified with each other (all distinct)
477 (c) been unified with a variable free in the environment
480 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
482 allDistinctTyVars [] acc
484 allDistinctTyVars (ty:tys) acc
485 = case tcGetTyVar_maybe ty of
486 Nothing -> False -- (a)
487 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
488 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
492 %************************************************************************
494 \subsection{Predicate types}
496 %************************************************************************
498 "Predicates" are particular source types, namelyClassP or IParams
501 isPred :: SourceType -> Bool
502 isPred (ClassP _ _) = True
503 isPred (IParam _ _) = True
504 isPred (NType _ _) = False
506 isPredTy :: Type -> Bool
507 isPredTy (NoteTy _ ty) = isPredTy ty
508 isPredTy (SourceTy sty) = isPred sty
511 tcSplitPredTy_maybe :: Type -> Maybe PredType
512 -- Returns Just for predicates only
513 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
514 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
515 tcSplitPredTy_maybe other = Nothing
517 predTyUnique :: PredType -> Unique
518 predTyUnique (IParam n _) = getUnique (ipNameName n)
519 predTyUnique (ClassP clas tys) = getUnique clas
521 predHasFDs :: PredType -> Bool
522 -- True if the predicate has functional depenencies;
523 -- I.e. should participate in improvement
524 predHasFDs (IParam _ _) = True
525 predHasFDs (ClassP cls _) = classHasFDs cls
527 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
528 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
529 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
533 --------------------- Dictionary types ---------------------------------
536 mkClassPred clas tys = ClassP clas tys
538 isClassPred :: SourceType -> Bool
539 isClassPred (ClassP clas tys) = True
540 isClassPred other = False
542 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
543 isTyVarClassPred other = False
545 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
546 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
547 getClassPredTys_maybe _ = Nothing
549 getClassPredTys :: PredType -> (Class, [Type])
550 getClassPredTys (ClassP clas tys) = (clas, tys)
552 mkDictTy :: Class -> [Type] -> Type
553 mkDictTy clas tys = mkPredTy (ClassP clas tys)
555 isDictTy :: Type -> Bool
556 isDictTy (SourceTy p) = isClassPred p
557 isDictTy (NoteTy _ ty) = isDictTy ty
558 isDictTy other = False
561 --------------------- Implicit parameters ---------------------------------
564 isIPPred :: SourceType -> Bool
565 isIPPred (IParam _ _) = True
566 isIPPred other = False
568 isInheritablePred :: PredType -> Bool
569 -- Can be inherited by a context. For example, consider
570 -- f x = let g y = (?v, y+x)
571 -- in (g 3 with ?v = 8,
573 -- The point is that g's type must be quantifed over ?v:
574 -- g :: (?v :: a) => a -> a
575 -- but it doesn't need to be quantified over the Num a dictionary
576 -- which can be free in g's rhs, and shared by both calls to g
577 isInheritablePred (ClassP _ _) = True
578 isInheritablePred other = False
580 isLinearPred :: TcPredType -> Bool
581 isLinearPred (IParam (Linear n) _) = True
582 isLinearPred other = False
586 %************************************************************************
588 \subsection{Comparison}
590 %************************************************************************
592 Comparison, taking note of newtypes, predicates, etc,
593 But ignoring usage types
596 tcEqType :: Type -> Type -> Bool
597 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
599 tcEqTypes :: [Type] -> [Type] -> Bool
600 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
602 tcEqPred :: PredType -> PredType -> Bool
603 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
606 tcCmpType :: Type -> Type -> Ordering
607 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
609 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
611 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
613 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
616 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
617 -- The "env" maps type variables in ty1 to type variables in ty2
618 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
619 -- we in effect substitute tv2 for tv1 in t1 before continuing
621 -- Look through NoteTy
622 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
623 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
625 -- Deal with equal constructors
626 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
627 Just tv1a -> tv1a `compare` tv2
628 Nothing -> tv1 `compare` tv2
630 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
631 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
632 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
633 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
634 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
636 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
637 cmpTy env (AppTy _ _) (TyVarTy _) = GT
639 cmpTy env (FunTy _ _) (TyVarTy _) = GT
640 cmpTy env (FunTy _ _) (AppTy _ _) = GT
642 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
643 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
644 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
646 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
647 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
648 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
649 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
651 cmpTy env (SourceTy _) t2 = GT
657 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
658 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
659 -- Compare types as well as names for implicit parameters
660 -- This comparison is used exclusively (I think) for the
661 -- finite map built in TcSimplify
662 cmpSourceTy env (IParam _ _) sty = LT
664 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
665 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
666 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
668 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
669 cmpSourceTy env (NType _ _) sty = GT
672 PredTypes are used as a FM key in TcSimplify,
673 so we take the easy path and make them an instance of Ord
676 instance Eq SourceType where { (==) = tcEqPred }
677 instance Ord SourceType where { compare = tcCmpPred }
681 %************************************************************************
683 \subsection{Predicates}
685 %************************************************************************
687 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
689 f :: (?x::Int) => Int -> Int
692 isSigmaTy :: Type -> Bool
693 isSigmaTy (ForAllTy tyvar ty) = True
694 isSigmaTy (FunTy a b) = isPredTy a
695 isSigmaTy (NoteTy n ty) = isSigmaTy ty
698 isOverloadedTy :: Type -> Bool
699 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
700 isOverloadedTy (FunTy a b) = isPredTy a
701 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
702 isOverloadedTy _ = False
706 isFloatTy = is_tc floatTyConKey
707 isDoubleTy = is_tc doubleTyConKey
708 isIntegerTy = is_tc integerTyConKey
709 isIntTy = is_tc intTyConKey
710 isAddrTy = is_tc addrTyConKey
711 isBoolTy = is_tc boolTyConKey
712 isUnitTy = is_tc unitTyConKey
714 is_tc :: Unique -> Type -> Bool
715 -- Newtypes are opaque to this
716 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
717 Just (tc, _) -> uniq == getUnique tc
722 %************************************************************************
726 %************************************************************************
729 deNoteType :: Type -> Type
730 -- Remove synonyms, but not source types
731 deNoteType ty@(TyVarTy tyvar) = ty
732 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
733 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
734 deNoteType (NoteTy _ ty) = deNoteType ty
735 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
736 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
737 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
739 deNoteSourceType :: SourceType -> SourceType
740 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
741 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
742 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
745 Find the free tycons and classes of a type. This is used in the front
749 tyClsNamesOfType :: Type -> NameSet
750 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
751 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
752 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
753 tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
754 tyClsNamesOfType (SourceTy (IParam n ty)) = tyClsNamesOfType ty
755 tyClsNamesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
756 tyClsNamesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` tyClsNamesOfTypes tys
757 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
758 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
759 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
761 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
763 tyClsNamesOfDFunHead :: Type -> NameSet
764 -- Find the free type constructors and classes
765 -- of the head of the dfun instance type
766 -- The 'dfun_head_type' is because of
767 -- instance Foo a => Baz T where ...
768 -- The decl is an orphan if Baz and T are both not locally defined,
769 -- even if Foo *is* locally defined
770 tyClsNamesOfDFunHead dfun_ty
771 = case tcSplitSigmaTy dfun_ty of
772 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
774 classNamesOfTheta :: ThetaType -> [Name]
775 -- Looks just for ClassP things; maybe it should check
776 classNamesOfTheta preds = [ getName c | ClassP c _ <- preds ]
780 %************************************************************************
782 \subsection[TysWiredIn-ext-type]{External types}
784 %************************************************************************
786 The compiler's foreign function interface supports the passing of a
787 restricted set of types as arguments and results (the restricting factor
791 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
792 -- Checks for valid argument type for a 'foreign import'
793 isFFIArgumentTy dflags safety ty
794 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
796 isFFIExternalTy :: Type -> Bool
797 -- Types that are allowed as arguments of a 'foreign export'
798 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
800 isFFIImportResultTy :: DynFlags -> Type -> Bool
801 isFFIImportResultTy dflags ty
802 = checkRepTyCon (legalFIResultTyCon dflags) ty
804 isFFIExportResultTy :: Type -> Bool
805 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
807 isFFIDynArgumentTy :: Type -> Bool
808 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
809 -- or a newtype of either.
810 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
812 isFFIDynResultTy :: Type -> Bool
813 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
814 -- or a newtype of either.
815 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
817 isFFILabelTy :: Type -> Bool
818 -- The type of a foreign label must be Ptr, FunPtr, Addr,
819 -- or a newtype of either.
820 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
822 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
823 -- Look through newtypes
824 -- Non-recursive ones are transparent to splitTyConApp,
825 -- but recursive ones aren't; hence the splitNewType_maybe
826 checkRepTyCon check_tc ty
827 | Just ty' <- splitNewType_maybe ty = checkRepTyCon check_tc ty'
828 | Just (tc,_) <- splitTyConApp_maybe ty = check_tc tc
832 ----------------------------------------------
833 These chaps do the work; they are not exported
834 ----------------------------------------------
837 legalFEArgTyCon :: TyCon -> Bool
838 -- It's illegal to return foreign objects and (mutable)
839 -- bytearrays from a _ccall_ / foreign declaration
840 -- (or be passed them as arguments in foreign exported functions).
842 | getUnique tc `elem` [ byteArrayTyConKey, mutableByteArrayTyConKey ]
844 -- It's also illegal to make foreign exports that take unboxed
845 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
847 = boxedMarshalableTyCon tc
849 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
850 legalFIResultTyCon dflags tc
851 | getUnique tc `elem`
852 [ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
853 | tc == unitTyCon = True
854 | otherwise = marshalableTyCon dflags tc
856 legalFEResultTyCon :: TyCon -> Bool
857 legalFEResultTyCon tc
858 | getUnique tc `elem`
859 [ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
860 | tc == unitTyCon = True
861 | otherwise = boxedMarshalableTyCon tc
863 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
864 -- Checks validity of types going from Haskell -> external world
865 legalOutgoingTyCon dflags safety tc
866 | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
869 = marshalableTyCon dflags tc
871 marshalableTyCon dflags tc
872 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
873 || boxedMarshalableTyCon tc
875 boxedMarshalableTyCon tc
876 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
877 , int32TyConKey, int64TyConKey
878 , wordTyConKey, word8TyConKey, word16TyConKey
879 , word32TyConKey, word64TyConKey
880 , floatTyConKey, doubleTyConKey
881 , addrTyConKey, ptrTyConKey, funPtrTyConKey
884 , byteArrayTyConKey, mutableByteArrayTyConKey
890 %************************************************************************
892 \subsection{Unification with an explicit substitution}
894 %************************************************************************
896 Unify types with an explicit substitution and no monad.
897 Ignore usage annotations.
901 = (TyVarSet, -- Set of template tyvars
902 TyVarSubstEnv) -- Not necessarily idempotent
904 unifyTysX :: TyVarSet -- Template tyvars
907 -> Maybe TyVarSubstEnv
908 unifyTysX tmpl_tyvars ty1 ty2
909 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
911 unifyExtendTysX :: TyVarSet -- Template tyvars
912 -> TyVarSubstEnv -- Substitution to start with
915 -> Maybe TyVarSubstEnv -- Extended substitution
916 unifyExtendTysX tmpl_tyvars subst ty1 ty2
917 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
919 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
920 -> Maybe TyVarSubstEnv
921 unifyTyListsX tmpl_tyvars tys1 tys2
922 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
927 -> (MySubst -> Maybe result)
931 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
932 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
934 -- Variables; go for uVar
935 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
938 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
939 | tyvar1 `elemVarSet` tmpls
940 = uVarX tyvar1 ty2 k subst
941 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
942 | tyvar2 `elemVarSet` tmpls
943 = uVarX tyvar2 ty1 k subst
946 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
947 | n1 == n2 = uTysX t1 t2 k subst
948 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
949 | c1 == c2 = uTyListsX tys1 tys2 k subst
950 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
951 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
953 -- Functions; just check the two parts
954 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
955 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
957 -- Type constructors must match
958 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
959 | (con1 == con2 && equalLength tys1 tys2)
960 = uTyListsX tys1 tys2 k subst
962 -- Applications need a bit of care!
963 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
964 -- NB: we've already dealt with type variables and Notes,
965 -- so if one type is an App the other one jolly well better be too
966 uTysX (AppTy s1 t1) ty2 k subst
967 = case tcSplitAppTy_maybe ty2 of
968 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
969 Nothing -> Nothing -- Fail
971 uTysX ty1 (AppTy s2 t2) k subst
972 = case tcSplitAppTy_maybe ty1 of
973 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
974 Nothing -> Nothing -- Fail
976 -- Not expecting for-alls in unification
978 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
979 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
982 -- Anything else fails
983 uTysX ty1 ty2 k subst = Nothing
986 uTyListsX [] [] k subst = k subst
987 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
988 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
992 -- Invariant: tv1 is a unifiable variable
993 uVarX tv1 ty2 k subst@(tmpls, env)
994 = case lookupSubstEnv env tv1 of
995 Just (DoneTy ty1) -> -- Already bound
996 uTysX ty1 ty2 k subst
998 Nothing -- Not already bound
999 | typeKind ty2 `eqKind` tyVarKind tv1
1000 && occur_check_ok ty2
1001 -> -- No kind mismatch nor occur check
1002 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1004 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1006 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1007 occur_check_ok_tv tv | tv1 == tv = False
1008 | otherwise = case lookupSubstEnv env tv of
1010 Just (DoneTy ty) -> occur_check_ok ty
1015 %************************************************************************
1017 \subsection{Matching on types}
1019 %************************************************************************
1021 Matching is a {\em unidirectional} process, matching a type against a
1022 template (which is just a type with type variables in it). The
1023 matcher assumes that there are no repeated type variables in the
1024 template, so that it simply returns a mapping of type variables to
1025 types. It also fails on nested foralls.
1027 @matchTys@ matches corresponding elements of a list of templates and
1028 types. It and @matchTy@ both ignore usage annotations, unlike the
1029 main function @match@.
1032 matchTy :: TyVarSet -- Template tyvars
1034 -> Type -- Proposed instance of template
1035 -> Maybe TyVarSubstEnv -- Matching substitution
1038 matchTys :: TyVarSet -- Template tyvars
1039 -> [Type] -- Templates
1040 -> [Type] -- Proposed instance of template
1041 -> Maybe (TyVarSubstEnv, -- Matching substitution
1042 [Type]) -- Left over instance types
1044 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1046 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1047 (\ (senv,tys) -> Just (senv,tys))
1051 @match@ is the main function. It takes a flag indicating whether
1052 usage annotations are to be respected.
1055 match :: Type -> Type -- Current match pair
1056 -> TyVarSet -- Template vars
1057 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1058 -> TyVarSubstEnv -- Current subst
1061 -- When matching against a type variable, see if the variable
1062 -- has already been bound. If so, check that what it's bound to
1063 -- is the same as ty; if not, bind it and carry on.
1065 match (TyVarTy v) ty tmpls k senv
1066 | v `elemVarSet` tmpls
1067 = -- v is a template variable
1068 case lookupSubstEnv senv v of
1069 Nothing | typeKind ty `eqKind` tyVarKind v
1070 -- We do a kind check, just as in the uVarX above
1071 -- The kind check is needed to avoid bogus matches
1072 -- of (a b) with (c d), where the kinds don't match
1073 -- An occur check isn't needed when matching.
1074 -> k (extendSubstEnv senv v (DoneTy ty))
1076 | otherwise -> Nothing -- Fails
1078 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1079 | otherwise -> Nothing -- Fails
1082 = -- v is not a template variable; ty had better match
1083 -- Can't use (==) because types differ
1084 case tcGetTyVar_maybe ty of
1085 Just v' | v == v' -> k senv -- Success
1086 other -> Nothing -- Failure
1087 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1088 -- I guess the reason the Note-stripping case is *last* rather than first
1089 -- is to preserve type synonyms etc., so I'm not moving it to the
1090 -- top; but this means that (without the deNotetype) a type
1091 -- variable may not match the pattern (TyVarTy v') as one would
1092 -- expect, due to an intervening Note. KSW 2000-06.
1095 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1096 | n1 == n2 = match t1 t2 tmpls k senv
1097 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1098 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1099 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1100 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1102 -- Functions; just check the two parts
1103 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1104 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1106 match (AppTy fun1 arg1) ty2 tmpls k senv
1107 = case tcSplitAppTy_maybe ty2 of
1108 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1109 Nothing -> Nothing -- Fail
1111 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1112 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1114 -- Newtypes are opaque; other source types should not happen
1115 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1116 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1118 -- With type synonyms, we have to be careful for the exact
1119 -- same reasons as in the unifier. Please see the
1120 -- considerable commentary there before changing anything
1121 -- here! (WDP 95/05)
1122 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1123 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1126 match _ _ _ _ _ = Nothing
1128 match_list_exactly tys1 tys2 tmpls k senv
1129 = match_list tys1 tys2 tmpls k' senv
1131 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1132 | otherwise = Nothing -- Fail
1134 match_list [] tys2 tmpls k senv = k (senv, tys2)
1135 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1136 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1137 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv