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