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 -- By being non-recursive and inlined, this case analysis gets efficiently
235 -- joined onto the case analysis that the caller is already doing
236 coreView (PredTy p) = Just (predTypeRep p)
237 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
238 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
239 -- Its important to use mkAppTys, rather than (foldl AppTy),
240 -- because the function part might well return a
241 -- partially-applied type constructor; indeed, usually will!
245 -----------------------------------------------
246 {-# INLINE tcView #-}
247 tcView :: Type -> Maybe Type
248 -- ^ Similar to 'coreView', but for the type checker, which just looks through synonyms
249 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
250 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
253 -----------------------------------------------
254 expandTypeSynonyms :: Type -> Type
255 -- ^ Expand out all type synonyms. Actually, it'd suffice to expand out
256 -- just the ones that discard type variables (e.g. type Funny a = Int)
257 -- But we don't know which those are currently, so we just expand all.
258 expandTypeSynonyms ty
262 | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
263 = go (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
265 = TyConApp tc (map go tys)
266 go (TyVarTy tv) = TyVarTy tv
267 go (AppTy t1 t2) = AppTy (go t1) (go t2)
268 go (FunTy t1 t2) = FunTy (go t1) (go t2)
269 go (ForAllTy tv t) = ForAllTy tv (go t)
270 go (PredTy p) = PredTy (go_pred p)
272 go_pred (ClassP c ts) = ClassP c (map go ts)
273 go_pred (IParam ip t) = IParam ip (go t)
274 go_pred (EqPred t1 t2) = EqPred (go t1) (go t2)
278 %************************************************************************
280 \subsection{Constructor-specific functions}
282 %************************************************************************
285 ---------------------------------------------------------------------
289 -- | Attempts to obtain the type variable underlying a 'Type', and panics with the
290 -- given message if this is not a type variable type. See also 'getTyVar_maybe'
291 getTyVar :: String -> Type -> TyVar
292 getTyVar msg ty = case getTyVar_maybe ty of
294 Nothing -> panic ("getTyVar: " ++ msg)
296 isTyVarTy :: Type -> Bool
297 isTyVarTy ty = isJust (getTyVar_maybe ty)
299 -- | Attempts to obtain the type variable underlying a 'Type'
300 getTyVar_maybe :: Type -> Maybe TyVar
301 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
302 getTyVar_maybe (TyVarTy tv) = Just tv
303 getTyVar_maybe _ = Nothing
308 ---------------------------------------------------------------------
311 We need to be pretty careful with AppTy to make sure we obey the
312 invariant that a TyConApp is always visibly so. mkAppTy maintains the
316 -- | Applies a type to another, as in e.g. @k a@
317 mkAppTy :: Type -> Type -> Type
318 mkAppTy orig_ty1 orig_ty2
321 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
322 mk_app _ = AppTy orig_ty1 orig_ty2
323 -- Note that the TyConApp could be an
324 -- under-saturated type synonym. GHC allows that; e.g.
325 -- type Foo k = k a -> k a
327 -- foo :: Foo Id -> Foo Id
329 -- Here Id is partially applied in the type sig for Foo,
330 -- but once the type synonyms are expanded all is well
332 mkAppTys :: Type -> [Type] -> Type
333 mkAppTys orig_ty1 [] = orig_ty1
334 -- This check for an empty list of type arguments
335 -- avoids the needless loss of a type synonym constructor.
336 -- For example: mkAppTys Rational []
337 -- returns to (Ratio Integer), which has needlessly lost
338 -- the Rational part.
339 mkAppTys orig_ty1 orig_tys2
342 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
343 -- mkTyConApp: see notes with mkAppTy
344 mk_app _ = foldl AppTy orig_ty1 orig_tys2
347 splitAppTy_maybe :: Type -> Maybe (Type, Type)
348 -- ^ Attempt to take a type application apart, whether it is a
349 -- function, type constructor, or plain type application. Note
350 -- that type family applications are NEVER unsaturated by this!
351 splitAppTy_maybe ty | Just ty' <- coreView ty
352 = splitAppTy_maybe ty'
353 splitAppTy_maybe ty = repSplitAppTy_maybe ty
356 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
357 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
358 -- any Core view stuff is already done
359 repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
360 repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
361 repSplitAppTy_maybe (TyConApp tc tys)
362 | isDecomposableTyCon tc || tys `lengthExceeds` tyConArity tc
363 , Just (tys', ty') <- snocView tys
364 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
365 repSplitAppTy_maybe _other = Nothing
367 splitAppTy :: Type -> (Type, Type)
368 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
369 -- and panics if this is not possible
370 splitAppTy ty = case splitAppTy_maybe ty of
372 Nothing -> panic "splitAppTy"
375 splitAppTys :: Type -> (Type, [Type])
376 -- ^ Recursively splits a type as far as is possible, leaving a residual
377 -- type being applied to and the type arguments applied to it. Never fails,
378 -- even if that means returning an empty list of type applications.
379 splitAppTys ty = split ty ty []
381 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
382 split _ (AppTy ty arg) args = split ty ty (arg:args)
383 split _ (TyConApp tc tc_args) args
384 = let -- keep type families saturated
385 n | isDecomposableTyCon tc = 0
386 | otherwise = tyConArity tc
387 (tc_args1, tc_args2) = splitAt n tc_args
389 (TyConApp tc tc_args1, tc_args2 ++ args)
390 split _ (FunTy ty1 ty2) args = ASSERT( null args )
391 (TyConApp funTyCon [], [ty1,ty2])
392 split orig_ty _ args = (orig_ty, args)
397 ---------------------------------------------------------------------
402 mkFunTy :: Type -> Type -> Type
403 -- ^ Creates a function type from the given argument and result type
404 mkFunTy arg res = FunTy arg res
406 mkFunTys :: [Type] -> Type -> Type
407 mkFunTys tys ty = foldr mkFunTy ty tys
409 isFunTy :: Type -> Bool
410 isFunTy ty = isJust (splitFunTy_maybe ty)
412 splitFunTy :: Type -> (Type, Type)
413 -- ^ Attempts to extract the argument and result types from a type, and
414 -- panics if that is not possible. See also 'splitFunTy_maybe'
415 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
416 splitFunTy (FunTy arg res) = (arg, res)
417 splitFunTy other = pprPanic "splitFunTy" (ppr other)
419 splitFunTy_maybe :: Type -> Maybe (Type, Type)
420 -- ^ Attempts to extract the argument and result types from a type
421 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
422 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
423 splitFunTy_maybe _ = Nothing
425 splitFunTys :: Type -> ([Type], Type)
426 splitFunTys ty = split [] ty ty
428 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
429 split args _ (FunTy arg res) = split (arg:args) res res
430 split args orig_ty _ = (reverse args, orig_ty)
432 splitFunTysN :: Int -> Type -> ([Type], Type)
433 -- ^ Split off exactly the given number argument types, and panics if that is not possible
434 splitFunTysN 0 ty = ([], ty)
435 splitFunTysN n ty = ASSERT2( isFunTy ty, int n <+> ppr ty )
436 case splitFunTy ty of { (arg, res) ->
437 case splitFunTysN (n-1) res of { (args, res) ->
440 -- | Splits off argument types from the given type and associating
441 -- them with the things in the input list from left to right. The
442 -- final result type is returned, along with the resulting pairs of
443 -- objects and types, albeit with the list of pairs in reverse order.
444 -- Panics if there are not enough argument types for the input list.
445 zipFunTys :: Outputable a => [a] -> Type -> ([(a, Type)], Type)
446 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
448 split acc [] nty _ = (reverse acc, nty)
450 | Just ty' <- coreView ty = split acc xs nty ty'
451 split acc (x:xs) _ (FunTy arg res) = split ((x,arg):acc) xs res res
452 split _ _ _ _ = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
454 funResultTy :: Type -> Type
455 -- ^ Extract the function result type and panic if that is not possible
456 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
457 funResultTy (FunTy _arg res) = res
458 funResultTy ty = pprPanic "funResultTy" (ppr ty)
460 funArgTy :: Type -> Type
461 -- ^ Extract the function argument type and panic if that is not possible
462 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
463 funArgTy (FunTy arg _res) = arg
464 funArgTy ty = pprPanic "funArgTy" (ppr ty)
467 ---------------------------------------------------------------------
472 -- splitTyConApp "looks through" synonyms, because they don't
473 -- mean a distinct type, but all other type-constructor applications
474 -- including functions are returned as Just ..
476 -- | The same as @fst . splitTyConApp@
477 tyConAppTyCon :: Type -> TyCon
478 tyConAppTyCon ty = fst (splitTyConApp ty)
480 -- | The same as @snd . splitTyConApp@
481 tyConAppArgs :: Type -> [Type]
482 tyConAppArgs ty = snd (splitTyConApp ty)
484 -- | Attempts to tease a type apart into a type constructor and the application
485 -- of a number of arguments to that constructor. Panics if that is not possible.
486 -- See also 'splitTyConApp_maybe'
487 splitTyConApp :: Type -> (TyCon, [Type])
488 splitTyConApp ty = case splitTyConApp_maybe ty of
490 Nothing -> pprPanic "splitTyConApp" (ppr ty)
492 -- | Attempts to tease a type apart into a type constructor and the application
493 -- of a number of arguments to that constructor
494 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
495 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
496 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
497 splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
498 splitTyConApp_maybe _ = Nothing
500 newTyConInstRhs :: TyCon -> [Type] -> Type
501 -- ^ Unwrap one 'layer' of newtype on a type constructor and its arguments, using an
502 -- eta-reduced version of the @newtype@ if possible
503 newTyConInstRhs tycon tys
504 = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs )
505 mkAppTys (substTyWith tvs tys1 ty) tys2
507 (tvs, ty) = newTyConEtadRhs tycon
508 (tys1, tys2) = splitAtList tvs tys
512 ---------------------------------------------------------------------
516 Notes on type synonyms
517 ~~~~~~~~~~~~~~~~~~~~~~
518 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
519 to return type synonyms whereever possible. Thus
524 splitFunTys (a -> Foo a) = ([a], Foo a)
527 The reason is that we then get better (shorter) type signatures in
528 interfaces. Notably this plays a role in tcTySigs in TcBinds.lhs.
531 Note [Expanding newtypes]
532 ~~~~~~~~~~~~~~~~~~~~~~~~~
533 When expanding a type to expose a data-type constructor, we need to be
534 careful about newtypes, lest we fall into an infinite loop. Here are
537 newtype Id x = MkId x
538 newtype Fix f = MkFix (f (Fix f))
539 newtype T = MkT (T -> T)
542 --------------------------
544 Fix Maybe Maybe (Fix Maybe)
548 Notice that we can expand T, even though it's recursive.
549 And we can expand Id (Id Int), even though the Id shows up
550 twice at the outer level.
552 So, when expanding, we keep track of when we've seen a recursive
553 newtype at outermost level; and bale out if we see it again.
565 -- 4. All newtypes, including recursive ones, but not newtype families
567 -- It's useful in the back end of the compiler.
568 repType :: Type -> Type
569 -- Only applied to types of kind *; hence tycons are saturated
573 go :: [TyCon] -> Type -> Type
574 go rec_nts (ForAllTy _ ty) -- Look through foralls
577 go rec_nts (PredTy p) -- Expand predicates
578 = go rec_nts (predTypeRep p)
580 go rec_nts (TyConApp tc tys) -- Expand newtypes and synonyms
581 | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
582 = go rec_nts (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
584 | Just (rec_nts', ty') <- carefullySplitNewType_maybe rec_nts tc tys
590 carefullySplitNewType_maybe :: [TyCon] -> TyCon -> [Type] -> Maybe ([TyCon],Type)
591 -- Return the representation of a newtype, unless
592 -- we've seen it already: see Note [Expanding newtypes]
593 carefullySplitNewType_maybe rec_nts tc tys
595 , not (tc `elem` rec_nts) = Just (rec_nts', newTyConInstRhs tc tys)
596 | otherwise = Nothing
598 rec_nts' | isRecursiveTyCon tc = tc:rec_nts
599 | otherwise = rec_nts
602 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
603 -- of inspecting the type directly.
605 -- | Discovers the primitive representation of a more abstract 'Type'
606 typePrimRep :: Type -> PrimRep
607 typePrimRep ty = case repType ty of
608 TyConApp tc _ -> tyConPrimRep tc
610 AppTy _ _ -> PtrRep -- See note below
612 _ -> pprPanic "typePrimRep" (ppr ty)
613 -- Types of the form 'f a' must be of kind *, not *#, so
614 -- we are guaranteed that they are represented by pointers.
615 -- The reason is that f must have kind *->*, not *->*#, because
616 -- (we claim) there is no way to constrain f's kind any other
621 ---------------------------------------------------------------------
626 mkForAllTy :: TyVar -> Type -> Type
630 -- | Wraps foralls over the type using the provided 'TyVar's from left to right
631 mkForAllTys :: [TyVar] -> Type -> Type
632 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
634 isForAllTy :: Type -> Bool
635 isForAllTy (ForAllTy _ _) = True
638 -- | Attempts to take a forall type apart, returning the bound type variable
639 -- and the remainder of the type
640 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
641 splitForAllTy_maybe ty = splitFAT_m ty
643 splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
644 splitFAT_m (ForAllTy tyvar ty) = Just(tyvar, ty)
645 splitFAT_m _ = Nothing
647 -- | Attempts to take a forall type apart, returning all the immediate such bound
648 -- type variables and the remainder of the type. Always suceeds, even if that means
649 -- returning an empty list of 'TyVar's
650 splitForAllTys :: Type -> ([TyVar], Type)
651 splitForAllTys ty = split ty ty []
653 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
654 split _ (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
655 split orig_ty _ tvs = (reverse tvs, orig_ty)
657 -- | Equivalent to @snd . splitForAllTys@
658 dropForAlls :: Type -> Type
659 dropForAlls ty = snd (splitForAllTys ty)
662 -- (mkPiType now in CoreUtils)
668 -- | Instantiate a forall type with one or more type arguments.
669 -- Used when we have a polymorphic function applied to type args:
673 -- We use @applyTys type-of-f [t1,t2]@ to compute the type of the expression.
674 -- Panics if no application is possible.
675 applyTy :: Type -> Type -> Type
676 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
677 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
678 applyTy _ _ = panic "applyTy"
680 applyTys :: Type -> [Type] -> Type
681 -- ^ This function is interesting because:
683 -- 1. The function may have more for-alls than there are args
685 -- 2. Less obviously, it may have fewer for-alls
687 -- For case 2. think of:
689 -- > applyTys (forall a.a) [forall b.b, Int]
691 -- This really can happen, via dressing up polymorphic types with newtype
692 -- clothing. Here's an example:
694 -- > newtype R = R (forall a. a->a)
695 -- > foo = case undefined :: R of
698 applyTys ty args = applyTysD empty ty args
700 applyTysD :: SDoc -> Type -> [Type] -> Type -- Debug version
701 applyTysD _ orig_fun_ty [] = orig_fun_ty
702 applyTysD doc orig_fun_ty arg_tys
703 | n_tvs == n_args -- The vastly common case
704 = substTyWith tvs arg_tys rho_ty
705 | n_tvs > n_args -- Too many for-alls
706 = substTyWith (take n_args tvs) arg_tys
707 (mkForAllTys (drop n_args tvs) rho_ty)
708 | otherwise -- Too many type args
709 = ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty ) -- Zero case gives infnite loop!
710 applyTysD doc (substTyWith tvs (take n_tvs arg_tys) rho_ty)
713 (tvs, rho_ty) = splitForAllTys orig_fun_ty
715 n_args = length arg_tys
719 %************************************************************************
723 %************************************************************************
725 Polymorphic functions over Pred
728 allPred :: (a -> Bool) -> Pred a -> Bool
729 allPred p (ClassP _ ts) = all p ts
730 allPred p (IParam _ t) = p t
731 allPred p (EqPred t1 t2) = p t1 && p t2
733 isClassPred :: Pred a -> Bool
734 isClassPred (ClassP {}) = True
735 isClassPred _ = False
737 isEqPred :: Pred a -> Bool
738 isEqPred (EqPred {}) = True
741 isIPPred :: Pred a -> Bool
742 isIPPred (IParam {}) = True
749 mkPredTy :: PredType -> Type
750 mkPredTy pred = PredTy pred
752 mkPredTys :: ThetaType -> [Type]
753 mkPredTys preds = map PredTy preds
755 predTypeRep :: PredType -> Type
756 -- ^ Convert a 'PredType' to its representation type. However, it unwraps
757 -- only the outermost level; for example, the result might be a newtype application
758 predTypeRep (IParam _ ty) = ty
759 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
760 predTypeRep (EqPred ty1 ty2) = mkTyConApp eqPredPrimTyCon [ty1,ty2]
762 splitPredTy_maybe :: Type -> Maybe PredType
763 -- Returns Just for predicates only
764 splitPredTy_maybe ty | Just ty' <- tcView ty = splitPredTy_maybe ty'
765 splitPredTy_maybe (PredTy p) = Just p
766 splitPredTy_maybe _ = Nothing
768 isPredTy :: Type -> Bool
769 isPredTy ty = isJust (splitPredTy_maybe ty)
772 --------------------- Equality types ---------------------------------
774 isReflPredTy :: Type -> Bool
775 isReflPredTy ty = case splitPredTy_maybe ty of
776 Just (EqPred ty1 ty2) -> ty1 `eqType` ty2
779 splitEqPredTy_maybe :: Type -> Maybe (Type,Type)
780 splitEqPredTy_maybe ty = case splitPredTy_maybe ty of
781 Just (EqPred ty1 ty2) -> Just (ty1,ty2)
784 isEqPredTy :: Type -> Bool
785 isEqPredTy ty = case splitPredTy_maybe ty of
786 Just (EqPred {}) -> True
789 -- | Creates a type equality predicate
790 mkEqPred :: (a, a) -> Pred a
791 mkEqPred (ty1, ty2) = EqPred ty1 ty2
794 --------------------- Dictionary types ---------------------------------
796 mkClassPred :: Class -> [Type] -> PredType
797 mkClassPred clas tys = ClassP clas tys
799 isDictTy :: Type -> Bool
800 isDictTy ty = case splitPredTy_maybe ty of
801 Just p -> isClassPred p
804 isTyVarClassPred :: PredType -> Bool
805 isTyVarClassPred (ClassP _ tys) = all isTyVarTy tys
806 isTyVarClassPred _ = False
808 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
809 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
810 getClassPredTys_maybe _ = Nothing
812 getClassPredTys :: PredType -> (Class, [Type])
813 getClassPredTys (ClassP clas tys) = (clas, tys)
814 getClassPredTys _ = panic "getClassPredTys"
816 mkDictTy :: Class -> [Type] -> Type
817 mkDictTy clas tys = mkPredTy (ClassP clas tys)
819 isDictLikeTy :: Type -> Bool
820 -- Note [Dictionary-like types]
821 isDictLikeTy ty | Just ty' <- tcView ty = isDictTy ty'
822 isDictLikeTy (PredTy p) = isClassPred p
823 isDictLikeTy (TyConApp tc tys)
824 | isTupleTyCon tc = all isDictLikeTy tys
825 isDictLikeTy _ = False
828 Note [Dictionary-like types]
829 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
830 Being "dictionary-like" means either a dictionary type or a tuple thereof.
831 In GHC 6.10 we build implication constraints which construct such tuples,
832 and if we land up with a binding
835 then we want to treat t as cheap under "-fdicts-cheap" for example.
836 (Implication constraints are normally inlined, but sadly not if the
837 occurrence is itself inside an INLINE function! Until we revise the
838 handling of implication constraints, that is.) This turned out to
839 be important in getting good arities in DPH code. Example:
842 class D a where { foo :: a -> a }
843 instance C a => D (Maybe a) where { foo x = x }
845 bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
847 bar x y = (foo (Just x), foo (Just y))
849 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
850 we ended up with something like
851 bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
854 This is all a bit ad-hoc; eg it relies on knowing that implication
855 constraints build tuples.
857 --------------------- Implicit parameters ---------------------------------
860 mkIPPred :: IPName Name -> Type -> PredType
861 mkIPPred ip ty = IParam ip ty
864 %************************************************************************
868 %************************************************************************
871 typeSize :: Type -> Int
872 typeSize (TyVarTy _) = 1
873 typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2
874 typeSize (FunTy t1 t2) = typeSize t1 + typeSize t2
875 typeSize (PredTy p) = predSize typeSize p
876 typeSize (ForAllTy _ t) = 1 + typeSize t
877 typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
881 %************************************************************************
883 \subsection{Type families}
885 %************************************************************************
888 -- | Finds type family instances occuring in a type after expanding synonyms.
889 tyFamInsts :: Type -> [(TyCon, [Type])]
891 | Just exp_ty <- tcView ty = tyFamInsts exp_ty
892 tyFamInsts (TyVarTy _) = []
893 tyFamInsts (TyConApp tc tys)
894 | isSynFamilyTyCon tc = [(tc, tys)]
895 | otherwise = concat (map tyFamInsts tys)
896 tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
897 tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
898 tyFamInsts (ForAllTy _ ty) = tyFamInsts ty
899 tyFamInsts (PredTy pty) = predFamInsts pty
901 -- | Finds type family instances occuring in a predicate type after expanding
903 predFamInsts :: PredType -> [(TyCon, [Type])]
904 predFamInsts (ClassP _cla tys) = concat (map tyFamInsts tys)
905 predFamInsts (IParam _ ty) = tyFamInsts ty
906 predFamInsts (EqPred ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
908 mkFamilyTyConApp :: TyCon -> [Type] -> Type
909 -- ^ Given a family instance TyCon and its arg types, return the
910 -- corresponding family type. E.g:
913 -- > data instance T (Maybe b) = MkT b
915 -- Where the instance tycon is :RTL, so:
917 -- > mkFamilyTyConApp :RTL Int = T (Maybe Int)
918 mkFamilyTyConApp tc tys
919 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
920 , let fam_subst = zipTopTvSubst (tyConTyVars tc) tys
921 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
925 -- | Pretty prints a 'TyCon', using the family instance in case of a
926 -- representation tycon. For example:
928 -- > data T [a] = ...
930 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
931 pprSourceTyCon :: TyCon -> SDoc
933 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
934 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
939 %************************************************************************
941 \subsection{Liftedness}
943 %************************************************************************
946 -- | See "Type#type_classification" for what an unlifted type is
947 isUnLiftedType :: Type -> Bool
948 -- isUnLiftedType returns True for forall'd unlifted types:
949 -- x :: forall a. Int#
950 -- I found bindings like these were getting floated to the top level.
951 -- They are pretty bogus types, mind you. It would be better never to
954 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
955 isUnLiftedType (ForAllTy _ ty) = isUnLiftedType ty
956 isUnLiftedType (PredTy p) = isEqPred p
957 isUnLiftedType (TyConApp tc _) = isUnLiftedTyCon tc
958 isUnLiftedType _ = False
960 isUnboxedTupleType :: Type -> Bool
961 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
962 Just (tc, _ty_args) -> isUnboxedTupleTyCon tc
965 -- | See "Type#type_classification" for what an algebraic type is.
966 -- Should only be applied to /types/, as opposed to e.g. partially
967 -- saturated type constructors
968 isAlgType :: Type -> Bool
970 = case splitTyConApp_maybe ty of
971 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
975 -- | See "Type#type_classification" for what an algebraic type is.
976 -- Should only be applied to /types/, as opposed to e.g. partially
977 -- saturated type constructors. Closed type constructors are those
978 -- with a fixed right hand side, as opposed to e.g. associated types
979 isClosedAlgType :: Type -> Bool
981 = case splitTyConApp_maybe ty of
982 Just (tc, ty_args) | isAlgTyCon tc && not (isFamilyTyCon tc)
983 -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
988 -- | Computes whether an argument (or let right hand side) should
989 -- be computed strictly or lazily, based only on its type.
990 -- Works just like 'isUnLiftedType', except that it has a special case
991 -- for dictionaries (i.e. does not work purely on representation types)
993 -- Since it takes account of class 'PredType's, you might think
994 -- this function should be in 'TcType', but 'isStrictType' is used by 'DataCon',
995 -- which is below 'TcType' in the hierarchy, so it's convenient to put it here.
996 isStrictType :: Type -> Bool
997 isStrictType (PredTy pred) = isStrictPred pred
998 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
999 isStrictType (ForAllTy _ ty) = isStrictType ty
1000 isStrictType (TyConApp tc _) = isUnLiftedTyCon tc
1001 isStrictType _ = False
1003 -- | We may be strict in dictionary types, but only if it
1004 -- has more than one component.
1006 -- (Being strict in a single-component dictionary risks
1007 -- poking the dictionary component, which is wrong.)
1008 isStrictPred :: PredType -> Bool
1009 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
1010 isStrictPred (EqPred {}) = True
1011 isStrictPred (IParam {}) = False
1015 isPrimitiveType :: Type -> Bool
1016 -- ^ Returns true of types that are opaque to Haskell.
1017 -- Most of these are unlifted, but now that we interact with .NET, we
1018 -- may have primtive (foreign-imported) types that are lifted
1019 isPrimitiveType ty = case splitTyConApp_maybe ty of
1020 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1026 %************************************************************************
1028 The "exact" free variables of a type
1030 %************************************************************************
1032 Note [Silly type synonym]
1033 ~~~~~~~~~~~~~~~~~~~~~~~~~
1036 What are the free tyvars of (T x)? Empty, of course!
1037 Here's the example that Ralf Laemmel showed me:
1038 foo :: (forall a. C u a -> C u a) -> u
1039 mappend :: Monoid u => u -> u -> u
1041 bar :: Monoid u => u
1042 bar = foo (\t -> t `mappend` t)
1043 We have to generalise at the arg to f, and we don't
1044 want to capture the constraint (Monad (C u a)) because
1045 it appears to mention a. Pretty silly, but it was useful to him.
1047 exactTyVarsOfType is used by the type checker to figure out exactly
1048 which type variables are mentioned in a type. It's also used in the
1049 smart-app checking code --- see TcExpr.tcIdApp
1051 On the other hand, consider a *top-level* definition
1052 f = (\x -> x) :: T a -> T a
1053 If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
1054 if we have an application like (f "x") we get a confusing error message
1055 involving Any. So the conclusion is this: when generalising
1056 - at top level use tyVarsOfType
1057 - in nested bindings use exactTyVarsOfType
1058 See Trac #1813 for example.
1061 exactTyVarsOfType :: Type -> TyVarSet
1062 -- Find the free type variables (of any kind)
1063 -- but *expand* type synonyms. See Note [Silly type synonym] above.
1064 exactTyVarsOfType ty
1067 go ty | Just ty' <- tcView ty = go ty' -- This is the key line
1068 go (TyVarTy tv) = unitVarSet tv
1069 go (TyConApp _ tys) = exactTyVarsOfTypes tys
1070 go (PredTy ty) = go_pred ty
1071 go (FunTy arg res) = go arg `unionVarSet` go res
1072 go (AppTy fun arg) = go fun `unionVarSet` go arg
1073 go (ForAllTy tyvar ty) = delVarSet (go ty) tyvar
1075 go_pred (IParam _ ty) = go ty
1076 go_pred (ClassP _ tys) = exactTyVarsOfTypes tys
1077 go_pred (EqPred ty1 ty2) = go ty1 `unionVarSet` go ty2
1079 exactTyVarsOfTypes :: [Type] -> TyVarSet
1080 exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
1084 %************************************************************************
1086 \subsection{Sequencing on types}
1088 %************************************************************************
1091 seqType :: Type -> ()
1092 seqType (TyVarTy tv) = tv `seq` ()
1093 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
1094 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
1095 seqType (PredTy p) = seqPred seqType p
1096 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
1097 seqType (ForAllTy tv ty) = tv `seq` seqType ty
1099 seqTypes :: [Type] -> ()
1101 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
1103 seqPred :: (a -> ()) -> Pred a -> ()
1104 seqPred seqt (ClassP c tys) = c `seq` foldr (seq . seqt) () tys
1105 seqPred seqt (IParam n ty) = n `seq` seqt ty
1106 seqPred seqt (EqPred ty1 ty2) = seqt ty1 `seq` seqt ty2
1110 %************************************************************************
1112 Comparision for types
1113 (We don't use instances so that we know where it happens)
1115 %************************************************************************
1118 eqKind :: Kind -> Kind -> Bool
1121 eqType :: Type -> Type -> Bool
1122 -- ^ Type equality on source types. Does not look through @newtypes@ or
1123 -- 'PredType's, but it does look through type synonyms.
1124 eqType t1 t2 = isEqual $ cmpType t1 t2
1126 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
1127 eqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
1129 eqTypes :: [Type] -> [Type] -> Bool
1130 eqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
1132 eqPred :: PredType -> PredType -> Bool
1133 eqPred p1 p2 = isEqual $ cmpPred p1 p2
1135 eqPredX :: RnEnv2 -> PredType -> PredType -> Bool
1136 eqPredX env p1 p2 = isEqual $ cmpPredX env p1 p2
1139 Now here comes the real worker
1142 cmpType :: Type -> Type -> Ordering
1143 cmpType t1 t2 = cmpTypeX rn_env t1 t2
1145 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
1147 cmpTypes :: [Type] -> [Type] -> Ordering
1148 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
1150 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
1152 cmpPred :: PredType -> PredType -> Ordering
1153 cmpPred p1 p2 = cmpPredX rn_env p1 p2
1155 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
1157 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
1158 cmpTypeX env t1 t2 | Just t1' <- coreView t1 = cmpTypeX env t1' t2
1159 | Just t2' <- coreView t2 = cmpTypeX env t1 t2'
1160 -- We expand predicate types, because in Core-land we have
1161 -- lots of definitions like
1162 -- fOrdBool :: Ord Bool
1163 -- fOrdBool = D:Ord .. .. ..
1164 -- So the RHS has a data type
1166 cmpTypeX env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 `compare` rnOccR env tv2
1167 cmpTypeX env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
1168 cmpTypeX env (AppTy s1 t1) (AppTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1169 cmpTypeX env (FunTy s1 t1) (FunTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1170 cmpTypeX env (PredTy p1) (PredTy p2) = cmpPredX env p1 p2
1171 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
1173 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
1174 cmpTypeX _ (AppTy _ _) (TyVarTy _) = GT
1176 cmpTypeX _ (FunTy _ _) (TyVarTy _) = GT
1177 cmpTypeX _ (FunTy _ _) (AppTy _ _) = GT
1179 cmpTypeX _ (TyConApp _ _) (TyVarTy _) = GT
1180 cmpTypeX _ (TyConApp _ _) (AppTy _ _) = GT
1181 cmpTypeX _ (TyConApp _ _) (FunTy _ _) = GT
1183 cmpTypeX _ (ForAllTy _ _) (TyVarTy _) = GT
1184 cmpTypeX _ (ForAllTy _ _) (AppTy _ _) = GT
1185 cmpTypeX _ (ForAllTy _ _) (FunTy _ _) = GT
1186 cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = GT
1188 cmpTypeX _ (PredTy _) _ = GT
1193 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1194 cmpTypesX _ [] [] = EQ
1195 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1196 cmpTypesX _ [] _ = LT
1197 cmpTypesX _ _ [] = GT
1200 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1201 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1202 -- Compare names only for implicit parameters
1203 -- This comparison is used exclusively (I believe)
1204 -- for the Avails finite map built in TcSimplify
1205 -- If the types differ we keep them distinct so that we see
1206 -- a distinct pair to run improvement on
1207 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTypesX env tys1 tys2)
1208 cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
1210 -- Constructor order: IParam < ClassP < EqPred
1211 cmpPredX _ (IParam {}) _ = LT
1212 cmpPredX _ (ClassP {}) (IParam {}) = GT
1213 cmpPredX _ (ClassP {}) (EqPred {}) = LT
1214 cmpPredX _ (EqPred {}) _ = GT
1217 PredTypes are used as a FM key in TcSimplify,
1218 so we take the easy path and make them an instance of Ord
1221 instance Eq PredType where { (==) = eqPred }
1222 instance Ord PredType where { compare = cmpPred }
1226 %************************************************************************
1230 %************************************************************************
1233 emptyTvSubstEnv :: TvSubstEnv
1234 emptyTvSubstEnv = emptyVarEnv
1236 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1237 -- ^ @(compose env1 env2)(x)@ is @env1(env2(x))@; i.e. apply @env2@ then @env1@.
1238 -- It assumes that both are idempotent.
1239 -- Typically, @env1@ is the refinement to a base substitution @env2@
1240 composeTvSubst in_scope env1 env2
1241 = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1242 -- First apply env1 to the range of env2
1243 -- Then combine the two, making sure that env1 loses if
1244 -- both bind the same variable; that's why env1 is the
1245 -- *left* argument to plusVarEnv, because the right arg wins
1247 subst1 = TvSubst in_scope env1
1249 emptyTvSubst :: TvSubst
1250 emptyTvSubst = TvSubst emptyInScopeSet emptyTvSubstEnv
1252 isEmptyTvSubst :: TvSubst -> Bool
1253 -- See Note [Extending the TvSubstEnv]
1254 isEmptyTvSubst (TvSubst _ tenv) = isEmptyVarEnv tenv
1256 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1259 getTvSubstEnv :: TvSubst -> TvSubstEnv
1260 getTvSubstEnv (TvSubst _ env) = env
1262 getTvInScope :: TvSubst -> InScopeSet
1263 getTvInScope (TvSubst in_scope _) = in_scope
1265 isInScope :: Var -> TvSubst -> Bool
1266 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1268 notElemTvSubst :: TyCoVar -> TvSubst -> Bool
1269 notElemTvSubst v (TvSubst _ tenv) = not (v `elemVarEnv` tenv)
1271 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1272 setTvSubstEnv (TvSubst in_scope _) tenv = TvSubst in_scope tenv
1274 zapTvSubstEnv :: TvSubst -> TvSubst
1275 zapTvSubstEnv (TvSubst in_scope _) = TvSubst in_scope emptyVarEnv
1277 extendTvInScope :: TvSubst -> Var -> TvSubst
1278 extendTvInScope (TvSubst in_scope tenv) var = TvSubst (extendInScopeSet in_scope var) tenv
1280 extendTvInScopeList :: TvSubst -> [Var] -> TvSubst
1281 extendTvInScopeList (TvSubst in_scope tenv) vars = TvSubst (extendInScopeSetList in_scope vars) tenv
1283 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1284 extendTvSubst (TvSubst in_scope tenv) tv ty = TvSubst in_scope (extendVarEnv tenv tv ty)
1286 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1287 extendTvSubstList (TvSubst in_scope tenv) tvs tys
1288 = TvSubst in_scope (extendVarEnvList tenv (tvs `zip` tys))
1290 unionTvSubst :: TvSubst -> TvSubst -> TvSubst
1291 -- Works when the ranges are disjoint
1292 unionTvSubst (TvSubst in_scope1 tenv1) (TvSubst in_scope2 tenv2)
1293 = ASSERT( not (tenv1 `intersectsVarEnv` tenv2) )
1294 TvSubst (in_scope1 `unionInScope` in_scope2)
1295 (tenv1 `plusVarEnv` tenv2)
1297 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1298 -- the types given; but it's just a thunk so with a bit of luck
1299 -- it'll never be evaluated
1301 -- Note [Generating the in-scope set for a substitution]
1302 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1303 -- If we want to substitute [a -> ty1, b -> ty2] I used to
1304 -- think it was enough to generate an in-scope set that includes
1305 -- fv(ty1,ty2). But that's not enough; we really should also take the
1306 -- free vars of the type we are substituting into! Example:
1307 -- (forall b. (a,b,x)) [a -> List b]
1308 -- Then if we use the in-scope set {b}, there is a danger we will rename
1309 -- the forall'd variable to 'x' by mistake, getting this:
1310 -- (forall x. (List b, x, x)
1311 -- Urk! This means looking at all the calls to mkOpenTvSubst....
1314 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1315 -- environment, hence "open"
1316 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1317 mkOpenTvSubst tenv = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts tenv))) tenv
1319 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1320 -- environment, hence "open"
1321 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1322 zipOpenTvSubst tyvars tys
1323 | debugIsOn && (length tyvars /= length tys)
1324 = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1326 = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1328 -- | Called when doing top-level substitutions. Here we expect that the
1329 -- free vars of the range of the substitution will be empty.
1330 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1331 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1333 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1334 zipTopTvSubst tyvars tys
1335 | debugIsOn && (length tyvars /= length tys)
1336 = pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1338 = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1340 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1342 | debugIsOn && (length tyvars /= length tys)
1343 = pprTrace "zipTyEnv" (ppr tyvars $$ ppr tys) emptyVarEnv
1345 = zip_ty_env tyvars tys emptyVarEnv
1347 -- Later substitutions in the list over-ride earlier ones,
1348 -- but there should be no loops
1349 zip_ty_env :: [TyVar] -> [Type] -> TvSubstEnv -> TvSubstEnv
1350 zip_ty_env [] [] env = env
1351 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1352 -- There used to be a special case for when
1354 -- (a not-uncommon case) in which case the substitution was dropped.
1355 -- But the type-tidier changes the print-name of a type variable without
1356 -- changing the unique, and that led to a bug. Why? Pre-tidying, we had
1357 -- a type {Foo t}, where Foo is a one-method class. So Foo is really a newtype.
1358 -- And it happened that t was the type variable of the class. Post-tiding,
1359 -- it got turned into {Foo t2}. The ext-core printer expanded this using
1360 -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1361 -- and so generated a rep type mentioning t not t2.
1363 -- Simplest fix is to nuke the "optimisation"
1364 zip_ty_env tvs tys env = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1365 -- zip_ty_env _ _ env = env
1367 instance Outputable TvSubst where
1368 ppr (TvSubst ins tenv)
1369 = brackets $ sep[ ptext (sLit "TvSubst"),
1370 nest 2 (ptext (sLit "In scope:") <+> ppr ins),
1371 nest 2 (ptext (sLit "Type env:") <+> ppr tenv) ]
1374 %************************************************************************
1376 Performing type substitutions
1378 %************************************************************************
1381 -- | Type substitution making use of an 'TvSubst' that
1382 -- is assumed to be open, see 'zipOpenTvSubst'
1383 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1384 substTyWith tvs tys = ASSERT( length tvs == length tys )
1385 substTy (zipOpenTvSubst tvs tys)
1387 -- | Type substitution making use of an 'TvSubst' that
1388 -- is assumed to be open, see 'zipOpenTvSubst'
1389 substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
1390 substTysWith tvs tys = ASSERT( length tvs == length tys )
1391 substTys (zipOpenTvSubst tvs tys)
1393 -- | Substitute within a 'Type'
1394 substTy :: TvSubst -> Type -> Type
1395 substTy subst ty | isEmptyTvSubst subst = ty
1396 | otherwise = subst_ty subst ty
1398 -- | Substitute within several 'Type's
1399 substTys :: TvSubst -> [Type] -> [Type]
1400 substTys subst tys | isEmptyTvSubst subst = tys
1401 | otherwise = map (subst_ty subst) tys
1403 -- | Substitute within a 'ThetaType'
1404 substTheta :: TvSubst -> ThetaType -> ThetaType
1405 substTheta subst theta
1406 | isEmptyTvSubst subst = theta
1407 | otherwise = map (substPred subst) theta
1409 -- | Substitute within a 'PredType'
1410 substPred :: TvSubst -> PredType -> PredType
1411 substPred subst (IParam n ty) = IParam n (subst_ty subst ty)
1412 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1413 substPred subst (EqPred ty1 ty2) = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
1415 -- | Remove any nested binders mentioning the 'TyVar's in the 'TyVarSet'
1416 deShadowTy :: TyVarSet -> Type -> Type
1418 = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1420 in_scope = mkInScopeSet tvs
1422 subst_ty :: TvSubst -> Type -> Type
1423 -- subst_ty is the main workhorse for type substitution
1425 -- Note that the in_scope set is poked only if we hit a forall
1426 -- so it may often never be fully computed
1430 go (TyVarTy tv) = substTyVar subst tv
1431 go (TyConApp tc tys) = let args = map go tys
1432 in args `seqList` TyConApp tc args
1434 go (PredTy p) = PredTy $! (substPred subst p)
1436 go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
1437 go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
1438 -- The mkAppTy smart constructor is important
1439 -- we might be replacing (a Int), represented with App
1440 -- by [Int], represented with TyConApp
1441 go (ForAllTy tv ty) = case substTyVarBndr subst tv of
1443 ForAllTy tv' $! (subst_ty subst' ty)
1445 substTyVar :: TvSubst -> TyVar -> Type
1446 substTyVar (TvSubst _ tenv) tv
1447 | Just ty <- lookupVarEnv tenv tv = ty -- See Note [Apply Once]
1448 | otherwise = ASSERT( isTyVar tv ) TyVarTy tv
1449 -- We do not require that the tyvar is in scope
1450 -- Reason: we do quite a bit of (substTyWith [tv] [ty] tau)
1451 -- and it's a nuisance to bring all the free vars of tau into
1452 -- scope --- and then force that thunk at every tyvar
1453 -- Instead we have an ASSERT in substTyVarBndr to check for capture
1455 substTyVars :: TvSubst -> [TyVar] -> [Type]
1456 substTyVars subst tvs = map (substTyVar subst) tvs
1458 lookupTyVar :: TvSubst -> TyVar -> Maybe Type
1459 -- See Note [Extending the TvSubst]
1460 lookupTyVar (TvSubst _ tenv) tv = lookupVarEnv tenv tv
1462 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1463 substTyVarBndr subst@(TvSubst in_scope tenv) old_var
1464 = ASSERT2( _no_capture, ppr old_var $$ ppr subst )
1465 (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1467 new_env | no_change = delVarEnv tenv old_var
1468 | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
1470 _no_capture = not (new_var `elemVarSet` tyVarsOfTypes (varEnvElts tenv))
1471 -- Check that we are not capturing something in the substitution
1473 no_change = new_var == old_var
1474 -- no_change means that the new_var is identical in
1475 -- all respects to the old_var (same unique, same kind)
1476 -- See Note [Extending the TvSubst]
1478 -- In that case we don't need to extend the substitution
1479 -- to map old to new. But instead we must zap any
1480 -- current substitution for the variable. For example:
1481 -- (\x.e) with id_subst = [x |-> e']
1482 -- Here we must simply zap the substitution for x
1484 new_var = uniqAway in_scope old_var
1485 -- The uniqAway part makes sure the new variable is not already in scope
1488 ----------------------------------------------------
1497 -- There's a little subtyping at the kind level:
1507 -- Where: \* [LiftedTypeKind] means boxed type
1508 -- \# [UnliftedTypeKind] means unboxed type
1509 -- (\#) [UbxTupleKind] means unboxed tuple
1510 -- ?? [ArgTypeKind] is the lub of {\*, \#}
1511 -- ? [OpenTypeKind] means any type at all
1516 -- > error :: forall a:?. String -> a
1517 -- > (->) :: ?? -> ? -> \*
1518 -- > (\\(x::t) -> ...)
1520 -- Where in the last example @t :: ??@ (i.e. is not an unboxed tuple)
1522 type KindVar = TyVar -- invariant: KindVar will always be a
1523 -- TcTyVar with details MetaTv TauTv ...
1524 -- kind var constructors and functions are in TcType
1526 type SimpleKind = Kind
1531 During kind inference, a kind variable unifies only with
1533 sk ::= * | sk1 -> sk2
1535 data T a = MkT a (T Int#)
1536 fails. We give T the kind (k -> *), and the kind variable k won't unify
1537 with # (the kind of Int#).
1541 When creating a fresh internal type variable, we give it a kind to express
1542 constraints on it. E.g. in (\x->e) we make up a fresh type variable for x,
1545 During unification we only bind an internal type variable to a type
1546 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1548 When unifying two internal type variables, we collect their kind constraints by
1549 finding the GLB of the two. Since the partial order is a tree, they only
1550 have a glb if one is a sub-kind of the other. In that case, we bind the
1551 less-informative one to the more informative one. Neat, eh?