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,
115 tyVarsOfTheta, Kind, Type, SourceType(..),
116 PredType, ThetaType, unliftedTypeKind,
117 liftedTypeKind, openTypeKind, mkArrowKind,
118 mkArrowKinds, mkForAllTy, mkForAllTys,
119 defaultKind, isTypeKind, isAnyTypeKind,
120 mkFunTy, mkFunTys, zipFunTys, isTyVarTy,
121 mkTyConApp, mkGenTyConApp, mkAppTy,
122 mkAppTys, mkSynTy, applyTy, applyTys,
123 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
124 mkPredTys, isUnLiftedType,
125 isUnboxedTupleType, isPrimitiveType,
126 splitNewType_maybe, splitTyConApp_maybe,
127 tidyTopType, tidyType, tidyPred, tidyTypes,
128 tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
129 tidyTyVarBndr, tidyOpenTyVar,
130 tidyOpenTyVars, eqKind, eqUsage,
131 hasMoreBoxityInfo, liftedBoxity,
132 superBoxity, typeKind, superKind, repType
134 import TyCon ( TyCon, isUnLiftedTyCon )
135 import Class ( classHasFDs, Class )
136 import Var ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
137 import ForeignCall ( Safety, playSafe )
142 import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
143 import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
144 import OccName ( OccName, mkDictOcc )
146 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
147 import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
148 import BasicTypes ( IPName(..), ipNameName )
149 import Unique ( Unique, Uniquable(..) )
150 import SrcLoc ( SrcLoc )
151 import Util ( cmpList, thenCmp, equalLength, snocView )
152 import Maybes ( maybeToBool, expectJust )
157 %************************************************************************
161 %************************************************************************
163 The type checker divides the generic Type world into the
164 following more structured beasts:
166 sigma ::= forall tyvars. phi
167 -- A sigma type is a qualified type
169 -- Note that even if 'tyvars' is empty, theta
170 -- may not be: e.g. (?x::Int) => Int
172 -- Note that 'sigma' is in prenex form:
173 -- all the foralls are at the front.
174 -- A 'phi' type has no foralls to the right of
182 -- A 'tau' type has no quantification anywhere
183 -- Note that the args of a type constructor must be taus
185 | tycon tau_1 .. tau_n
189 -- In all cases, a (saturated) type synonym application is legal,
190 -- provided it expands to the required form.
194 type SigmaType = Type
200 type TcTyVar = TyVar -- Might be a mutable tyvar
201 type TcTyVarSet = TyVarSet
203 type TcType = Type -- A TcType can have mutable type variables
204 -- Invariant on ForAllTy in TcTypes:
206 -- a cannot occur inside a MutTyVar in T; that is,
207 -- T is "flattened" before quantifying over a
209 type TcPredType = PredType
210 type TcThetaType = ThetaType
211 type TcSigmaType = TcType
212 type TcRhoType = TcType
213 type TcTauType = TcType
218 %************************************************************************
220 \subsection{TyVarDetails}
222 %************************************************************************
224 TyVarDetails gives extra info about type variables, used during type
225 checking. It's attached to mutable type variables only.
226 It's knot-tied back to Var.lhs. There is no reason in principle
227 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
231 = HoleTv -- Used *only* by the type checker when passing in a type
232 -- variable that should be side-effected to the result type.
233 -- Always has kind openTypeKind.
234 -- Never appears in types
236 | SigTv -- Introduced when instantiating a type signature,
237 -- prior to checking that the defn of a fn does
238 -- have the expected type. Should not be instantiated.
240 -- f :: forall a. a -> a
242 -- When checking e, with expected type (a->a), we
243 -- should not instantiate a
245 | ClsTv -- Scoped type variable introduced by a class decl
246 -- class C a where ...
248 | InstTv -- Ditto, but instance decl
250 | PatSigTv -- Scoped type variable, introduced by a pattern
254 | VanillaTv -- Everything else
256 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
257 isUserTyVar tv = case mutTyVarDetails tv of
261 isSkolemTyVar :: TcTyVar -> Bool
262 isSkolemTyVar tv = case mutTyVarDetails tv of
268 isHoleTyVar :: TcTyVar -> Bool
269 -- NB: the hole might be filled in by now, and this
270 -- function does not check for that
271 isHoleTyVar tv = ASSERT( isMutTyVar tv )
272 case mutTyVarDetails tv of
276 tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
279 = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
280 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
284 details SigTv = ptext SLIT("type signature")
285 details ClsTv = ptext SLIT("class declaration")
286 details InstTv = ptext SLIT("instance declaration")
287 details PatSigTv = ptext SLIT("pattern type signature")
288 details HoleTv = ptext SLIT("//hole//") -- Should not happen
289 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
293 %************************************************************************
295 \subsection{Tau, sigma and rho}
297 %************************************************************************
300 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
302 mkPhiTy :: [SourceType] -> Type -> Type
303 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
307 @isTauTy@ tests for nested for-alls.
310 isTauTy :: Type -> Bool
311 isTauTy (TyVarTy v) = True
312 isTauTy (TyConApp _ tys) = all isTauTy tys
313 isTauTy (AppTy a b) = isTauTy a && isTauTy b
314 isTauTy (FunTy a b) = isTauTy a && isTauTy b
315 isTauTy (SourceTy p) = True -- Don't look through source types
316 isTauTy (NoteTy _ ty) = isTauTy ty
317 isTauTy other = False
321 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
322 -- construct a dictionary function name
323 getDFunTyKey (TyVarTy tv) = getOccName tv
324 getDFunTyKey (TyConApp tc _) = getOccName tc
325 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
326 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
327 getDFunTyKey (FunTy arg _) = getOccName funTyCon
328 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
329 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
330 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
331 -- SourceTy shouldn't happen
335 %************************************************************************
337 \subsection{Expanding and splitting}
339 %************************************************************************
341 These tcSplit functions are like their non-Tc analogues, but
342 a) they do not look through newtypes
343 b) they do not look through PredTys
344 c) [future] they ignore usage-type annotations
346 However, they are non-monadic and do not follow through mutable type
347 variables. It's up to you to make sure this doesn't matter.
350 tcSplitForAllTys :: Type -> ([TyVar], Type)
351 tcSplitForAllTys ty = split ty ty []
353 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
354 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
355 split orig_ty t tvs = (reverse tvs, orig_ty)
357 tcIsForAllTy (ForAllTy tv ty) = True
358 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
359 tcIsForAllTy t = False
361 tcSplitPhiTy :: Type -> ([PredType], Type)
362 tcSplitPhiTy ty = split ty ty []
364 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
365 Just p -> split res res (p:ts)
366 Nothing -> (reverse ts, orig_ty)
367 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
368 split orig_ty ty ts = (reverse ts, orig_ty)
370 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
371 (tvs, rho) -> case tcSplitPhiTy rho of
372 (theta, tau) -> (tvs, theta, tau)
374 tcTyConAppTyCon :: Type -> TyCon
375 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
377 tcTyConAppArgs :: Type -> [Type]
378 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
380 tcSplitTyConApp :: Type -> (TyCon, [Type])
381 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
383 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
385 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
386 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
387 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
388 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
389 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
390 -- Newtypes are opaque, so they may be split
391 -- However, predicates are not treated
392 -- as tycon applications by the type checker
393 tcSplitTyConApp_maybe other = Nothing
395 tcSplitFunTys :: Type -> ([Type], Type)
396 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
398 Just (arg,res) -> (arg:args, res')
400 (args,res') = tcSplitFunTys res
402 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
403 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
404 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
405 tcSplitFunTy_maybe other = Nothing
407 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
408 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
411 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
412 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
413 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
414 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
415 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys --- Don't forget that newtype!
416 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
417 tcSplitAppTy_maybe other = Nothing
419 tc_split_app tc tys = case snocView tys of
420 Just (tys',ty') -> Just (TyConApp tc tys', ty')
423 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
425 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
427 tcSplitAppTys :: Type -> (Type, [Type])
431 go ty args = case tcSplitAppTy_maybe ty of
432 Just (ty', arg) -> go ty' (arg:args)
435 tcGetTyVar_maybe :: Type -> Maybe TyVar
436 tcGetTyVar_maybe (TyVarTy tv) = Just tv
437 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
438 tcGetTyVar_maybe other = Nothing
440 tcGetTyVar :: String -> Type -> TyVar
441 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
443 tcIsTyVarTy :: Type -> Bool
444 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
447 The type of a method for class C is always of the form:
448 Forall a1..an. C a1..an => sig_ty
449 where sig_ty is the type given by the method's signature, and thus in general
450 is a ForallTy. At the point that splitMethodTy is called, it is expected
451 that the outer Forall has already been stripped off. splitMethodTy then
452 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
456 tcSplitMethodTy :: Type -> (PredType, Type)
457 tcSplitMethodTy ty = split ty
459 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
461 Nothing -> panic "splitMethodTy"
462 split (NoteTy n ty) = split ty
463 split _ = panic "splitMethodTy"
465 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
466 -- Split the type of a dictionary function
468 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
469 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
470 (tvs, theta, clas, tys) }}
473 (allDistinctTyVars tys tvs) = True
475 all the types tys are type variables,
476 distinct from each other and from tvs.
478 This is useful when checking that unification hasn't unified signature
479 type variables. For example, if the type sig is
480 f :: forall a b. a -> b -> b
481 we want to check that 'a' and 'b' havn't
482 (a) been unified with a non-tyvar type
483 (b) been unified with each other (all distinct)
484 (c) been unified with a variable free in the environment
487 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
489 allDistinctTyVars [] acc
491 allDistinctTyVars (ty:tys) acc
492 = case tcGetTyVar_maybe ty of
493 Nothing -> False -- (a)
494 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
495 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
499 %************************************************************************
501 \subsection{Predicate types}
503 %************************************************************************
505 "Predicates" are particular source types, namelyClassP or IParams
508 isPred :: SourceType -> Bool
509 isPred (ClassP _ _) = True
510 isPred (IParam _ _) = True
511 isPred (NType _ _) = False
513 isPredTy :: Type -> Bool
514 isPredTy (NoteTy _ ty) = isPredTy ty
515 isPredTy (SourceTy sty) = isPred sty
518 tcSplitPredTy_maybe :: Type -> Maybe PredType
519 -- Returns Just for predicates only
520 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
521 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
522 tcSplitPredTy_maybe other = Nothing
524 predTyUnique :: PredType -> Unique
525 predTyUnique (IParam n _) = getUnique (ipNameName n)
526 predTyUnique (ClassP clas tys) = getUnique clas
528 predHasFDs :: PredType -> Bool
529 -- True if the predicate has functional depenencies;
530 -- I.e. should participate in improvement
531 predHasFDs (IParam _ _) = True
532 predHasFDs (ClassP cls _) = classHasFDs cls
534 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
535 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
536 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
540 --------------------- Dictionary types ---------------------------------
543 mkClassPred clas tys = ClassP clas tys
545 isClassPred :: SourceType -> Bool
546 isClassPred (ClassP clas tys) = True
547 isClassPred other = False
549 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
550 isTyVarClassPred other = False
552 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
553 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
554 getClassPredTys_maybe _ = Nothing
556 getClassPredTys :: PredType -> (Class, [Type])
557 getClassPredTys (ClassP clas tys) = (clas, tys)
559 mkDictTy :: Class -> [Type] -> Type
560 mkDictTy clas tys = mkPredTy (ClassP clas tys)
562 isDictTy :: Type -> Bool
563 isDictTy (SourceTy p) = isClassPred p
564 isDictTy (NoteTy _ ty) = isDictTy ty
565 isDictTy other = False
568 --------------------- Implicit parameters ---------------------------------
571 isIPPred :: SourceType -> Bool
572 isIPPred (IParam _ _) = True
573 isIPPred other = False
575 isInheritablePred :: PredType -> Bool
576 -- Can be inherited by a context. For example, consider
577 -- f x = let g y = (?v, y+x)
578 -- in (g 3 with ?v = 8,
580 -- The point is that g's type must be quantifed over ?v:
581 -- g :: (?v :: a) => a -> a
582 -- but it doesn't need to be quantified over the Num a dictionary
583 -- which can be free in g's rhs, and shared by both calls to g
584 isInheritablePred (ClassP _ _) = True
585 isInheritablePred other = False
587 isLinearPred :: TcPredType -> Bool
588 isLinearPred (IParam (Linear n) _) = True
589 isLinearPred other = False
593 %************************************************************************
595 \subsection{Comparison}
597 %************************************************************************
599 Comparison, taking note of newtypes, predicates, etc,
600 But ignoring usage types
603 tcEqType :: Type -> Type -> Bool
604 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
606 tcEqTypes :: [Type] -> [Type] -> Bool
607 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
609 tcEqPred :: PredType -> PredType -> Bool
610 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
613 tcCmpType :: Type -> Type -> Ordering
614 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
616 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
618 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
620 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
623 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
624 -- The "env" maps type variables in ty1 to type variables in ty2
625 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
626 -- we in effect substitute tv2 for tv1 in t1 before continuing
628 -- Look through NoteTy
629 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
630 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
632 -- Deal with equal constructors
633 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
634 Just tv1a -> tv1a `compare` tv2
635 Nothing -> tv1 `compare` tv2
637 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
638 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
639 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
640 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
641 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
643 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
644 cmpTy env (AppTy _ _) (TyVarTy _) = GT
646 cmpTy env (FunTy _ _) (TyVarTy _) = GT
647 cmpTy env (FunTy _ _) (AppTy _ _) = GT
649 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
650 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
651 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
653 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
654 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
655 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
656 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
658 cmpTy env (SourceTy _) t2 = GT
664 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
665 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
666 -- Compare types as well as names for implicit parameters
667 -- This comparison is used exclusively (I think) for the
668 -- finite map built in TcSimplify
669 cmpSourceTy env (IParam _ _) sty = LT
671 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
672 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
673 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
675 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
676 cmpSourceTy env (NType _ _) sty = GT
679 PredTypes are used as a FM key in TcSimplify,
680 so we take the easy path and make them an instance of Ord
683 instance Eq SourceType where { (==) = tcEqPred }
684 instance Ord SourceType where { compare = tcCmpPred }
688 %************************************************************************
690 \subsection{Predicates}
692 %************************************************************************
694 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
696 f :: (?x::Int) => Int -> Int
699 isSigmaTy :: Type -> Bool
700 isSigmaTy (ForAllTy tyvar ty) = True
701 isSigmaTy (FunTy a b) = isPredTy a
702 isSigmaTy (NoteTy n ty) = isSigmaTy ty
705 isOverloadedTy :: Type -> Bool
706 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
707 isOverloadedTy (FunTy a b) = isPredTy a
708 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
709 isOverloadedTy _ = False
713 isFloatTy = is_tc floatTyConKey
714 isDoubleTy = is_tc doubleTyConKey
715 isIntegerTy = is_tc integerTyConKey
716 isIntTy = is_tc intTyConKey
717 isAddrTy = is_tc addrTyConKey
718 isBoolTy = is_tc boolTyConKey
719 isUnitTy = is_tc unitTyConKey
721 is_tc :: Unique -> Type -> Bool
722 -- Newtypes are opaque to this
723 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
724 Just (tc, _) -> uniq == getUnique tc
729 %************************************************************************
733 %************************************************************************
736 deNoteType :: Type -> Type
737 -- Remove synonyms, but not source types
738 deNoteType ty@(TyVarTy tyvar) = ty
739 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
740 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
741 deNoteType (NoteTy _ ty) = deNoteType ty
742 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
743 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
744 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
746 deNoteSourceType :: SourceType -> SourceType
747 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
748 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
749 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
752 Find the free tycons and classes of a type. This is used in the front
756 tyClsNamesOfType :: Type -> NameSet
757 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
758 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
759 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
760 tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
761 tyClsNamesOfType (SourceTy (IParam n ty)) = tyClsNamesOfType ty
762 tyClsNamesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
763 tyClsNamesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` tyClsNamesOfTypes tys
764 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
765 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
766 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
768 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
770 tyClsNamesOfDFunHead :: Type -> NameSet
771 -- Find the free type constructors and classes
772 -- of the head of the dfun instance type
773 -- The 'dfun_head_type' is because of
774 -- instance Foo a => Baz T where ...
775 -- The decl is an orphan if Baz and T are both not locally defined,
776 -- even if Foo *is* locally defined
777 tyClsNamesOfDFunHead dfun_ty
778 = case tcSplitSigmaTy dfun_ty of
779 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
781 classNamesOfTheta :: ThetaType -> [Name]
782 -- Looks just for ClassP things; maybe it should check
783 classNamesOfTheta preds = [ getName c | ClassP c _ <- preds ]
787 %************************************************************************
789 \subsection[TysWiredIn-ext-type]{External types}
791 %************************************************************************
793 The compiler's foreign function interface supports the passing of a
794 restricted set of types as arguments and results (the restricting factor
798 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
799 -- Checks for valid argument type for a 'foreign import'
800 isFFIArgumentTy dflags safety ty
801 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
803 isFFIExternalTy :: Type -> Bool
804 -- Types that are allowed as arguments of a 'foreign export'
805 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
807 isFFIImportResultTy :: DynFlags -> Type -> Bool
808 isFFIImportResultTy dflags ty
809 = checkRepTyCon (legalFIResultTyCon dflags) ty
811 isFFIExportResultTy :: Type -> Bool
812 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
814 isFFIDynArgumentTy :: Type -> Bool
815 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
816 -- or a newtype of either.
817 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
819 isFFIDynResultTy :: Type -> Bool
820 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
821 -- or a newtype of either.
822 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
824 isFFILabelTy :: Type -> Bool
825 -- The type of a foreign label must be Ptr, FunPtr, Addr,
826 -- or a newtype of either.
827 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
829 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
830 -- Look through newtypes
831 -- Non-recursive ones are transparent to splitTyConApp,
832 -- but recursive ones aren't; hence the splitNewType_maybe
833 checkRepTyCon check_tc ty
834 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
838 ----------------------------------------------
839 These chaps do the work; they are not exported
840 ----------------------------------------------
843 legalFEArgTyCon :: TyCon -> Bool
844 -- It's illegal to return foreign objects and (mutable)
845 -- bytearrays from a _ccall_ / foreign declaration
846 -- (or be passed them as arguments in foreign exported functions).
848 | getUnique tc `elem` [ byteArrayTyConKey, mutableByteArrayTyConKey ]
850 -- It's also illegal to make foreign exports that take unboxed
851 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
853 = boxedMarshalableTyCon tc
855 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
856 legalFIResultTyCon dflags tc
857 | getUnique tc `elem`
858 [ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
859 | tc == unitTyCon = True
860 | otherwise = marshalableTyCon dflags tc
862 legalFEResultTyCon :: TyCon -> Bool
863 legalFEResultTyCon tc
864 | getUnique tc `elem`
865 [ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
866 | tc == unitTyCon = True
867 | otherwise = boxedMarshalableTyCon tc
869 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
870 -- Checks validity of types going from Haskell -> external world
871 legalOutgoingTyCon dflags safety tc
872 | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
875 = marshalableTyCon dflags tc
877 marshalableTyCon dflags tc
878 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
879 || boxedMarshalableTyCon tc
881 boxedMarshalableTyCon tc
882 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
883 , int32TyConKey, int64TyConKey
884 , wordTyConKey, word8TyConKey, word16TyConKey
885 , word32TyConKey, word64TyConKey
886 , floatTyConKey, doubleTyConKey
887 , addrTyConKey, ptrTyConKey, funPtrTyConKey
890 , byteArrayTyConKey, mutableByteArrayTyConKey
896 %************************************************************************
898 \subsection{Unification with an explicit substitution}
900 %************************************************************************
902 Unify types with an explicit substitution and no monad.
903 Ignore usage annotations.
907 = (TyVarSet, -- Set of template tyvars
908 TyVarSubstEnv) -- Not necessarily idempotent
910 unifyTysX :: TyVarSet -- Template tyvars
913 -> Maybe TyVarSubstEnv
914 unifyTysX tmpl_tyvars ty1 ty2
915 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
917 unifyExtendTysX :: TyVarSet -- Template tyvars
918 -> TyVarSubstEnv -- Substitution to start with
921 -> Maybe TyVarSubstEnv -- Extended substitution
922 unifyExtendTysX tmpl_tyvars subst ty1 ty2
923 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
925 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
926 -> Maybe TyVarSubstEnv
927 unifyTyListsX tmpl_tyvars tys1 tys2
928 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
933 -> (MySubst -> Maybe result)
937 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
938 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
940 -- Variables; go for uVar
941 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
944 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
945 | tyvar1 `elemVarSet` tmpls
946 = uVarX tyvar1 ty2 k subst
947 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
948 | tyvar2 `elemVarSet` tmpls
949 = uVarX tyvar2 ty1 k subst
952 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
953 | n1 == n2 = uTysX t1 t2 k subst
954 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
955 | c1 == c2 = uTyListsX tys1 tys2 k subst
956 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
957 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
959 -- Functions; just check the two parts
960 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
961 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
963 -- Type constructors must match
964 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
965 | (con1 == con2 && equalLength tys1 tys2)
966 = uTyListsX tys1 tys2 k subst
968 -- Applications need a bit of care!
969 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
970 -- NB: we've already dealt with type variables and Notes,
971 -- so if one type is an App the other one jolly well better be too
972 uTysX (AppTy s1 t1) ty2 k subst
973 = case tcSplitAppTy_maybe ty2 of
974 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
975 Nothing -> Nothing -- Fail
977 uTysX ty1 (AppTy s2 t2) k subst
978 = case tcSplitAppTy_maybe ty1 of
979 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
980 Nothing -> Nothing -- Fail
982 -- Not expecting for-alls in unification
984 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
985 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
988 -- Anything else fails
989 uTysX ty1 ty2 k subst = Nothing
992 uTyListsX [] [] k subst = k subst
993 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
994 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
998 -- Invariant: tv1 is a unifiable variable
999 uVarX tv1 ty2 k subst@(tmpls, env)
1000 = case lookupSubstEnv env tv1 of
1001 Just (DoneTy ty1) -> -- Already bound
1002 uTysX ty1 ty2 k subst
1004 Nothing -- Not already bound
1005 | typeKind ty2 `eqKind` tyVarKind tv1
1006 && occur_check_ok ty2
1007 -> -- No kind mismatch nor occur check
1008 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1010 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1012 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1013 occur_check_ok_tv tv | tv1 == tv = False
1014 | otherwise = case lookupSubstEnv env tv of
1016 Just (DoneTy ty) -> occur_check_ok ty
1021 %************************************************************************
1023 \subsection{Matching on types}
1025 %************************************************************************
1027 Matching is a {\em unidirectional} process, matching a type against a
1028 template (which is just a type with type variables in it). The
1029 matcher assumes that there are no repeated type variables in the
1030 template, so that it simply returns a mapping of type variables to
1031 types. It also fails on nested foralls.
1033 @matchTys@ matches corresponding elements of a list of templates and
1034 types. It and @matchTy@ both ignore usage annotations, unlike the
1035 main function @match@.
1038 matchTy :: TyVarSet -- Template tyvars
1040 -> Type -- Proposed instance of template
1041 -> Maybe TyVarSubstEnv -- Matching substitution
1044 matchTys :: TyVarSet -- Template tyvars
1045 -> [Type] -- Templates
1046 -> [Type] -- Proposed instance of template
1047 -> Maybe (TyVarSubstEnv, -- Matching substitution
1048 [Type]) -- Left over instance types
1050 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1052 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1053 (\ (senv,tys) -> Just (senv,tys))
1057 @match@ is the main function. It takes a flag indicating whether
1058 usage annotations are to be respected.
1061 match :: Type -> Type -- Current match pair
1062 -> TyVarSet -- Template vars
1063 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1064 -> TyVarSubstEnv -- Current subst
1067 -- When matching against a type variable, see if the variable
1068 -- has already been bound. If so, check that what it's bound to
1069 -- is the same as ty; if not, bind it and carry on.
1071 match (TyVarTy v) ty tmpls k senv
1072 | v `elemVarSet` tmpls
1073 = -- v is a template variable
1074 case lookupSubstEnv senv v of
1075 Nothing | typeKind ty `eqKind` tyVarKind v
1076 -- We do a kind check, just as in the uVarX above
1077 -- The kind check is needed to avoid bogus matches
1078 -- of (a b) with (c d), where the kinds don't match
1079 -- An occur check isn't needed when matching.
1080 -> k (extendSubstEnv senv v (DoneTy ty))
1082 | otherwise -> Nothing -- Fails
1084 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1085 | otherwise -> Nothing -- Fails
1088 = -- v is not a template variable; ty had better match
1089 -- Can't use (==) because types differ
1090 case tcGetTyVar_maybe ty of
1091 Just v' | v == v' -> k senv -- Success
1092 other -> Nothing -- Failure
1093 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1094 -- I guess the reason the Note-stripping case is *last* rather than first
1095 -- is to preserve type synonyms etc., so I'm not moving it to the
1096 -- top; but this means that (without the deNotetype) a type
1097 -- variable may not match the pattern (TyVarTy v') as one would
1098 -- expect, due to an intervening Note. KSW 2000-06.
1101 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1102 | n1 == n2 = match t1 t2 tmpls k senv
1103 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1104 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1105 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1106 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1108 -- Functions; just check the two parts
1109 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1110 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1112 match (AppTy fun1 arg1) ty2 tmpls k senv
1113 = case tcSplitAppTy_maybe ty2 of
1114 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1115 Nothing -> Nothing -- Fail
1117 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1118 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1120 -- Newtypes are opaque; other source types should not happen
1121 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1122 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1124 -- With type synonyms, we have to be careful for the exact
1125 -- same reasons as in the unifier. Please see the
1126 -- considerable commentary there before changing anything
1127 -- here! (WDP 95/05)
1128 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1129 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1132 match _ _ _ _ _ = Nothing
1134 match_list_exactly tys1 tys2 tmpls k senv
1135 = match_list tys1 tys2 tmpls k' senv
1137 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1138 | otherwise = Nothing -- Fail
1140 match_list [] tys2 tmpls k senv = k (senv, tys2)
1141 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1142 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1143 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv