01ec26cae55b9f509360a5349b27c97caea07a2b
[ghc.git] / compiler / types / Type.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1998
4 %
5
6 Type - public interface
7
8 \begin{code}
9 {-# LANGUAGE CPP #-}
10 {-# OPTIONS_GHC -fno-warn-orphans #-}
11
12 -- | Main functions for manipulating types and type-related things
13 module Type (
14         -- Note some of this is just re-exports from TyCon..
15
16         -- * Main data types representing Types
17         -- $type_classification
18
19         -- $representation_types
20         TyThing(..), Type, KindOrType, PredType, ThetaType,
21         Var, TyVar, isTyVar,
22
23         -- ** Constructing and deconstructing types
24         mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe,
25
26         mkAppTy, mkAppTys, splitAppTy, splitAppTys,
27         splitAppTy_maybe, repSplitAppTy_maybe,
28
29         mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
30         splitFunTys, splitFunTysN,
31         funResultTy, funArgTy, zipFunTys,
32
33         mkTyConApp, mkTyConTy,
34         tyConAppTyCon_maybe, tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
35         splitTyConApp_maybe, splitTyConApp, tyConAppArgN,
36
37         mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
38         mkPiKinds, mkPiType, mkPiTypes,
39         applyTy, applyTys, applyTysD, applyTysX, dropForAlls,
40
41         mkNumLitTy, isNumLitTy,
42         mkStrLitTy, isStrLitTy,
43
44         coAxNthLHS,
45
46         -- (Newtypes)
47         newTyConInstRhs,
48
49         -- Pred types
50         mkFamilyTyConApp,
51         isDictLikeTy,
52         mkEqPred, mkCoerciblePred, mkPrimEqPred, mkReprPrimEqPred,
53         mkClassPred,
54         isClassPred, isEqPred,
55         isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
56
57         -- Deconstructing predicate types
58         PredTree(..), classifyPredType,
59         getClassPredTys, getClassPredTys_maybe,
60         getEqPredTys, getEqPredTys_maybe, getEqPredRole,
61
62         -- ** Common type constructors
63         funTyCon,
64
65         -- ** Predicates on types
66         isTypeVar, isKindVar, allDistinctTyVars, isForAllTy,
67         isTyVarTy, isFunTy, isDictTy, isPredTy, isVoidTy,
68
69         -- (Lifting and boxity)
70         isUnLiftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
71         isPrimitiveType, isStrictType,
72
73         -- * Main data types representing Kinds
74         -- $kind_subtyping
75         Kind, SimpleKind, MetaKindVar,
76
77         -- ** Finding the kind of a type
78         typeKind,
79
80         -- ** Common Kinds and SuperKinds
81         anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind,
82         constraintKind, superKind,
83
84         -- ** Common Kind type constructors
85         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
86         constraintKindTyCon, anyKindTyCon,
87
88         -- * Type free variables
89         tyVarsOfType, tyVarsOfTypes, closeOverKinds,
90         expandTypeSynonyms,
91         typeSize, varSetElemsKvsFirst,
92
93         -- * Type comparison
94         eqType, eqTypeX, eqTypes, cmpType, cmpTypes,
95         eqPred, eqPredX, cmpPred, eqKind, eqTyVarBndrs,
96
97         -- * Forcing evaluation of types
98         seqType, seqTypes,
99
100         -- * Other views onto Types
101         coreView, tcView,
102
103         UnaryType, RepType(..), flattenRepType, repType,
104         tyConsOfType,
105
106         -- * Type representation for the code generator
107         typePrimRep, typeRepArity,
108
109         -- * Main type substitution data types
110         TvSubstEnv,     -- Representation widely visible
111         TvSubst(..),    -- Representation visible to a few friends
112
113         -- ** Manipulating type substitutions
114         emptyTvSubstEnv, emptyTvSubst,
115
116         mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
117         getTvSubstEnv, setTvSubstEnv,
118         zapTvSubstEnv, getTvInScope,
119         extendTvInScope, extendTvInScopeList,
120         extendTvSubst, extendTvSubstList,
121         isInScope, composeTvSubst, zipTyEnv,
122         isEmptyTvSubst, unionTvSubst,
123
124         -- ** Performing substitution on types and kinds
125         substTy, substTys, substTyWith, substTysWith, substTheta,
126         substTyVar, substTyVars, substTyVarBndr,
127         cloneTyVarBndr, deShadowTy, lookupTyVar,
128         substKiWith, substKisWith,
129
130         -- * Pretty-printing
131         pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing,
132         pprTvBndr, pprTvBndrs, pprForAll, pprUserForAll, pprSigmaType,
133         pprTheta, pprThetaArrowTy, pprClassPred,
134         pprKind, pprParendKind, pprSourceTyCon,
135         TyPrec(..), maybeParen,
136
137         -- * Tidying type related things up for printing
138         tidyType,      tidyTypes,
139         tidyOpenType,  tidyOpenTypes,
140         tidyOpenKind,
141         tidyTyVarBndr, tidyTyVarBndrs, tidyFreeTyVars,
142         tidyOpenTyVar, tidyOpenTyVars,
143         tidyTyVarOcc,
144         tidyTopType,
145         tidyKind,
146     ) where
147
148 #include "HsVersions.h"
149
150 -- We import the representation and primitive functions from TypeRep.
151 -- Many things are reexported, but not the representation!
152
153 import Kind
154 import TypeRep
155
156 -- friends:
157 import Var
158 import VarEnv
159 import VarSet
160 import NameEnv
161
162 import Class
163 import TyCon
164 import TysPrim
165 import {-# SOURCE #-} TysWiredIn ( eqTyCon, coercibleTyCon, typeNatKind, typeSymbolKind )
166 import PrelNames ( eqTyConKey, coercibleTyConKey,
167                    ipClassNameKey, openTypeKindTyConKey,
168                    constraintKindTyConKey, liftedTypeKindTyConKey )
169 import CoAxiom
170
171 -- others
172 import Unique           ( Unique, hasKey )
173 import BasicTypes       ( Arity, RepArity )
174 import Util
175 import Outputable
176 import FastString
177
178 import Maybes           ( orElse )
179 import Data.Maybe       ( isJust )
180 import Control.Monad    ( guard )
181
182 infixr 3 `mkFunTy`      -- Associates to the right
183 \end{code}
184
185 \begin{code}
186 -- $type_classification
187 -- #type_classification#
188 --
189 -- Types are one of:
190 --
191 -- [Unboxed]            Iff its representation is other than a pointer
192 --                      Unboxed types are also unlifted.
193 --
194 -- [Lifted]             Iff it has bottom as an element.
195 --                      Closures always have lifted types: i.e. any
196 --                      let-bound identifier in Core must have a lifted
197 --                      type. Operationally, a lifted object is one that
198 --                      can be entered.
199 --                      Only lifted types may be unified with a type variable.
200 --
201 -- [Algebraic]          Iff it is a type with one or more constructors, whether
202 --                      declared with @data@ or @newtype@.
203 --                      An algebraic type is one that can be deconstructed
204 --                      with a case expression. This is /not/ the same as
205 --                      lifted types, because we also include unboxed
206 --                      tuples in this classification.
207 --
208 -- [Data]               Iff it is a type declared with @data@, or a boxed tuple.
209 --
210 -- [Primitive]          Iff it is a built-in type that can't be expressed in Haskell.
211 --
212 -- Currently, all primitive types are unlifted, but that's not necessarily
213 -- the case: for example, @Int@ could be primitive.
214 --
215 -- Some primitive types are unboxed, such as @Int#@, whereas some are boxed
216 -- but unlifted (such as @ByteArray#@).  The only primitive types that we
217 -- classify as algebraic are the unboxed tuples.
218 --
219 -- Some examples of type classifications that may make this a bit clearer are:
220 --
221 -- @
222 -- Type         primitive       boxed           lifted          algebraic
223 -- -----------------------------------------------------------------------------
224 -- Int#         Yes             No              No              No
225 -- ByteArray#   Yes             Yes             No              No
226 -- (\# a, b \#)   Yes             No              No              Yes
227 -- (  a, b  )   No              Yes             Yes             Yes
228 -- [a]          No              Yes             Yes             Yes
229 -- @
230
231 -- $representation_types
232 -- A /source type/ is a type that is a separate type as far as the type checker is
233 -- concerned, but which has a more low-level representation as far as Core-to-Core
234 -- passes and the rest of the back end is concerned.
235 --
236 -- You don't normally have to worry about this, as the utility functions in
237 -- this module will automatically convert a source into a representation type
238 -- if they are spotted, to the best of it's abilities. If you don't want this
239 -- to happen, use the equivalent functions from the "TcType" module.
240 \end{code}
241
242 %************************************************************************
243 %*                                                                      *
244                 Type representation
245 %*                                                                      *
246 %************************************************************************
247
248 \begin{code}
249 {-# INLINE coreView #-}
250 coreView :: Type -> Maybe Type
251 -- ^ In Core, we \"look through\" non-recursive newtypes and 'PredTypes': this
252 -- function tries to obtain a different view of the supplied type given this
253 --
254 -- Strips off the /top layer only/ of a type to give
255 -- its underlying representation type.
256 -- Returns Nothing if there is nothing to look through.
257 --
258 -- By being non-recursive and inlined, this case analysis gets efficiently
259 -- joined onto the case analysis that the caller is already doing
260 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
261               = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
262                -- Its important to use mkAppTys, rather than (foldl AppTy),
263                -- because the function part might well return a
264                -- partially-applied type constructor; indeed, usually will!
265 coreView _                 = Nothing
266
267 -----------------------------------------------
268 {-# INLINE tcView #-}
269 tcView :: Type -> Maybe Type
270 -- ^ Similar to 'coreView', but for the type checker, which just looks through synonyms
271 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
272                          = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
273 tcView _                 = Nothing
274   -- You might think that tcView belows in TcType rather than Type, but unfortunately
275   -- it is needed by Unify, which is turn imported by Coercion (for MatchEnv and matchList).
276   -- So we will leave it here to avoid module loops.
277
278 -----------------------------------------------
279 expandTypeSynonyms :: Type -> Type
280 -- ^ Expand out all type synonyms.  Actually, it'd suffice to expand out
281 -- just the ones that discard type variables (e.g.  type Funny a = Int)
282 -- But we don't know which those are currently, so we just expand all.
283 expandTypeSynonyms ty
284   = go ty
285   where
286     go (TyConApp tc tys)
287       | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
288       = go (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
289       | otherwise
290       = TyConApp tc (map go tys)
291     go (LitTy l)       = LitTy l
292     go (TyVarTy tv)    = TyVarTy tv
293     go (AppTy t1 t2)   = mkAppTy (go t1) (go t2)
294     go (FunTy t1 t2)   = FunTy (go t1) (go t2)
295     go (ForAllTy tv t) = ForAllTy tv (go t)
296 \end{code}
297
298
299 %************************************************************************
300 %*                                                                      *
301 \subsection{Constructor-specific functions}
302 %*                                                                      *
303 %************************************************************************
304
305
306 ---------------------------------------------------------------------
307                                 TyVarTy
308                                 ~~~~~~~
309 \begin{code}
310 -- | Attempts to obtain the type variable underlying a 'Type', and panics with the
311 -- given message if this is not a type variable type. See also 'getTyVar_maybe'
312 getTyVar :: String -> Type -> TyVar
313 getTyVar msg ty = case getTyVar_maybe ty of
314                     Just tv -> tv
315                     Nothing -> panic ("getTyVar: " ++ msg)
316
317 isTyVarTy :: Type -> Bool
318 isTyVarTy ty = isJust (getTyVar_maybe ty)
319
320 -- | Attempts to obtain the type variable underlying a 'Type'
321 getTyVar_maybe :: Type -> Maybe TyVar
322 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
323 getTyVar_maybe (TyVarTy tv)                 = Just tv
324 getTyVar_maybe _                            = Nothing
325
326 allDistinctTyVars :: [KindOrType] -> Bool
327 allDistinctTyVars tkvs = go emptyVarSet tkvs
328   where
329     go _      [] = True
330     go so_far (ty : tys)
331        = case getTyVar_maybe ty of
332              Nothing -> False
333              Just tv | tv `elemVarSet` so_far -> False
334                      | otherwise -> go (so_far `extendVarSet` tv) tys
335 \end{code}
336
337
338 ---------------------------------------------------------------------
339                                 AppTy
340                                 ~~~~~
341 We need to be pretty careful with AppTy to make sure we obey the
342 invariant that a TyConApp is always visibly so.  mkAppTy maintains the
343 invariant: use it.
344
345 \begin{code}
346 -- | Applies a type to another, as in e.g. @k a@
347 mkAppTy :: Type -> Type -> Type
348 mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
349 mkAppTy ty1               ty2 = AppTy ty1 ty2
350         -- Note that the TyConApp could be an
351         -- under-saturated type synonym.  GHC allows that; e.g.
352         --      type Foo k = k a -> k a
353         --      type Id x = x
354         --      foo :: Foo Id -> Foo Id
355         --
356         -- Here Id is partially applied in the type sig for Foo,
357         -- but once the type synonyms are expanded all is well
358
359 mkAppTys :: Type -> [Type] -> Type
360 mkAppTys ty1                []   = ty1
361 mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
362 mkAppTys ty1                tys2 = foldl AppTy ty1 tys2
363
364 -------------
365 splitAppTy_maybe :: Type -> Maybe (Type, Type)
366 -- ^ Attempt to take a type application apart, whether it is a
367 -- function, type constructor, or plain type application. Note
368 -- that type family applications are NEVER unsaturated by this!
369 splitAppTy_maybe ty | Just ty' <- coreView ty
370                     = splitAppTy_maybe ty'
371 splitAppTy_maybe ty = repSplitAppTy_maybe ty
372
373 -------------
374 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
375 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
376 -- any Core view stuff is already done
377 repSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
378 repSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
379 repSplitAppTy_maybe (TyConApp tc tys)
380   | isDecomposableTyCon tc || tys `lengthExceeds` tyConArity tc
381   , Just (tys', ty') <- snocView tys
382   = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
383 repSplitAppTy_maybe _other = Nothing
384 -------------
385 splitAppTy :: Type -> (Type, Type)
386 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
387 -- and panics if this is not possible
388 splitAppTy ty = case splitAppTy_maybe ty of
389                 Just pr -> pr
390                 Nothing -> panic "splitAppTy"
391
392 -------------
393 splitAppTys :: Type -> (Type, [Type])
394 -- ^ Recursively splits a type as far as is possible, leaving a residual
395 -- type being applied to and the type arguments applied to it. Never fails,
396 -- even if that means returning an empty list of type applications.
397 splitAppTys ty = split ty ty []
398   where
399     split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
400     split _       (AppTy ty arg)        args = split ty ty (arg:args)
401     split _       (TyConApp tc tc_args) args
402       = let -- keep type families saturated
403             n | isDecomposableTyCon tc = 0
404               | otherwise              = tyConArity tc
405             (tc_args1, tc_args2) = splitAt n tc_args
406         in
407         (TyConApp tc tc_args1, tc_args2 ++ args)
408     split _       (FunTy ty1 ty2)       args = ASSERT( null args )
409                                                (TyConApp funTyCon [], [ty1,ty2])
410     split orig_ty _                     args = (orig_ty, args)
411
412 \end{code}
413
414
415                       LitTy
416                       ~~~~~
417
418 \begin{code}
419 mkNumLitTy :: Integer -> Type
420 mkNumLitTy n = LitTy (NumTyLit n)
421
422 -- | Is this a numeric literal. We also look through type synonyms.
423 isNumLitTy :: Type -> Maybe Integer
424 isNumLitTy ty | Just ty1 <- tcView ty = isNumLitTy ty1
425 isNumLitTy (LitTy (NumTyLit n)) = Just n
426 isNumLitTy _                    = Nothing
427
428 mkStrLitTy :: FastString -> Type
429 mkStrLitTy s = LitTy (StrTyLit s)
430
431 -- | Is this a symbol literal. We also look through type synonyms.
432 isStrLitTy :: Type -> Maybe FastString
433 isStrLitTy ty | Just ty1 <- tcView ty = isStrLitTy ty1
434 isStrLitTy (LitTy (StrTyLit s)) = Just s
435 isStrLitTy _                    = Nothing
436
437 \end{code}
438
439
440 ---------------------------------------------------------------------
441                                 FunTy
442                                 ~~~~~
443
444 \begin{code}
445 mkFunTy :: Type -> Type -> Type
446 -- ^ Creates a function type from the given argument and result type
447 mkFunTy arg res = FunTy arg res
448
449 mkFunTys :: [Type] -> Type -> Type
450 mkFunTys tys ty = foldr mkFunTy ty tys
451
452 isFunTy :: Type -> Bool
453 isFunTy ty = isJust (splitFunTy_maybe ty)
454
455 splitFunTy :: Type -> (Type, Type)
456 -- ^ Attempts to extract the argument and result types from a type, and
457 -- panics if that is not possible. See also 'splitFunTy_maybe'
458 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
459 splitFunTy (FunTy arg res) = (arg, res)
460 splitFunTy other           = pprPanic "splitFunTy" (ppr other)
461
462 splitFunTy_maybe :: Type -> Maybe (Type, Type)
463 -- ^ Attempts to extract the argument and result types from a type
464 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
465 splitFunTy_maybe (FunTy arg res)   = Just (arg, res)
466 splitFunTy_maybe _                 = Nothing
467
468 splitFunTys :: Type -> ([Type], Type)
469 splitFunTys ty = split [] ty ty
470   where
471     split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
472     split args _       (FunTy arg res)   = split (arg:args) res res
473     split args orig_ty _                 = (reverse args, orig_ty)
474
475 splitFunTysN :: Int -> Type -> ([Type], Type)
476 -- ^ Split off exactly the given number argument types, and panics if that is not possible
477 splitFunTysN 0 ty = ([], ty)
478 splitFunTysN n ty = ASSERT2( isFunTy ty, int n <+> ppr ty )
479                     case splitFunTy ty of { (arg, res) ->
480                     case splitFunTysN (n-1) res of { (args, res) ->
481                     (arg:args, res) }}
482
483 -- | Splits off argument types from the given type and associating
484 -- them with the things in the input list from left to right. The
485 -- final result type is returned, along with the resulting pairs of
486 -- objects and types, albeit with the list of pairs in reverse order.
487 -- Panics if there are not enough argument types for the input list.
488 zipFunTys :: Outputable a => [a] -> Type -> ([(a, Type)], Type)
489 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
490   where
491     split acc []     nty _                 = (reverse acc, nty)
492     split acc xs     nty ty
493           | Just ty' <- coreView ty        = split acc xs nty ty'
494     split acc (x:xs) _   (FunTy arg res)   = split ((x,arg):acc) xs res res
495     split _   _      _   _                 = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
496
497 funResultTy :: Type -> Type
498 -- ^ Extract the function result type and panic if that is not possible
499 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
500 funResultTy (FunTy _arg res)  = res
501 funResultTy ty                = pprPanic "funResultTy" (ppr ty)
502
503 funArgTy :: Type -> Type
504 -- ^ Extract the function argument type and panic if that is not possible
505 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
506 funArgTy (FunTy arg _res)  = arg
507 funArgTy ty                = pprPanic "funArgTy" (ppr ty)
508 \end{code}
509
510 ---------------------------------------------------------------------
511                                 TyConApp
512                                 ~~~~~~~~
513
514 \begin{code}
515 -- | A key function: builds a 'TyConApp' or 'FunTy' as appropriate to
516 -- its arguments.  Applies its arguments to the constructor from left to right.
517 mkTyConApp :: TyCon -> [Type] -> Type
518 mkTyConApp tycon tys
519   | isFunTyCon tycon, [ty1,ty2] <- tys
520   = FunTy ty1 ty2
521
522   | otherwise
523   = TyConApp tycon tys
524
525 -- splitTyConApp "looks through" synonyms, because they don't
526 -- mean a distinct type, but all other type-constructor applications
527 -- including functions are returned as Just ..
528
529 -- | The same as @fst . splitTyConApp@
530 tyConAppTyCon_maybe :: Type -> Maybe TyCon
531 tyConAppTyCon_maybe ty | Just ty' <- coreView ty = tyConAppTyCon_maybe ty'
532 tyConAppTyCon_maybe (TyConApp tc _) = Just tc
533 tyConAppTyCon_maybe (FunTy {})      = Just funTyCon
534 tyConAppTyCon_maybe _               = Nothing
535
536 tyConAppTyCon :: Type -> TyCon
537 tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr ty)
538
539 -- | The same as @snd . splitTyConApp@
540 tyConAppArgs_maybe :: Type -> Maybe [Type]
541 tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty'
542 tyConAppArgs_maybe (TyConApp _ tys) = Just tys
543 tyConAppArgs_maybe (FunTy arg res)  = Just [arg,res]
544 tyConAppArgs_maybe _                = Nothing
545
546
547 tyConAppArgs :: Type -> [Type]
548 tyConAppArgs ty = tyConAppArgs_maybe ty `orElse` pprPanic "tyConAppArgs" (ppr ty)
549
550 tyConAppArgN :: Int -> Type -> Type
551 -- Executing Nth
552 tyConAppArgN n ty
553   = case tyConAppArgs_maybe ty of
554       Just tys -> ASSERT2( n < length tys, ppr n <+> ppr tys ) tys !! n
555       Nothing  -> pprPanic "tyConAppArgN" (ppr n <+> ppr ty)
556
557 -- | Attempts to tease a type apart into a type constructor and the application
558 -- of a number of arguments to that constructor. Panics if that is not possible.
559 -- See also 'splitTyConApp_maybe'
560 splitTyConApp :: Type -> (TyCon, [Type])
561 splitTyConApp ty = case splitTyConApp_maybe ty of
562                    Just stuff -> stuff
563                    Nothing    -> pprPanic "splitTyConApp" (ppr ty)
564
565 -- | Attempts to tease a type apart into a type constructor and the application
566 -- of a number of arguments to that constructor
567 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
568 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
569 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
570 splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
571 splitTyConApp_maybe _                 = Nothing
572
573 newTyConInstRhs :: TyCon -> [Type] -> Type
574 -- ^ Unwrap one 'layer' of newtype on a type constructor and its
575 -- arguments, using an eta-reduced version of the @newtype@ if possible.
576 -- This requires tys to have at least @newTyConInstArity tycon@ elements.
577 newTyConInstRhs tycon tys
578     = ASSERT2( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs )
579       applyTysX tvs rhs tys
580   where
581     (tvs, rhs) = newTyConEtadRhs tycon
582 \end{code}
583
584
585 ---------------------------------------------------------------------
586                                 SynTy
587                                 ~~~~~
588
589 Notes on type synonyms
590 ~~~~~~~~~~~~~~~~~~~~~~
591 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
592 to return type synonyms wherever possible. Thus
593
594         type Foo a = a -> a
595
596 we want
597         splitFunTys (a -> Foo a) = ([a], Foo a)
598 not                                ([a], a -> a)
599
600 The reason is that we then get better (shorter) type signatures in
601 interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
602
603
604                 Representation types
605                 ~~~~~~~~~~~~~~~~~~~~
606
607 Note [Nullary unboxed tuple]
608 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
609 We represent the nullary unboxed tuple as the unary (but void) type
610 Void#.  The reason for this is that the ReprArity is never
611 less than the Arity (as it would otherwise be for a function type like
612 (# #) -> Int).
613
614 As a result, ReprArity is always strictly positive if Arity is. This
615 is important because it allows us to distinguish at runtime between a
616 thunk and a function takes a nullary unboxed tuple as an argument!
617
618 \begin{code}
619 type UnaryType = Type
620
621 data RepType = UbxTupleRep [UnaryType] -- INVARIANT: never an empty list (see Note [Nullary unboxed tuple])
622              | UnaryRep UnaryType
623
624 flattenRepType :: RepType -> [UnaryType]
625 flattenRepType (UbxTupleRep tys) = tys
626 flattenRepType (UnaryRep ty)     = [ty]
627
628 -- | Looks through:
629 --
630 --      1. For-alls
631 --      2. Synonyms
632 --      3. Predicates
633 --      4. All newtypes, including recursive ones, but not newtype families
634 --
635 -- It's useful in the back end of the compiler.
636 repType :: Type -> RepType
637 repType ty
638   = go initRecTc ty
639   where
640     go :: RecTcChecker -> Type -> RepType
641     go rec_nts ty                       -- Expand predicates and synonyms
642       | Just ty' <- coreView ty
643       = go rec_nts ty'
644
645     go rec_nts (ForAllTy _ ty)          -- Drop foralls
646         = go rec_nts ty
647
648     go rec_nts (TyConApp tc tys)        -- Expand newtypes
649       | isNewTyCon tc
650       , tys `lengthAtLeast` tyConArity tc
651       , Just rec_nts' <- checkRecTc rec_nts tc   -- See Note [Expanding newtypes] in TyCon
652       = go rec_nts' (newTyConInstRhs tc tys)
653
654       | isUnboxedTupleTyCon tc
655       = if null tys
656          then UnaryRep voidPrimTy -- See Note [Nullary unboxed tuple]
657          else UbxTupleRep (concatMap (flattenRepType . go rec_nts) tys)
658
659     go _ ty = UnaryRep ty
660
661
662 -- | All type constructors occurring in the type; looking through type
663 --   synonyms, but not newtypes.
664 --  When it finds a Class, it returns the class TyCon.
665 tyConsOfType :: Type -> NameEnv TyCon
666 tyConsOfType ty
667   = go ty
668   where
669      go :: Type -> NameEnv TyCon  -- The NameEnv does duplicate elim
670      go ty | Just ty' <- tcView ty = go ty'
671      go (TyVarTy {})               = emptyNameEnv
672      go (LitTy {})                 = emptyNameEnv
673      go (TyConApp tc tys)          = go_tc tc tys
674      go (AppTy a b)                = go a `plusNameEnv` go b
675      go (FunTy a b)                = go a `plusNameEnv` go b
676      go (ForAllTy _ ty)            = go ty
677
678      go_tc tc tys = extendNameEnv (go_s tys) (tyConName tc) tc
679      go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
680
681 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
682 -- of inspecting the type directly.
683
684 -- | Discovers the primitive representation of a more abstract 'UnaryType'
685 typePrimRep :: UnaryType -> PrimRep
686 typePrimRep ty
687   = case repType ty of
688       UbxTupleRep _ -> pprPanic "typePrimRep: UbxTupleRep" (ppr ty)
689       UnaryRep rep -> case rep of
690         TyConApp tc _ -> tyConPrimRep tc
691         FunTy _ _     -> PtrRep
692         AppTy _ _     -> PtrRep      -- See Note [AppTy rep]
693         TyVarTy _     -> PtrRep
694         _             -> pprPanic "typePrimRep: UnaryRep" (ppr ty)
695
696 typeRepArity :: Arity -> Type -> RepArity
697 typeRepArity 0 _ = 0
698 typeRepArity n ty = case repType ty of
699   UnaryRep (FunTy ty1 ty2) -> length (flattenRepType (repType ty1)) + typeRepArity (n - 1) ty2
700   _                        -> pprPanic "typeRepArity: arity greater than type can handle" (ppr (n, ty))
701
702 isVoidTy :: Type -> Bool
703 -- True if the type has zero width
704 isVoidTy ty = case repType ty of
705                 UnaryRep (TyConApp tc _) -> isVoidRep (tyConPrimRep tc)
706                 _                        -> False
707 \end{code}
708
709 Note [AppTy rep]
710 ~~~~~~~~~~~~~~~~
711 Types of the form 'f a' must be of kind *, not #, so we are guaranteed
712 that they are represented by pointers.  The reason is that f must have
713 kind (kk -> kk) and kk cannot be unlifted; see Note [The kind invariant]
714 in TypeRep.
715
716 ---------------------------------------------------------------------
717                                 ForAllTy
718                                 ~~~~~~~~
719
720 \begin{code}
721 mkForAllTy :: TyVar -> Type -> Type
722 mkForAllTy tyvar ty
723   = ForAllTy tyvar ty
724
725 -- | Wraps foralls over the type using the provided 'TyVar's from left to right
726 mkForAllTys :: [TyVar] -> Type -> Type
727 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
728
729 mkPiKinds :: [TyVar] -> Kind -> Kind
730 -- mkPiKinds [k1, k2, (a:k1 -> *)] k2
731 -- returns forall k1 k2. (k1 -> *) -> k2
732 mkPiKinds [] res = res
733 mkPiKinds (tv:tvs) res
734   | isKindVar tv = ForAllTy tv          (mkPiKinds tvs res)
735   | otherwise    = FunTy (tyVarKind tv) (mkPiKinds tvs res)
736
737 mkPiType  :: Var -> Type -> Type
738 -- ^ Makes a @(->)@ type or a forall type, depending
739 -- on whether it is given a type variable or a term variable.
740 mkPiTypes :: [Var] -> Type -> Type
741 -- ^ 'mkPiType' for multiple type or value arguments
742
743 mkPiType v ty
744    | isId v    = mkFunTy (varType v) ty
745    | otherwise = mkForAllTy v ty
746
747 mkPiTypes vs ty = foldr mkPiType ty vs
748
749 isForAllTy :: Type -> Bool
750 isForAllTy (ForAllTy _ _) = True
751 isForAllTy _              = False
752
753 -- | Attempts to take a forall type apart, returning the bound type variable
754 -- and the remainder of the type
755 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
756 splitForAllTy_maybe ty = splitFAT_m ty
757   where
758     splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
759     splitFAT_m (ForAllTy tyvar ty)          = Just(tyvar, ty)
760     splitFAT_m _                            = Nothing
761
762 -- | Attempts to take a forall type apart, returning all the immediate such bound
763 -- type variables and the remainder of the type. Always suceeds, even if that means
764 -- returning an empty list of 'TyVar's
765 splitForAllTys :: Type -> ([TyVar], Type)
766 splitForAllTys ty = split ty ty []
767    where
768      split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
769      split _       (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
770      split orig_ty _                 tvs = (reverse tvs, orig_ty)
771
772 -- | Equivalent to @snd . splitForAllTys@
773 dropForAlls :: Type -> Type
774 dropForAlls ty = snd (splitForAllTys ty)
775 \end{code}
776
777 -- (mkPiType now in CoreUtils)
778
779 applyTy, applyTys
780 ~~~~~~~~~~~~~~~~~
781
782 \begin{code}
783 -- | Instantiate a forall type with one or more type arguments.
784 -- Used when we have a polymorphic function applied to type args:
785 --
786 -- > f t1 t2
787 --
788 -- We use @applyTys type-of-f [t1,t2]@ to compute the type of the expression.
789 -- Panics if no application is possible.
790 applyTy :: Type -> KindOrType -> Type
791 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
792 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
793 applyTy _                _   = panic "applyTy"
794
795 applyTys :: Type -> [KindOrType] -> Type
796 -- ^ This function is interesting because:
797 --
798 --      1. The function may have more for-alls than there are args
799 --
800 --      2. Less obviously, it may have fewer for-alls
801 --
802 -- For case 2. think of:
803 --
804 -- > applyTys (forall a.a) [forall b.b, Int]
805 --
806 -- This really can happen, but only (I think) in situations involving
807 -- undefined.  For example:
808 --       undefined :: forall a. a
809 -- Term: undefined @(forall b. b->b) @Int
810 -- This term should have type (Int -> Int), but notice that
811 -- there are more type args than foralls in 'undefined's type.
812
813 -- If you edit this function, you may need to update the GHC formalism
814 -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
815 applyTys ty args = applyTysD empty ty args
816
817 applyTysD :: SDoc -> Type -> [Type] -> Type     -- Debug version
818 applyTysD _   orig_fun_ty []      = orig_fun_ty
819 applyTysD doc orig_fun_ty arg_tys
820   | n_tvs == n_args     -- The vastly common case
821   = substTyWith tvs arg_tys rho_ty
822   | n_tvs > n_args      -- Too many for-alls
823   = substTyWith (take n_args tvs) arg_tys
824                 (mkForAllTys (drop n_args tvs) rho_ty)
825   | otherwise           -- Too many type args
826   = ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty $$ ppr arg_tys )        -- Zero case gives infinite loop!
827     applyTysD doc (substTyWith tvs (take n_tvs arg_tys) rho_ty)
828                   (drop n_tvs arg_tys)
829   where
830     (tvs, rho_ty) = splitForAllTys orig_fun_ty
831     n_tvs  = length tvs
832     n_args = length arg_tys
833
834 applyTysX :: [TyVar] -> Type -> [Type] -> Type
835 -- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
836 applyTysX tvs body_ty arg_tys
837   = ASSERT2( length arg_tys >= n_tvs, ppr tvs $$ ppr body_ty $$ ppr arg_tys )
838     mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
839              (drop n_tvs arg_tys)
840   where
841     n_tvs = length tvs
842 \end{code}
843
844
845 %************************************************************************
846 %*                                                                      *
847                          Pred
848 %*                                                                      *
849 %************************************************************************
850
851 Predicates on PredType
852
853 \begin{code}
854 isPredTy :: Type -> Bool
855   -- NB: isPredTy is used when printing types, which can happen in debug printing
856   --     during type checking of not-fully-zonked types.  So it's not cool to say
857   --     isConstraintKind (typeKind ty) because absent zonking the type might 
858   --     be ill-kinded, and typeKind crashes
859   --     Hence the rather tiresome story here
860 isPredTy ty = go ty []
861   where
862     go :: Type -> [KindOrType] -> Bool
863     go (AppTy ty1 ty2)   args = go ty1 (ty2 : args)
864     go (TyConApp tc tys) args = go_k (tyConKind tc) (tys ++ args)
865     go (TyVarTy tv)      args = go_k (tyVarKind tv) args
866     go _                 _    = False
867
868     go_k :: Kind -> [KindOrType] -> Bool
869     -- True <=> kind is k1 -> .. -> kn -> Constraint
870     go_k k                [] = isConstraintKind k
871     go_k (FunTy _ k1)     (_ :args) = go_k k1 args
872     go_k (ForAllTy kv k1) (k2:args) = go_k (substKiWith [kv] [k2] k1) args
873     go_k _ _ = False                  -- Typeable * Int :: Constraint
874
875 isClassPred, isEqPred, isIPPred :: PredType -> Bool
876 isClassPred ty = case tyConAppTyCon_maybe ty of
877     Just tyCon | isClassTyCon tyCon -> True
878     _                               -> False
879 isEqPred ty = case tyConAppTyCon_maybe ty of
880     Just tyCon -> tyCon `hasKey` eqTyConKey
881     _          -> False
882
883 isIPPred ty = case tyConAppTyCon_maybe ty of
884     Just tc -> isIPTyCon tc
885     _       -> False
886
887 isIPTyCon :: TyCon -> Bool
888 isIPTyCon tc = tc `hasKey` ipClassNameKey
889
890 isIPClass :: Class -> Bool
891 isIPClass cls = cls `hasKey` ipClassNameKey
892   -- Class and it corresponding TyCon have the same Unique
893
894 isIPPred_maybe :: Type -> Maybe (FastString, Type)
895 isIPPred_maybe ty =
896   do (tc,[t1,t2]) <- splitTyConApp_maybe ty
897      guard (isIPTyCon tc)
898      x <- isStrLitTy t1
899      return (x,t2)
900 \end{code}
901
902 Make PredTypes
903
904 --------------------- Equality types ---------------------------------
905 \begin{code}
906 -- | Creates a type equality predicate
907 mkEqPred :: Type -> Type -> PredType
908 mkEqPred ty1 ty2
909   = WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 $$ ppr k $$ ppr (typeKind ty2) )
910     TyConApp eqTyCon [k, ty1, ty2]
911   where
912     k = typeKind ty1
913
914 mkCoerciblePred :: Type -> Type -> PredType
915 mkCoerciblePred ty1 ty2
916   = WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 $$ ppr k $$ ppr (typeKind ty2) )
917     TyConApp coercibleTyCon [k, ty1, ty2]
918   where
919     k = typeKind ty1
920
921 mkPrimEqPred :: Type -> Type -> Type
922 mkPrimEqPred ty1  ty2
923   = WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 )
924     TyConApp eqPrimTyCon [k, ty1, ty2]
925   where
926     k = typeKind ty1
927
928 mkReprPrimEqPred :: Type -> Type -> Type
929 mkReprPrimEqPred ty1  ty2
930   = WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 )
931     TyConApp eqReprPrimTyCon [k, ty1, ty2]
932   where
933     k = typeKind ty1
934 \end{code}
935
936 --------------------- Dictionary types ---------------------------------
937 \begin{code}
938 mkClassPred :: Class -> [Type] -> PredType
939 mkClassPred clas tys = TyConApp (classTyCon clas) tys
940
941 isDictTy :: Type -> Bool
942 isDictTy = isClassPred
943
944 isDictLikeTy :: Type -> Bool
945 -- Note [Dictionary-like types]
946 isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
947 isDictLikeTy ty = case splitTyConApp_maybe ty of
948         Just (tc, tys) | isClassTyCon tc -> True
949                        | isTupleTyCon tc -> all isDictLikeTy tys
950         _other                           -> False
951 \end{code}
952
953 Note [Dictionary-like types]
954 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
955 Being "dictionary-like" means either a dictionary type or a tuple thereof.
956 In GHC 6.10 we build implication constraints which construct such tuples,
957 and if we land up with a binding
958     t :: (C [a], Eq [a])
959     t = blah
960 then we want to treat t as cheap under "-fdicts-cheap" for example.
961 (Implication constraints are normally inlined, but sadly not if the
962 occurrence is itself inside an INLINE function!  Until we revise the
963 handling of implication constraints, that is.)  This turned out to
964 be important in getting good arities in DPH code.  Example:
965
966     class C a
967     class D a where { foo :: a -> a }
968     instance C a => D (Maybe a) where { foo x = x }
969
970     bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
971     {-# INLINE bar #-}
972     bar x y = (foo (Just x), foo (Just y))
973
974 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
975 we ended up with something like
976    bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
977                                 in \x,y. <blah>)
978
979 This is all a bit ad-hoc; eg it relies on knowing that implication
980 constraints build tuples.
981
982
983 Decomposing PredType
984
985 \begin{code}
986 data PredTree = ClassPred Class [Type]
987               | EqPred Type Type
988               | TuplePred [PredType]
989               | IrredPred PredType
990
991 classifyPredType :: PredType -> PredTree
992 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
993     Just (tc, tys) | Just clas <- tyConClass_maybe tc
994                    -> ClassPred clas tys
995     Just (tc, tys) | tc `hasKey` eqTyConKey
996                    , let [_, ty1, ty2] = tys
997                    -> EqPred ty1 ty2
998     Just (tc, tys) | isTupleTyCon tc
999                    -> TuplePred tys
1000     _ -> IrredPred ev_ty
1001 \end{code}
1002
1003 \begin{code}
1004 getClassPredTys :: PredType -> (Class, [Type])
1005 getClassPredTys ty = case getClassPredTys_maybe ty of
1006         Just (clas, tys) -> (clas, tys)
1007         Nothing          -> pprPanic "getClassPredTys" (ppr ty)
1008
1009 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
1010 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
1011         Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
1012         _ -> Nothing
1013
1014 getEqPredTys :: PredType -> (Type, Type)
1015 getEqPredTys ty
1016   = case splitTyConApp_maybe ty of
1017       Just (tc, (_ : ty1 : ty2 : tys)) ->
1018         ASSERT( null tys && (tc `hasKey` eqTyConKey || tc `hasKey` coercibleTyConKey) )
1019         (ty1, ty2)
1020       _ -> pprPanic "getEqPredTys" (ppr ty)
1021
1022 getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
1023 getEqPredTys_maybe ty
1024   = case splitTyConApp_maybe ty of
1025       Just (tc, [_, ty1, ty2])
1026         | tc `hasKey` eqTyConKey -> Just (Nominal, ty1, ty2)
1027         | tc `hasKey` coercibleTyConKey -> Just (Representational, ty1, ty2)
1028       _ -> Nothing
1029
1030 getEqPredRole :: PredType -> Role
1031 getEqPredRole ty
1032   = case splitTyConApp_maybe ty of
1033       Just (tc, [_, _, _])
1034         | tc `hasKey` eqTyConKey -> Nominal
1035         | tc `hasKey` coercibleTyConKey -> Representational
1036       _ -> pprPanic "getEqPredRole" (ppr ty)
1037
1038 \end{code}
1039
1040 %************************************************************************
1041 %*                                                                      *
1042                    Size
1043 %*                                                                      *
1044 %************************************************************************
1045
1046 \begin{code}
1047 typeSize :: Type -> Int
1048 typeSize (LitTy {})      = 1
1049 typeSize (TyVarTy {})    = 1
1050 typeSize (AppTy t1 t2)   = typeSize t1 + typeSize t2
1051 typeSize (FunTy t1 t2)   = typeSize t1 + typeSize t2
1052 typeSize (ForAllTy _ t)  = 1 + typeSize t
1053 typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
1054 \end{code}
1055
1056
1057 %************************************************************************
1058 %*                                                                      *
1059 \subsection{Type families}
1060 %*                                                                      *
1061 %************************************************************************
1062
1063 \begin{code}
1064 mkFamilyTyConApp :: TyCon -> [Type] -> Type
1065 -- ^ Given a family instance TyCon and its arg types, return the
1066 -- corresponding family type.  E.g:
1067 --
1068 -- > data family T a
1069 -- > data instance T (Maybe b) = MkT b
1070 --
1071 -- Where the instance tycon is :RTL, so:
1072 --
1073 -- > mkFamilyTyConApp :RTL Int  =  T (Maybe Int)
1074 mkFamilyTyConApp tc tys
1075   | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
1076   , let tvs = tyConTyVars tc
1077         fam_subst = ASSERT2( length tvs == length tys, ppr tc <+> ppr tys )
1078                     zipTopTvSubst tvs tys
1079   = mkTyConApp fam_tc (substTys fam_subst fam_tys)
1080   | otherwise
1081   = mkTyConApp tc tys
1082
1083 -- | Get the type on the LHS of a coercion induced by a type/data
1084 -- family instance.
1085 coAxNthLHS :: CoAxiom br -> Int -> Type
1086 coAxNthLHS ax ind =
1087   mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind))
1088
1089 -- | Pretty prints a 'TyCon', using the family instance in case of a
1090 -- representation tycon.  For example:
1091 --
1092 -- > data T [a] = ...
1093 --
1094 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
1095 pprSourceTyCon :: TyCon -> SDoc
1096 pprSourceTyCon tycon
1097   | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
1098   = ppr $ fam_tc `TyConApp` tys        -- can't be FunTyCon
1099   | otherwise
1100   = ppr tycon
1101 \end{code}
1102
1103 %************************************************************************
1104 %*                                                                      *
1105 \subsection{Liftedness}
1106 %*                                                                      *
1107 %************************************************************************
1108
1109 \begin{code}
1110 -- | See "Type#type_classification" for what an unlifted type is
1111 isUnLiftedType :: Type -> Bool
1112         -- isUnLiftedType returns True for forall'd unlifted types:
1113         --      x :: forall a. Int#
1114         -- I found bindings like these were getting floated to the top level.
1115         -- They are pretty bogus types, mind you.  It would be better never to
1116         -- construct them
1117
1118 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
1119 isUnLiftedType (ForAllTy _ ty)      = isUnLiftedType ty
1120 isUnLiftedType (TyConApp tc _)      = isUnLiftedTyCon tc
1121 isUnLiftedType _                    = False
1122
1123 isUnboxedTupleType :: Type -> Bool
1124 isUnboxedTupleType ty = case tyConAppTyCon_maybe ty of
1125                            Just tc -> isUnboxedTupleTyCon tc
1126                            _       -> False
1127
1128 -- | See "Type#type_classification" for what an algebraic type is.
1129 -- Should only be applied to /types/, as opposed to e.g. partially
1130 -- saturated type constructors
1131 isAlgType :: Type -> Bool
1132 isAlgType ty
1133   = case splitTyConApp_maybe ty of
1134       Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1135                             isAlgTyCon tc
1136       _other             -> False
1137
1138 -- | See "Type#type_classification" for what an algebraic type is.
1139 -- Should only be applied to /types/, as opposed to e.g. partially
1140 -- saturated type constructors. Closed type constructors are those
1141 -- with a fixed right hand side, as opposed to e.g. associated types
1142 isClosedAlgType :: Type -> Bool
1143 isClosedAlgType ty
1144   = case splitTyConApp_maybe ty of
1145       Just (tc, ty_args) | isAlgTyCon tc && not (isFamilyTyCon tc)
1146              -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
1147       _other -> False
1148 \end{code}
1149
1150 \begin{code}
1151 -- | Computes whether an argument (or let right hand side) should
1152 -- be computed strictly or lazily, based only on its type.
1153 -- Currently, it's just 'isUnLiftedType'.
1154
1155 isStrictType :: Type -> Bool
1156 isStrictType = isUnLiftedType
1157 \end{code}
1158
1159 \begin{code}
1160 isPrimitiveType :: Type -> Bool
1161 -- ^ Returns true of types that are opaque to Haskell.
1162 isPrimitiveType ty = case splitTyConApp_maybe ty of
1163                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1164                                               isPrimTyCon tc
1165                         _                  -> False
1166 \end{code}
1167
1168
1169 %************************************************************************
1170 %*                                                                      *
1171 \subsection{Sequencing on types}
1172 %*                                                                      *
1173 %************************************************************************
1174
1175 \begin{code}
1176 seqType :: Type -> ()
1177 seqType (LitTy n)         = n `seq` ()
1178 seqType (TyVarTy tv)      = tv `seq` ()
1179 seqType (AppTy t1 t2)     = seqType t1 `seq` seqType t2
1180 seqType (FunTy t1 t2)     = seqType t1 `seq` seqType t2
1181 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
1182 seqType (ForAllTy tv ty)  = seqType (tyVarKind tv) `seq` seqType ty
1183
1184 seqTypes :: [Type] -> ()
1185 seqTypes []       = ()
1186 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
1187 \end{code}
1188
1189
1190 %************************************************************************
1191 %*                                                                      *
1192                 Comparison for types
1193         (We don't use instances so that we know where it happens)
1194 %*                                                                      *
1195 %************************************************************************
1196
1197 \begin{code}
1198 eqKind :: Kind -> Kind -> Bool
1199 -- Watch out for horrible hack: See Note [Comparison with OpenTypeKind]
1200 eqKind = eqType
1201
1202 eqType :: Type -> Type -> Bool
1203 -- ^ Type equality on source types. Does not look through @newtypes@ or
1204 -- 'PredType's, but it does look through type synonyms.
1205 -- Watch out for horrible hack: See Note [Comparison with OpenTypeKind]
1206 eqType t1 t2 = isEqual $ cmpType t1 t2
1207
1208 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
1209 eqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
1210
1211 eqTypes :: [Type] -> [Type] -> Bool
1212 eqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
1213
1214 eqPred :: PredType -> PredType -> Bool
1215 eqPred = eqType
1216
1217 eqPredX :: RnEnv2 -> PredType -> PredType -> Bool
1218 eqPredX env p1 p2 = isEqual $ cmpTypeX env p1 p2
1219
1220 eqTyVarBndrs :: RnEnv2 -> [TyVar] -> [TyVar] -> Maybe RnEnv2
1221 -- Check that the tyvar lists are the same length
1222 -- and have matching kinds; if so, extend the RnEnv2
1223 -- Returns Nothing if they don't match
1224 eqTyVarBndrs env [] []
1225  = Just env
1226 eqTyVarBndrs env (tv1:tvs1) (tv2:tvs2)
1227  | eqTypeX env (tyVarKind tv1) (tyVarKind tv2)
1228  = eqTyVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
1229 eqTyVarBndrs _ _ _= Nothing
1230 \end{code}
1231
1232 Now here comes the real worker
1233
1234 \begin{code}
1235 cmpType :: Type -> Type -> Ordering
1236 -- Watch out for horrible hack: See Note [Comparison with OpenTypeKind]
1237 cmpType t1 t2 = cmpTypeX rn_env t1 t2
1238   where
1239     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
1240
1241 cmpTypes :: [Type] -> [Type] -> Ordering
1242 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
1243   where
1244     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
1245
1246 cmpPred :: PredType -> PredType -> Ordering
1247 cmpPred p1 p2 = cmpTypeX rn_env p1 p2
1248   where
1249     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType p1 `unionVarSet` tyVarsOfType p2))
1250
1251 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
1252 cmpTypeX env t1 t2 | Just t1' <- coreView t1 = cmpTypeX env t1' t2
1253                    | Just t2' <- coreView t2 = cmpTypeX env t1 t2'
1254 -- We expand predicate types, because in Core-land we have
1255 -- lots of definitions like
1256 --      fOrdBool :: Ord Bool
1257 --      fOrdBool = D:Ord .. .. ..
1258 -- So the RHS has a data type
1259
1260 cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
1261 cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX env (tyVarKind tv1) (tyVarKind tv2)
1262                                                        `thenCmp` cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
1263 cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1264 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1265 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `cmpTc` tc2) `thenCmp` cmpTypesX env tys1 tys2
1266 cmpTypeX _   (LitTy l1)          (LitTy l2)          = compare l1 l2
1267
1268     -- Deal with the rest: TyVarTy < AppTy < FunTy < LitTy < TyConApp < ForAllTy < PredTy
1269 cmpTypeX _ (AppTy _ _)    (TyVarTy _)    = GT
1270
1271 cmpTypeX _ (FunTy _ _)    (TyVarTy _)    = GT
1272 cmpTypeX _ (FunTy _ _)    (AppTy _ _)    = GT
1273
1274 cmpTypeX _ (LitTy _)      (TyVarTy _)    = GT
1275 cmpTypeX _ (LitTy _)      (AppTy _ _)    = GT
1276 cmpTypeX _ (LitTy _)      (FunTy _ _)    = GT
1277
1278 cmpTypeX _ (TyConApp _ _) (TyVarTy _)    = GT
1279 cmpTypeX _ (TyConApp _ _) (AppTy _ _)    = GT
1280 cmpTypeX _ (TyConApp _ _) (FunTy _ _)    = GT
1281 cmpTypeX _ (TyConApp _ _) (LitTy _)      = GT
1282
1283 cmpTypeX _ (ForAllTy _ _) (TyVarTy _)    = GT
1284 cmpTypeX _ (ForAllTy _ _) (AppTy _ _)    = GT
1285 cmpTypeX _ (ForAllTy _ _) (FunTy _ _)    = GT
1286 cmpTypeX _ (ForAllTy _ _) (LitTy _)      = GT
1287 cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = GT
1288
1289 cmpTypeX _ _              _              = LT
1290
1291 -------------
1292 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1293 cmpTypesX _   []        []        = EQ
1294 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1295 cmpTypesX _   []        _         = LT
1296 cmpTypesX _   _         []        = GT
1297
1298 -------------
1299 cmpTc :: TyCon -> TyCon -> Ordering
1300 -- Here we treat * and Constraint as equal
1301 -- See Note [Kind Constraint and kind *] in Kinds.lhs
1302 --
1303 -- Also we treat OpenTypeKind as equal to either * or #
1304 -- See Note [Comparison with OpenTypeKind]
1305 cmpTc tc1 tc2 
1306   | u1 == openTypeKindTyConKey, isSubOpenTypeKindKey u2 = EQ
1307   | u2 == openTypeKindTyConKey, isSubOpenTypeKindKey u1 = EQ
1308   | otherwise = nu1 `compare` nu2
1309   where
1310     u1  = tyConUnique tc1
1311     nu1 = if u1==constraintKindTyConKey then liftedTypeKindTyConKey else u1
1312     u2  = tyConUnique tc2
1313     nu2 = if u2==constraintKindTyConKey then liftedTypeKindTyConKey else u2
1314 \end{code}
1315
1316 Note [Comparison with OpenTypeKind]
1317 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1318 In PrimOpWrappers we have things like
1319    PrimOpWrappers.mkWeak# = /\ a b c. Prim.mkWeak# a b c
1320 where
1321    Prim.mkWeak# :: forall (a:Open) b c. a -> b -> c 
1322                                      -> State# RealWorld -> (# State# RealWorld, Weak# b #)
1323 Now, eta reduction will turn the definition into
1324      PrimOpWrappers.mkWeak# = Prim.mkWeak#
1325 which is kind-of OK, but now the types aren't really equal.  So HACK HACK
1326 we pretend (in Core) that Open is equal to * or #.  I hate this.
1327
1328 Note [cmpTypeX]
1329 ~~~~~~~~~~~~~~~
1330
1331 When we compare foralls, we should look at the kinds. But if we do so,
1332 we get a corelint error like the following (in
1333 libraries/ghc-prim/GHC/PrimopWrappers.hs):
1334
1335     Binder's type: forall (o_abY :: *).
1336                    o_abY
1337                    -> GHC.Prim.State# GHC.Prim.RealWorld
1338                    -> GHC.Prim.State# GHC.Prim.RealWorld
1339     Rhs type: forall (a_12 :: ?).
1340               a_12
1341               -> GHC.Prim.State# GHC.Prim.RealWorld
1342               -> GHC.Prim.State# GHC.Prim.RealWorld
1343
1344 This is why we don't look at the kind. Maybe we should look if the
1345 kinds are compatible.
1346
1347 -- cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)
1348 --   = cmpTypeX env (tyVarKind tv1) (tyVarKind tv2) `thenCmp`
1349 --     cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
1350
1351 %************************************************************************
1352 %*                                                                      *
1353                 Type substitutions
1354 %*                                                                      *
1355 %************************************************************************
1356
1357 \begin{code}
1358 emptyTvSubstEnv :: TvSubstEnv
1359 emptyTvSubstEnv = emptyVarEnv
1360
1361 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1362 -- ^ @(compose env1 env2)(x)@ is @env1(env2(x))@; i.e. apply @env2@ then @env1@.
1363 -- It assumes that both are idempotent.
1364 -- Typically, @env1@ is the refinement to a base substitution @env2@
1365 composeTvSubst in_scope env1 env2
1366   = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1367         -- First apply env1 to the range of env2
1368         -- Then combine the two, making sure that env1 loses if
1369         -- both bind the same variable; that's why env1 is the
1370         --  *left* argument to plusVarEnv, because the right arg wins
1371   where
1372     subst1 = TvSubst in_scope env1
1373
1374 emptyTvSubst :: TvSubst
1375 emptyTvSubst = TvSubst emptyInScopeSet emptyTvSubstEnv
1376
1377 isEmptyTvSubst :: TvSubst -> Bool
1378          -- See Note [Extending the TvSubstEnv] in TypeRep
1379 isEmptyTvSubst (TvSubst _ tenv) = isEmptyVarEnv tenv
1380
1381 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1382 mkTvSubst = TvSubst
1383
1384 getTvSubstEnv :: TvSubst -> TvSubstEnv
1385 getTvSubstEnv (TvSubst _ env) = env
1386
1387 getTvInScope :: TvSubst -> InScopeSet
1388 getTvInScope (TvSubst in_scope _) = in_scope
1389
1390 isInScope :: Var -> TvSubst -> Bool
1391 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1392
1393 notElemTvSubst :: CoVar -> TvSubst -> Bool
1394 notElemTvSubst v (TvSubst _ tenv) = not (v `elemVarEnv` tenv)
1395
1396 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1397 setTvSubstEnv (TvSubst in_scope _) tenv = TvSubst in_scope tenv
1398
1399 zapTvSubstEnv :: TvSubst -> TvSubst
1400 zapTvSubstEnv (TvSubst in_scope _) = TvSubst in_scope emptyVarEnv
1401
1402 extendTvInScope :: TvSubst -> Var -> TvSubst
1403 extendTvInScope (TvSubst in_scope tenv) var = TvSubst (extendInScopeSet in_scope var) tenv
1404
1405 extendTvInScopeList :: TvSubst -> [Var] -> TvSubst
1406 extendTvInScopeList (TvSubst in_scope tenv) vars = TvSubst (extendInScopeSetList in_scope vars) tenv
1407
1408 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1409 extendTvSubst (TvSubst in_scope tenv) tv ty = TvSubst in_scope (extendVarEnv tenv tv ty)
1410
1411 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1412 extendTvSubstList (TvSubst in_scope tenv) tvs tys
1413   = TvSubst in_scope (extendVarEnvList tenv (tvs `zip` tys))
1414
1415 unionTvSubst :: TvSubst -> TvSubst -> TvSubst
1416 -- Works when the ranges are disjoint
1417 unionTvSubst (TvSubst in_scope1 tenv1) (TvSubst in_scope2 tenv2)
1418   = ASSERT( not (tenv1 `intersectsVarEnv` tenv2) )
1419     TvSubst (in_scope1 `unionInScope` in_scope2)
1420             (tenv1     `plusVarEnv`   tenv2)
1421
1422 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1423 -- the types given; but it's just a thunk so with a bit of luck
1424 -- it'll never be evaluated
1425
1426 -- Note [Generating the in-scope set for a substitution]
1427 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1428 -- If we want to substitute [a -> ty1, b -> ty2] I used to
1429 -- think it was enough to generate an in-scope set that includes
1430 -- fv(ty1,ty2).  But that's not enough; we really should also take the
1431 -- free vars of the type we are substituting into!  Example:
1432 --      (forall b. (a,b,x)) [a -> List b]
1433 -- Then if we use the in-scope set {b}, there is a danger we will rename
1434 -- the forall'd variable to 'x' by mistake, getting this:
1435 --      (forall x. (List b, x, x)
1436 -- Urk!  This means looking at all the calls to mkOpenTvSubst....
1437
1438
1439 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1440 -- environment, hence "open"
1441 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1442 mkOpenTvSubst tenv = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts tenv))) tenv
1443
1444 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1445 -- environment, hence "open"
1446 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1447 zipOpenTvSubst tyvars tys
1448   | debugIsOn && (length tyvars /= length tys)
1449   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1450   | otherwise
1451   = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1452
1453 -- | Called when doing top-level substitutions. Here we expect that the
1454 -- free vars of the range of the substitution will be empty.
1455 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1456 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1457
1458 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1459 zipTopTvSubst tyvars tys
1460   | debugIsOn && (length tyvars /= length tys)
1461   = pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1462   | otherwise
1463   = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1464
1465 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1466 zipTyEnv tyvars tys
1467   | debugIsOn && (length tyvars /= length tys)
1468   = pprTrace "zipTyEnv" (ppr tyvars $$ ppr tys) emptyVarEnv
1469   | otherwise
1470   = zip_ty_env tyvars tys emptyVarEnv
1471
1472 -- Later substitutions in the list over-ride earlier ones,
1473 -- but there should be no loops
1474 zip_ty_env :: [TyVar] -> [Type] -> TvSubstEnv -> TvSubstEnv
1475 zip_ty_env []       []       env = env
1476 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1477         -- There used to be a special case for when
1478         --      ty == TyVarTy tv
1479         -- (a not-uncommon case) in which case the substitution was dropped.
1480         -- But the type-tidier changes the print-name of a type variable without
1481         -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had
1482         -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
1483         -- And it happened that t was the type variable of the class.  Post-tiding,
1484         -- it got turned into {Foo t2}.  The ext-core printer expanded this using
1485         -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1486         -- and so generated a rep type mentioning t not t2.
1487         --
1488         -- Simplest fix is to nuke the "optimisation"
1489 zip_ty_env tvs      tys      env   = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1490 -- zip_ty_env _ _ env = env
1491
1492 instance Outputable TvSubst where
1493   ppr (TvSubst ins tenv)
1494     = brackets $ sep[ ptext (sLit "TvSubst"),
1495                       nest 2 (ptext (sLit "In scope:") <+> ppr ins),
1496                       nest 2 (ptext (sLit "Type env:") <+> ppr tenv) ]
1497 \end{code}
1498
1499 %************************************************************************
1500 %*                                                                      *
1501                 Performing type or kind substitutions
1502 %*                                                                      *
1503 %************************************************************************
1504
1505 \begin{code}
1506 -- | Type substitution making use of an 'TvSubst' that
1507 -- is assumed to be open, see 'zipOpenTvSubst'
1508 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1509 substTyWith tvs tys = ASSERT( length tvs == length tys )
1510                       substTy (zipOpenTvSubst tvs tys)
1511
1512 substKiWith :: [KindVar] -> [Kind] -> Kind -> Kind
1513 substKiWith = substTyWith
1514
1515 -- | Type substitution making use of an 'TvSubst' that
1516 -- is assumed to be open, see 'zipOpenTvSubst'
1517 substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
1518 substTysWith tvs tys = ASSERT( length tvs == length tys )
1519                        substTys (zipOpenTvSubst tvs tys)
1520
1521 substKisWith :: [KindVar] -> [Kind] -> [Kind] -> [Kind]
1522 substKisWith = substTysWith
1523
1524 -- | Substitute within a 'Type'
1525 substTy :: TvSubst -> Type  -> Type
1526 substTy subst ty | isEmptyTvSubst subst = ty
1527                  | otherwise            = subst_ty subst ty
1528
1529 -- | Substitute within several 'Type's
1530 substTys :: TvSubst -> [Type] -> [Type]
1531 substTys subst tys | isEmptyTvSubst subst = tys
1532                    | otherwise            = map (subst_ty subst) tys
1533
1534 -- | Substitute within a 'ThetaType'
1535 substTheta :: TvSubst -> ThetaType -> ThetaType
1536 substTheta subst theta
1537   | isEmptyTvSubst subst = theta
1538   | otherwise            = map (substTy subst) theta
1539
1540 -- | Remove any nested binders mentioning the 'TyVar's in the 'TyVarSet'
1541 deShadowTy :: TyVarSet -> Type -> Type
1542 deShadowTy tvs ty
1543   = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1544   where
1545     in_scope = mkInScopeSet tvs
1546
1547 subst_ty :: TvSubst -> Type -> Type
1548 -- subst_ty is the main workhorse for type substitution
1549 --
1550 -- Note that the in_scope set is poked only if we hit a forall
1551 -- so it may often never be fully computed
1552 subst_ty subst ty
1553    = go ty
1554   where
1555     go (LitTy n)         = n `seq` LitTy n
1556     go (TyVarTy tv)      = substTyVar subst tv
1557     go (TyConApp tc tys) = let args = map go tys
1558                            in  args `seqList` TyConApp tc args
1559
1560     go (FunTy arg res)   = (FunTy $! (go arg)) $! (go res)
1561     go (AppTy fun arg)   = mkAppTy (go fun) $! (go arg)
1562                 -- The mkAppTy smart constructor is important
1563                 -- we might be replacing (a Int), represented with App
1564                 -- by [Int], represented with TyConApp
1565     go (ForAllTy tv ty)  = case substTyVarBndr subst tv of
1566                               (subst', tv') ->
1567                                  ForAllTy tv' $! (subst_ty subst' ty)
1568
1569 substTyVar :: TvSubst -> TyVar  -> Type
1570 substTyVar (TvSubst _ tenv) tv
1571   | Just ty  <- lookupVarEnv tenv tv      = ty  -- See Note [Apply Once]
1572   | otherwise = ASSERT( isTyVar tv ) TyVarTy tv --     in TypeRep
1573   -- We do not require that the tyvar is in scope
1574   -- Reason: we do quite a bit of (substTyWith [tv] [ty] tau)
1575   -- and it's a nuisance to bring all the free vars of tau into
1576   -- scope --- and then force that thunk at every tyvar
1577   -- Instead we have an ASSERT in substTyVarBndr to check for capture
1578
1579 substTyVars :: TvSubst -> [TyVar] -> [Type]
1580 substTyVars subst tvs = map (substTyVar subst) tvs
1581
1582 lookupTyVar :: TvSubst -> TyVar  -> Maybe Type
1583         -- See Note [Extending the TvSubst] in TypeRep
1584 lookupTyVar (TvSubst _ tenv) tv = lookupVarEnv tenv tv
1585
1586 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1587 substTyVarBndr subst@(TvSubst in_scope tenv) old_var
1588   = ASSERT2( _no_capture, ppr old_var $$ ppr subst )
1589     (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1590   where
1591     new_env | no_change = delVarEnv tenv old_var
1592             | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
1593
1594     _no_capture = not (new_var `elemVarSet` tyVarsOfTypes (varEnvElts tenv))
1595     -- Assertion check that we are not capturing something in the substitution
1596
1597     old_ki = tyVarKind old_var
1598     no_kind_change = isEmptyVarSet (tyVarsOfType old_ki) -- verify that kind is closed
1599     no_change = no_kind_change && (new_var == old_var)
1600         -- no_change means that the new_var is identical in
1601         -- all respects to the old_var (same unique, same kind)
1602         -- See Note [Extending the TvSubst] in TypeRep
1603         --
1604         -- In that case we don't need to extend the substitution
1605         -- to map old to new.  But instead we must zap any
1606         -- current substitution for the variable. For example:
1607         --      (\x.e) with id_subst = [x |-> e']
1608         -- Here we must simply zap the substitution for x
1609
1610     new_var | no_kind_change = uniqAway in_scope old_var
1611             | otherwise = uniqAway in_scope $ updateTyVarKind (substTy subst) old_var
1612         -- The uniqAway part makes sure the new variable is not already in scope
1613
1614 cloneTyVarBndr :: TvSubst -> TyVar -> Unique -> (TvSubst, TyVar)
1615 cloneTyVarBndr (TvSubst in_scope tv_env) tv uniq
1616   = (TvSubst (extendInScopeSet in_scope tv')
1617              (extendVarEnv tv_env tv (mkTyVarTy tv')), tv')
1618   where
1619     tv' = setVarUnique tv uniq  -- Simply set the unique; the kind
1620                                 -- has no type variables to worry about
1621 \end{code}
1622
1623 ----------------------------------------------------
1624 -- Kind Stuff
1625
1626 Kinds
1627 ~~~~~
1628
1629 For the description of subkinding in GHC, see
1630   http://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType#Kinds
1631
1632 \begin{code}
1633 type MetaKindVar = TyVar  -- invariant: MetaKindVar will always be a
1634                           -- TcTyVar with details MetaTv TauTv ...
1635 -- meta kind var constructors and functions are in TcType
1636
1637 type SimpleKind = Kind
1638 \end{code}
1639
1640 %************************************************************************
1641 %*                                                                      *
1642         The kind of a type
1643 %*                                                                      *
1644 %************************************************************************
1645
1646 \begin{code}
1647 typeKind :: Type -> Kind
1648 typeKind orig_ty = go orig_ty
1649   where
1650     
1651     go ty@(TyConApp tc tys)
1652       | isPromotedTyCon tc
1653       = ASSERT( tyConArity tc == length tys ) superKind
1654       | otherwise
1655       = kindAppResult (ptext (sLit "typeKind 1") <+> ppr ty $$ ppr orig_ty)
1656                       (tyConKind tc) tys
1657
1658     go ty@(AppTy fun arg)   = kindAppResult (ptext (sLit "typeKind 2") <+> ppr ty $$ ppr orig_ty)
1659                                             (go fun) [arg]
1660     go (LitTy l)            = typeLiteralKind l
1661     go (ForAllTy _ ty)      = go ty
1662     go (TyVarTy tyvar)      = tyVarKind tyvar
1663     go _ty@(FunTy _arg res)
1664         -- Hack alert.  The kind of (Int -> Int#) is liftedTypeKind (*),
1665         --              not unliftedTypeKind (#)
1666         -- The only things that can be after a function arrow are
1667         --   (a) types (of kind openTypeKind or its sub-kinds)
1668         --   (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
1669         | isSuperKind k         = k
1670         | otherwise             = ASSERT2( isSubOpenTypeKind k, ppr _ty $$ ppr k ) liftedTypeKind
1671         where
1672           k = go res
1673
1674 typeLiteralKind :: TyLit -> Kind
1675 typeLiteralKind l =
1676   case l of
1677     NumTyLit _ -> typeNatKind
1678     StrTyLit _ -> typeSymbolKind
1679 \end{code}
1680
1681 Kind inference
1682 ~~~~~~~~~~~~~~
1683 During kind inference, a kind variable unifies only with
1684 a "simple kind", sk
1685         sk ::= * | sk1 -> sk2
1686 For example
1687         data T a = MkT a (T Int#)
1688 fails.  We give T the kind (k -> *), and the kind variable k won't unify
1689 with # (the kind of Int#).
1690
1691 Type inference
1692 ~~~~~~~~~~~~~~
1693 When creating a fresh internal type variable, we give it a kind to express
1694 constraints on it.  E.g. in (\x->e) we make up a fresh type variable for x,
1695 with kind ??.
1696
1697 During unification we only bind an internal type variable to a type
1698 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1699
1700 When unifying two internal type variables, we collect their kind constraints by
1701 finding the GLB of the two.  Since the partial order is a tree, they only
1702 have a glb if one is a sub-kind of the other.  In that case, we bind the
1703 less-informative one to the more informative one.  Neat, eh?