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,
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, classesOfTheta,
54 tyClsNamesOfType, tyClsNamesOfDFunHead,
57 ---------------------------------
59 getClassPredTys_maybe, getClassPredTys,
60 isClassPred, isTyVarClassPred,
61 mkDictTy, tcSplitPredTy_maybe,
62 isPredTy, 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
74 isFFIDotnetTy, -- :: DynFlags -> Type -> Bool
75 isFFIDotnetObjTy, -- :: Type -> Bool
77 toDNType, -- :: Type -> DNType
79 ---------------------------------
80 -- Unifier and matcher
81 unifyTysX, unifyTyListsX, unifyExtendTysX,
82 matchTy, matchTys, match,
84 --------------------------------
85 -- Rexported from Type
86 Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
87 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
88 superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
89 isTypeKind, isAnyTypeKind, typeCon,
91 Type, PredType(..), ThetaType,
92 mkForAllTy, mkForAllTys,
93 mkFunTy, mkFunTys, zipFunTys,
94 mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
95 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
97 isUnLiftedType, -- Source types are always lifted
98 isUnboxedTupleType, -- Ditto
101 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
102 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
105 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
108 #include "HsVersions.h"
111 import {-# SOURCE #-} PprType( pprType )
112 -- PprType imports TcType so that it can print intelligently
115 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
117 import Type ( -- Re-exports
118 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
119 tyVarsOfTheta, Kind, Type, PredType(..),
120 ThetaType, unliftedTypeKind, typeCon,
121 liftedTypeKind, openTypeKind, mkArrowKind,
122 mkArrowKinds, mkForAllTy, mkForAllTys,
123 defaultKind, isTypeKind, isAnyTypeKind,
124 mkFunTy, mkFunTys, zipFunTys, isTyVarTy,
125 mkTyConApp, mkGenTyConApp, mkAppTy,
126 mkAppTys, mkSynTy, applyTy, applyTys,
127 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
128 mkPredTys, isUnLiftedType,
129 isUnboxedTupleType, isPrimitiveType,
131 tidyTopType, tidyType, tidyPred, tidyTypes,
132 tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
133 tidyTyVarBndr, tidyOpenTyVar,
134 tidyOpenTyVars, eqKind,
135 hasMoreBoxityInfo, liftedBoxity,
136 superBoxity, typeKind, superKind, repType
138 import TyCon ( TyCon, isUnLiftedTyCon, tyConUnique )
139 import Class ( Class )
140 import Var ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
141 import ForeignCall ( Safety, playSafe
148 import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
149 import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
151 import OccName ( OccName, mkDictOcc )
152 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
153 import TysWiredIn ( unitTyCon, charTyCon, listTyCon )
154 import BasicTypes ( IPName(..), ipNameName )
155 import Unique ( Unique, Uniquable(..) )
156 import SrcLoc ( SrcLoc )
157 import Util ( cmpList, thenCmp, equalLength, snocView )
158 import Maybes ( maybeToBool, expectJust )
163 %************************************************************************
167 %************************************************************************
169 The type checker divides the generic Type world into the
170 following more structured beasts:
172 sigma ::= forall tyvars. phi
173 -- A sigma type is a qualified type
175 -- Note that even if 'tyvars' is empty, theta
176 -- may not be: e.g. (?x::Int) => Int
178 -- Note that 'sigma' is in prenex form:
179 -- all the foralls are at the front.
180 -- A 'phi' type has no foralls to the right of
188 -- A 'tau' type has no quantification anywhere
189 -- Note that the args of a type constructor must be taus
191 | tycon tau_1 .. tau_n
195 -- In all cases, a (saturated) type synonym application is legal,
196 -- provided it expands to the required form.
199 type TcTyVar = TyVar -- Might be a mutable tyvar
200 type TcTyVarSet = TyVarSet
202 type TcType = Type -- A TcType can have mutable type variables
203 -- Invariant on ForAllTy in TcTypes:
205 -- a cannot occur inside a MutTyVar in T; that is,
206 -- T is "flattened" before quantifying over a
208 type TcPredType = PredType
209 type TcThetaType = ThetaType
210 type TcSigmaType = TcType
211 type TcRhoType = TcType
212 type TcTauType = TcType
217 %************************************************************************
219 \subsection{TyVarDetails}
221 %************************************************************************
223 TyVarDetails gives extra info about type variables, used during type
224 checking. It's attached to mutable type variables only.
225 It's knot-tied back to Var.lhs. There is no reason in principle
226 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
230 = SigTv -- Introduced when instantiating a type signature,
231 -- prior to checking that the defn of a fn does
232 -- have the expected type. Should not be instantiated.
234 -- f :: forall a. a -> a
236 -- When checking e, with expected type (a->a), we
237 -- should not instantiate a
239 | ClsTv -- Scoped type variable introduced by a class decl
240 -- class C a where ...
242 | InstTv -- Ditto, but instance decl
244 | PatSigTv -- Scoped type variable, introduced by a pattern
248 | VanillaTv -- Everything else
250 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
251 isUserTyVar tv = case mutTyVarDetails tv of
255 isSkolemTyVar :: TcTyVar -> Bool
256 isSkolemTyVar tv = case mutTyVarDetails tv of
262 tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
265 = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
266 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
270 details SigTv = ptext SLIT("type signature")
271 details ClsTv = ptext SLIT("class declaration")
272 details InstTv = ptext SLIT("instance declaration")
273 details PatSigTv = ptext SLIT("pattern type signature")
274 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
278 %************************************************************************
280 \subsection{Tau, sigma and rho}
282 %************************************************************************
285 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
287 mkPhiTy :: [PredType] -> Type -> Type
288 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
291 @isTauTy@ tests for nested for-alls.
294 isTauTy :: Type -> Bool
295 isTauTy (TyVarTy v) = True
296 isTauTy (TyConApp _ tys) = all isTauTy tys
297 isTauTy (NewTcApp _ tys) = all isTauTy tys
298 isTauTy (AppTy a b) = isTauTy a && isTauTy b
299 isTauTy (FunTy a b) = isTauTy a && isTauTy b
300 isTauTy (PredTy p) = True -- Don't look through source types
301 isTauTy (NoteTy _ ty) = isTauTy ty
302 isTauTy other = False
306 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
307 -- construct a dictionary function name
308 getDFunTyKey (TyVarTy tv) = getOccName tv
309 getDFunTyKey (TyConApp tc _) = getOccName tc
310 getDFunTyKey (NewTcApp tc _) = getOccName tc
311 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
312 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
313 getDFunTyKey (FunTy arg _) = getOccName funTyCon
314 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
315 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
316 -- PredTy shouldn't happen
320 %************************************************************************
322 \subsection{Expanding and splitting}
324 %************************************************************************
326 These tcSplit functions are like their non-Tc analogues, but
327 a) they do not look through newtypes
328 b) they do not look through PredTys
329 c) [future] they ignore usage-type annotations
331 However, they are non-monadic and do not follow through mutable type
332 variables. It's up to you to make sure this doesn't matter.
335 tcSplitForAllTys :: Type -> ([TyVar], Type)
336 tcSplitForAllTys ty = split ty ty []
338 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
339 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
340 split orig_ty t tvs = (reverse tvs, orig_ty)
342 tcIsForAllTy (ForAllTy tv ty) = True
343 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
344 tcIsForAllTy t = False
346 tcSplitPhiTy :: Type -> ([PredType], Type)
347 tcSplitPhiTy ty = split ty ty []
349 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
350 Just p -> split res res (p:ts)
351 Nothing -> (reverse ts, orig_ty)
352 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
353 split orig_ty ty ts = (reverse ts, orig_ty)
355 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
356 (tvs, rho) -> case tcSplitPhiTy rho of
357 (theta, tau) -> (tvs, theta, tau)
359 tcTyConAppTyCon :: Type -> TyCon
360 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
362 tcTyConAppArgs :: Type -> [Type]
363 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
365 tcSplitTyConApp :: Type -> (TyCon, [Type])
366 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
368 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
370 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
371 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
372 tcSplitTyConApp_maybe (NewTcApp tc tys) = Just (tc, tys)
373 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
374 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
375 -- Newtypes are opaque, so they may be split
376 -- However, predicates are not treated
377 -- as tycon applications by the type checker
378 tcSplitTyConApp_maybe other = Nothing
380 tcSplitFunTys :: Type -> ([Type], Type)
381 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
383 Just (arg,res) -> (arg:args, res')
385 (args,res') = tcSplitFunTys res
387 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
388 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
389 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
390 tcSplitFunTy_maybe other = Nothing
392 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
393 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
396 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
397 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
398 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
399 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
400 tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
401 Just (tys', ty') -> Just (TyConApp tc tys', ty')
403 tcSplitAppTy_maybe (NewTcApp tc tys) = case snocView tys of
404 Just (tys', ty') -> Just (NewTcApp tc tys', ty')
406 tcSplitAppTy_maybe other = Nothing
408 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
410 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
412 tcSplitAppTys :: Type -> (Type, [Type])
416 go ty args = case tcSplitAppTy_maybe ty of
417 Just (ty', arg) -> go ty' (arg:args)
420 tcGetTyVar_maybe :: Type -> Maybe TyVar
421 tcGetTyVar_maybe (TyVarTy tv) = Just tv
422 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
423 tcGetTyVar_maybe other = Nothing
425 tcGetTyVar :: String -> Type -> TyVar
426 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
428 tcIsTyVarTy :: Type -> Bool
429 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
432 The type of a method for class C is always of the form:
433 Forall a1..an. C a1..an => sig_ty
434 where sig_ty is the type given by the method's signature, and thus in general
435 is a ForallTy. At the point that splitMethodTy is called, it is expected
436 that the outer Forall has already been stripped off. splitMethodTy then
437 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off.
440 tcSplitMethodTy :: Type -> (PredType, Type)
441 tcSplitMethodTy ty = split ty
443 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
445 Nothing -> panic "splitMethodTy"
446 split (NoteTy n ty) = split ty
447 split _ = panic "splitMethodTy"
449 tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
450 -- Split the type of a dictionary function
452 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
453 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
454 (tvs, theta, clas, tys) }}
457 (allDistinctTyVars tys tvs) = True
459 all the types tys are type variables,
460 distinct from each other and from tvs.
462 This is useful when checking that unification hasn't unified signature
463 type variables. For example, if the type sig is
464 f :: forall a b. a -> b -> b
465 we want to check that 'a' and 'b' havn't
466 (a) been unified with a non-tyvar type
467 (b) been unified with each other (all distinct)
468 (c) been unified with a variable free in the environment
471 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
473 allDistinctTyVars [] acc
475 allDistinctTyVars (ty:tys) acc
476 = case tcGetTyVar_maybe ty of
477 Nothing -> False -- (a)
478 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
479 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
483 %************************************************************************
485 \subsection{Predicate types}
487 %************************************************************************
490 tcSplitPredTy_maybe :: Type -> Maybe PredType
491 -- Returns Just for predicates only
492 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
493 tcSplitPredTy_maybe (PredTy p) = Just p
494 tcSplitPredTy_maybe other = Nothing
496 predTyUnique :: PredType -> Unique
497 predTyUnique (IParam n _) = getUnique (ipNameName n)
498 predTyUnique (ClassP clas tys) = getUnique clas
500 mkPredName :: Unique -> SrcLoc -> PredType -> Name
501 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
502 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
506 --------------------- Dictionary types ---------------------------------
509 mkClassPred clas tys = ClassP clas tys
511 isClassPred :: PredType -> Bool
512 isClassPred (ClassP clas tys) = True
513 isClassPred other = False
515 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
516 isTyVarClassPred other = False
518 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
519 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
520 getClassPredTys_maybe _ = Nothing
522 getClassPredTys :: PredType -> (Class, [Type])
523 getClassPredTys (ClassP clas tys) = (clas, tys)
525 mkDictTy :: Class -> [Type] -> Type
526 mkDictTy clas tys = mkPredTy (ClassP clas tys)
528 isDictTy :: Type -> Bool
529 isDictTy (PredTy p) = isClassPred p
530 isDictTy (NoteTy _ ty) = isDictTy ty
531 isDictTy other = False
534 --------------------- Implicit parameters ---------------------------------
537 isIPPred :: PredType -> Bool
538 isIPPred (IParam _ _) = True
539 isIPPred other = False
541 isInheritablePred :: PredType -> Bool
542 -- Can be inherited by a context. For example, consider
543 -- f x = let g y = (?v, y+x)
544 -- in (g 3 with ?v = 8,
546 -- The point is that g's type must be quantifed over ?v:
547 -- g :: (?v :: a) => a -> a
548 -- but it doesn't need to be quantified over the Num a dictionary
549 -- which can be free in g's rhs, and shared by both calls to g
550 isInheritablePred (ClassP _ _) = True
551 isInheritablePred other = False
553 isLinearPred :: TcPredType -> Bool
554 isLinearPred (IParam (Linear n) _) = True
555 isLinearPred other = False
559 %************************************************************************
561 \subsection{Comparison}
563 %************************************************************************
565 Comparison, taking note of newtypes, predicates, etc,
568 tcEqType :: Type -> Type -> Bool
569 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
571 tcEqTypes :: [Type] -> [Type] -> Bool
572 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
574 tcEqPred :: PredType -> PredType -> Bool
575 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
578 tcCmpType :: Type -> Type -> Ordering
579 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
581 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
583 tcCmpPred p1 p2 = cmpPredTy emptyVarEnv p1 p2
585 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
588 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
589 -- The "env" maps type variables in ty1 to type variables in ty2
590 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
591 -- we in effect substitute tv2 for tv1 in t1 before continuing
593 -- Look through NoteTy
594 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
595 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
597 -- Deal with equal constructors
598 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
599 Just tv1a -> tv1a `compare` tv2
600 Nothing -> tv1 `compare` tv2
602 cmpTy env (PredTy p1) (PredTy p2) = cmpPredTy env p1 p2
603 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
604 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
605 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
606 cmpTy env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
607 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
609 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < NewTcApp < ForAllTy < PredTy
610 cmpTy env (AppTy _ _) (TyVarTy _) = GT
612 cmpTy env (FunTy _ _) (TyVarTy _) = GT
613 cmpTy env (FunTy _ _) (AppTy _ _) = GT
615 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
616 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
617 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
619 cmpTy env (NewTcApp _ _) (TyVarTy _) = GT
620 cmpTy env (NewTcApp _ _) (AppTy _ _) = GT
621 cmpTy env (NewTcApp _ _) (FunTy _ _) = GT
622 cmpTy env (NewTcApp _ _) (TyConApp _ _) = GT
624 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
625 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
626 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
627 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
628 cmpTy env (ForAllTy _ _) (NewTcApp _ _) = GT
630 cmpTy env (PredTy _) t2 = GT
636 cmpPredTy :: TyVarEnv TyVar -> PredType -> PredType -> Ordering
637 cmpPredTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
638 -- Compare types as well as names for implicit parameters
639 -- This comparison is used exclusively (I think) for the
640 -- finite map built in TcSimplify
641 cmpPredTy env (IParam _ _) (ClassP _ _) = LT
642 cmpPredTy env (ClassP _ _) (IParam _ _) = GT
643 cmpPredTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
646 PredTypes are used as a FM key in TcSimplify,
647 so we take the easy path and make them an instance of Ord
650 instance Eq PredType where { (==) = tcEqPred }
651 instance Ord PredType where { compare = tcCmpPred }
655 %************************************************************************
657 \subsection{Predicates}
659 %************************************************************************
661 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
663 f :: (?x::Int) => Int -> Int
666 isSigmaTy :: Type -> Bool
667 isSigmaTy (ForAllTy tyvar ty) = True
668 isSigmaTy (FunTy a b) = isPredTy a
669 isSigmaTy (NoteTy n ty) = isSigmaTy ty
672 isOverloadedTy :: Type -> Bool
673 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
674 isOverloadedTy (FunTy a b) = isPredTy a
675 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
676 isOverloadedTy _ = False
678 isPredTy :: Type -> Bool -- Belongs in TcType because it does
679 -- not look through newtypes, or predtypes (of course)
680 isPredTy (NoteTy _ ty) = isPredTy ty
681 isPredTy (PredTy sty) = True
686 isFloatTy = is_tc floatTyConKey
687 isDoubleTy = is_tc doubleTyConKey
688 isIntegerTy = is_tc integerTyConKey
689 isIntTy = is_tc intTyConKey
690 isAddrTy = is_tc addrTyConKey
691 isBoolTy = is_tc boolTyConKey
692 isUnitTy = is_tc unitTyConKey
694 is_tc :: Unique -> Type -> Bool
695 -- Newtypes are opaque to this
696 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
697 Just (tc, _) -> uniq == getUnique tc
702 %************************************************************************
706 %************************************************************************
709 deNoteType :: Type -> Type
710 -- Remove synonyms, but not predicate types
711 deNoteType ty@(TyVarTy tyvar) = ty
712 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
713 deNoteType (NewTcApp tycon tys) = NewTcApp tycon (map deNoteType tys)
714 deNoteType (PredTy p) = PredTy (deNotePredType p)
715 deNoteType (NoteTy _ ty) = deNoteType ty
716 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
717 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
718 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
720 deNotePredType :: PredType -> PredType
721 deNotePredType (ClassP c tys) = ClassP c (map deNoteType tys)
722 deNotePredType (IParam n ty) = IParam n (deNoteType ty)
725 Find the free tycons and classes of a type. This is used in the front
729 tyClsNamesOfType :: Type -> NameSet
730 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
731 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
732 tyClsNamesOfType (NewTcApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
733 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
734 tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
735 tyClsNamesOfType (PredTy (IParam n ty)) = tyClsNamesOfType ty
736 tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
737 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
738 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
739 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
741 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
743 tyClsNamesOfDFunHead :: Type -> NameSet
744 -- Find the free type constructors and classes
745 -- of the head of the dfun instance type
746 -- The 'dfun_head_type' is because of
747 -- instance Foo a => Baz T where ...
748 -- The decl is an orphan if Baz and T are both not locally defined,
749 -- even if Foo *is* locally defined
750 tyClsNamesOfDFunHead dfun_ty
751 = case tcSplitSigmaTy dfun_ty of
752 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
754 classesOfTheta :: ThetaType -> [Class]
755 -- Looks just for ClassP things; maybe it should check
756 classesOfTheta preds = [ c | ClassP c _ <- preds ]
760 %************************************************************************
762 \subsection[TysWiredIn-ext-type]{External types}
764 %************************************************************************
766 The compiler's foreign function interface supports the passing of a
767 restricted set of types as arguments and results (the restricting factor
771 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
772 -- Checks for valid argument type for a 'foreign import'
773 isFFIArgumentTy dflags safety ty
774 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
776 isFFIExternalTy :: Type -> Bool
777 -- Types that are allowed as arguments of a 'foreign export'
778 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
780 isFFIImportResultTy :: DynFlags -> Type -> Bool
781 isFFIImportResultTy dflags ty
782 = checkRepTyCon (legalFIResultTyCon dflags) ty
784 isFFIExportResultTy :: Type -> Bool
785 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
787 isFFIDynArgumentTy :: Type -> Bool
788 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
789 -- or a newtype of either.
790 isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
792 isFFIDynResultTy :: Type -> Bool
793 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
794 -- or a newtype of either.
795 isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
797 isFFILabelTy :: Type -> Bool
798 -- The type of a foreign label must be Ptr, FunPtr, Addr,
799 -- or a newtype of either.
800 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
802 isFFIDotnetTy :: DynFlags -> Type -> Bool
803 isFFIDotnetTy dflags ty
804 = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
805 (legalFIResultTyCon dflags tc ||
806 isFFIDotnetObjTy ty || isStringTy ty)) ty
808 -- Support String as an argument or result from a .NET FFI call.
810 case tcSplitTyConApp_maybe (repType ty) of
813 case tcSplitTyConApp_maybe (repType arg_ty) of
814 Just (cc,[]) -> cc == charTyCon
818 -- Support String as an argument or result from a .NET FFI call.
819 isFFIDotnetObjTy ty =
821 (_, t_ty) = tcSplitForAllTys ty
823 case tcSplitTyConApp_maybe (repType t_ty) of
824 Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
827 toDNType :: Type -> DNType
829 | isStringTy ty = DNString
830 | isFFIDotnetObjTy ty = DNObject
831 | Just (tc,argTys) <- tcSplitTyConApp_maybe ty =
832 case lookup (getUnique tc) dn_assoc of
835 | tc `hasKey` ioTyConKey -> toDNType (head argTys)
836 | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
838 dn_assoc :: [ (Unique, DNType) ]
839 dn_assoc = [ (unitTyConKey, DNUnit)
840 , (intTyConKey, DNInt)
841 , (int8TyConKey, DNInt8)
842 , (int16TyConKey, DNInt16)
843 , (int32TyConKey, DNInt32)
844 , (int64TyConKey, DNInt64)
845 , (wordTyConKey, DNInt)
846 , (word8TyConKey, DNWord8)
847 , (word16TyConKey, DNWord16)
848 , (word32TyConKey, DNWord32)
849 , (word64TyConKey, DNWord64)
850 , (floatTyConKey, DNFloat)
851 , (doubleTyConKey, DNDouble)
852 , (addrTyConKey, DNPtr)
853 , (ptrTyConKey, DNPtr)
854 , (funPtrTyConKey, DNPtr)
855 , (charTyConKey, DNChar)
856 , (boolTyConKey, DNBool)
859 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
860 -- Look through newtypes
861 -- Non-recursive ones are transparent to splitTyConApp,
862 -- but recursive ones aren't
863 checkRepTyCon check_tc ty
864 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
867 checkRepTyConKey :: [Unique] -> Type -> Bool
868 -- Like checkRepTyCon, but just looks at the TyCon key
869 checkRepTyConKey keys
870 = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
873 ----------------------------------------------
874 These chaps do the work; they are not exported
875 ----------------------------------------------
878 legalFEArgTyCon :: TyCon -> Bool
879 -- It's illegal to return foreign objects and (mutable)
880 -- bytearrays from a _ccall_ / foreign declaration
881 -- (or be passed them as arguments in foreign exported functions).
883 | isByteArrayLikeTyCon tc
885 -- It's also illegal to make foreign exports that take unboxed
886 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
888 = boxedMarshalableTyCon tc
890 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
891 legalFIResultTyCon dflags tc
892 | isByteArrayLikeTyCon tc = False
893 | tc == unitTyCon = True
894 | otherwise = marshalableTyCon dflags tc
896 legalFEResultTyCon :: TyCon -> Bool
897 legalFEResultTyCon tc
898 | isByteArrayLikeTyCon tc = False
899 | tc == unitTyCon = True
900 | otherwise = boxedMarshalableTyCon tc
902 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
903 -- Checks validity of types going from Haskell -> external world
904 legalOutgoingTyCon dflags safety tc
905 | playSafe safety && isByteArrayLikeTyCon tc
908 = marshalableTyCon dflags tc
910 marshalableTyCon dflags tc
911 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
912 || boxedMarshalableTyCon tc
914 boxedMarshalableTyCon tc
915 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
916 , int32TyConKey, int64TyConKey
917 , wordTyConKey, word8TyConKey, word16TyConKey
918 , word32TyConKey, word64TyConKey
919 , floatTyConKey, doubleTyConKey
920 , addrTyConKey, ptrTyConKey, funPtrTyConKey
923 , byteArrayTyConKey, mutableByteArrayTyConKey
927 isByteArrayLikeTyCon :: TyCon -> Bool
928 isByteArrayLikeTyCon tc =
929 getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
933 %************************************************************************
935 \subsection{Unification with an explicit substitution}
937 %************************************************************************
939 Unify types with an explicit substitution and no monad.
940 Ignore usage annotations.
944 = (TyVarSet, -- Set of template tyvars
945 TyVarSubstEnv) -- Not necessarily idempotent
947 unifyTysX :: TyVarSet -- Template tyvars
950 -> Maybe TyVarSubstEnv
951 unifyTysX tmpl_tyvars ty1 ty2
952 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
954 unifyExtendTysX :: TyVarSet -- Template tyvars
955 -> TyVarSubstEnv -- Substitution to start with
958 -> Maybe TyVarSubstEnv -- Extended substitution
959 unifyExtendTysX tmpl_tyvars subst ty1 ty2
960 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
962 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
963 -> Maybe TyVarSubstEnv
964 unifyTyListsX tmpl_tyvars tys1 tys2
965 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
970 -> (MySubst -> Maybe result)
974 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
975 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
977 -- Variables; go for uVar
978 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
981 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
982 | tyvar1 `elemVarSet` tmpls
983 = uVarX tyvar1 ty2 k subst
984 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
985 | tyvar2 `elemVarSet` tmpls
986 = uVarX tyvar2 ty1 k subst
989 uTysX (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) k subst
990 | n1 == n2 = uTysX t1 t2 k subst
991 uTysX (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) k subst
992 | c1 == c2 = uTyListsX tys1 tys2 k subst
994 -- Functions; just check the two parts
995 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
996 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
998 -- Type constructors must match
999 uTysX (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) k subst
1000 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
1001 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
1002 | (con1 == con2 && equalLength tys1 tys2)
1003 = uTyListsX tys1 tys2 k subst
1005 -- Applications need a bit of care!
1006 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1007 -- NB: we've already dealt with type variables and Notes,
1008 -- so if one type is an App the other one jolly well better be too
1009 uTysX (AppTy s1 t1) ty2 k subst
1010 = case tcSplitAppTy_maybe ty2 of
1011 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1012 Nothing -> Nothing -- Fail
1014 uTysX ty1 (AppTy s2 t2) k subst
1015 = case tcSplitAppTy_maybe ty1 of
1016 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1017 Nothing -> Nothing -- Fail
1019 -- Not expecting for-alls in unification
1021 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
1022 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1025 -- Anything else fails
1026 uTysX ty1 ty2 k subst = Nothing
1029 uTyListsX [] [] k subst = k subst
1030 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1031 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1035 -- Invariant: tv1 is a unifiable variable
1036 uVarX tv1 ty2 k subst@(tmpls, env)
1037 = case lookupSubstEnv env tv1 of
1038 Just (DoneTy ty1) -> -- Already bound
1039 uTysX ty1 ty2 k subst
1041 Nothing -- Not already bound
1042 | typeKind ty2 `eqKind` tyVarKind tv1
1043 && occur_check_ok ty2
1044 -> -- No kind mismatch nor occur check
1045 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1047 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1049 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1050 occur_check_ok_tv tv | tv1 == tv = False
1051 | otherwise = case lookupSubstEnv env tv of
1053 Just (DoneTy ty) -> occur_check_ok ty
1058 %************************************************************************
1060 \subsection{Matching on types}
1062 %************************************************************************
1064 Matching is a {\em unidirectional} process, matching a type against a
1065 template (which is just a type with type variables in it). The
1066 matcher assumes that there are no repeated type variables in the
1067 template, so that it simply returns a mapping of type variables to
1068 types. It also fails on nested foralls.
1070 @matchTys@ matches corresponding elements of a list of templates and
1071 types. It and @matchTy@ both ignore usage annotations, unlike the
1072 main function @match@.
1075 matchTy :: TyVarSet -- Template tyvars
1077 -> Type -- Proposed instance of template
1078 -> Maybe TyVarSubstEnv -- Matching substitution
1081 matchTys :: TyVarSet -- Template tyvars
1082 -> [Type] -- Templates
1083 -> [Type] -- Proposed instance of template
1084 -> Maybe (TyVarSubstEnv, -- Matching substitution
1085 [Type]) -- Left over instance types
1087 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1089 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1090 (\ (senv,tys) -> Just (senv,tys))
1094 @match@ is the main function. It takes a flag indicating whether
1095 usage annotations are to be respected.
1098 match :: Type -> Type -- Current match pair
1099 -> TyVarSet -- Template vars
1100 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1101 -> TyVarSubstEnv -- Current subst
1104 -- When matching against a type variable, see if the variable
1105 -- has already been bound. If so, check that what it's bound to
1106 -- is the same as ty; if not, bind it and carry on.
1108 match (TyVarTy v) ty tmpls k senv
1109 | v `elemVarSet` tmpls
1110 = -- v is a template variable
1111 case lookupSubstEnv senv v of
1112 Nothing | typeKind ty `eqKind` tyVarKind v
1113 -- We do a kind check, just as in the uVarX above
1114 -- The kind check is needed to avoid bogus matches
1115 -- of (a b) with (c d), where the kinds don't match
1116 -- An occur check isn't needed when matching.
1117 -> k (extendSubstEnv senv v (DoneTy ty))
1119 | otherwise -> Nothing -- Fails
1121 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1122 | otherwise -> Nothing -- Fails
1125 = -- v is not a template variable; ty had better match
1126 -- Can't use (==) because types differ
1127 case tcGetTyVar_maybe ty of
1128 Just v' | v == v' -> k senv -- Success
1129 other -> Nothing -- Failure
1130 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1131 -- I guess the reason the Note-stripping case is *last* rather than first
1132 -- is to preserve type synonyms etc., so I'm not moving it to the
1133 -- top; but this means that (without the deNotetype) a type
1134 -- variable may not match the pattern (TyVarTy v') as one would
1135 -- expect, due to an intervening Note. KSW 2000-06.
1138 match (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) tmpls k senv
1139 | n1 == n2 = match t1 t2 tmpls k senv
1140 match (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) tmpls k senv
1141 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1143 -- Functions; just check the two parts
1144 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1145 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1147 match (AppTy fun1 arg1) ty2 tmpls k senv
1148 = case tcSplitAppTy_maybe ty2 of
1149 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1150 Nothing -> Nothing -- Fail
1152 -- Newtypes are opaque; predicate types should not happen
1153 match (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) tmpls k senv
1154 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1155 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1156 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1158 -- With type synonyms, we have to be careful for the exact
1159 -- same reasons as in the unifier. Please see the
1160 -- considerable commentary there before changing anything
1161 -- here! (WDP 95/05)
1162 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1163 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1166 match _ _ _ _ _ = Nothing
1168 match_list_exactly tys1 tys2 tmpls k senv
1169 = match_list tys1 tys2 tmpls k' senv
1171 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1172 | otherwise = Nothing -- Fail
1174 match_list [] tys2 tmpls k senv = k (senv, tys2)
1175 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1176 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1177 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv