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