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