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, Pred(..), PredType, ThetaType,
26 -- ** Constructing and deconstructing types
27 mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe,
29 mkAppTy, mkAppTys, splitAppTy, splitAppTys,
30 splitAppTy_maybe, repSplitAppTy_maybe,
32 mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
33 splitFunTys, splitFunTysN,
34 funResultTy, funArgTy, zipFunTys,
36 mkTyConApp, mkTyConTy,
37 tyConAppTyCon, tyConAppArgs,
38 splitTyConApp_maybe, splitTyConApp,
40 mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
41 applyTy, applyTys, applyTysD, isForAllTy, dropForAlls,
44 newTyConInstRhs, carefullySplitNewType_maybe,
47 tyFamInsts, predFamInsts,
50 mkPredTy, mkPredTys, mkFamilyTyConApp,
51 mkDictTy, isDictLikeTy, isClassPred,
52 isEqPred, allPred, mkEqPred,
53 mkClassPred, getClassPredTys, getClassPredTys_maybe,
57 -- ** Common type constructors
60 -- ** Predicates on types
61 isTyVarTy, isFunTy, isPredTy,
62 isDictTy, isEqPredTy, isReflPredTy, splitPredTy_maybe, splitEqPredTy_maybe,
64 -- (Lifting and boxity)
65 isUnLiftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
66 isPrimitiveType, isStrictType, isStrictPred,
68 -- * Main data types representing Kinds
70 Kind, SimpleKind, KindVar,
72 -- ** Common Kinds and SuperKinds
73 liftedTypeKind, unliftedTypeKind, openTypeKind,
74 argTypeKind, ubxTupleKind,
77 -- ** Common Kind type constructors
78 liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
79 argTypeKindTyCon, ubxTupleKindTyCon,
81 -- * Type free variables
82 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
83 exactTyVarsOfType, exactTyVarsOfTypes, expandTypeSynonyms,
87 eqType, eqTypeX, eqTypes, cmpType, cmpTypes,
88 eqPred, eqPredX, cmpPred, eqKind,
90 -- * Forcing evaluation of types
91 seqType, seqTypes, seqPred,
93 -- * Other views onto Types
98 -- * Type representation for the code generator
101 typePrimRep, predTypeRep,
103 -- * Main type substitution data types
104 TvSubstEnv, -- Representation widely visible
105 TvSubst(..), -- Representation visible to a few friends
107 -- ** Manipulating type substitutions
108 emptyTvSubstEnv, emptyTvSubst,
110 mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
111 getTvSubstEnv, setTvSubstEnv,
112 zapTvSubstEnv, getTvInScope,
113 extendTvInScope, extendTvInScopeList,
114 extendTvSubst, extendTvSubstList,
115 isInScope, composeTvSubst, zipTyEnv,
116 isEmptyTvSubst, unionTvSubst,
118 -- ** Performing substitution on types
119 substTy, substTys, substTyWith, substTysWith, substTheta,
120 substPred, substTyVar, substTyVars, substTyVarBndr,
121 deShadowTy, lookupTyVar,
124 pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll,
125 pprPred, pprPredTy, pprEqPred, pprTheta, pprThetaArrowTy, pprClassPred,
126 pprKind, pprParendKind,
131 #include "HsVersions.h"
133 -- We import the representation and primitive functions from TypeRep.
134 -- Many things are reexported, but not the representation!
148 import BasicTypes ( IPName )
155 import Data.Maybe ( isJust )
157 infixr 3 `mkFunTy` -- Associates to the right
161 -- $type_classification
162 -- #type_classification#
166 -- [Unboxed] Iff its representation is other than a pointer
167 -- Unboxed types are also unlifted.
169 -- [Lifted] Iff it has bottom as an element.
170 -- Closures always have lifted types: i.e. any
171 -- let-bound identifier in Core must have a lifted
172 -- type. Operationally, a lifted object is one that
174 -- Only lifted types may be unified with a type variable.
176 -- [Algebraic] Iff it is a type with one or more constructors, whether
177 -- declared with @data@ or @newtype@.
178 -- An algebraic type is one that can be deconstructed
179 -- with a case expression. This is /not/ the same as
180 -- lifted types, because we also include unboxed
181 -- tuples in this classification.
183 -- [Data] Iff it is a type declared with @data@, or a boxed tuple.
185 -- [Primitive] Iff it is a built-in type that can't be expressed in Haskell.
187 -- Currently, all primitive types are unlifted, but that's not necessarily
188 -- the case: for example, @Int@ could be primitive.
190 -- Some primitive types are unboxed, such as @Int#@, whereas some are boxed
191 -- but unlifted (such as @ByteArray#@). The only primitive types that we
192 -- classify as algebraic are the unboxed tuples.
194 -- Some examples of type classifications that may make this a bit clearer are:
197 -- Type primitive boxed lifted algebraic
198 -- -----------------------------------------------------------------------------
200 -- ByteArray# Yes Yes No No
201 -- (\# a, b \#) Yes No No Yes
202 -- ( a, b ) No Yes Yes Yes
203 -- [a] No Yes Yes Yes
206 -- $representation_types
207 -- A /source type/ is a type that is a separate type as far as the type checker is
208 -- concerned, but which has a more low-level representation as far as Core-to-Core
209 -- passes and the rest of the back end is concerned. Notably, 'PredTy's are removed
210 -- from the representation type while they do exist in the source types.
212 -- You don't normally have to worry about this, as the utility functions in
213 -- this module will automatically convert a source into a representation type
214 -- if they are spotted, to the best of it's abilities. If you don't want this
215 -- to happen, use the equivalent functions from the "TcType" module.
218 %************************************************************************
222 %************************************************************************
225 {-# INLINE coreView #-}
226 coreView :: Type -> Maybe Type
227 -- ^ In Core, we \"look through\" non-recursive newtypes and 'PredTypes': this
228 -- function tries to obtain a different view of the supplied type given this
230 -- Strips off the /top layer only/ of a type to give
231 -- its underlying representation type.
232 -- Returns Nothing if there is nothing to look through.
234 -- In the case of @newtype@s, it returns one of:
236 -- 1) A vanilla 'TyConApp' (recursive newtype, or non-saturated)
238 -- 2) The newtype representation (otherwise), meaning the
239 -- type written in the RHS of the newtype declaration,
240 -- which may itself be a newtype
242 -- For example, with:
244 -- > newtype R = MkR S
245 -- > newtype S = MkS T
246 -- > newtype T = MkT (T -> T)
248 -- 'expandNewTcApp' on:
250 -- * @R@ gives @Just S@
251 -- * @S@ gives @Just T@
252 -- * @T@ gives @Nothing@ (no expansion)
254 -- By being non-recursive and inlined, this case analysis gets efficiently
255 -- joined onto the case analysis that the caller is already doing
257 | isEqPred p = Nothing
258 | otherwise = Just (predTypeRep p)
259 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
260 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
261 -- Its important to use mkAppTys, rather than (foldl AppTy),
262 -- because the function part might well return a
263 -- partially-applied type constructor; indeed, usually will!
268 -----------------------------------------------
269 {-# INLINE tcView #-}
270 tcView :: Type -> Maybe Type
271 -- ^ Similar to 'coreView', but for the type checker, which just looks through synonyms
272 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
273 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
276 -----------------------------------------------
277 expandTypeSynonyms :: Type -> Type
278 -- ^ Expand out all type synonyms. Actually, it'd suffice to expand out
279 -- just the ones that discard type variables (e.g. type Funny a = Int)
280 -- But we don't know which those are currently, so we just expand all.
281 expandTypeSynonyms ty
285 | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
286 = go (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
288 = TyConApp tc (map go tys)
289 go (TyVarTy tv) = TyVarTy tv
290 go (AppTy t1 t2) = AppTy (go t1) (go t2)
291 go (FunTy t1 t2) = FunTy (go t1) (go t2)
292 go (ForAllTy tv t) = ForAllTy tv (go t)
293 go (PredTy p) = PredTy (go_pred p)
295 go_pred (ClassP c ts) = ClassP c (map go ts)
296 go_pred (IParam ip t) = IParam ip (go t)
297 go_pred (EqPred t1 t2) = EqPred (go t1) (go t2)
301 %************************************************************************
303 \subsection{Constructor-specific functions}
305 %************************************************************************
308 ---------------------------------------------------------------------
312 -- | Attempts to obtain the type variable underlying a 'Type', and panics with the
313 -- given message if this is not a type variable type. See also 'getTyVar_maybe'
314 getTyVar :: String -> Type -> TyVar
315 getTyVar msg ty = case getTyVar_maybe ty of
317 Nothing -> panic ("getTyVar: " ++ msg)
319 isTyVarTy :: Type -> Bool
320 isTyVarTy ty = isJust (getTyVar_maybe ty)
322 -- | Attempts to obtain the type variable underlying a 'Type'
323 getTyVar_maybe :: Type -> Maybe TyVar
324 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
325 getTyVar_maybe (TyVarTy tv) = Just tv
326 getTyVar_maybe _ = Nothing
331 ---------------------------------------------------------------------
334 We need to be pretty careful with AppTy to make sure we obey the
335 invariant that a TyConApp is always visibly so. mkAppTy maintains the
339 -- | Applies a type to another, as in e.g. @k a@
340 mkAppTy :: Type -> Type -> Type
341 mkAppTy orig_ty1 orig_ty2
344 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
345 mk_app _ = AppTy orig_ty1 orig_ty2
346 -- Note that the TyConApp could be an
347 -- under-saturated type synonym. GHC allows that; e.g.
348 -- type Foo k = k a -> k a
350 -- foo :: Foo Id -> Foo Id
352 -- Here Id is partially applied in the type sig for Foo,
353 -- but once the type synonyms are expanded all is well
355 mkAppTys :: Type -> [Type] -> Type
356 mkAppTys orig_ty1 [] = orig_ty1
357 -- This check for an empty list of type arguments
358 -- avoids the needless loss of a type synonym constructor.
359 -- For example: mkAppTys Rational []
360 -- returns to (Ratio Integer), which has needlessly lost
361 -- the Rational part.
362 mkAppTys orig_ty1 orig_tys2
365 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
366 -- mkTyConApp: see notes with mkAppTy
367 mk_app _ = foldl AppTy orig_ty1 orig_tys2
370 splitAppTy_maybe :: Type -> Maybe (Type, Type)
371 -- ^ Attempt to take a type application apart, whether it is a
372 -- function, type constructor, or plain type application. Note
373 -- that type family applications are NEVER unsaturated by this!
374 splitAppTy_maybe ty | Just ty' <- coreView ty
375 = splitAppTy_maybe ty'
376 splitAppTy_maybe ty = repSplitAppTy_maybe ty
379 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
380 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
381 -- any Core view stuff is already done
382 repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
383 repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
384 repSplitAppTy_maybe (TyConApp tc tys)
385 | isDecomposableTyCon tc || length tys > tyConArity tc
386 = case snocView tys of -- never create unsaturated type family apps
387 Just (tys', ty') -> Just (TyConApp tc tys', ty')
389 repSplitAppTy_maybe _other = Nothing
391 splitAppTy :: Type -> (Type, Type)
392 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
393 -- and panics if this is not possible
394 splitAppTy ty = case splitAppTy_maybe ty of
396 Nothing -> panic "splitAppTy"
399 splitAppTys :: Type -> (Type, [Type])
400 -- ^ Recursively splits a type as far as is possible, leaving a residual
401 -- type being applied to and the type arguments applied to it. Never fails,
402 -- even if that means returning an empty list of type applications.
403 splitAppTys ty = split ty ty []
405 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
406 split _ (AppTy ty arg) args = split ty ty (arg:args)
407 split _ (TyConApp tc tc_args) args
408 = let -- keep type families saturated
409 n | isDecomposableTyCon tc = 0
410 | otherwise = tyConArity tc
411 (tc_args1, tc_args2) = splitAt n tc_args
413 (TyConApp tc tc_args1, tc_args2 ++ args)
414 split _ (FunTy ty1 ty2) args = ASSERT( null args )
415 (TyConApp funTyCon [], [ty1,ty2])
416 split orig_ty _ args = (orig_ty, args)
421 ---------------------------------------------------------------------
426 mkFunTy :: Type -> Type -> Type
427 -- ^ Creates a function type from the given argument and result type
428 mkFunTy arg res = FunTy arg res
430 mkFunTys :: [Type] -> Type -> Type
431 mkFunTys tys ty = foldr mkFunTy ty tys
433 isFunTy :: Type -> Bool
434 isFunTy ty = isJust (splitFunTy_maybe ty)
436 splitFunTy :: Type -> (Type, Type)
437 -- ^ Attempts to extract the argument and result types from a type, and
438 -- panics if that is not possible. See also 'splitFunTy_maybe'
439 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
440 splitFunTy (FunTy arg res) = (arg, res)
441 splitFunTy other = pprPanic "splitFunTy" (ppr other)
443 splitFunTy_maybe :: Type -> Maybe (Type, Type)
444 -- ^ Attempts to extract the argument and result types from a type
445 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
446 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
447 splitFunTy_maybe _ = Nothing
449 splitFunTys :: Type -> ([Type], Type)
450 splitFunTys ty = split [] ty ty
452 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
453 split args _ (FunTy arg res) = split (arg:args) res res
454 split args orig_ty _ = (reverse args, orig_ty)
456 splitFunTysN :: Int -> Type -> ([Type], Type)
457 -- ^ Split off exactly the given number argument types, and panics if that is not possible
458 splitFunTysN 0 ty = ([], ty)
459 splitFunTysN n ty = ASSERT2( isFunTy ty, int n <+> ppr ty )
460 case splitFunTy ty of { (arg, res) ->
461 case splitFunTysN (n-1) res of { (args, res) ->
464 -- | Splits off argument types from the given type and associating
465 -- them with the things in the input list from left to right. The
466 -- final result type is returned, along with the resulting pairs of
467 -- objects and types, albeit with the list of pairs in reverse order.
468 -- Panics if there are not enough argument types for the input list.
469 zipFunTys :: Outputable a => [a] -> Type -> ([(a, Type)], Type)
470 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
472 split acc [] nty _ = (reverse acc, nty)
474 | Just ty' <- coreView ty = split acc xs nty ty'
475 split acc (x:xs) _ (FunTy arg res) = split ((x,arg):acc) xs res res
476 split _ _ _ _ = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
478 funResultTy :: Type -> Type
479 -- ^ Extract the function result type and panic if that is not possible
480 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
481 funResultTy (FunTy _arg res) = res
482 funResultTy ty = pprPanic "funResultTy" (ppr ty)
484 funArgTy :: Type -> Type
485 -- ^ Extract the function argument type and panic if that is not possible
486 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
487 funArgTy (FunTy arg _res) = arg
488 funArgTy ty = pprPanic "funArgTy" (ppr ty)
491 ---------------------------------------------------------------------
496 -- splitTyConApp "looks through" synonyms, because they don't
497 -- mean a distinct type, but all other type-constructor applications
498 -- including functions are returned as Just ..
500 -- | The same as @fst . splitTyConApp@
501 tyConAppTyCon :: Type -> TyCon
502 tyConAppTyCon ty = fst (splitTyConApp ty)
504 -- | The same as @snd . splitTyConApp@
505 tyConAppArgs :: Type -> [Type]
506 tyConAppArgs ty = snd (splitTyConApp ty)
508 -- | Attempts to tease a type apart into a type constructor and the application
509 -- of a number of arguments to that constructor. Panics if that is not possible.
510 -- See also 'splitTyConApp_maybe'
511 splitTyConApp :: Type -> (TyCon, [Type])
512 splitTyConApp ty = case splitTyConApp_maybe ty of
514 Nothing -> pprPanic "splitTyConApp" (ppr ty)
516 -- | Attempts to tease a type apart into a type constructor and the application
517 -- of a number of arguments to that constructor
518 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
519 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
520 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
521 splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
522 splitTyConApp_maybe _ = Nothing
524 newTyConInstRhs :: TyCon -> [Type] -> Type
525 -- ^ Unwrap one 'layer' of newtype on a type constructor and its arguments, using an
526 -- eta-reduced version of the @newtype@ if possible
527 newTyConInstRhs tycon tys
528 = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs )
529 mkAppTys (substTyWith tvs tys1 ty) tys2
531 (tvs, ty) = newTyConEtadRhs tycon
532 (tys1, tys2) = splitAtList tvs tys
536 ---------------------------------------------------------------------
540 Notes on type synonyms
541 ~~~~~~~~~~~~~~~~~~~~~~
542 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
543 to return type synonyms whereever possible. Thus
548 splitFunTys (a -> Foo a) = ([a], Foo a)
551 The reason is that we then get better (shorter) type signatures in
552 interfaces. Notably this plays a role in tcTySigs in TcBinds.lhs.
555 Note [Expanding newtypes]
556 ~~~~~~~~~~~~~~~~~~~~~~~~~
557 When expanding a type to expose a data-type constructor, we need to be
558 careful about newtypes, lest we fall into an infinite loop. Here are
561 newtype Id x = MkId x
562 newtype Fix f = MkFix (f (Fix f))
563 newtype T = MkT (T -> T)
566 --------------------------
568 Fix Maybe Maybe (Fix Maybe)
572 Notice that we can expand T, even though it's recursive.
573 And we can expand Id (Id Int), even though the Id shows up
574 twice at the outer level.
576 So, when expanding, we keep track of when we've seen a recursive
577 newtype at outermost level; and bale out if we see it again.
589 -- 4. All newtypes, including recursive ones, but not newtype families
591 -- It's useful in the back end of the compiler.
592 repType :: Type -> Type
593 -- Only applied to types of kind *; hence tycons are saturated
597 go :: [TyCon] -> Type -> Type
598 go rec_nts (ForAllTy _ ty) -- Look through foralls
601 go rec_nts (PredTy p) -- Expand predicates
602 = go rec_nts (predTypeRep p)
604 go rec_nts (TyConApp tc tys) -- Expand newtypes and synonyms
605 | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
606 = go rec_nts (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
608 | Just (rec_nts', ty') <- carefullySplitNewType_maybe rec_nts tc tys
614 carefullySplitNewType_maybe :: [TyCon] -> TyCon -> [Type] -> Maybe ([TyCon],Type)
615 -- Return the representation of a newtype, unless
616 -- we've seen it already: see Note [Expanding newtypes]
617 carefullySplitNewType_maybe rec_nts tc tys
619 , not (tc `elem` rec_nts) = Just (rec_nts', newTyConInstRhs tc tys)
620 | otherwise = Nothing
622 rec_nts' | isRecursiveTyCon tc = tc:rec_nts
623 | otherwise = rec_nts
626 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
627 -- of inspecting the type directly.
629 -- | Discovers the primitive representation of a more abstract 'Type'
630 typePrimRep :: Type -> PrimRep
631 typePrimRep ty = case repType ty of
632 TyConApp tc _ -> tyConPrimRep tc
634 AppTy _ _ -> PtrRep -- See note below
636 _ -> pprPanic "typePrimRep" (ppr ty)
637 -- Types of the form 'f a' must be of kind *, not *#, so
638 -- we are guaranteed that they are represented by pointers.
639 -- The reason is that f must have kind *->*, not *->*#, because
640 -- (we claim) there is no way to constrain f's kind any other
645 ---------------------------------------------------------------------
650 mkForAllTy :: TyVar -> Type -> Type
654 -- | Wraps foralls over the type using the provided 'TyVar's from left to right
655 mkForAllTys :: [TyVar] -> Type -> Type
656 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
658 isForAllTy :: Type -> Bool
659 isForAllTy (ForAllTy _ _) = True
662 -- | Attempts to take a forall type apart, returning the bound type variable
663 -- and the remainder of the type
664 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
665 splitForAllTy_maybe ty = splitFAT_m ty
667 splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
668 splitFAT_m (ForAllTy tyvar ty) = Just(tyvar, ty)
669 splitFAT_m _ = Nothing
671 -- | Attempts to take a forall type apart, returning all the immediate such bound
672 -- type variables and the remainder of the type. Always suceeds, even if that means
673 -- returning an empty list of 'TyVar's
674 splitForAllTys :: Type -> ([TyVar], Type)
675 splitForAllTys ty = split ty ty []
677 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
678 split _ (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
679 split orig_ty _ tvs = (reverse tvs, orig_ty)
681 -- | Equivalent to @snd . splitForAllTys@
682 dropForAlls :: Type -> Type
683 dropForAlls ty = snd (splitForAllTys ty)
686 -- (mkPiType now in CoreUtils)
692 -- | Instantiate a forall type with one or more type arguments.
693 -- Used when we have a polymorphic function applied to type args:
697 -- We use @applyTys type-of-f [t1,t2]@ to compute the type of the expression.
698 -- Panics if no application is possible.
699 applyTy :: Type -> Type -> Type
700 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
701 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
702 applyTy _ _ = panic "applyTy"
704 applyTys :: Type -> [Type] -> Type
705 -- ^ This function is interesting because:
707 -- 1. The function may have more for-alls than there are args
709 -- 2. Less obviously, it may have fewer for-alls
711 -- For case 2. think of:
713 -- > applyTys (forall a.a) [forall b.b, Int]
715 -- This really can happen, via dressing up polymorphic types with newtype
716 -- clothing. Here's an example:
718 -- > newtype R = R (forall a. a->a)
719 -- > foo = case undefined :: R of
722 applyTys ty args = applyTysD empty ty args
724 applyTysD :: SDoc -> Type -> [Type] -> Type -- Debug version
725 applyTysD _ orig_fun_ty [] = orig_fun_ty
726 applyTysD doc orig_fun_ty arg_tys
727 | n_tvs == n_args -- The vastly common case
728 = substTyWith tvs arg_tys rho_ty
729 | n_tvs > n_args -- Too many for-alls
730 = substTyWith (take n_args tvs) arg_tys
731 (mkForAllTys (drop n_args tvs) rho_ty)
732 | otherwise -- Too many type args
733 = ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty ) -- Zero case gives infnite loop!
734 applyTysD doc (substTyWith tvs (take n_tvs arg_tys) rho_ty)
737 (tvs, rho_ty) = splitForAllTys orig_fun_ty
739 n_args = length arg_tys
743 %************************************************************************
747 %************************************************************************
749 Polymorphic functions over Pred
752 allPred :: (a -> Bool) -> Pred a -> Bool
753 allPred p (ClassP _ ts) = all p ts
754 allPred p (IParam _ t) = p t
755 allPred p (EqPred t1 t2) = p t1 && p t2
757 isClassPred :: Pred a -> Bool
758 isClassPred (ClassP {}) = True
759 isClassPred _ = False
761 isEqPred :: Pred a -> Bool
762 isEqPred (EqPred {}) = True
765 isIPPred :: Pred a -> Bool
766 isIPPred (IParam {}) = True
773 mkPredTy :: PredType -> Type
774 mkPredTy pred = PredTy pred
776 mkPredTys :: ThetaType -> [Type]
777 mkPredTys preds = map PredTy preds
779 predTypeRep :: PredType -> Type
780 -- ^ Convert a 'PredType' to its representation type. However, it unwraps
781 -- only the outermost level; for example, the result might be a newtype application
782 predTypeRep (IParam _ ty) = ty
783 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
784 predTypeRep (EqPred ty1 ty2) = mkTyConApp eqPredPrimTyCon [ty1,ty2]
786 splitPredTy_maybe :: Type -> Maybe PredType
787 -- Returns Just for predicates only
788 splitPredTy_maybe ty | Just ty' <- tcView ty = splitPredTy_maybe ty'
789 splitPredTy_maybe (PredTy p) = Just p
790 splitPredTy_maybe _ = Nothing
792 isPredTy :: Type -> Bool
793 isPredTy ty = isJust (splitPredTy_maybe ty)
796 --------------------- Equality types ---------------------------------
798 isReflPredTy :: Type -> Bool
799 isReflPredTy ty = case splitPredTy_maybe ty of
800 Just (EqPred ty1 ty2) -> ty1 `eqType` ty2
803 splitEqPredTy_maybe :: Type -> Maybe (Type,Type)
804 splitEqPredTy_maybe ty = case splitPredTy_maybe ty of
805 Just (EqPred ty1 ty2) -> Just (ty1,ty2)
808 isEqPredTy :: Type -> Bool
809 isEqPredTy ty = case splitPredTy_maybe ty of
810 Just (EqPred {}) -> True
813 -- | Creates a type equality predicate
814 mkEqPred :: (a, a) -> Pred a
815 mkEqPred (ty1, ty2) = EqPred ty1 ty2
818 --------------------- Dictionary types ---------------------------------
820 mkClassPred :: Class -> [Type] -> PredType
821 mkClassPred clas tys = ClassP clas tys
823 isDictTy :: Type -> Bool
824 isDictTy ty = case splitPredTy_maybe ty of
825 Just p -> isClassPred p
828 isTyVarClassPred :: PredType -> Bool
829 isTyVarClassPred (ClassP _ tys) = all isTyVarTy tys
830 isTyVarClassPred _ = False
832 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
833 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
834 getClassPredTys_maybe _ = Nothing
836 getClassPredTys :: PredType -> (Class, [Type])
837 getClassPredTys (ClassP clas tys) = (clas, tys)
838 getClassPredTys _ = panic "getClassPredTys"
840 mkDictTy :: Class -> [Type] -> Type
841 mkDictTy clas tys = mkPredTy (ClassP clas tys)
843 isDictLikeTy :: Type -> Bool
844 -- Note [Dictionary-like types]
845 isDictLikeTy ty | Just ty' <- tcView ty = isDictTy ty'
846 isDictLikeTy (PredTy p) = isClassPred p
847 isDictLikeTy (TyConApp tc tys)
848 | isTupleTyCon tc = all isDictLikeTy tys
849 isDictLikeTy _ = False
852 Note [Dictionary-like types]
853 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
854 Being "dictionary-like" means either a dictionary type or a tuple thereof.
855 In GHC 6.10 we build implication constraints which construct such tuples,
856 and if we land up with a binding
859 then we want to treat t as cheap under "-fdicts-cheap" for example.
860 (Implication constraints are normally inlined, but sadly not if the
861 occurrence is itself inside an INLINE function! Until we revise the
862 handling of implication constraints, that is.) This turned out to
863 be important in getting good arities in DPH code. Example:
866 class D a where { foo :: a -> a }
867 instance C a => D (Maybe a) where { foo x = x }
869 bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
871 bar x y = (foo (Just x), foo (Just y))
873 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
874 we ended up with something like
875 bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
878 This is all a bit ad-hoc; eg it relies on knowing that implication
879 constraints build tuples.
881 --------------------- Implicit parameters ---------------------------------
884 mkIPPred :: IPName Name -> Type -> PredType
885 mkIPPred ip ty = IParam ip ty
888 %************************************************************************
892 %************************************************************************
895 typeSize :: Type -> Int
896 typeSize (TyVarTy _) = 1
897 typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2
898 typeSize (FunTy t1 t2) = typeSize t1 + typeSize t2
899 typeSize (PredTy p) = predSize typeSize p
900 typeSize (ForAllTy _ t) = 1 + typeSize t
901 typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
905 %************************************************************************
907 \subsection{Type families}
909 %************************************************************************
912 -- | Finds type family instances occuring in a type after expanding synonyms.
913 tyFamInsts :: Type -> [(TyCon, [Type])]
915 | Just exp_ty <- tcView ty = tyFamInsts exp_ty
916 tyFamInsts (TyVarTy _) = []
917 tyFamInsts (TyConApp tc tys)
918 | isSynFamilyTyCon tc = [(tc, tys)]
919 | otherwise = concat (map tyFamInsts tys)
920 tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
921 tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
922 tyFamInsts (ForAllTy _ ty) = tyFamInsts ty
923 tyFamInsts (PredTy pty) = predFamInsts pty
925 -- | Finds type family instances occuring in a predicate type after expanding
927 predFamInsts :: PredType -> [(TyCon, [Type])]
928 predFamInsts (ClassP _cla tys) = concat (map tyFamInsts tys)
929 predFamInsts (IParam _ ty) = tyFamInsts ty
930 predFamInsts (EqPred ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
932 mkFamilyTyConApp :: TyCon -> [Type] -> Type
933 -- ^ Given a family instance TyCon and its arg types, return the
934 -- corresponding family type. E.g:
937 -- > data instance T (Maybe b) = MkT b
939 -- Where the instance tycon is :RTL, so:
941 -- > mkFamilyTyConApp :RTL Int = T (Maybe Int)
942 mkFamilyTyConApp tc tys
943 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
944 , let fam_subst = zipTopTvSubst (tyConTyVars tc) tys
945 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
949 -- | Pretty prints a 'TyCon', using the family instance in case of a
950 -- representation tycon. For example:
952 -- > data T [a] = ...
954 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
955 pprSourceTyCon :: TyCon -> SDoc
957 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
958 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
963 %************************************************************************
965 \subsection{Liftedness}
967 %************************************************************************
970 -- | See "Type#type_classification" for what an unlifted type is
971 isUnLiftedType :: Type -> Bool
972 -- isUnLiftedType returns True for forall'd unlifted types:
973 -- x :: forall a. Int#
974 -- I found bindings like these were getting floated to the top level.
975 -- They are pretty bogus types, mind you. It would be better never to
978 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
979 isUnLiftedType (ForAllTy _ ty) = isUnLiftedType ty
980 isUnLiftedType (PredTy p) = isEqPred p
981 isUnLiftedType (TyConApp tc _) = isUnLiftedTyCon tc
982 isUnLiftedType _ = False
984 isUnboxedTupleType :: Type -> Bool
985 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
986 Just (tc, _ty_args) -> isUnboxedTupleTyCon tc
989 -- | See "Type#type_classification" for what an algebraic type is.
990 -- Should only be applied to /types/, as opposed to e.g. partially
991 -- saturated type constructors
992 isAlgType :: Type -> Bool
994 = case splitTyConApp_maybe ty of
995 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
999 -- | See "Type#type_classification" for what an algebraic type is.
1000 -- Should only be applied to /types/, as opposed to e.g. partially
1001 -- saturated type constructors. Closed type constructors are those
1002 -- with a fixed right hand side, as opposed to e.g. associated types
1003 isClosedAlgType :: Type -> Bool
1005 = case splitTyConApp_maybe ty of
1006 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1007 isAlgTyCon tc && not (isFamilyTyCon tc)
1012 -- | Computes whether an argument (or let right hand side) should
1013 -- be computed strictly or lazily, based only on its type.
1014 -- Works just like 'isUnLiftedType', except that it has a special case
1015 -- for dictionaries (i.e. does not work purely on representation types)
1017 -- Since it takes account of class 'PredType's, you might think
1018 -- this function should be in 'TcType', but 'isStrictType' is used by 'DataCon',
1019 -- which is below 'TcType' in the hierarchy, so it's convenient to put it here.
1020 isStrictType :: Type -> Bool
1021 isStrictType (PredTy pred) = isStrictPred pred
1022 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
1023 isStrictType (ForAllTy _ ty) = isStrictType ty
1024 isStrictType (TyConApp tc _) = isUnLiftedTyCon tc
1025 isStrictType _ = False
1027 -- | We may be strict in dictionary types, but only if it
1028 -- has more than one component.
1030 -- (Being strict in a single-component dictionary risks
1031 -- poking the dictionary component, which is wrong.)
1032 isStrictPred :: PredType -> Bool
1033 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
1034 isStrictPred (EqPred {}) = True
1035 isStrictPred (IParam {}) = False
1039 isPrimitiveType :: Type -> Bool
1040 -- ^ Returns true of types that are opaque to Haskell.
1041 -- Most of these are unlifted, but now that we interact with .NET, we
1042 -- may have primtive (foreign-imported) types that are lifted
1043 isPrimitiveType ty = case splitTyConApp_maybe ty of
1044 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1050 %************************************************************************
1052 The "exact" free variables of a type
1054 %************************************************************************
1056 Note [Silly type synonym]
1057 ~~~~~~~~~~~~~~~~~~~~~~~~~
1060 What are the free tyvars of (T x)? Empty, of course!
1061 Here's the example that Ralf Laemmel showed me:
1062 foo :: (forall a. C u a -> C u a) -> u
1063 mappend :: Monoid u => u -> u -> u
1065 bar :: Monoid u => u
1066 bar = foo (\t -> t `mappend` t)
1067 We have to generalise at the arg to f, and we don't
1068 want to capture the constraint (Monad (C u a)) because
1069 it appears to mention a. Pretty silly, but it was useful to him.
1071 exactTyVarsOfType is used by the type checker to figure out exactly
1072 which type variables are mentioned in a type. It's also used in the
1073 smart-app checking code --- see TcExpr.tcIdApp
1075 On the other hand, consider a *top-level* definition
1076 f = (\x -> x) :: T a -> T a
1077 If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
1078 if we have an application like (f "x") we get a confusing error message
1079 involving Any. So the conclusion is this: when generalising
1080 - at top level use tyVarsOfType
1081 - in nested bindings use exactTyVarsOfType
1082 See Trac #1813 for example.
1085 exactTyVarsOfType :: Type -> TyVarSet
1086 -- Find the free type variables (of any kind)
1087 -- but *expand* type synonyms. See Note [Silly type synonym] above.
1088 exactTyVarsOfType ty
1091 go ty | Just ty' <- tcView ty = go ty' -- This is the key line
1092 go (TyVarTy tv) = unitVarSet tv
1093 go (TyConApp _ tys) = exactTyVarsOfTypes tys
1094 go (PredTy ty) = go_pred ty
1095 go (FunTy arg res) = go arg `unionVarSet` go res
1096 go (AppTy fun arg) = go fun `unionVarSet` go arg
1097 go (ForAllTy tyvar ty) = delVarSet (go ty) tyvar
1099 go_pred (IParam _ ty) = go ty
1100 go_pred (ClassP _ tys) = exactTyVarsOfTypes tys
1101 go_pred (EqPred ty1 ty2) = go ty1 `unionVarSet` go ty2
1103 exactTyVarsOfTypes :: [Type] -> TyVarSet
1104 exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
1108 %************************************************************************
1110 \subsection{Sequencing on types}
1112 %************************************************************************
1115 seqType :: Type -> ()
1116 seqType (TyVarTy tv) = tv `seq` ()
1117 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
1118 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
1119 seqType (PredTy p) = seqPred seqType p
1120 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
1121 seqType (ForAllTy tv ty) = tv `seq` seqType ty
1123 seqTypes :: [Type] -> ()
1125 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
1127 seqPred :: (a -> ()) -> Pred a -> ()
1128 seqPred seqt (ClassP c tys) = c `seq` foldr (seq . seqt) () tys
1129 seqPred seqt (IParam n ty) = n `seq` seqt ty
1130 seqPred seqt (EqPred ty1 ty2) = seqt ty1 `seq` seqt ty2
1134 %************************************************************************
1136 Comparision for types
1137 (We don't use instances so that we know where it happens)
1139 %************************************************************************
1142 eqKind :: Kind -> Kind -> Bool
1145 eqType :: Type -> Type -> Bool
1146 -- ^ Type equality on source types. Does not look through @newtypes@ or
1147 -- 'PredType's, but it does look through type synonyms.
1148 eqType t1 t2 = isEqual $ cmpType t1 t2
1150 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
1151 eqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
1153 eqTypes :: [Type] -> [Type] -> Bool
1154 eqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
1156 eqPred :: PredType -> PredType -> Bool
1157 eqPred p1 p2 = isEqual $ cmpPred p1 p2
1159 eqPredX :: RnEnv2 -> PredType -> PredType -> Bool
1160 eqPredX env p1 p2 = isEqual $ cmpPredX env p1 p2
1163 Now here comes the real worker
1166 cmpType :: Type -> Type -> Ordering
1167 cmpType t1 t2 = cmpTypeX rn_env t1 t2
1169 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
1171 cmpTypes :: [Type] -> [Type] -> Ordering
1172 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
1174 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
1176 cmpPred :: PredType -> PredType -> Ordering
1177 cmpPred p1 p2 = cmpPredX rn_env p1 p2
1179 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
1181 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
1182 cmpTypeX env t1 t2 | Just t1' <- coreView t1 = cmpTypeX env t1' t2
1183 | Just t2' <- coreView t2 = cmpTypeX env t1 t2'
1184 -- We expand predicate types, because in Core-land we have
1185 -- lots of definitions like
1186 -- fOrdBool :: Ord Bool
1187 -- fOrdBool = D:Ord .. .. ..
1188 -- So the RHS has a data type
1190 cmpTypeX env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 `compare` rnOccR env tv2
1191 cmpTypeX env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
1192 cmpTypeX env (AppTy s1 t1) (AppTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1193 cmpTypeX env (FunTy s1 t1) (FunTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1194 cmpTypeX env (PredTy p1) (PredTy p2) = cmpPredX env p1 p2
1195 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
1197 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
1198 cmpTypeX _ (AppTy _ _) (TyVarTy _) = GT
1200 cmpTypeX _ (FunTy _ _) (TyVarTy _) = GT
1201 cmpTypeX _ (FunTy _ _) (AppTy _ _) = GT
1203 cmpTypeX _ (TyConApp _ _) (TyVarTy _) = GT
1204 cmpTypeX _ (TyConApp _ _) (AppTy _ _) = GT
1205 cmpTypeX _ (TyConApp _ _) (FunTy _ _) = GT
1207 cmpTypeX _ (ForAllTy _ _) (TyVarTy _) = GT
1208 cmpTypeX _ (ForAllTy _ _) (AppTy _ _) = GT
1209 cmpTypeX _ (ForAllTy _ _) (FunTy _ _) = GT
1210 cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = GT
1212 cmpTypeX _ (PredTy _) _ = GT
1217 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1218 cmpTypesX _ [] [] = EQ
1219 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1220 cmpTypesX _ [] _ = LT
1221 cmpTypesX _ _ [] = GT
1224 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1225 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1226 -- Compare names only for implicit parameters
1227 -- This comparison is used exclusively (I believe)
1228 -- for the Avails finite map built in TcSimplify
1229 -- If the types differ we keep them distinct so that we see
1230 -- a distinct pair to run improvement on
1231 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTypesX env tys1 tys2)
1232 cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
1234 -- Constructor order: IParam < ClassP < EqPred
1235 cmpPredX _ (IParam {}) _ = LT
1236 cmpPredX _ (ClassP {}) (IParam {}) = GT
1237 cmpPredX _ (ClassP {}) (EqPred {}) = LT
1238 cmpPredX _ (EqPred {}) _ = GT
1241 PredTypes are used as a FM key in TcSimplify,
1242 so we take the easy path and make them an instance of Ord
1245 instance Eq PredType where { (==) = eqPred }
1246 instance Ord PredType where { compare = cmpPred }
1250 %************************************************************************
1254 %************************************************************************
1257 emptyTvSubstEnv :: TvSubstEnv
1258 emptyTvSubstEnv = emptyVarEnv
1260 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1261 -- ^ @(compose env1 env2)(x)@ is @env1(env2(x))@; i.e. apply @env2@ then @env1@.
1262 -- It assumes that both are idempotent.
1263 -- Typically, @env1@ is the refinement to a base substitution @env2@
1264 composeTvSubst in_scope env1 env2
1265 = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1266 -- First apply env1 to the range of env2
1267 -- Then combine the two, making sure that env1 loses if
1268 -- both bind the same variable; that's why env1 is the
1269 -- *left* argument to plusVarEnv, because the right arg wins
1271 subst1 = TvSubst in_scope env1
1273 emptyTvSubst :: TvSubst
1274 emptyTvSubst = TvSubst emptyInScopeSet emptyTvSubstEnv
1276 isEmptyTvSubst :: TvSubst -> Bool
1277 -- See Note [Extending the TvSubstEnv]
1278 isEmptyTvSubst (TvSubst _ tenv) = isEmptyVarEnv tenv
1280 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1283 getTvSubstEnv :: TvSubst -> TvSubstEnv
1284 getTvSubstEnv (TvSubst _ env) = env
1286 getTvInScope :: TvSubst -> InScopeSet
1287 getTvInScope (TvSubst in_scope _) = in_scope
1289 isInScope :: Var -> TvSubst -> Bool
1290 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1292 notElemTvSubst :: TyCoVar -> TvSubst -> Bool
1293 notElemTvSubst v (TvSubst _ tenv) = not (v `elemVarEnv` tenv)
1295 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1296 setTvSubstEnv (TvSubst in_scope _) tenv = TvSubst in_scope tenv
1298 zapTvSubstEnv :: TvSubst -> TvSubst
1299 zapTvSubstEnv (TvSubst in_scope _) = TvSubst in_scope emptyVarEnv
1301 extendTvInScope :: TvSubst -> Var -> TvSubst
1302 extendTvInScope (TvSubst in_scope tenv) var = TvSubst (extendInScopeSet in_scope var) tenv
1304 extendTvInScopeList :: TvSubst -> [Var] -> TvSubst
1305 extendTvInScopeList (TvSubst in_scope tenv) vars = TvSubst (extendInScopeSetList in_scope vars) tenv
1307 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1308 extendTvSubst (TvSubst in_scope tenv) tv ty = TvSubst in_scope (extendVarEnv tenv tv ty)
1310 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1311 extendTvSubstList (TvSubst in_scope tenv) tvs tys
1312 = TvSubst in_scope (extendVarEnvList tenv (tvs `zip` tys))
1314 unionTvSubst :: TvSubst -> TvSubst -> TvSubst
1315 -- Works when the ranges are disjoint
1316 unionTvSubst (TvSubst in_scope1 tenv1) (TvSubst in_scope2 tenv2)
1317 = ASSERT( not (tenv1 `intersectsVarEnv` tenv2) )
1318 TvSubst (in_scope1 `unionInScope` in_scope2)
1319 (tenv1 `plusVarEnv` tenv2)
1321 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1322 -- the types given; but it's just a thunk so with a bit of luck
1323 -- it'll never be evaluated
1325 -- Note [Generating the in-scope set for a substitution]
1326 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1327 -- If we want to substitute [a -> ty1, b -> ty2] I used to
1328 -- think it was enough to generate an in-scope set that includes
1329 -- fv(ty1,ty2). But that's not enough; we really should also take the
1330 -- free vars of the type we are substituting into! Example:
1331 -- (forall b. (a,b,x)) [a -> List b]
1332 -- Then if we use the in-scope set {b}, there is a danger we will rename
1333 -- the forall'd variable to 'x' by mistake, getting this:
1334 -- (forall x. (List b, x, x)
1335 -- Urk! This means looking at all the calls to mkOpenTvSubst....
1338 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1339 -- environment, hence "open"
1340 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1341 mkOpenTvSubst tenv = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts tenv))) tenv
1343 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1344 -- environment, hence "open"
1345 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1346 zipOpenTvSubst tyvars tys
1347 | debugIsOn && (length tyvars /= length tys)
1348 = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1350 = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1352 -- | Called when doing top-level substitutions. Here we expect that the
1353 -- free vars of the range of the substitution will be empty.
1354 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1355 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1357 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1358 zipTopTvSubst tyvars tys
1359 | debugIsOn && (length tyvars /= length tys)
1360 = pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1362 = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1364 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1366 | debugIsOn && (length tyvars /= length tys)
1367 = pprTrace "zipTyEnv" (ppr tyvars $$ ppr tys) emptyVarEnv
1369 = zip_ty_env tyvars tys emptyVarEnv
1371 -- Later substitutions in the list over-ride earlier ones,
1372 -- but there should be no loops
1373 zip_ty_env :: [TyVar] -> [Type] -> TvSubstEnv -> TvSubstEnv
1374 zip_ty_env [] [] env = env
1375 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1376 -- There used to be a special case for when
1378 -- (a not-uncommon case) in which case the substitution was dropped.
1379 -- But the type-tidier changes the print-name of a type variable without
1380 -- changing the unique, and that led to a bug. Why? Pre-tidying, we had
1381 -- a type {Foo t}, where Foo is a one-method class. So Foo is really a newtype.
1382 -- And it happened that t was the type variable of the class. Post-tiding,
1383 -- it got turned into {Foo t2}. The ext-core printer expanded this using
1384 -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1385 -- and so generated a rep type mentioning t not t2.
1387 -- Simplest fix is to nuke the "optimisation"
1388 zip_ty_env tvs tys env = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1389 -- zip_ty_env _ _ env = env
1391 instance Outputable TvSubst where
1392 ppr (TvSubst ins tenv)
1393 = brackets $ sep[ ptext (sLit "TvSubst"),
1394 nest 2 (ptext (sLit "In scope:") <+> ppr ins),
1395 nest 2 (ptext (sLit "Type env:") <+> ppr tenv) ]
1398 %************************************************************************
1400 Performing type substitutions
1402 %************************************************************************
1405 -- | Type substitution making use of an 'TvSubst' that
1406 -- is assumed to be open, see 'zipOpenTvSubst'
1407 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1408 substTyWith tvs tys = ASSERT( length tvs == length tys )
1409 substTy (zipOpenTvSubst tvs tys)
1411 -- | Type substitution making use of an 'TvSubst' that
1412 -- is assumed to be open, see 'zipOpenTvSubst'
1413 substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
1414 substTysWith tvs tys = ASSERT( length tvs == length tys )
1415 substTys (zipOpenTvSubst tvs tys)
1417 -- | Substitute within a 'Type'
1418 substTy :: TvSubst -> Type -> Type
1419 substTy subst ty | isEmptyTvSubst subst = ty
1420 | otherwise = subst_ty subst ty
1422 -- | Substitute within several 'Type's
1423 substTys :: TvSubst -> [Type] -> [Type]
1424 substTys subst tys | isEmptyTvSubst subst = tys
1425 | otherwise = map (subst_ty subst) tys
1427 -- | Substitute within a 'ThetaType'
1428 substTheta :: TvSubst -> ThetaType -> ThetaType
1429 substTheta subst theta
1430 | isEmptyTvSubst subst = theta
1431 | otherwise = map (substPred subst) theta
1433 -- | Substitute within a 'PredType'
1434 substPred :: TvSubst -> PredType -> PredType
1435 substPred subst (IParam n ty) = IParam n (subst_ty subst ty)
1436 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1437 substPred subst (EqPred ty1 ty2) = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
1439 -- | Remove any nested binders mentioning the 'TyVar's in the 'TyVarSet'
1440 deShadowTy :: TyVarSet -> Type -> Type
1442 = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1444 in_scope = mkInScopeSet tvs
1446 subst_ty :: TvSubst -> Type -> Type
1447 -- subst_ty is the main workhorse for type substitution
1449 -- Note that the in_scope set is poked only if we hit a forall
1450 -- so it may often never be fully computed
1454 go (TyVarTy tv) = substTyVar subst tv
1455 go (TyConApp tc tys) = let args = map go tys
1456 in args `seqList` TyConApp tc args
1458 go (PredTy p) = PredTy $! (substPred subst p)
1460 go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
1461 go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
1462 -- The mkAppTy smart constructor is important
1463 -- we might be replacing (a Int), represented with App
1464 -- by [Int], represented with TyConApp
1465 go (ForAllTy tv ty) = case substTyVarBndr subst tv of
1467 ForAllTy tv' $! (subst_ty subst' ty)
1469 substTyVar :: TvSubst -> TyVar -> Type
1470 substTyVar (TvSubst _ tenv) tv
1471 | Just ty <- lookupVarEnv tenv tv = ty -- See Note [Apply Once]
1472 | otherwise = ASSERT( isTyVar tv ) TyVarTy tv
1473 -- We do not require that the tyvar is in scope
1474 -- Reason: we do quite a bit of (substTyWith [tv] [ty] tau)
1475 -- and it's a nuisance to bring all the free vars of tau into
1476 -- scope --- and then force that thunk at every tyvar
1477 -- Instead we have an ASSERT in substTyVarBndr to check for capture
1479 substTyVars :: TvSubst -> [TyVar] -> [Type]
1480 substTyVars subst tvs = map (substTyVar subst) tvs
1482 lookupTyVar :: TvSubst -> TyVar -> Maybe Type
1483 -- See Note [Extending the TvSubst]
1484 lookupTyVar (TvSubst _ tenv) tv = lookupVarEnv tenv tv
1486 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1487 substTyVarBndr subst@(TvSubst in_scope tenv) old_var
1488 = ASSERT2( _no_capture, ppr old_var $$ ppr subst )
1489 (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1491 new_env | no_change = delVarEnv tenv old_var
1492 | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
1494 _no_capture = not (new_var `elemVarSet` tyVarsOfTypes (varEnvElts tenv))
1495 -- Check that we are not capturing something in the substitution
1497 no_change = new_var == old_var
1498 -- no_change means that the new_var is identical in
1499 -- all respects to the old_var (same unique, same kind)
1500 -- See Note [Extending the TvSubst]
1502 -- In that case we don't need to extend the substitution
1503 -- to map old to new. But instead we must zap any
1504 -- current substitution for the variable. For example:
1505 -- (\x.e) with id_subst = [x |-> e']
1506 -- Here we must simply zap the substitution for x
1508 new_var = uniqAway in_scope old_var
1509 -- The uniqAway part makes sure the new variable is not already in scope
1512 ----------------------------------------------------
1521 -- There's a little subtyping at the kind level:
1531 -- Where: \* [LiftedTypeKind] means boxed type
1532 -- \# [UnliftedTypeKind] means unboxed type
1533 -- (\#) [UbxTupleKind] means unboxed tuple
1534 -- ?? [ArgTypeKind] is the lub of {\*, \#}
1535 -- ? [OpenTypeKind] means any type at all
1540 -- > error :: forall a:?. String -> a
1541 -- > (->) :: ?? -> ? -> \*
1542 -- > (\\(x::t) -> ...)
1544 -- Where in the last example @t :: ??@ (i.e. is not an unboxed tuple)
1546 type KindVar = TyVar -- invariant: KindVar will always be a
1547 -- TcTyVar with details MetaTv TauTv ...
1548 -- kind var constructors and functions are in TcType
1550 type SimpleKind = Kind
1555 During kind inference, a kind variable unifies only with
1557 sk ::= * | sk1 -> sk2
1559 data T a = MkT a (T Int#)
1560 fails. We give T the kind (k -> *), and the kind variable k won't unify
1561 with # (the kind of Int#).
1565 When creating a fresh internal type variable, we give it a kind to express
1566 constraints on it. E.g. in (\x->e) we make up a fresh type variable for x,
1569 During unification we only bind an internal type variable to a type
1570 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1572 When unifying two internal type variables, we collect their kind constraints by
1573 finding the GLB of the two. Since the partial order is a tree, they only
1574 have a glb if one is a sub-kind of the other. In that case, we bind the
1575 less-informative one to the more informative one. Neat, eh?