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