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