2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1998
6 Type - public interface
10 -- The above warning supression flag is a temporary kludge.
11 -- While working on this module you are encouraged to remove it and fix
12 -- any warnings in the module. See
13 -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
17 -- re-exports from TypeRep
18 TyThing(..), Type, PredType(..), ThetaType,
22 Kind, SimpleKind, KindVar,
23 kindFunResult, splitKindFunTys, splitKindFunTysN,
25 liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
26 argTypeKindTyCon, ubxTupleKindTyCon,
28 liftedTypeKind, unliftedTypeKind, openTypeKind,
29 argTypeKind, ubxTupleKind,
31 tySuperKind, coSuperKind,
33 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
34 isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind,
35 isCoSuperKind, isSuperKind, isCoercionKind, isEqPred,
36 mkArrowKind, mkArrowKinds,
38 isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
41 -- Re-exports from TyCon
44 mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,
46 mkAppTy, mkAppTys, splitAppTy, splitAppTys,
47 splitAppTy_maybe, repSplitAppTy_maybe,
49 mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
50 splitFunTys, splitFunTysN,
51 funResultTy, funArgTy, zipFunTys, isFunTy,
53 mkTyConApp, mkTyConTy,
54 tyConAppTyCon, tyConAppArgs,
55 splitTyConApp_maybe, splitTyConApp,
56 splitNewTyConApp_maybe, splitNewTyConApp,
58 repType, repType', typePrimRep, coreView, tcView, kindView,
60 mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
61 applyTy, applyTys, isForAllTy, dropForAlls,
64 predTypeRep, mkPredTy, mkPredTys, pprSourceTyCon, mkFamilyTyConApp,
70 isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType,
71 isStrictType, isStrictPred,
74 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
75 typeKind, addFreeTyVars,
77 -- Tidying up for printing
79 tidyOpenType, tidyOpenTypes,
80 tidyTyVarBndr, tidyFreeTyVars,
81 tidyOpenTyVar, tidyOpenTyVars,
82 tidyTopType, tidyPred,
86 coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
87 tcEqPred, tcCmpPred, tcEqTypeX,
93 TvSubstEnv, emptyTvSubstEnv, -- Representation widely visible
94 TvSubst(..), emptyTvSubst, -- Representation visible to a few friends
95 mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
96 getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
97 extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
100 -- Performing substitution on types
101 substTy, substTys, substTyWith, substTheta,
102 substPred, substTyVar, substTyVars, substTyVarBndr, deShadowTy, lookupTyVar,
105 pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprForAll,
106 pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind
109 #include "HsVersions.h"
111 -- We import the representation and primitive functions from TypeRep.
112 -- Many things are reexported, but not the representation!
133 import Data.Maybe ( isJust )
137 %************************************************************************
141 %************************************************************************
143 In Core, we "look through" non-recursive newtypes and PredTypes.
146 {-# INLINE coreView #-}
147 coreView :: Type -> Maybe Type
148 -- Strips off the *top layer only* of a type to give
149 -- its underlying representation type.
150 -- Returns Nothing if there is nothing to look through.
152 -- In the case of newtypes, it returns
153 -- *either* a vanilla TyConApp (recursive newtype, or non-saturated)
154 -- *or* the newtype representation (otherwise), meaning the
155 -- type written in the RHS of the newtype decl,
156 -- which may itself be a newtype
158 -- Example: newtype R = MkR S
160 -- newtype T = MkT (T -> T)
161 -- expandNewTcApp on R gives Just S
163 -- on T gives Nothing (no expansion)
165 -- By being non-recursive and inlined, this case analysis gets efficiently
166 -- joined onto the case analysis that the caller is already doing
167 coreView (NoteTy _ ty) = Just ty
169 | isEqPred p = Nothing
170 | otherwise = Just (predTypeRep p)
171 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
172 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
173 -- Its important to use mkAppTys, rather than (foldl AppTy),
174 -- because the function part might well return a
175 -- partially-applied type constructor; indeed, usually will!
176 coreView ty = Nothing
180 -----------------------------------------------
181 {-# INLINE tcView #-}
182 tcView :: Type -> Maybe Type
183 -- Same, but for the type checker, which just looks through synonyms
184 tcView (NoteTy _ ty) = Just ty
185 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
186 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
189 -----------------------------------------------
190 {-# INLINE kindView #-}
191 kindView :: Kind -> Maybe Kind
192 -- C.f. coreView, tcView
193 -- For the moment, we don't even handle synonyms in kinds
194 kindView (NoteTy _ k) = Just k
195 kindView other = Nothing
199 %************************************************************************
201 \subsection{Constructor-specific functions}
203 %************************************************************************
206 ---------------------------------------------------------------------
210 mkTyVarTy :: TyVar -> Type
213 mkTyVarTys :: [TyVar] -> [Type]
214 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
216 getTyVar :: String -> Type -> TyVar
217 getTyVar msg ty = case getTyVar_maybe ty of
219 Nothing -> panic ("getTyVar: " ++ msg)
221 isTyVarTy :: Type -> Bool
222 isTyVarTy ty = isJust (getTyVar_maybe ty)
224 getTyVar_maybe :: Type -> Maybe TyVar
225 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
226 getTyVar_maybe (TyVarTy tv) = Just tv
227 getTyVar_maybe other = Nothing
232 ---------------------------------------------------------------------
235 We need to be pretty careful with AppTy to make sure we obey the
236 invariant that a TyConApp is always visibly so. mkAppTy maintains the
240 mkAppTy orig_ty1 orig_ty2
243 mk_app (NoteTy _ ty1) = mk_app ty1
244 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
245 mk_app ty1 = AppTy orig_ty1 orig_ty2
246 -- Note that the TyConApp could be an
247 -- under-saturated type synonym. GHC allows that; e.g.
248 -- type Foo k = k a -> k a
250 -- foo :: Foo Id -> Foo Id
252 -- Here Id is partially applied in the type sig for Foo,
253 -- but once the type synonyms are expanded all is well
255 mkAppTys :: Type -> [Type] -> Type
256 mkAppTys orig_ty1 [] = orig_ty1
257 -- This check for an empty list of type arguments
258 -- avoids the needless loss of a type synonym constructor.
259 -- For example: mkAppTys Rational []
260 -- returns to (Ratio Integer), which has needlessly lost
261 -- the Rational part.
262 mkAppTys orig_ty1 orig_tys2
265 mk_app (NoteTy _ ty1) = mk_app ty1
266 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
267 -- mkTyConApp: see notes with mkAppTy
268 mk_app ty1 = foldl AppTy orig_ty1 orig_tys2
271 splitAppTy_maybe :: Type -> Maybe (Type, Type)
272 splitAppTy_maybe ty | Just ty' <- coreView ty
273 = splitAppTy_maybe ty'
274 splitAppTy_maybe ty = repSplitAppTy_maybe ty
277 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
278 -- Does the AppTy split, but assumes that any view stuff is already done
279 repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
280 repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
281 repSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
282 Just (tys', ty') -> Just (TyConApp tc tys', ty')
284 repSplitAppTy_maybe other = Nothing
286 splitAppTy :: Type -> (Type, Type)
287 splitAppTy ty = case splitAppTy_maybe ty of
289 Nothing -> panic "splitAppTy"
292 splitAppTys :: Type -> (Type, [Type])
293 splitAppTys ty = split ty ty []
295 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
296 split orig_ty (AppTy ty arg) args = split ty ty (arg:args)
297 split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
298 split orig_ty (FunTy ty1 ty2) args = ASSERT( null args )
299 (TyConApp funTyCon [], [ty1,ty2])
300 split orig_ty ty args = (orig_ty, args)
305 ---------------------------------------------------------------------
310 mkFunTy :: Type -> Type -> Type
311 mkFunTy (PredTy (EqPred ty1 ty2)) res = mkForAllTy (mkWildCoVar (PredTy (EqPred ty1 ty2))) res
312 mkFunTy arg res = FunTy arg res
314 mkFunTys :: [Type] -> Type -> Type
315 mkFunTys tys ty = foldr mkFunTy ty tys
317 isFunTy :: Type -> Bool
318 isFunTy ty = isJust (splitFunTy_maybe ty)
320 splitFunTy :: Type -> (Type, Type)
321 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
322 splitFunTy (FunTy arg res) = (arg, res)
323 splitFunTy other = pprPanic "splitFunTy" (ppr other)
325 splitFunTy_maybe :: Type -> Maybe (Type, Type)
326 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
327 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
328 splitFunTy_maybe other = Nothing
330 splitFunTys :: Type -> ([Type], Type)
331 splitFunTys ty = split [] ty ty
333 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
334 split args orig_ty (FunTy arg res) = split (arg:args) res res
335 split args orig_ty ty = (reverse args, orig_ty)
337 splitFunTysN :: Int -> Type -> ([Type], Type)
338 -- Split off exactly n arg tys
339 splitFunTysN 0 ty = ([], ty)
340 splitFunTysN n ty = case splitFunTy ty of { (arg, res) ->
341 case splitFunTysN (n-1) res of { (args, res) ->
344 zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
345 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
347 split acc [] nty ty = (reverse acc, nty)
349 | Just ty' <- coreView ty = split acc xs nty ty'
350 split acc (x:xs) nty (FunTy arg res) = split ((x,arg):acc) xs res res
351 split acc (x:xs) nty ty = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
353 funResultTy :: Type -> Type
354 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
355 funResultTy (FunTy arg res) = res
356 funResultTy ty = pprPanic "funResultTy" (ppr ty)
358 funArgTy :: Type -> Type
359 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
360 funArgTy (FunTy arg res) = arg
361 funArgTy ty = pprPanic "funArgTy" (ppr ty)
365 ---------------------------------------------------------------------
368 @mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or PredTy,
372 mkTyConApp :: TyCon -> [Type] -> Type
374 | isFunTyCon tycon, [ty1,ty2] <- tys
380 mkTyConTy :: TyCon -> Type
381 mkTyConTy tycon = mkTyConApp tycon []
383 -- splitTyConApp "looks through" synonyms, because they don't
384 -- mean a distinct type, but all other type-constructor applications
385 -- including functions are returned as Just ..
387 tyConAppTyCon :: Type -> TyCon
388 tyConAppTyCon ty = fst (splitTyConApp ty)
390 tyConAppArgs :: Type -> [Type]
391 tyConAppArgs ty = snd (splitTyConApp ty)
393 splitTyConApp :: Type -> (TyCon, [Type])
394 splitTyConApp ty = case splitTyConApp_maybe ty of
396 Nothing -> pprPanic "splitTyConApp" (ppr ty)
398 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
399 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
400 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
401 splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
402 splitTyConApp_maybe other = Nothing
404 -- Sometimes we do NOT want to look throught a newtype. When case matching
405 -- on a newtype we want a convenient way to access the arguments of a newty
406 -- constructor so as to properly form a coercion.
407 splitNewTyConApp :: Type -> (TyCon, [Type])
408 splitNewTyConApp ty = case splitNewTyConApp_maybe ty of
410 Nothing -> pprPanic "splitNewTyConApp" (ppr ty)
411 splitNewTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
412 splitNewTyConApp_maybe ty | Just ty' <- tcView ty = splitNewTyConApp_maybe ty'
413 splitNewTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
414 splitNewTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
415 splitNewTyConApp_maybe other = Nothing
417 newTyConInstRhs :: TyCon -> [Type] -> Type
418 newTyConInstRhs tycon tys =
419 let (tvs, ty) = newTyConRhs tycon in substTyWith tvs tys ty
423 ---------------------------------------------------------------------
427 Notes on type synonyms
428 ~~~~~~~~~~~~~~~~~~~~~~
429 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
430 to return type synonyms whereever possible. Thus
435 splitFunTys (a -> Foo a) = ([a], Foo a)
438 The reason is that we then get better (shorter) type signatures in
439 interfaces. Notably this plays a role in tcTySigs in TcBinds.lhs.
444 repType looks through
448 (d) usage annotations
449 (e) all newtypes, including recursive ones, but not newtype families
450 It's useful in the back end.
453 repType :: Type -> Type
454 -- Only applied to types of kind *; hence tycons are saturated
455 repType ty | Just ty' <- coreView ty = repType ty'
456 repType (ForAllTy _ ty) = repType ty
457 repType (TyConApp tc tys)
459 , (tvs, rep_ty) <- newTyConRep tc
460 = -- Recursive newtypes are opaque to coreView
461 -- but we must expand them here. Sure to
462 -- be saturated because repType is only applied
463 -- to types of kind *
464 ASSERT( tys `lengthIs` tyConArity tc )
465 repType (substTyWith tvs tys rep_ty)
469 -- repType' aims to be a more thorough version of repType
470 -- For now it simply looks through the TyConApp args too
471 repType' ty -- | pprTrace "repType'" (ppr ty $$ ppr (go1 ty)) False = undefined
475 go (TyConApp tc tys) = mkTyConApp tc (map repType' tys)
479 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
480 -- of inspecting the type directly.
481 typePrimRep :: Type -> PrimRep
482 typePrimRep ty = case repType ty of
483 TyConApp tc _ -> tyConPrimRep tc
485 AppTy _ _ -> PtrRep -- See note below
487 other -> pprPanic "typePrimRep" (ppr ty)
488 -- Types of the form 'f a' must be of kind *, not *#, so
489 -- we are guaranteed that they are represented by pointers.
490 -- The reason is that f must have kind *->*, not *->*#, because
491 -- (we claim) there is no way to constrain f's kind any other
496 ---------------------------------------------------------------------
501 mkForAllTy :: TyVar -> Type -> Type
503 = mkForAllTys [tyvar] ty
505 mkForAllTys :: [TyVar] -> Type -> Type
506 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
508 isForAllTy :: Type -> Bool
509 isForAllTy (NoteTy _ ty) = isForAllTy ty
510 isForAllTy (ForAllTy _ _) = True
511 isForAllTy other_ty = False
513 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
514 splitForAllTy_maybe ty = splitFAT_m ty
516 splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
517 splitFAT_m (ForAllTy tyvar ty) = Just(tyvar, ty)
518 splitFAT_m _ = Nothing
520 splitForAllTys :: Type -> ([TyVar], Type)
521 splitForAllTys ty = split ty ty []
523 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
524 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
525 split orig_ty t tvs = (reverse tvs, orig_ty)
527 dropForAlls :: Type -> Type
528 dropForAlls ty = snd (splitForAllTys ty)
531 -- (mkPiType now in CoreUtils)
535 Instantiate a for-all type with one or more type arguments.
536 Used when we have a polymorphic function applied to type args:
538 Then we use (applyTys type-of-f [t1,t2]) to compute the type of
542 applyTy :: Type -> Type -> Type
543 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
544 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
545 applyTy other arg = panic "applyTy"
547 applyTys :: Type -> [Type] -> Type
548 -- This function is interesting because
549 -- a) the function may have more for-alls than there are args
550 -- b) less obviously, it may have fewer for-alls
551 -- For case (b) think of
552 -- applyTys (forall a.a) [forall b.b, Int]
553 -- This really can happen, via dressing up polymorphic types with newtype
554 -- clothing. Here's an example:
555 -- newtype R = R (forall a. a->a)
556 -- foo = case undefined :: R of
559 applyTys orig_fun_ty [] = orig_fun_ty
560 applyTys orig_fun_ty arg_tys
561 | n_tvs == n_args -- The vastly common case
562 = substTyWith tvs arg_tys rho_ty
563 | n_tvs > n_args -- Too many for-alls
564 = substTyWith (take n_args tvs) arg_tys
565 (mkForAllTys (drop n_args tvs) rho_ty)
566 | otherwise -- Too many type args
567 = ASSERT2( n_tvs > 0, ppr orig_fun_ty ) -- Zero case gives infnite loop!
568 applyTys (substTyWith tvs (take n_tvs arg_tys) rho_ty)
571 (tvs, rho_ty) = splitForAllTys orig_fun_ty
573 n_args = length arg_tys
577 %************************************************************************
579 \subsection{Source types}
581 %************************************************************************
583 A "source type" is a type that is a separate type as far as the type checker is
584 concerned, but which has low-level representation as far as the back end is concerned.
586 Source types are always lifted.
588 The key function is predTypeRep which gives the representation of a source type:
591 mkPredTy :: PredType -> Type
592 mkPredTy pred = PredTy pred
594 mkPredTys :: ThetaType -> [Type]
595 mkPredTys preds = map PredTy preds
597 predTypeRep :: PredType -> Type
598 -- Convert a PredType to its "representation type";
599 -- the post-type-checking type used by all the Core passes of GHC.
600 -- Unwraps only the outermost level; for example, the result might
601 -- be a newtype application
602 predTypeRep (IParam _ ty) = ty
603 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
604 -- Result might be a newtype application, but the consumer will
605 -- look through that too if necessary
606 predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2))
608 mkFamilyTyConApp :: TyCon -> [Type] -> Type
609 -- Given a family instance TyCon and its arg types, return the
610 -- corresponding family type. E.g.
612 -- data instance T (Maybe b) = MkT b -- Instance tycon :RTL
614 -- mkFamilyTyConApp :RTL Int = T (Maybe Int)
615 mkFamilyTyConApp tc tys
616 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
617 , let fam_subst = zipTopTvSubst (tyConTyVars tc) tys
618 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
622 -- Pretty prints a tycon, using the family instance in case of a
623 -- representation tycon. For example
624 -- e.g. data T [a] = ...
625 -- In that case we want to print `T [a]', where T is the family TyCon
627 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
628 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
634 %************************************************************************
636 \subsection{Kinds and free variables}
638 %************************************************************************
640 ---------------------------------------------------------------------
641 Finding the kind of a type
642 ~~~~~~~~~~~~~~~~~~~~~~~~~~
644 typeKind :: Type -> Kind
645 typeKind (TyConApp tycon tys) = ASSERT( not (isCoercionTyCon tycon) )
646 -- We should be looking for the coercion kind,
648 foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
649 typeKind (NoteTy _ ty) = typeKind ty
650 typeKind (PredTy pred) = predKind pred
651 typeKind (AppTy fun arg) = kindFunResult (typeKind fun)
652 typeKind (ForAllTy tv ty) = typeKind ty
653 typeKind (TyVarTy tyvar) = tyVarKind tyvar
654 typeKind (FunTy arg res)
655 -- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*),
656 -- not unliftedTypKind (#)
657 -- The only things that can be after a function arrow are
658 -- (a) types (of kind openTypeKind or its sub-kinds)
659 -- (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
660 | isTySuperKind k = k
661 | otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind
665 predKind :: PredType -> Kind
666 predKind (EqPred {}) = coSuperKind -- A coercion kind!
667 predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are
668 predKind (IParam {}) = liftedTypeKind -- always represented by lifted types
672 ---------------------------------------------------------------------
673 Free variables of a type
674 ~~~~~~~~~~~~~~~~~~~~~~~~
676 tyVarsOfType :: Type -> TyVarSet
677 -- NB: for type synonyms tyVarsOfType does *not* expand the synonym
678 tyVarsOfType (TyVarTy tv) = unitVarSet tv
679 tyVarsOfType (TyConApp tycon tys) = tyVarsOfTypes tys
680 tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
681 tyVarsOfType (PredTy sty) = tyVarsOfPred sty
682 tyVarsOfType (FunTy arg res) = tyVarsOfType arg `unionVarSet` tyVarsOfType res
683 tyVarsOfType (AppTy fun arg) = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
684 tyVarsOfType (ForAllTy tyvar ty) = delVarSet (tyVarsOfType ty) tyvar
686 tyVarsOfTypes :: [Type] -> TyVarSet
687 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
689 tyVarsOfPred :: PredType -> TyVarSet
690 tyVarsOfPred (IParam _ ty) = tyVarsOfType ty
691 tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys
692 tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
694 tyVarsOfTheta :: ThetaType -> TyVarSet
695 tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
697 -- Add a Note with the free tyvars to the top of the type
698 addFreeTyVars :: Type -> Type
699 addFreeTyVars ty@(NoteTy (FTVNote _) _) = ty
700 addFreeTyVars ty = NoteTy (FTVNote (tyVarsOfType ty)) ty
704 %************************************************************************
706 \subsection{TidyType}
708 %************************************************************************
710 tidyTy tidies up a type for printing in an error message, or in
713 It doesn't change the uniques at all, just the print names.
716 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
717 tidyTyVarBndr env@(tidy_env, subst) tyvar
718 = case tidyOccName tidy_env (getOccName name) of
719 (tidy', occ') -> ((tidy', subst'), tyvar'')
721 subst' = extendVarEnv subst tyvar tyvar''
722 tyvar' = setTyVarName tyvar name'
723 name' = tidyNameOcc name occ'
724 -- Don't forget to tidy the kind for coercions!
725 tyvar'' | isCoVar tyvar = setTyVarKind tyvar' kind'
727 kind' = tidyType env (tyVarKind tyvar)
729 name = tyVarName tyvar
731 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
732 -- Add the free tyvars to the env in tidy form,
733 -- so that we can tidy the type they are free in
734 tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))
736 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
737 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
739 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
740 -- Treat a new tyvar as a binder, and give it a fresh tidy name
741 tidyOpenTyVar env@(tidy_env, subst) tyvar
742 = case lookupVarEnv subst tyvar of
743 Just tyvar' -> (env, tyvar') -- Already substituted
744 Nothing -> tidyTyVarBndr env tyvar -- Treat it as a binder
746 tidyType :: TidyEnv -> Type -> Type
747 tidyType env@(tidy_env, subst) ty
750 go (TyVarTy tv) = case lookupVarEnv subst tv of
751 Nothing -> TyVarTy tv
752 Just tv' -> TyVarTy tv'
753 go (TyConApp tycon tys) = let args = map go tys
754 in args `seqList` TyConApp tycon args
755 go (NoteTy note ty) = (NoteTy $! (go_note note)) $! (go ty)
756 go (PredTy sty) = PredTy (tidyPred env sty)
757 go (AppTy fun arg) = (AppTy $! (go fun)) $! (go arg)
758 go (FunTy fun arg) = (FunTy $! (go fun)) $! (go arg)
759 go (ForAllTy tv ty) = ForAllTy tvp $! (tidyType envp ty)
761 (envp, tvp) = tidyTyVarBndr env tv
763 go_note note@(FTVNote ftvs) = note -- No need to tidy the free tyvars
765 tidyTypes env tys = map (tidyType env) tys
767 tidyPred :: TidyEnv -> PredType -> PredType
768 tidyPred env (IParam n ty) = IParam n (tidyType env ty)
769 tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
770 tidyPred env (EqPred ty1 ty2) = EqPred (tidyType env ty1) (tidyType env ty2)
774 @tidyOpenType@ grabs the free type variables, tidies them
775 and then uses @tidyType@ to work over the type itself
778 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
780 = (env', tidyType env' ty)
782 env' = tidyFreeTyVars env (tyVarsOfType ty)
784 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
785 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
787 tidyTopType :: Type -> Type
788 tidyTopType ty = tidyType emptyTidyEnv ty
793 tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
794 tidyKind env k = tidyOpenType env k
799 %************************************************************************
801 \subsection{Liftedness}
803 %************************************************************************
806 isUnLiftedType :: Type -> Bool
807 -- isUnLiftedType returns True for forall'd unlifted types:
808 -- x :: forall a. Int#
809 -- I found bindings like these were getting floated to the top level.
810 -- They are pretty bogus types, mind you. It would be better never to
813 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
814 isUnLiftedType (ForAllTy tv ty) = isUnLiftedType ty
815 isUnLiftedType (TyConApp tc _) = isUnLiftedTyCon tc
816 isUnLiftedType other = False
818 isUnboxedTupleType :: Type -> Bool
819 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
820 Just (tc, ty_args) -> isUnboxedTupleTyCon tc
823 -- Should only be applied to *types*; hence the assert
824 isAlgType :: Type -> Bool
825 isAlgType ty = case splitTyConApp_maybe ty of
826 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
831 @isStrictType@ computes whether an argument (or let RHS) should
832 be computed strictly or lazily, based only on its type.
833 Works just like isUnLiftedType, except that it has a special case
834 for dictionaries. Since it takes account of ClassP, you might think
835 this function should be in TcType, but isStrictType is used by DataCon,
836 which is below TcType in the hierarchy, so it's convenient to put it here.
839 isStrictType (PredTy pred) = isStrictPred pred
840 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
841 isStrictType (ForAllTy tv ty) = isStrictType ty
842 isStrictType (TyConApp tc _) = isUnLiftedTyCon tc
843 isStrictType other = False
845 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
846 isStrictPred other = False
847 -- We may be strict in dictionary types, but only if it
848 -- has more than one component.
849 -- [Being strict in a single-component dictionary risks
850 -- poking the dictionary component, which is wrong.]
854 isPrimitiveType :: Type -> Bool
855 -- Returns types that are opaque to Haskell.
856 -- Most of these are unlifted, but now that we interact with .NET, we
857 -- may have primtive (foreign-imported) types that are lifted
858 isPrimitiveType ty = case splitTyConApp_maybe ty of
859 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
865 %************************************************************************
867 \subsection{Sequencing on types
869 %************************************************************************
872 seqType :: Type -> ()
873 seqType (TyVarTy tv) = tv `seq` ()
874 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
875 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
876 seqType (NoteTy note t2) = seqNote note `seq` seqType t2
877 seqType (PredTy p) = seqPred p
878 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
879 seqType (ForAllTy tv ty) = tv `seq` seqType ty
881 seqTypes :: [Type] -> ()
883 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
885 seqNote :: TyNote -> ()
886 seqNote (FTVNote set) = sizeUniqSet set `seq` ()
888 seqPred :: PredType -> ()
889 seqPred (ClassP c tys) = c `seq` seqTypes tys
890 seqPred (IParam n ty) = n `seq` seqType ty
891 seqPred (EqPred ty1 ty2) = seqType ty1 `seq` seqType ty2
895 %************************************************************************
897 Equality for Core types
898 (We don't use instances so that we know where it happens)
900 %************************************************************************
902 Note that eqType works right even for partial applications of newtypes.
903 See Note [Newtype eta] in TyCon.lhs
906 coreEqType :: Type -> Type -> Bool
910 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
912 eq env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2
913 eq env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
914 eq env (AppTy s1 t1) (AppTy s2 t2) = eq env s1 s2 && eq env t1 t2
915 eq env (FunTy s1 t1) (FunTy s2 t2) = eq env s1 s2 && eq env t1 t2
916 eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
917 | tc1 == tc2, all2 (eq env) tys1 tys2 = True
918 -- The lengths should be equal because
919 -- the two types have the same kind
920 -- NB: if the type constructors differ that does not
921 -- necessarily mean that the types aren't equal
922 -- (synonyms, newtypes)
923 -- Even if the type constructors are the same, but the arguments
924 -- differ, the two types could be the same (e.g. if the arg is just
925 -- ignored in the RHS). In both these cases we fall through to an
926 -- attempt to expand one side or the other.
928 -- Now deal with newtypes, synonyms, pred-tys
929 eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
930 | Just t2' <- coreView t2 = eq env t1 t2'
932 -- Fall through case; not equal!
937 %************************************************************************
939 Comparision for source types
940 (We don't use instances so that we know where it happens)
942 %************************************************************************
946 do *not* look through newtypes, PredTypes
949 tcEqType :: Type -> Type -> Bool
950 tcEqType t1 t2 = isEqual $ cmpType t1 t2
952 tcEqTypes :: [Type] -> [Type] -> Bool
953 tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
955 tcCmpType :: Type -> Type -> Ordering
956 tcCmpType t1 t2 = cmpType t1 t2
958 tcCmpTypes :: [Type] -> [Type] -> Ordering
959 tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
961 tcEqPred :: PredType -> PredType -> Bool
962 tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
964 tcCmpPred :: PredType -> PredType -> Ordering
965 tcCmpPred p1 p2 = cmpPred p1 p2
967 tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
968 tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
971 Now here comes the real worker
974 cmpType :: Type -> Type -> Ordering
975 cmpType t1 t2 = cmpTypeX rn_env t1 t2
977 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
979 cmpTypes :: [Type] -> [Type] -> Ordering
980 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
982 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
984 cmpPred :: PredType -> PredType -> Ordering
985 cmpPred p1 p2 = cmpPredX rn_env p1 p2
987 rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
989 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
990 cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
991 | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
993 cmpTypeX env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 `compare` rnOccR env tv2
994 cmpTypeX env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
995 cmpTypeX env (AppTy s1 t1) (AppTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
996 cmpTypeX env (FunTy s1 t1) (FunTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
997 cmpTypeX env (PredTy p1) (PredTy p2) = cmpPredX env p1 p2
998 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
999 cmpTypeX env t1 (NoteTy _ t2) = cmpTypeX env t1 t2
1001 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
1002 cmpTypeX env (AppTy _ _) (TyVarTy _) = GT
1004 cmpTypeX env (FunTy _ _) (TyVarTy _) = GT
1005 cmpTypeX env (FunTy _ _) (AppTy _ _) = GT
1007 cmpTypeX env (TyConApp _ _) (TyVarTy _) = GT
1008 cmpTypeX env (TyConApp _ _) (AppTy _ _) = GT
1009 cmpTypeX env (TyConApp _ _) (FunTy _ _) = GT
1011 cmpTypeX env (ForAllTy _ _) (TyVarTy _) = GT
1012 cmpTypeX env (ForAllTy _ _) (AppTy _ _) = GT
1013 cmpTypeX env (ForAllTy _ _) (FunTy _ _) = GT
1014 cmpTypeX env (ForAllTy _ _) (TyConApp _ _) = GT
1016 cmpTypeX env (PredTy _) t2 = GT
1018 cmpTypeX env _ _ = LT
1021 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1022 cmpTypesX env [] [] = EQ
1023 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1024 cmpTypesX env [] tys = LT
1025 cmpTypesX env ty [] = GT
1028 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1029 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1030 -- Compare names only for implicit parameters
1031 -- This comparison is used exclusively (I believe)
1032 -- for the Avails finite map built in TcSimplify
1033 -- If the types differ we keep them distinct so that we see
1034 -- a distinct pair to run improvement on
1035 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTypesX env tys1 tys2)
1036 cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
1038 -- Constructor order: IParam < ClassP < EqPred
1039 cmpPredX env (IParam {}) _ = LT
1040 cmpPredX env (ClassP {}) (IParam {}) = GT
1041 cmpPredX env (ClassP {}) (EqPred {}) = LT
1042 cmpPredX env (EqPred {}) _ = GT
1045 PredTypes are used as a FM key in TcSimplify,
1046 so we take the easy path and make them an instance of Ord
1049 instance Eq PredType where { (==) = tcEqPred }
1050 instance Ord PredType where { compare = tcCmpPred }
1054 %************************************************************************
1058 %************************************************************************
1062 = TvSubst InScopeSet -- The in-scope type variables
1063 TvSubstEnv -- The substitution itself
1064 -- See Note [Apply Once]
1065 -- and Note [Extending the TvSubstEnv]
1067 {- ----------------------------------------------------------
1071 We use TvSubsts to instantiate things, and we might instantiate
1075 So the substition might go [a->b, b->a]. A similar situation arises in Core
1076 when we find a beta redex like
1077 (/\ a /\ b -> e) b a
1078 Then we also end up with a substition that permutes type variables. Other
1079 variations happen to; for example [a -> (a, b)].
1081 ***************************************************
1082 *** So a TvSubst must be applied precisely once ***
1083 ***************************************************
1085 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
1086 we use during unifications, it must not be repeatedly applied.
1088 Note [Extending the TvSubst]
1089 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1090 The following invariant should hold of a TvSubst
1092 The in-scope set is needed *only* to
1093 guide the generation of fresh uniques
1095 In particular, the *kind* of the type variables in
1096 the in-scope set is not relevant
1098 This invariant allows a short-cut when the TvSubstEnv is empty:
1099 if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) holds ---
1100 then (substTy subst ty) does nothing.
1102 For example, consider:
1103 (/\a. /\b:(a~Int). ...b..) Int
1104 We substitute Int for 'a'. The Unique of 'b' does not change, but
1105 nevertheless we add 'b' to the TvSubstEnv, because b's type does change
1107 This invariant has several crucial consequences:
1109 * In substTyVarBndr, we need extend the TvSubstEnv
1110 - if the unique has changed
1111 - or if the kind has changed
1113 * In substTyVar, we do not need to consult the in-scope set;
1114 the TvSubstEnv is enough
1116 * In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
1119 -------------------------------------------------------------- -}
1122 type TvSubstEnv = TyVarEnv Type
1123 -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
1124 -- invariant discussed in Note [Apply Once]), and also independently
1125 -- in the middle of matching, and unification (see Types.Unify)
1126 -- So you have to look at the context to know if it's idempotent or
1127 -- apply-once or whatever
1128 emptyTvSubstEnv :: TvSubstEnv
1129 emptyTvSubstEnv = emptyVarEnv
1131 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1132 -- (compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1
1133 -- It assumes that both are idempotent
1134 -- Typically, env1 is the refinement to a base substitution env2
1135 composeTvSubst in_scope env1 env2
1136 = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1137 -- First apply env1 to the range of env2
1138 -- Then combine the two, making sure that env1 loses if
1139 -- both bind the same variable; that's why env1 is the
1140 -- *left* argument to plusVarEnv, because the right arg wins
1142 subst1 = TvSubst in_scope env1
1144 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1146 isEmptyTvSubst :: TvSubst -> Bool
1147 -- See Note [Extending the TvSubstEnv]
1148 isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
1150 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1153 getTvSubstEnv :: TvSubst -> TvSubstEnv
1154 getTvSubstEnv (TvSubst _ env) = env
1156 getTvInScope :: TvSubst -> InScopeSet
1157 getTvInScope (TvSubst in_scope _) = in_scope
1159 isInScope :: Var -> TvSubst -> Bool
1160 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1162 notElemTvSubst :: TyVar -> TvSubst -> Bool
1163 notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
1165 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1166 setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
1168 extendTvInScope :: TvSubst -> [Var] -> TvSubst
1169 extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
1171 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1172 extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
1174 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1175 extendTvSubstList (TvSubst in_scope env) tvs tys
1176 = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
1178 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1179 -- the types given; but it's just a thunk so with a bit of luck
1180 -- it'll never be evaluated
1182 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1183 mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
1185 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1186 zipOpenTvSubst tyvars tys
1188 | length tyvars /= length tys
1189 = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1192 = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1194 -- mkTopTvSubst is called when doing top-level substitutions.
1195 -- Here we expect that the free vars of the range of the
1196 -- substitution will be empty.
1197 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1198 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1200 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1201 zipTopTvSubst tyvars tys
1203 | length tyvars /= length tys
1204 = pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1207 = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1209 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1212 | length tyvars /= length tys
1213 = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
1216 = zip_ty_env tyvars tys emptyVarEnv
1218 -- Later substitutions in the list over-ride earlier ones,
1219 -- but there should be no loops
1220 zip_ty_env [] [] env = env
1221 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1222 -- There used to be a special case for when
1224 -- (a not-uncommon case) in which case the substitution was dropped.
1225 -- But the type-tidier changes the print-name of a type variable without
1226 -- changing the unique, and that led to a bug. Why? Pre-tidying, we had
1227 -- a type {Foo t}, where Foo is a one-method class. So Foo is really a newtype.
1228 -- And it happened that t was the type variable of the class. Post-tiding,
1229 -- it got turned into {Foo t2}. The ext-core printer expanded this using
1230 -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1231 -- and so generated a rep type mentioning t not t2.
1233 -- Simplest fix is to nuke the "optimisation"
1234 zip_ty_env tvs tys env = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1235 -- zip_ty_env _ _ env = env
1237 instance Outputable TvSubst where
1238 ppr (TvSubst ins env)
1239 = brackets $ sep[ ptext SLIT("TvSubst"),
1240 nest 2 (ptext SLIT("In scope:") <+> ppr ins),
1241 nest 2 (ptext SLIT("Env:") <+> ppr env) ]
1244 %************************************************************************
1246 Performing type substitutions
1248 %************************************************************************
1251 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1252 substTyWith tvs tys = ASSERT( length tvs == length tys )
1253 substTy (zipOpenTvSubst tvs tys)
1255 substTy :: TvSubst -> Type -> Type
1256 substTy subst ty | isEmptyTvSubst subst = ty
1257 | otherwise = subst_ty subst ty
1259 substTys :: TvSubst -> [Type] -> [Type]
1260 substTys subst tys | isEmptyTvSubst subst = tys
1261 | otherwise = map (subst_ty subst) tys
1263 substTheta :: TvSubst -> ThetaType -> ThetaType
1264 substTheta subst theta
1265 | isEmptyTvSubst subst = theta
1266 | otherwise = map (substPred subst) theta
1268 substPred :: TvSubst -> PredType -> PredType
1269 substPred subst (IParam n ty) = IParam n (subst_ty subst ty)
1270 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1271 substPred subst (EqPred ty1 ty2) = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
1273 deShadowTy :: TyVarSet -> Type -> Type -- Remove any nested binders mentioning tvs
1275 = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1277 in_scope = mkInScopeSet tvs
1279 subst_ty :: TvSubst -> Type -> Type
1280 -- subst_ty is the main workhorse for type substitution
1282 -- Note that the in_scope set is poked only if we hit a forall
1283 -- so it may often never be fully computed
1287 go (TyVarTy tv) = substTyVar subst tv
1288 go (TyConApp tc tys) = let args = map go tys
1289 in args `seqList` TyConApp tc args
1291 go (PredTy p) = PredTy $! (substPred subst p)
1293 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard the free tyvar note
1295 go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
1296 go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
1297 -- The mkAppTy smart constructor is important
1298 -- we might be replacing (a Int), represented with App
1299 -- by [Int], represented with TyConApp
1300 go (ForAllTy tv ty) = case substTyVarBndr subst tv of
1301 (subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)
1303 substTyVar :: TvSubst -> TyVar -> Type
1304 substTyVar subst@(TvSubst in_scope env) tv
1305 = case lookupTyVar subst tv of {
1306 Nothing -> TyVarTy tv;
1307 Just ty -> ty -- See Note [Apply Once]
1310 substTyVars :: TvSubst -> [TyVar] -> [Type]
1311 substTyVars subst tvs = map (substTyVar subst) tvs
1313 lookupTyVar :: TvSubst -> TyVar -> Maybe Type
1314 -- See Note [Extending the TvSubst]
1315 lookupTyVar (TvSubst in_scope env) tv = lookupVarEnv env tv
1317 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1318 substTyVarBndr subst@(TvSubst in_scope env) old_var
1319 = (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1321 is_co_var = isCoVar old_var
1323 new_env | no_change = delVarEnv env old_var
1324 | otherwise = extendVarEnv env old_var (TyVarTy new_var)
1326 no_change = new_var == old_var && not is_co_var
1327 -- no_change means that the new_var is identical in
1328 -- all respects to the old_var (same unique, same kind)
1329 -- See Note [Extending the TvSubst]
1331 -- In that case we don't need to extend the substitution
1332 -- to map old to new. But instead we must zap any
1333 -- current substitution for the variable. For example:
1334 -- (\x.e) with id_subst = [x |-> e']
1335 -- Here we must simply zap the substitution for x
1337 new_var = uniqAway in_scope subst_old_var
1338 -- The uniqAway part makes sure the new variable is not already in scope
1340 subst_old_var -- subst_old_var is old_var with the substitution applied to its kind
1341 -- It's only worth doing the substitution for coercions,
1342 -- becuase only they can have free type variables
1343 | is_co_var = setTyVarKind old_var (substTy subst (tyVarKind old_var))
1344 | otherwise = old_var
1347 ----------------------------------------------------
1352 There's a little subtyping at the kind level:
1361 where * [LiftedTypeKind] means boxed type
1362 # [UnliftedTypeKind] means unboxed type
1363 (#) [UbxTupleKind] means unboxed tuple
1364 ?? [ArgTypeKind] is the lub of *,#
1365 ? [OpenTypeKind] means any type at all
1369 error :: forall a:?. String -> a
1370 (->) :: ?? -> ? -> *
1371 (\(x::t) -> ...) Here t::?? (i.e. not unboxed tuple)
1374 type KindVar = TyVar -- invariant: KindVar will always be a
1375 -- TcTyVar with details MetaTv TauTv ...
1376 -- kind var constructors and functions are in TcType
1378 type SimpleKind = Kind
1383 During kind inference, a kind variable unifies only with
1385 sk ::= * | sk1 -> sk2
1387 data T a = MkT a (T Int#)
1388 fails. We give T the kind (k -> *), and the kind variable k won't unify
1389 with # (the kind of Int#).
1393 When creating a fresh internal type variable, we give it a kind to express
1394 constraints on it. E.g. in (\x->e) we make up a fresh type variable for x,
1397 During unification we only bind an internal type variable to a type
1398 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1400 When unifying two internal type variables, we collect their kind constraints by
1401 finding the GLB of the two. Since the partial order is a tree, they only
1402 have a glb if one is a sub-kind of the other. In that case, we bind the
1403 less-informative one to the more informative one. Neat, eh?
1410 %************************************************************************
1412 Functions over Kinds
1414 %************************************************************************
1417 kindFunResult :: Kind -> Kind
1418 kindFunResult k = funResultTy k
1420 splitKindFunTys :: Kind -> ([Kind],Kind)
1421 splitKindFunTys k = splitFunTys k
1423 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
1424 splitKindFunTysN k = splitFunTysN k
1426 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
1428 isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey
1430 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
1431 isOpenTypeKind other = False
1433 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
1435 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
1436 isUbxTupleKind other = False
1438 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
1440 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
1441 isArgTypeKind other = False
1443 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
1445 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
1446 isUnliftedTypeKind other = False
1448 isSubOpenTypeKind :: Kind -> Bool
1449 -- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
1450 isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
1451 ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
1453 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
1454 isSubOpenTypeKind other = ASSERT( isKind other ) False
1455 -- This is a conservative answer
1456 -- It matters in the call to isSubKind in
1457 -- checkExpectedKind.
1459 isSubArgTypeKindCon kc
1460 | isUnliftedTypeKindCon kc = True
1461 | isLiftedTypeKindCon kc = True
1462 | isArgTypeKindCon kc = True
1465 isSubArgTypeKind :: Kind -> Bool
1466 -- True of any sub-kind of ArgTypeKind
1467 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
1468 isSubArgTypeKind other = False
1470 isSuperKind :: Type -> Bool
1471 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
1472 isSuperKind other = False
1474 isKind :: Kind -> Bool
1475 isKind k = isSuperKind (typeKind k)
1477 isSubKind :: Kind -> Kind -> Bool
1478 -- (k1 `isSubKind` k2) checks that k1 <: k2
1479 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
1480 isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
1481 isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2'))
1482 = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
1483 isSubKind k1 k2 = False
1485 eqKind :: Kind -> Kind -> Bool
1488 isSubKindCon :: TyCon -> TyCon -> Bool
1489 -- (kc1 `isSubKindCon` kc2) checks that kc1 <: kc2
1490 isSubKindCon kc1 kc2
1491 | isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True
1492 | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
1493 | isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True
1494 | isOpenTypeKindCon kc2 = True
1495 -- we already know kc1 is not a fun, its a TyCon
1496 | isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True
1499 defaultKind :: Kind -> Kind
1500 -- Used when generalising: default kind '?' and '??' to '*'
1502 -- When we generalise, we make generic type variables whose kind is
1503 -- simple (* or *->* etc). So generic type variables (other than
1504 -- built-in constants like 'error') always have simple kinds. This is important;
1507 -- We want f to get type
1508 -- f :: forall (a::*). a -> Bool
1510 -- f :: forall (a::??). a -> Bool
1511 -- because that would allow a call like (f 3#) as well as (f True),
1512 --and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr.
1514 | isSubOpenTypeKind k = liftedTypeKind
1515 | isSubArgTypeKind k = liftedTypeKind
1518 isEqPred :: PredType -> Bool
1519 isEqPred (EqPred _ _) = True
1520 isEqPred other = False