2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1998
6 Type - public interface
9 -- The above warning supression flag is a temporary kludge.
10 -- While working on this module you are encouraged to remove it and fix
11 -- any warnings in the module. See
12 -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
15 -- | Main functions for manipulating types and type-related things
17 -- Note some of this is just re-exports from TyCon..
19 -- * Main data types representing Types
20 -- $type_classification
22 -- $representation_types
23 TyThing(..), Type, PredType(..), ThetaType,
25 -- ** Constructing and deconstructing types
26 mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe,
28 mkAppTy, mkAppTys, splitAppTy, splitAppTys,
29 splitAppTy_maybe, repSplitAppTy_maybe,
31 mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
32 splitFunTys, splitFunTysN,
33 funResultTy, funArgTy, zipFunTys, typeArity,
35 mkTyConApp, mkTyConTy,
36 tyConAppTyCon, tyConAppArgs,
37 splitTyConApp_maybe, splitTyConApp,
39 mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
40 applyTy, applyTys, applyTysD, isForAllTy, dropForAlls,
43 newTyConInstRhs, carefullySplitNewType_maybe,
46 tyFamInsts, predFamInsts,
49 mkPredTy, mkPredTys, mkFamilyTyConApp, isEqPred,
51 -- ** Common type constructors
54 -- ** Predicates on types
55 isTyVarTy, isFunTy, isDictTy,
57 -- (Lifting and boxity)
58 isUnLiftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
59 isPrimitiveType, isStrictType, isStrictPred,
61 -- * Main data types representing Kinds
63 Kind, SimpleKind, KindVar,
65 -- ** Common Kinds and SuperKinds
66 liftedTypeKind, unliftedTypeKind, openTypeKind,
67 argTypeKind, ubxTupleKind,
69 tySuperKind, coSuperKind,
71 -- ** Common Kind type constructors
72 liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
73 argTypeKindTyCon, ubxTupleKindTyCon,
75 -- * Type free variables
76 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
79 -- * Tidying type related things up for printing
81 tidyOpenType, tidyOpenTypes,
82 tidyTyVarBndr, tidyFreeTyVars,
83 tidyOpenTyVar, tidyOpenTyVars,
84 tidyTopType, tidyPred,
88 coreEqType, coreEqType2,
89 tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
90 tcEqPred, tcEqPredX, tcCmpPred, tcEqTypeX, tcPartOfType, tcPartOfPred,
92 -- * Forcing evaluation of types
95 -- * Other views onto Types
96 coreView, tcView, kindView,
100 -- * Type representation for the code generator
103 typePrimRep, predTypeRep,
105 -- * Main type substitution data types
106 TvSubstEnv, -- Representation widely visible
107 TvSubst(..), -- Representation visible to a few friends
109 -- ** Manipulating type substitutions
110 emptyTvSubstEnv, emptyTvSubst,
112 mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
113 getTvSubstEnv, setTvSubstEnv, zapTvSubstEnv, getTvInScope,
114 extendTvInScope, extendTvInScopeList,
115 extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
118 -- ** Performing substitution on types
119 substTy, substTys, substTyWith, substTysWith, substTheta,
120 substPred, substTyVar, substTyVars, substTyVarBndr, deShadowTy, lookupTyVar,
123 pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll,
124 pprPred, pprEqPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind,
129 #include "HsVersions.h"
131 -- We import the representation and primitive functions from TypeRep.
132 -- Many things are reexported, but not the representation!
144 import BasicTypes ( Arity )
153 import Data.Maybe ( isJust )
155 infixr 3 `mkFunTy` -- Associates to the right
159 -- $type_classification
160 -- #type_classification#
164 -- [Unboxed] Iff its representation is other than a pointer
165 -- Unboxed types are also unlifted.
167 -- [Lifted] Iff it has bottom as an element.
168 -- Closures always have lifted types: i.e. any
169 -- let-bound identifier in Core must have a lifted
170 -- type. Operationally, a lifted object is one that
172 -- Only lifted types may be unified with a type variable.
174 -- [Algebraic] Iff it is a type with one or more constructors, whether
175 -- declared with @data@ or @newtype@.
176 -- An algebraic type is one that can be deconstructed
177 -- with a case expression. This is /not/ the same as
178 -- lifted types, because we also include unboxed
179 -- tuples in this classification.
181 -- [Data] Iff it is a type declared with @data@, or a boxed tuple.
183 -- [Primitive] Iff it is a built-in type that can't be expressed in Haskell.
185 -- Currently, all primitive types are unlifted, but that's not necessarily
186 -- the case: for example, @Int@ could be primitive.
188 -- Some primitive types are unboxed, such as @Int#@, whereas some are boxed
189 -- but unlifted (such as @ByteArray#@). The only primitive types that we
190 -- classify as algebraic are the unboxed tuples.
192 -- Some examples of type classifications that may make this a bit clearer are:
195 -- Type primitive boxed lifted algebraic
196 -- -----------------------------------------------------------------------------
198 -- ByteArray# Yes Yes No No
199 -- (\# a, b \#) Yes No No Yes
200 -- ( a, b ) No Yes Yes Yes
201 -- [a] No Yes Yes Yes
204 -- $representation_types
205 -- A /source type/ is a type that is a separate type as far as the type checker is
206 -- concerned, but which has a more low-level representation as far as Core-to-Core
207 -- passes and the rest of the back end is concerned. Notably, 'PredTy's are removed
208 -- from the representation type while they do exist in the source types.
210 -- You don't normally have to worry about this, as the utility functions in
211 -- this module will automatically convert a source into a representation type
212 -- if they are spotted, to the best of it's abilities. If you don't want this
213 -- to happen, use the equivalent functions from the "TcType" module.
216 %************************************************************************
220 %************************************************************************
223 {-# INLINE coreView #-}
224 coreView :: Type -> Maybe Type
225 -- ^ In Core, we \"look through\" non-recursive newtypes and 'PredTypes': this
226 -- function tries to obtain a different view of the supplied type given this
228 -- Strips off the /top layer only/ of a type to give
229 -- its underlying representation type.
230 -- Returns Nothing if there is nothing to look through.
232 -- In the case of @newtype@s, it returns one of:
234 -- 1) A vanilla 'TyConApp' (recursive newtype, or non-saturated)
236 -- 2) The newtype representation (otherwise), meaning the
237 -- type written in the RHS of the newtype declaration,
238 -- which may itself be a newtype
240 -- For example, with:
242 -- > newtype R = MkR S
243 -- > newtype S = MkS T
244 -- > newtype T = MkT (T -> T)
246 -- 'expandNewTcApp' on:
248 -- * @R@ gives @Just S@
249 -- * @S@ gives @Just T@
250 -- * @T@ gives @Nothing@ (no expansion)
252 -- By being non-recursive and inlined, this case analysis gets efficiently
253 -- joined onto the case analysis that the caller is already doing
255 | isEqPred p = Nothing
256 | otherwise = Just (predTypeRep p)
257 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
258 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
259 -- Its important to use mkAppTys, rather than (foldl AppTy),
260 -- because the function part might well return a
261 -- partially-applied type constructor; indeed, usually will!
266 -----------------------------------------------
267 {-# INLINE tcView #-}
268 tcView :: Type -> Maybe Type
269 -- ^ Similar to 'coreView', but for the type checker, which just looks through synonyms
270 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
271 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
274 -----------------------------------------------
275 expandTypeSynonyms :: Type -> Type
276 -- ^ Expand out all type synonyms. Actually, it'd suffice to expand out
277 -- just the ones that discard type variables (e.g. type Funny a = Int)
278 -- But we don't know which those are currently, so we just expand all.
279 expandTypeSynonyms ty
283 | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
284 = go (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
286 = TyConApp tc (map go tys)
287 go (TyVarTy tv) = TyVarTy tv
288 go (AppTy t1 t2) = AppTy (go t1) (go t2)
289 go (FunTy t1 t2) = FunTy (go t1) (go t2)
290 go (ForAllTy tv t) = ForAllTy tv (go t)
291 go (PredTy p) = PredTy (go_pred p)
293 go_pred (ClassP c ts) = ClassP c (map go ts)
294 go_pred (IParam ip t) = IParam ip (go t)
295 go_pred (EqPred t1 t2) = EqPred (go t1) (go t2)
297 -----------------------------------------------
298 {-# INLINE kindView #-}
299 kindView :: Kind -> Maybe Kind
300 -- ^ Similar to 'coreView' or 'tcView', but works on 'Kind's
302 -- For the moment, we don't even handle synonyms in kinds
307 %************************************************************************
309 \subsection{Constructor-specific functions}
311 %************************************************************************
314 ---------------------------------------------------------------------
318 mkTyVarTy :: TyVar -> Type
321 mkTyVarTys :: [TyVar] -> [Type]
322 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
324 -- | Attempts to obtain the type variable underlying a 'Type', and panics with the
325 -- given message if this is not a type variable type. See also 'getTyVar_maybe'
326 getTyVar :: String -> Type -> TyVar
327 getTyVar msg ty = case getTyVar_maybe ty of
329 Nothing -> panic ("getTyVar: " ++ msg)
331 isTyVarTy :: Type -> Bool
332 isTyVarTy ty = isJust (getTyVar_maybe ty)
334 -- | Attempts to obtain the type variable underlying a 'Type'
335 getTyVar_maybe :: Type -> Maybe TyVar
336 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
337 getTyVar_maybe (TyVarTy tv) = Just tv
338 getTyVar_maybe _ = Nothing
343 ---------------------------------------------------------------------
346 We need to be pretty careful with AppTy to make sure we obey the
347 invariant that a TyConApp is always visibly so. mkAppTy maintains the
351 -- | Applies a type to another, as in e.g. @k a@
352 mkAppTy :: Type -> Type -> Type
353 mkAppTy orig_ty1 orig_ty2
356 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
357 mk_app _ = AppTy orig_ty1 orig_ty2
358 -- Note that the TyConApp could be an
359 -- under-saturated type synonym. GHC allows that; e.g.
360 -- type Foo k = k a -> k a
362 -- foo :: Foo Id -> Foo Id
364 -- Here Id is partially applied in the type sig for Foo,
365 -- but once the type synonyms are expanded all is well
367 mkAppTys :: Type -> [Type] -> Type
368 mkAppTys orig_ty1 [] = orig_ty1
369 -- This check for an empty list of type arguments
370 -- avoids the needless loss of a type synonym constructor.
371 -- For example: mkAppTys Rational []
372 -- returns to (Ratio Integer), which has needlessly lost
373 -- the Rational part.
374 mkAppTys orig_ty1 orig_tys2
377 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
378 -- mkTyConApp: see notes with mkAppTy
379 mk_app _ = foldl AppTy orig_ty1 orig_tys2
382 splitAppTy_maybe :: Type -> Maybe (Type, Type)
383 -- ^ Attempt to take a type application apart, whether it is a
384 -- function, type constructor, or plain type application. Note
385 -- that type family applications are NEVER unsaturated by this!
386 splitAppTy_maybe ty | Just ty' <- coreView ty
387 = splitAppTy_maybe ty'
388 splitAppTy_maybe ty = repSplitAppTy_maybe ty
391 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
392 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
393 -- any Core view stuff is already done
394 repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
395 repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
396 repSplitAppTy_maybe (TyConApp tc tys)
397 | isDecomposableTyCon tc || length tys > tyConArity tc
398 = case snocView tys of -- never create unsaturated type family apps
399 Just (tys', ty') -> Just (TyConApp tc tys', ty')
401 repSplitAppTy_maybe _other = Nothing
403 splitAppTy :: Type -> (Type, Type)
404 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
405 -- and panics if this is not possible
406 splitAppTy ty = case splitAppTy_maybe ty of
408 Nothing -> panic "splitAppTy"
411 splitAppTys :: Type -> (Type, [Type])
412 -- ^ Recursively splits a type as far as is possible, leaving a residual
413 -- type being applied to and the type arguments applied to it. Never fails,
414 -- even if that means returning an empty list of type applications.
415 splitAppTys ty = split ty ty []
417 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
418 split _ (AppTy ty arg) args = split ty ty (arg:args)
419 split _ (TyConApp tc tc_args) args
420 = let -- keep type families saturated
421 n | isDecomposableTyCon tc = 0
422 | otherwise = tyConArity tc
423 (tc_args1, tc_args2) = splitAt n tc_args
425 (TyConApp tc tc_args1, tc_args2 ++ args)
426 split _ (FunTy ty1 ty2) args = ASSERT( null args )
427 (TyConApp funTyCon [], [ty1,ty2])
428 split orig_ty _ args = (orig_ty, args)
433 ---------------------------------------------------------------------
438 mkFunTy :: Type -> Type -> Type
439 -- ^ Creates a function type from the given argument and result type
440 mkFunTy arg@(PredTy (EqPred {})) res = ForAllTy (mkWildCoVar arg) res
441 mkFunTy arg res = FunTy arg res
443 mkFunTys :: [Type] -> Type -> Type
444 mkFunTys tys ty = foldr mkFunTy ty tys
446 isFunTy :: Type -> Bool
447 isFunTy ty = isJust (splitFunTy_maybe ty)
449 splitFunTy :: Type -> (Type, Type)
450 -- ^ Attempts to extract the argument and result types from a type, and
451 -- panics if that is not possible. See also 'splitFunTy_maybe'
452 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
453 splitFunTy (FunTy arg res) = (arg, res)
454 splitFunTy other = pprPanic "splitFunTy" (ppr other)
456 splitFunTy_maybe :: Type -> Maybe (Type, Type)
457 -- ^ Attempts to extract the argument and result types from a type
458 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
459 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
460 splitFunTy_maybe _ = Nothing
462 splitFunTys :: Type -> ([Type], Type)
463 splitFunTys ty = split [] ty ty
465 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
466 split args _ (FunTy arg res) = split (arg:args) res res
467 split args orig_ty _ = (reverse args, orig_ty)
469 splitFunTysN :: Int -> Type -> ([Type], Type)
470 -- ^ Split off exactly the given number argument types, and panics if that is not possible
471 splitFunTysN 0 ty = ([], ty)
472 splitFunTysN n ty = case splitFunTy ty of { (arg, res) ->
473 case splitFunTysN (n-1) res of { (args, res) ->
476 -- | Splits off argument types from the given type and associating
477 -- them with the things in the input list from left to right. The
478 -- final result type is returned, along with the resulting pairs of
479 -- objects and types, albeit with the list of pairs in reverse order.
480 -- Panics if there are not enough argument types for the input list.
481 zipFunTys :: Outputable a => [a] -> Type -> ([(a, Type)], Type)
482 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
484 split acc [] nty _ = (reverse acc, nty)
486 | Just ty' <- coreView ty = split acc xs nty ty'
487 split acc (x:xs) _ (FunTy arg res) = split ((x,arg):acc) xs res res
488 split _ _ _ _ = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
490 funResultTy :: Type -> Type
491 -- ^ Extract the function result type and panic if that is not possible
492 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
493 funResultTy (FunTy _arg res) = res
494 funResultTy ty = pprPanic "funResultTy" (ppr ty)
496 funArgTy :: Type -> Type
497 -- ^ Extract the function argument type and panic if that is not possible
498 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
499 funArgTy (FunTy arg _res) = arg
500 funArgTy ty = pprPanic "funArgTy" (ppr ty)
502 typeArity :: Type -> Arity
503 -- How many value arrows are visible in the type?
504 -- We look through foralls, but not through newtypes, dictionaries etc
505 typeArity ty | Just ty' <- coreView ty = typeArity ty'
506 typeArity (FunTy _ ty) = 1 + typeArity ty
507 typeArity (ForAllTy _ ty) = typeArity ty
511 ---------------------------------------------------------------------
516 -- | A key function: builds a 'TyConApp' or 'FunTy' as apppropriate to its arguments.
517 -- Applies its arguments to the constructor from left to right
518 mkTyConApp :: TyCon -> [Type] -> Type
520 | isFunTyCon tycon, [ty1,ty2] <- tys
526 -- | Create the plain type constructor type which has been applied to no type arguments at all.
527 mkTyConTy :: TyCon -> Type
528 mkTyConTy tycon = mkTyConApp tycon []
530 -- splitTyConApp "looks through" synonyms, because they don't
531 -- mean a distinct type, but all other type-constructor applications
532 -- including functions are returned as Just ..
534 -- | The same as @fst . splitTyConApp@
535 tyConAppTyCon :: Type -> TyCon
536 tyConAppTyCon ty = fst (splitTyConApp ty)
538 -- | The same as @snd . splitTyConApp@
539 tyConAppArgs :: Type -> [Type]
540 tyConAppArgs ty = snd (splitTyConApp ty)
542 -- | Attempts to tease a type apart into a type constructor and the application
543 -- of a number of arguments to that constructor. Panics if that is not possible.
544 -- See also 'splitTyConApp_maybe'
545 splitTyConApp :: Type -> (TyCon, [Type])
546 splitTyConApp ty = case splitTyConApp_maybe ty of
548 Nothing -> pprPanic "splitTyConApp" (ppr ty)
550 -- | Attempts to tease a type apart into a type constructor and the application
551 -- of a number of arguments to that constructor
552 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
553 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
554 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
555 splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
556 splitTyConApp_maybe _ = Nothing
558 newTyConInstRhs :: TyCon -> [Type] -> Type
559 -- ^ Unwrap one 'layer' of newtype on a type constructor and its arguments, using an
560 -- eta-reduced version of the @newtype@ if possible
561 newTyConInstRhs tycon tys
562 = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs )
563 mkAppTys (substTyWith tvs tys1 ty) tys2
565 (tvs, ty) = newTyConEtadRhs tycon
566 (tys1, tys2) = splitAtList tvs tys
570 ---------------------------------------------------------------------
574 Notes on type synonyms
575 ~~~~~~~~~~~~~~~~~~~~~~
576 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
577 to return type synonyms whereever possible. Thus
582 splitFunTys (a -> Foo a) = ([a], Foo a)
585 The reason is that we then get better (shorter) type signatures in
586 interfaces. Notably this plays a role in tcTySigs in TcBinds.lhs.
589 Note [Expanding newtypes]
590 ~~~~~~~~~~~~~~~~~~~~~~~~~
591 When expanding a type to expose a data-type constructor, we need to be
592 careful about newtypes, lest we fall into an infinite loop. Here are
595 newtype Id x = MkId x
596 newtype Fix f = MkFix (f (Fix f))
597 newtype T = MkT (T -> T)
600 --------------------------
602 Fix Maybe Maybe (Fix Maybe)
606 Notice that we can expand T, even though it's recursive.
607 And we can expand Id (Id Int), even though the Id shows up
608 twice at the outer level.
610 So, when expanding, we keep track of when we've seen a recursive
611 newtype at outermost level; and bale out if we see it again.
623 -- 4. All newtypes, including recursive ones, but not newtype families
625 -- It's useful in the back end of the compiler.
626 repType :: Type -> Type
627 -- Only applied to types of kind *; hence tycons are saturated
631 go :: [TyCon] -> Type -> Type
632 go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms
635 go rec_nts (ForAllTy _ ty) -- Look through foralls
638 go rec_nts (TyConApp tc tys) -- Expand newtypes
639 | Just (rec_nts', ty') <- carefullySplitNewType_maybe rec_nts tc tys
645 carefullySplitNewType_maybe :: [TyCon] -> TyCon -> [Type] -> Maybe ([TyCon],Type)
646 -- Return the representation of a newtype, unless
647 -- we've seen it already: see Note [Expanding newtypes]
648 carefullySplitNewType_maybe rec_nts tc tys
650 , not (tc `elem` rec_nts) = Just (rec_nts', newTyConInstRhs tc tys)
651 | otherwise = Nothing
653 rec_nts' | isRecursiveTyCon tc = tc:rec_nts
654 | otherwise = rec_nts
657 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
658 -- of inspecting the type directly.
660 -- | Discovers the primitive representation of a more abstract 'Type'
661 typePrimRep :: Type -> PrimRep
662 typePrimRep ty = case repType ty of
663 TyConApp tc _ -> tyConPrimRep tc
665 AppTy _ _ -> PtrRep -- See note below
667 _ -> pprPanic "typePrimRep" (ppr ty)
668 -- Types of the form 'f a' must be of kind *, not *#, so
669 -- we are guaranteed that they are represented by pointers.
670 -- The reason is that f must have kind *->*, not *->*#, because
671 -- (we claim) there is no way to constrain f's kind any other
676 ---------------------------------------------------------------------
681 mkForAllTy :: TyVar -> Type -> Type
685 -- | Wraps foralls over the type using the provided 'TyVar's from left to right
686 mkForAllTys :: [TyVar] -> Type -> Type
687 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
689 isForAllTy :: Type -> Bool
690 isForAllTy (ForAllTy _ _) = True
693 -- | Attempts to take a forall type apart, returning the bound type variable
694 -- and the remainder of the type
695 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
696 splitForAllTy_maybe ty = splitFAT_m ty
698 splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
699 splitFAT_m (ForAllTy tyvar ty) = Just(tyvar, ty)
700 splitFAT_m _ = Nothing
702 -- | Attempts to take a forall type apart, returning all the immediate such bound
703 -- type variables and the remainder of the type. Always suceeds, even if that means
704 -- returning an empty list of 'TyVar's
705 splitForAllTys :: Type -> ([TyVar], Type)
706 splitForAllTys ty = split ty ty []
708 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
709 split _ (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
710 split orig_ty _ tvs = (reverse tvs, orig_ty)
712 -- | Equivalent to @snd . splitForAllTys@
713 dropForAlls :: Type -> Type
714 dropForAlls ty = snd (splitForAllTys ty)
717 -- (mkPiType now in CoreUtils)
723 -- | Instantiate a forall type with one or more type arguments.
724 -- Used when we have a polymorphic function applied to type args:
728 -- We use @applyTys type-of-f [t1,t2]@ to compute the type of the expression.
729 -- Panics if no application is possible.
730 applyTy :: Type -> Type -> Type
731 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
732 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
733 applyTy _ _ = panic "applyTy"
735 applyTys :: Type -> [Type] -> Type
736 -- ^ This function is interesting because:
738 -- 1. The function may have more for-alls than there are args
740 -- 2. Less obviously, it may have fewer for-alls
742 -- For case 2. think of:
744 -- > applyTys (forall a.a) [forall b.b, Int]
746 -- This really can happen, via dressing up polymorphic types with newtype
747 -- clothing. Here's an example:
749 -- > newtype R = R (forall a. a->a)
750 -- > foo = case undefined :: R of
753 applyTys ty args = applyTysD empty ty args
755 applyTysD :: SDoc -> Type -> [Type] -> Type -- Debug version
756 applyTysD _ orig_fun_ty [] = orig_fun_ty
757 applyTysD doc orig_fun_ty arg_tys
758 | n_tvs == n_args -- The vastly common case
759 = substTyWith tvs arg_tys rho_ty
760 | n_tvs > n_args -- Too many for-alls
761 = substTyWith (take n_args tvs) arg_tys
762 (mkForAllTys (drop n_args tvs) rho_ty)
763 | otherwise -- Too many type args
764 = ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty ) -- Zero case gives infnite loop!
765 applyTysD doc (substTyWith tvs (take n_tvs arg_tys) rho_ty)
768 (tvs, rho_ty) = splitForAllTys orig_fun_ty
770 n_args = length arg_tys
774 %************************************************************************
776 \subsection{Source types}
778 %************************************************************************
780 Source types are always lifted.
782 The key function is predTypeRep which gives the representation of a source type:
785 mkPredTy :: PredType -> Type
786 mkPredTy pred = PredTy pred
788 mkPredTys :: ThetaType -> [Type]
789 mkPredTys preds = map PredTy preds
791 isEqPred :: PredType -> Bool
792 isEqPred (EqPred _ _) = True
795 predTypeRep :: PredType -> Type
796 -- ^ Convert a 'PredType' to its representation type. However, it unwraps
797 -- only the outermost level; for example, the result might be a newtype application
798 predTypeRep (IParam _ ty) = ty
799 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
800 -- Result might be a newtype application, but the consumer will
801 -- look through that too if necessary
802 predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2))
804 mkFamilyTyConApp :: TyCon -> [Type] -> Type
805 -- ^ Given a family instance TyCon and its arg types, return the
806 -- corresponding family type. E.g:
809 -- > data instance T (Maybe b) = MkT b
811 -- Where the instance tycon is :RTL, so:
813 -- > mkFamilyTyConApp :RTL Int = T (Maybe Int)
814 mkFamilyTyConApp tc tys
815 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
816 , let fam_subst = zipTopTvSubst (tyConTyVars tc) tys
817 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
821 -- | Pretty prints a 'TyCon', using the family instance in case of a
822 -- representation tycon. For example:
824 -- > data T [a] = ...
826 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
827 pprSourceTyCon :: TyCon -> SDoc
829 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
830 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
834 isDictTy :: Type -> Bool
835 isDictTy ty = case splitTyConApp_maybe ty of
836 Just (tc, _) -> isClassTyCon tc
841 %************************************************************************
843 The free variables of a type
845 %************************************************************************
848 tyVarsOfType :: Type -> TyVarSet
849 -- ^ NB: for type synonyms tyVarsOfType does /not/ expand the synonym
850 tyVarsOfType (TyVarTy tv) = unitVarSet tv
851 tyVarsOfType (TyConApp _ tys) = tyVarsOfTypes tys
852 tyVarsOfType (PredTy sty) = tyVarsOfPred sty
853 tyVarsOfType (FunTy arg res) = tyVarsOfType arg `unionVarSet` tyVarsOfType res
854 tyVarsOfType (AppTy fun arg) = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
855 tyVarsOfType (ForAllTy tyvar ty) = delVarSet (tyVarsOfType ty) tyvar
857 tyVarsOfTypes :: [Type] -> TyVarSet
858 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
860 tyVarsOfPred :: PredType -> TyVarSet
861 tyVarsOfPred (IParam _ ty) = tyVarsOfType ty
862 tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys
863 tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
865 tyVarsOfTheta :: ThetaType -> TyVarSet
866 tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
870 %************************************************************************
872 \subsection{Type families}
874 %************************************************************************
877 -- | Finds type family instances occuring in a type after expanding synonyms.
878 tyFamInsts :: Type -> [(TyCon, [Type])]
880 | Just exp_ty <- tcView ty = tyFamInsts exp_ty
881 tyFamInsts (TyVarTy _) = []
882 tyFamInsts (TyConApp tc tys)
883 | isOpenSynTyCon tc = [(tc, tys)]
884 | otherwise = concat (map tyFamInsts tys)
885 tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
886 tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
887 tyFamInsts (ForAllTy _ ty) = tyFamInsts ty
888 tyFamInsts (PredTy pty) = predFamInsts pty
890 -- | Finds type family instances occuring in a predicate type after expanding
892 predFamInsts :: PredType -> [(TyCon, [Type])]
893 predFamInsts (ClassP _cla tys) = concat (map tyFamInsts tys)
894 predFamInsts (IParam _ ty) = tyFamInsts ty
895 predFamInsts (EqPred ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
899 %************************************************************************
901 \subsection{TidyType}
903 %************************************************************************
906 -- | This tidies up a type for printing in an error message, or in
907 -- an interface file.
909 -- It doesn't change the uniques at all, just the print names.
910 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
911 tidyTyVarBndr env@(tidy_env, subst) tyvar
912 = case tidyOccName tidy_env (getOccName name) of
913 (tidy', occ') -> ((tidy', subst'), tyvar'')
915 subst' = extendVarEnv subst tyvar tyvar''
916 tyvar' = setTyVarName tyvar name'
917 name' = tidyNameOcc name occ'
918 -- Don't forget to tidy the kind for coercions!
919 tyvar'' | isCoVar tyvar = setTyVarKind tyvar' kind'
921 kind' = tidyType env (tyVarKind tyvar)
923 name = tyVarName tyvar
925 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
926 -- ^ Add the free 'TyVar's to the env in tidy form,
927 -- so that we can tidy the type they are free in
928 tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))
930 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
931 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
933 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
934 -- ^ Treat a new 'TyVar' as a binder, and give it a fresh tidy name
935 -- using the environment if one has not already been allocated. See
936 -- also 'tidyTyVarBndr'
937 tidyOpenTyVar env@(_, subst) tyvar
938 = case lookupVarEnv subst tyvar of
939 Just tyvar' -> (env, tyvar') -- Already substituted
940 Nothing -> tidyTyVarBndr env tyvar -- Treat it as a binder
942 tidyType :: TidyEnv -> Type -> Type
943 tidyType env@(_, subst) ty
946 go (TyVarTy tv) = case lookupVarEnv subst tv of
947 Nothing -> TyVarTy tv
948 Just tv' -> TyVarTy tv'
949 go (TyConApp tycon tys) = let args = map go tys
950 in args `seqList` TyConApp tycon args
951 go (PredTy sty) = PredTy (tidyPred env sty)
952 go (AppTy fun arg) = (AppTy $! (go fun)) $! (go arg)
953 go (FunTy fun arg) = (FunTy $! (go fun)) $! (go arg)
954 go (ForAllTy tv ty) = ForAllTy tvp $! (tidyType envp ty)
956 (envp, tvp) = tidyTyVarBndr env tv
958 tidyTypes :: TidyEnv -> [Type] -> [Type]
959 tidyTypes env tys = map (tidyType env) tys
961 tidyPred :: TidyEnv -> PredType -> PredType
962 tidyPred env (IParam n ty) = IParam n (tidyType env ty)
963 tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
964 tidyPred env (EqPred ty1 ty2) = EqPred (tidyType env ty1) (tidyType env ty2)
969 -- | Grabs the free type variables, tidies them
970 -- and then uses 'tidyType' to work over the type itself
971 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
973 = (env', tidyType env' ty)
975 env' = tidyFreeTyVars env (tyVarsOfType ty)
977 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
978 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
980 -- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
981 tidyTopType :: Type -> Type
982 tidyTopType ty = tidyType emptyTidyEnv ty
987 tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
988 tidyKind env k = tidyOpenType env k
993 %************************************************************************
995 \subsection{Liftedness}
997 %************************************************************************
1000 -- | See "Type#type_classification" for what an unlifted type is
1001 isUnLiftedType :: Type -> Bool
1002 -- isUnLiftedType returns True for forall'd unlifted types:
1003 -- x :: forall a. Int#
1004 -- I found bindings like these were getting floated to the top level.
1005 -- They are pretty bogus types, mind you. It would be better never to
1008 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
1009 isUnLiftedType (ForAllTy _ ty) = isUnLiftedType ty
1010 isUnLiftedType (TyConApp tc _) = isUnLiftedTyCon tc
1011 isUnLiftedType _ = False
1013 isUnboxedTupleType :: Type -> Bool
1014 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
1015 Just (tc, _ty_args) -> isUnboxedTupleTyCon tc
1018 -- | See "Type#type_classification" for what an algebraic type is.
1019 -- Should only be applied to /types/, as opposed to e.g. partially
1020 -- saturated type constructors
1021 isAlgType :: Type -> Bool
1023 = case splitTyConApp_maybe ty of
1024 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1028 -- | See "Type#type_classification" for what an algebraic type is.
1029 -- Should only be applied to /types/, as opposed to e.g. partially
1030 -- saturated type constructors. Closed type constructors are those
1031 -- with a fixed right hand side, as opposed to e.g. associated types
1032 isClosedAlgType :: Type -> Bool
1034 = case splitTyConApp_maybe ty of
1035 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1036 isAlgTyCon tc && not (isOpenTyCon tc)
1041 -- | Computes whether an argument (or let right hand side) should
1042 -- be computed strictly or lazily, based only on its type.
1043 -- Works just like 'isUnLiftedType', except that it has a special case
1044 -- for dictionaries (i.e. does not work purely on representation types)
1046 -- Since it takes account of class 'PredType's, you might think
1047 -- this function should be in 'TcType', but 'isStrictType' is used by 'DataCon',
1048 -- which is below 'TcType' in the hierarchy, so it's convenient to put it here.
1049 isStrictType :: Type -> Bool
1050 isStrictType (PredTy pred) = isStrictPred pred
1051 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
1052 isStrictType (ForAllTy _ ty) = isStrictType ty
1053 isStrictType (TyConApp tc _) = isUnLiftedTyCon tc
1054 isStrictType _ = False
1056 -- | We may be strict in dictionary types, but only if it
1057 -- has more than one component.
1059 -- (Being strict in a single-component dictionary risks
1060 -- poking the dictionary component, which is wrong.)
1061 isStrictPred :: PredType -> Bool
1062 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
1063 isStrictPred _ = False
1067 isPrimitiveType :: Type -> Bool
1068 -- ^ Returns true of types that are opaque to Haskell.
1069 -- Most of these are unlifted, but now that we interact with .NET, we
1070 -- may have primtive (foreign-imported) types that are lifted
1071 isPrimitiveType ty = case splitTyConApp_maybe ty of
1072 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1078 %************************************************************************
1080 \subsection{Sequencing on types}
1082 %************************************************************************
1085 seqType :: Type -> ()
1086 seqType (TyVarTy tv) = tv `seq` ()
1087 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
1088 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
1089 seqType (PredTy p) = seqPred p
1090 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
1091 seqType (ForAllTy tv ty) = tv `seq` seqType ty
1093 seqTypes :: [Type] -> ()
1095 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
1097 seqPred :: PredType -> ()
1098 seqPred (ClassP c tys) = c `seq` seqTypes tys
1099 seqPred (IParam n ty) = n `seq` seqType ty
1100 seqPred (EqPred ty1 ty2) = seqType ty1 `seq` seqType ty2
1104 %************************************************************************
1106 Equality for Core types
1107 (We don't use instances so that we know where it happens)
1109 %************************************************************************
1111 Note that eqType works right even for partial applications of newtypes.
1112 See Note [Newtype eta] in TyCon.lhs
1115 -- | Type equality test for Core types (i.e. ignores predicate-types, synonyms etc.)
1116 coreEqType :: Type -> Type -> Bool
1117 coreEqType t1 t2 = coreEqType2 rn_env t1 t2
1119 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
1121 coreEqType2 :: RnEnv2 -> Type -> Type -> Bool
1122 coreEqType2 rn_env t1 t2
1125 eq env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2
1126 eq env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
1127 eq env (AppTy s1 t1) (AppTy s2 t2) = eq env s1 s2 && eq env t1 t2
1128 eq env (FunTy s1 t1) (FunTy s2 t2) = eq env s1 s2 && eq env t1 t2
1129 eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1130 | tc1 == tc2, all2 (eq env) tys1 tys2 = True
1131 -- The lengths should be equal because
1132 -- the two types have the same kind
1133 -- NB: if the type constructors differ that does not
1134 -- necessarily mean that the types aren't equal
1135 -- (synonyms, newtypes)
1136 -- Even if the type constructors are the same, but the arguments
1137 -- differ, the two types could be the same (e.g. if the arg is just
1138 -- ignored in the RHS). In both these cases we fall through to an
1139 -- attempt to expand one side or the other.
1141 -- Now deal with newtypes, synonyms, pred-tys
1142 eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
1143 | Just t2' <- coreView t2 = eq env t1 t2'
1145 -- Fall through case; not equal!
1150 %************************************************************************
1152 Comparision for source types
1153 (We don't use instances so that we know where it happens)
1155 %************************************************************************
1158 tcEqType :: Type -> Type -> Bool
1159 -- ^ Type equality on source types. Does not look through @newtypes@ or
1160 -- 'PredType's, but it does look through type synonyms.
1161 tcEqType t1 t2 = isEqual $ cmpType t1 t2
1163 tcEqTypes :: [Type] -> [Type] -> Bool
1164 tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
1166 tcCmpType :: Type -> Type -> Ordering
1167 -- ^ Type ordering on source types. Does not look through @newtypes@ or
1168 -- 'PredType's, but it does look through type synonyms.
1169 tcCmpType t1 t2 = cmpType t1 t2
1171 tcCmpTypes :: [Type] -> [Type] -> Ordering
1172 tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
1174 tcEqPred :: PredType -> PredType -> Bool
1175 tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
1177 tcEqPredX :: RnEnv2 -> PredType -> PredType -> Bool
1178 tcEqPredX env p1 p2 = isEqual $ cmpPredX env p1 p2
1180 tcCmpPred :: PredType -> PredType -> Ordering
1181 tcCmpPred p1 p2 = cmpPred p1 p2
1183 tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
1184 tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
1188 -- | Checks whether the second argument is a subterm of the first. (We don't care
1189 -- about binders, as we are only interested in syntactic subterms.)
1190 tcPartOfType :: Type -> Type -> Bool
1192 | tcEqType t1 t2 = True
1194 | Just t2' <- tcView t2 = tcPartOfType t1 t2'
1195 tcPartOfType _ (TyVarTy _) = False
1196 tcPartOfType t1 (ForAllTy _ t2) = tcPartOfType t1 t2
1197 tcPartOfType t1 (AppTy s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2
1198 tcPartOfType t1 (FunTy s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2
1199 tcPartOfType t1 (PredTy p2) = tcPartOfPred t1 p2
1200 tcPartOfType t1 (TyConApp _ ts) = any (tcPartOfType t1) ts
1202 tcPartOfPred :: Type -> PredType -> Bool
1203 tcPartOfPred t1 (IParam _ t2) = tcPartOfType t1 t2
1204 tcPartOfPred t1 (ClassP _ ts) = any (tcPartOfType t1) ts
1205 tcPartOfPred t1 (EqPred s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2
1208 Now here comes the real worker
1211 cmpType :: Type -> Type -> Ordering
1212 cmpType t1 t2 = cmpTypeX rn_env t1 t2
1214 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
1216 cmpTypes :: [Type] -> [Type] -> Ordering
1217 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
1219 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
1221 cmpPred :: PredType -> PredType -> Ordering
1222 cmpPred p1 p2 = cmpPredX rn_env p1 p2
1224 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
1226 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
1227 cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
1228 | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
1230 cmpTypeX env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 `compare` rnOccR env tv2
1231 cmpTypeX env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
1232 cmpTypeX env (AppTy s1 t1) (AppTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1233 cmpTypeX env (FunTy s1 t1) (FunTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1234 cmpTypeX env (PredTy p1) (PredTy p2) = cmpPredX env p1 p2
1235 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
1237 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
1238 cmpTypeX _ (AppTy _ _) (TyVarTy _) = GT
1240 cmpTypeX _ (FunTy _ _) (TyVarTy _) = GT
1241 cmpTypeX _ (FunTy _ _) (AppTy _ _) = GT
1243 cmpTypeX _ (TyConApp _ _) (TyVarTy _) = GT
1244 cmpTypeX _ (TyConApp _ _) (AppTy _ _) = GT
1245 cmpTypeX _ (TyConApp _ _) (FunTy _ _) = GT
1247 cmpTypeX _ (ForAllTy _ _) (TyVarTy _) = GT
1248 cmpTypeX _ (ForAllTy _ _) (AppTy _ _) = GT
1249 cmpTypeX _ (ForAllTy _ _) (FunTy _ _) = GT
1250 cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = GT
1252 cmpTypeX _ (PredTy _) _ = GT
1257 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1258 cmpTypesX _ [] [] = EQ
1259 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1260 cmpTypesX _ [] _ = LT
1261 cmpTypesX _ _ [] = GT
1264 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1265 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1266 -- Compare names only for implicit parameters
1267 -- This comparison is used exclusively (I believe)
1268 -- for the Avails finite map built in TcSimplify
1269 -- If the types differ we keep them distinct so that we see
1270 -- a distinct pair to run improvement on
1271 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTypesX env tys1 tys2)
1272 cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
1274 -- Constructor order: IParam < ClassP < EqPred
1275 cmpPredX _ (IParam {}) _ = LT
1276 cmpPredX _ (ClassP {}) (IParam {}) = GT
1277 cmpPredX _ (ClassP {}) (EqPred {}) = LT
1278 cmpPredX _ (EqPred {}) _ = GT
1281 PredTypes are used as a FM key in TcSimplify,
1282 so we take the easy path and make them an instance of Ord
1285 instance Eq PredType where { (==) = tcEqPred }
1286 instance Ord PredType where { compare = tcCmpPred }
1290 %************************************************************************
1294 %************************************************************************
1297 -- | Type substitution
1299 -- #tvsubst_invariant#
1300 -- The following invariants must hold of a 'TvSubst':
1302 -- 1. The in-scope set is needed /only/ to
1303 -- guide the generation of fresh uniques
1305 -- 2. In particular, the /kind/ of the type variables in
1306 -- the in-scope set is not relevant
1308 -- 3. The substition is only applied ONCE! This is because
1309 -- in general such application will not reached a fixed point.
1311 = TvSubst InScopeSet -- The in-scope type variables
1312 TvSubstEnv -- The substitution itself
1313 -- See Note [Apply Once]
1314 -- and Note [Extending the TvSubstEnv]
1316 {- ----------------------------------------------------------
1320 We use TvSubsts to instantiate things, and we might instantiate
1324 So the substition might go [a->b, b->a]. A similar situation arises in Core
1325 when we find a beta redex like
1326 (/\ a /\ b -> e) b a
1327 Then we also end up with a substition that permutes type variables. Other
1328 variations happen to; for example [a -> (a, b)].
1330 ***************************************************
1331 *** So a TvSubst must be applied precisely once ***
1332 ***************************************************
1334 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
1335 we use during unifications, it must not be repeatedly applied.
1337 Note [Extending the TvSubst]
1338 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1339 See #tvsubst_invariant# for the invariants that must hold.
1341 This invariant allows a short-cut when the TvSubstEnv is empty:
1342 if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) holds ---
1343 then (substTy subst ty) does nothing.
1345 For example, consider:
1346 (/\a. /\b:(a~Int). ...b..) Int
1347 We substitute Int for 'a'. The Unique of 'b' does not change, but
1348 nevertheless we add 'b' to the TvSubstEnv, because b's kind does change
1350 This invariant has several crucial consequences:
1352 * In substTyVarBndr, we need extend the TvSubstEnv
1353 - if the unique has changed
1354 - or if the kind has changed
1356 * In substTyVar, we do not need to consult the in-scope set;
1357 the TvSubstEnv is enough
1359 * In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
1362 -------------------------------------------------------------- -}
1364 -- | A substitition of 'Type's for 'TyVar's
1365 type TvSubstEnv = TyVarEnv Type
1366 -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
1367 -- invariant discussed in Note [Apply Once]), and also independently
1368 -- in the middle of matching, and unification (see Types.Unify)
1369 -- So you have to look at the context to know if it's idempotent or
1370 -- apply-once or whatever
1372 emptyTvSubstEnv :: TvSubstEnv
1373 emptyTvSubstEnv = emptyVarEnv
1375 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1376 -- ^ @(compose env1 env2)(x)@ is @env1(env2(x))@; i.e. apply @env2@ then @env1@.
1377 -- It assumes that both are idempotent.
1378 -- Typically, @env1@ is the refinement to a base substitution @env2@
1379 composeTvSubst in_scope env1 env2
1380 = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1381 -- First apply env1 to the range of env2
1382 -- Then combine the two, making sure that env1 loses if
1383 -- both bind the same variable; that's why env1 is the
1384 -- *left* argument to plusVarEnv, because the right arg wins
1386 subst1 = TvSubst in_scope env1
1388 emptyTvSubst :: TvSubst
1389 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1391 isEmptyTvSubst :: TvSubst -> Bool
1392 -- See Note [Extending the TvSubstEnv]
1393 isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
1395 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1398 getTvSubstEnv :: TvSubst -> TvSubstEnv
1399 getTvSubstEnv (TvSubst _ env) = env
1401 getTvInScope :: TvSubst -> InScopeSet
1402 getTvInScope (TvSubst in_scope _) = in_scope
1404 isInScope :: Var -> TvSubst -> Bool
1405 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1407 notElemTvSubst :: TyVar -> TvSubst -> Bool
1408 notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
1410 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1411 setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
1413 zapTvSubstEnv :: TvSubst -> TvSubst
1414 zapTvSubstEnv (TvSubst in_scope _) = TvSubst in_scope emptyVarEnv
1416 extendTvInScope :: TvSubst -> Var -> TvSubst
1417 extendTvInScope (TvSubst in_scope env) var = TvSubst (extendInScopeSet in_scope var) env
1419 extendTvInScopeList :: TvSubst -> [Var] -> TvSubst
1420 extendTvInScopeList (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
1422 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1423 extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
1425 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1426 extendTvSubstList (TvSubst in_scope env) tvs tys
1427 = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
1429 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1430 -- the types given; but it's just a thunk so with a bit of luck
1431 -- it'll never be evaluated
1433 -- Note [Generating the in-scope set for a substitution]
1434 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1435 -- If we want to substitute [a -> ty1, b -> ty2] I used to
1436 -- think it was enough to generate an in-scope set that includes
1437 -- fv(ty1,ty2). But that's not enough; we really should also take the
1438 -- free vars of the type we are substituting into! Example:
1439 -- (forall b. (a,b,x)) [a -> List b]
1440 -- Then if we use the in-scope set {b}, there is a danger we will rename
1441 -- the forall'd variable to 'x' by mistake, getting this:
1442 -- (forall x. (List b, x, x)
1443 -- Urk! This means looking at all the calls to mkOpenTvSubst....
1446 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1447 -- environment, hence "open"
1448 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1449 mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
1451 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1452 -- environment, hence "open"
1453 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1454 zipOpenTvSubst tyvars tys
1455 | debugIsOn && (length tyvars /= length tys)
1456 = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1458 = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1460 -- | Called when doing top-level substitutions. Here we expect that the
1461 -- free vars of the range of the substitution will be empty.
1462 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1463 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1465 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1466 zipTopTvSubst tyvars tys
1467 | debugIsOn && (length tyvars /= length tys)
1468 = pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1470 = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1472 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1474 | debugIsOn && (length tyvars /= length tys)
1475 = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
1477 = zip_ty_env tyvars tys emptyVarEnv
1479 -- Later substitutions in the list over-ride earlier ones,
1480 -- but there should be no loops
1481 zip_ty_env :: [TyVar] -> [Type] -> TvSubstEnv -> TvSubstEnv
1482 zip_ty_env [] [] env = env
1483 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1484 -- There used to be a special case for when
1486 -- (a not-uncommon case) in which case the substitution was dropped.
1487 -- But the type-tidier changes the print-name of a type variable without
1488 -- changing the unique, and that led to a bug. Why? Pre-tidying, we had
1489 -- a type {Foo t}, where Foo is a one-method class. So Foo is really a newtype.
1490 -- And it happened that t was the type variable of the class. Post-tiding,
1491 -- it got turned into {Foo t2}. The ext-core printer expanded this using
1492 -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1493 -- and so generated a rep type mentioning t not t2.
1495 -- Simplest fix is to nuke the "optimisation"
1496 zip_ty_env tvs tys env = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1497 -- zip_ty_env _ _ env = env
1499 instance Outputable TvSubst where
1500 ppr (TvSubst ins env)
1501 = brackets $ sep[ ptext (sLit "TvSubst"),
1502 nest 2 (ptext (sLit "In scope:") <+> ppr ins),
1503 nest 2 (ptext (sLit "Env:") <+> ppr env) ]
1506 %************************************************************************
1508 Performing type substitutions
1510 %************************************************************************
1513 -- | Type substitution making use of an 'TvSubst' that
1514 -- is assumed to be open, see 'zipOpenTvSubst'
1515 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1516 substTyWith tvs tys = ASSERT( length tvs == length tys )
1517 substTy (zipOpenTvSubst tvs tys)
1519 -- | Type substitution making use of an 'TvSubst' that
1520 -- is assumed to be open, see 'zipOpenTvSubst'
1521 substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
1522 substTysWith tvs tys = ASSERT( length tvs == length tys )
1523 substTys (zipOpenTvSubst tvs tys)
1525 -- | Substitute within a 'Type'
1526 substTy :: TvSubst -> Type -> Type
1527 substTy subst ty | isEmptyTvSubst subst = ty
1528 | otherwise = subst_ty subst ty
1530 -- | Substitute within several 'Type's
1531 substTys :: TvSubst -> [Type] -> [Type]
1532 substTys subst tys | isEmptyTvSubst subst = tys
1533 | otherwise = map (subst_ty subst) tys
1535 -- | Substitute within a 'ThetaType'
1536 substTheta :: TvSubst -> ThetaType -> ThetaType
1537 substTheta subst theta
1538 | isEmptyTvSubst subst = theta
1539 | otherwise = map (substPred subst) theta
1541 -- | Substitute within a 'PredType'
1542 substPred :: TvSubst -> PredType -> PredType
1543 substPred subst (IParam n ty) = IParam n (subst_ty subst ty)
1544 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1545 substPred subst (EqPred ty1 ty2) = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
1547 -- | Remove any nested binders mentioning the 'TyVar's in the 'TyVarSet'
1548 deShadowTy :: TyVarSet -> Type -> Type
1550 = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1552 in_scope = mkInScopeSet tvs
1554 subst_ty :: TvSubst -> Type -> Type
1555 -- subst_ty is the main workhorse for type substitution
1557 -- Note that the in_scope set is poked only if we hit a forall
1558 -- so it may often never be fully computed
1562 go (TyVarTy tv) = substTyVar subst tv
1563 go (TyConApp tc tys) = let args = map go tys
1564 in args `seqList` TyConApp tc args
1566 go (PredTy p) = PredTy $! (substPred subst p)
1568 go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
1569 go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
1570 -- The mkAppTy smart constructor is important
1571 -- we might be replacing (a Int), represented with App
1572 -- by [Int], represented with TyConApp
1573 go (ForAllTy tv ty) = case substTyVarBndr subst tv of
1575 ForAllTy tv' $! (subst_ty subst' ty)
1577 substTyVar :: TvSubst -> TyVar -> Type
1578 substTyVar subst@(TvSubst _ _) tv
1579 = case lookupTyVar subst tv of {
1580 Nothing -> TyVarTy tv;
1581 Just ty -> ty -- See Note [Apply Once]
1584 substTyVars :: TvSubst -> [TyVar] -> [Type]
1585 substTyVars subst tvs = map (substTyVar subst) tvs
1587 lookupTyVar :: TvSubst -> TyVar -> Maybe Type
1588 -- See Note [Extending the TvSubst]
1589 lookupTyVar (TvSubst _ env) tv = lookupVarEnv env tv
1591 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1592 substTyVarBndr subst@(TvSubst in_scope env) old_var
1593 = (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1595 is_co_var = isCoVar old_var
1597 new_env | no_change = delVarEnv env old_var
1598 | otherwise = extendVarEnv env old_var (TyVarTy new_var)
1600 no_change = new_var == old_var && not is_co_var
1601 -- no_change means that the new_var is identical in
1602 -- all respects to the old_var (same unique, same kind)
1603 -- See Note [Extending the TvSubst]
1605 -- In that case we don't need to extend the substitution
1606 -- to map old to new. But instead we must zap any
1607 -- current substitution for the variable. For example:
1608 -- (\x.e) with id_subst = [x |-> e']
1609 -- Here we must simply zap the substitution for x
1611 new_var = uniqAway in_scope subst_old_var
1612 -- The uniqAway part makes sure the new variable is not already in scope
1614 subst_old_var -- subst_old_var is old_var with the substitution applied to its kind
1615 -- It's only worth doing the substitution for coercions,
1616 -- becuase only they can have free type variables
1617 | is_co_var = setTyVarKind old_var (substTy subst (tyVarKind old_var))
1618 | otherwise = old_var
1621 ----------------------------------------------------
1630 -- There's a little subtyping at the kind level:
1640 -- Where: \* [LiftedTypeKind] means boxed type
1641 -- \# [UnliftedTypeKind] means unboxed type
1642 -- (\#) [UbxTupleKind] means unboxed tuple
1643 -- ?? [ArgTypeKind] is the lub of {\*, \#}
1644 -- ? [OpenTypeKind] means any type at all
1649 -- > error :: forall a:?. String -> a
1650 -- > (->) :: ?? -> ? -> \*
1651 -- > (\\(x::t) -> ...)
1653 -- Where in the last example @t :: ??@ (i.e. is not an unboxed tuple)
1655 type KindVar = TyVar -- invariant: KindVar will always be a
1656 -- TcTyVar with details MetaTv TauTv ...
1657 -- kind var constructors and functions are in TcType
1659 type SimpleKind = Kind
1664 During kind inference, a kind variable unifies only with
1666 sk ::= * | sk1 -> sk2
1668 data T a = MkT a (T Int#)
1669 fails. We give T the kind (k -> *), and the kind variable k won't unify
1670 with # (the kind of Int#).
1674 When creating a fresh internal type variable, we give it a kind to express
1675 constraints on it. E.g. in (\x->e) we make up a fresh type variable for x,
1678 During unification we only bind an internal type variable to a type
1679 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1681 When unifying two internal type variables, we collect their kind constraints by
1682 finding the GLB of the two. Since the partial order is a tree, they only
1683 have a glb if one is a sub-kind of the other. In that case, we bind the
1684 less-informative one to the more informative one. Neat, eh?