De-orphan a load of Binary instances
[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,
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, openTypeKindTyConKey,
163                    constraintKindTyConKey, liftedTypeKindTyConKey )
164 import CoAxiom
165
166 -- others
167 import Unique           ( Unique, hasKey )
168 import BasicTypes       ( Arity, RepArity )
169 import StaticFlags
170 import Util
171 import Outputable
172 import FastString
173
174 import Data.List        ( partition )
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 newTyConInstRhs tycon tys
565     = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs )
566       mkAppTys (substTyWith tvs tys1 ty) tys2
567   where
568     (tvs, ty)    = newTyConEtadRhs tycon
569     (tys1, tys2) = splitAtList tvs tys
570 \end{code}
571
572
573 ---------------------------------------------------------------------
574                                 SynTy
575                                 ~~~~~
576
577 Notes on type synonyms
578 ~~~~~~~~~~~~~~~~~~~~~~
579 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
580 to return type synonyms whereever possible. Thus
581
582         type Foo a = a -> a
583
584 we want
585         splitFunTys (a -> Foo a) = ([a], Foo a)
586 not                                ([a], a -> a)
587
588 The reason is that we then get better (shorter) type signatures in
589 interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
590
591
592                 Representation types
593                 ~~~~~~~~~~~~~~~~~~~~
594
595 Note [Nullary unboxed tuple]
596 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
597 We represent the nullary unboxed tuple as the unary (but void) type
598 State# RealWorld.  The reason for this is that the ReprArity is never
599 less than the Arity (as it would otherwise be for a function type like
600 (# #) -> Int).
601
602 As a result, ReprArity is always strictly positive if Arity is. This
603 is important because it allows us to distinguish at runtime between a
604 thunk and a function takes a nullary unboxed tuple as an argument!
605
606 \begin{code}
607 type UnaryType = Type
608
609 data RepType = UbxTupleRep [UnaryType] -- INVARIANT: never an empty list (see Note [Nullary unboxed tuple])
610              | UnaryRep UnaryType
611
612 flattenRepType :: RepType -> [UnaryType]
613 flattenRepType (UbxTupleRep tys) = tys
614 flattenRepType (UnaryRep ty)     = [ty]
615
616 -- | Looks through:
617 --
618 --      1. For-alls
619 --      2. Synonyms
620 --      3. Predicates
621 --      4. All newtypes, including recursive ones, but not newtype families
622 --
623 -- It's useful in the back end of the compiler.
624 repType :: Type -> RepType
625 repType ty
626   = go initRecTc ty
627   where
628     go :: RecTcChecker -> Type -> RepType
629     go rec_nts ty                       -- Expand predicates and synonyms
630       | Just ty' <- coreView ty
631       = go rec_nts ty'
632
633     go rec_nts (ForAllTy _ ty)          -- Drop foralls
634         = go rec_nts ty
635
636     go rec_nts (TyConApp tc tys)        -- Expand newtypes
637       | isNewTyCon tc
638       , tys `lengthAtLeast` tyConArity tc
639       , Just rec_nts' <- checkRecTc rec_nts tc   -- See Note [Expanding newtypes] in TyCon
640       = go rec_nts' (newTyConInstRhs tc tys)
641
642       | isUnboxedTupleTyCon tc
643       = if null tys
644          then UnaryRep realWorldStatePrimTy -- See Note [Nullary unboxed tuple]
645          else UbxTupleRep (concatMap (flattenRepType . go rec_nts) tys)
646
647     go _ ty = UnaryRep ty
648
649 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
650 -- of inspecting the type directly.
651
652 -- | Discovers the primitive representation of a more abstract 'UnaryType'
653 typePrimRep :: UnaryType -> PrimRep
654 typePrimRep ty
655   = case repType ty of
656       UbxTupleRep _ -> pprPanic "typePrimRep: UbxTupleRep" (ppr ty)
657       UnaryRep rep -> case rep of
658         TyConApp tc _ -> tyConPrimRep tc
659         FunTy _ _     -> PtrRep
660         AppTy _ _     -> PtrRep      -- See Note [AppTy rep]
661         TyVarTy _     -> PtrRep
662         _             -> pprPanic "typePrimRep: UnaryRep" (ppr ty)
663
664 typeRepArity :: Arity -> Type -> RepArity
665 typeRepArity 0 _ = 0
666 typeRepArity n ty = case repType ty of
667   UnaryRep (FunTy ty1 ty2) -> length (flattenRepType (repType ty1)) + typeRepArity (n - 1) ty2
668   _                        -> pprPanic "typeRepArity: arity greater than type can handle" (ppr (n, ty))
669 \end{code}
670
671 Note [AppTy rep]
672 ~~~~~~~~~~~~~~~~
673 Types of the form 'f a' must be of kind *, not #, so we are guaranteed
674 that they are represented by pointers.  The reason is that f must have
675 kind (kk -> kk) and kk cannot be unlifted; see Note [The kind invariant]
676 in TypeRep.
677
678 ---------------------------------------------------------------------
679                                 ForAllTy
680                                 ~~~~~~~~
681
682 \begin{code}
683 mkForAllTy :: TyVar -> Type -> Type
684 mkForAllTy tyvar ty
685   = ForAllTy tyvar ty
686
687 -- | Wraps foralls over the type using the provided 'TyVar's from left to right
688 mkForAllTys :: [TyVar] -> Type -> Type
689 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
690
691 mkPiKinds :: [TyVar] -> Kind -> Kind
692 -- mkPiKinds [k1, k2, (a:k1 -> *)] k2
693 -- returns forall k1 k2. (k1 -> *) -> k2
694 mkPiKinds [] res = res
695 mkPiKinds (tv:tvs) res
696   | isKindVar tv = ForAllTy tv          (mkPiKinds tvs res)
697   | otherwise    = FunTy (tyVarKind tv) (mkPiKinds tvs res)
698
699 mkPiType  :: Var -> Type -> Type
700 -- ^ Makes a @(->)@ type or a forall type, depending
701 -- on whether it is given a type variable or a term variable.
702 mkPiTypes :: [Var] -> Type -> Type
703 -- ^ 'mkPiType' for multiple type or value arguments
704
705 mkPiType v ty
706    | isId v    = mkFunTy (varType v) ty
707    | otherwise = mkForAllTy v ty
708
709 mkPiTypes vs ty = foldr mkPiType ty vs
710
711 isForAllTy :: Type -> Bool
712 isForAllTy (ForAllTy _ _) = True
713 isForAllTy _              = False
714
715 -- | Attempts to take a forall type apart, returning the bound type variable
716 -- and the remainder of the type
717 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
718 splitForAllTy_maybe ty = splitFAT_m ty
719   where
720     splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
721     splitFAT_m (ForAllTy tyvar ty)          = Just(tyvar, ty)
722     splitFAT_m _                            = Nothing
723
724 -- | Attempts to take a forall type apart, returning all the immediate such bound
725 -- type variables and the remainder of the type. Always suceeds, even if that means
726 -- returning an empty list of 'TyVar's
727 splitForAllTys :: Type -> ([TyVar], Type)
728 splitForAllTys ty = split ty ty []
729    where
730      split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
731      split _       (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
732      split orig_ty _                 tvs = (reverse tvs, orig_ty)
733
734 -- | Equivalent to @snd . splitForAllTys@
735 dropForAlls :: Type -> Type
736 dropForAlls ty = snd (splitForAllTys ty)
737 \end{code}
738
739 -- (mkPiType now in CoreUtils)
740
741 applyTy, applyTys
742 ~~~~~~~~~~~~~~~~~
743
744 \begin{code}
745 -- | Instantiate a forall type with one or more type arguments.
746 -- Used when we have a polymorphic function applied to type args:
747 --
748 -- > f t1 t2
749 --
750 -- We use @applyTys type-of-f [t1,t2]@ to compute the type of the expression.
751 -- Panics if no application is possible.
752 applyTy :: Type -> KindOrType -> Type
753 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
754 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
755 applyTy _                _   = panic "applyTy"
756
757 applyTys :: Type -> [KindOrType] -> Type
758 -- ^ This function is interesting because:
759 --
760 --      1. The function may have more for-alls than there are args
761 --
762 --      2. Less obviously, it may have fewer for-alls
763 --
764 -- For case 2. think of:
765 --
766 -- > applyTys (forall a.a) [forall b.b, Int]
767 --
768 -- This really can happen, but only (I think) in situations involving
769 -- undefined.  For example:
770 --       undefined :: forall a. a
771 -- Term: undefined @(forall b. b->b) @Int
772 -- This term should have type (Int -> Int), but notice that
773 -- there are more type args than foralls in 'undefined's type.
774
775 -- If you edit this function, you may need to update the GHC formalism
776 -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
777 applyTys ty args = applyTysD empty ty args
778
779 applyTysD :: SDoc -> Type -> [Type] -> Type     -- Debug version
780 applyTysD _   orig_fun_ty []      = orig_fun_ty
781 applyTysD doc orig_fun_ty arg_tys
782   | n_tvs == n_args     -- The vastly common case
783   = substTyWith tvs arg_tys rho_ty
784   | n_tvs > n_args      -- Too many for-alls
785   = substTyWith (take n_args tvs) arg_tys
786                 (mkForAllTys (drop n_args tvs) rho_ty)
787   | otherwise           -- Too many type args
788   = ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty )        -- Zero case gives infnite loop!
789     applyTysD doc (substTyWith tvs (take n_tvs arg_tys) rho_ty)
790                   (drop n_tvs arg_tys)
791   where
792     (tvs, rho_ty) = splitForAllTys orig_fun_ty
793     n_tvs = length tvs
794     n_args = length arg_tys
795 \end{code}
796
797
798 %************************************************************************
799 %*                                                                      *
800                          Pred
801 %*                                                                      *
802 %************************************************************************
803
804 Predicates on PredType
805
806 \begin{code}
807 noParenPred :: PredType -> Bool
808 -- A predicate that can appear without parens before a "=>"
809 --       C a => a -> a
810 --       a~b => a -> b
811 -- But   (?x::Int) => Int -> Int
812 noParenPred p = not (isIPPred p) && isClassPred p || isEqPred p
813
814 isPredTy :: Type -> Bool
815   -- NB: isPredTy is used when printing types, which can happen in debug printing
816   --     during type checking of not-fully-zonked types.  So it's not cool to say
817   --     isConstraintKind (typeKind ty) because absent zonking the type might 
818   --     be ill-kinded, and typeKind crashes
819   --     Hence the rather tiresome story here
820 isPredTy ty = go ty []
821   where
822     go :: Type -> [KindOrType] -> Bool
823     go (AppTy ty1 ty2)   args = go ty1 (ty2 : args)
824     go (TyConApp tc tys) args = go_k (tyConKind tc) (tys ++ args)
825     go (TyVarTy tv)      args = go_k (tyVarKind tv) args
826     go _                 _    = False
827
828     go_k :: Kind -> [KindOrType] -> Bool
829     -- True <=> kind is k1 -> .. -> kn -> Constraint
830     go_k k                [] = isConstraintKind k
831     go_k (FunTy _ k1)     (_ :args) = go_k k1 args
832     go_k (ForAllTy kv k1) (k2:args) = go_k (substKiWith [kv] [k2] k1) args
833     go_k _ _ = False                  -- Typeable * Int :: Constraint
834
835 isKindTy :: Type -> Bool
836 isKindTy = isSuperKind . typeKind
837
838 isClassPred, isEqPred, isIPPred :: PredType -> Bool
839 isClassPred ty = case tyConAppTyCon_maybe ty of
840     Just tyCon | isClassTyCon tyCon -> True
841     _                               -> False
842 isEqPred ty = case tyConAppTyCon_maybe ty of
843     Just tyCon -> tyCon `hasKey` eqTyConKey
844     _          -> False
845
846 isIPPred ty = case tyConAppTyCon_maybe ty of
847     Just tc -> isIPTyCon tc
848     _       -> False
849
850 isIPTyCon :: TyCon -> Bool
851 isIPTyCon tc = tc `hasKey` ipClassNameKey
852
853 isIPClass :: Class -> Bool
854 isIPClass cls = cls `hasKey` ipClassNameKey
855   -- Class and it corresponding TyCon have the same Unique
856
857 isIPPred_maybe :: Type -> Maybe (FastString, Type)
858 isIPPred_maybe ty =
859   do (tc,[t1,t2]) <- splitTyConApp_maybe ty
860      guard (isIPTyCon tc)
861      x <- isStrLitTy t1
862      return (x,t2)
863 \end{code}
864
865 Make PredTypes
866
867 --------------------- Equality types ---------------------------------
868 \begin{code}
869 -- | Creates a type equality predicate
870 mkEqPred :: Type -> Type -> PredType
871 mkEqPred ty1 ty2
872   = WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 $$ ppr k $$ ppr (typeKind ty2) )
873     TyConApp eqTyCon [k, ty1, ty2]
874   where
875     k = typeKind ty1
876
877 mkPrimEqPred :: Type -> Type -> Type
878 mkPrimEqPred ty1  ty2
879   = WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 )
880     TyConApp eqPrimTyCon [k, ty1, ty2]
881   where
882     k = typeKind ty1
883 \end{code}
884
885 --------------------- Dictionary types ---------------------------------
886 \begin{code}
887 mkClassPred :: Class -> [Type] -> PredType
888 mkClassPred clas tys = TyConApp (classTyCon clas) tys
889
890 isDictTy :: Type -> Bool
891 isDictTy = isClassPred
892
893 isDictLikeTy :: Type -> Bool
894 -- Note [Dictionary-like types]
895 isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
896 isDictLikeTy ty = case splitTyConApp_maybe ty of
897         Just (tc, tys) | isClassTyCon tc -> True
898                        | isTupleTyCon tc -> all isDictLikeTy tys
899         _other                           -> False
900 \end{code}
901
902 Note [Dictionary-like types]
903 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
904 Being "dictionary-like" means either a dictionary type or a tuple thereof.
905 In GHC 6.10 we build implication constraints which construct such tuples,
906 and if we land up with a binding
907     t :: (C [a], Eq [a])
908     t = blah
909 then we want to treat t as cheap under "-fdicts-cheap" for example.
910 (Implication constraints are normally inlined, but sadly not if the
911 occurrence is itself inside an INLINE function!  Until we revise the
912 handling of implication constraints, that is.)  This turned out to
913 be important in getting good arities in DPH code.  Example:
914
915     class C a
916     class D a where { foo :: a -> a }
917     instance C a => D (Maybe a) where { foo x = x }
918
919     bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
920     {-# INLINE bar #-}
921     bar x y = (foo (Just x), foo (Just y))
922
923 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
924 we ended up with something like
925    bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
926                                 in \x,y. <blah>)
927
928 This is all a bit ad-hoc; eg it relies on knowing that implication
929 constraints build tuples.
930
931
932 Decomposing PredType
933
934 \begin{code}
935 data PredTree = ClassPred Class [Type]
936               | EqPred Type Type
937               | TuplePred [PredType]
938               | IrredPred PredType
939
940 classifyPredType :: PredType -> PredTree
941 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
942     Just (tc, tys) | Just clas <- tyConClass_maybe tc
943                    -> ClassPred clas tys
944     Just (tc, tys) | tc `hasKey` eqTyConKey
945                    , let [_, ty1, ty2] = tys
946                    -> EqPred ty1 ty2
947     Just (tc, tys) | isTupleTyCon tc
948                    -> TuplePred tys
949     _ -> IrredPred ev_ty
950 \end{code}
951
952 \begin{code}
953 getClassPredTys :: PredType -> (Class, [Type])
954 getClassPredTys ty = case getClassPredTys_maybe ty of
955         Just (clas, tys) -> (clas, tys)
956         Nothing          -> pprPanic "getClassPredTys" (ppr ty)
957
958 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
959 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
960         Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
961         _ -> Nothing
962
963 getEqPredTys :: PredType -> (Type, Type)
964 getEqPredTys ty
965   = case splitTyConApp_maybe ty of
966       Just (tc, (_ : ty1 : ty2 : tys)) -> ASSERT( tc `hasKey` eqTyConKey && null tys )
967                                           (ty1, ty2)
968       _ -> pprPanic "getEqPredTys" (ppr ty)
969
970 getEqPredTys_maybe :: PredType -> Maybe (Type, Type)
971 getEqPredTys_maybe ty
972   = case splitTyConApp_maybe ty of
973       Just (tc, [_, ty1, ty2]) | tc `hasKey` eqTyConKey -> Just (ty1, ty2)
974       _ -> Nothing
975 \end{code}
976
977 %************************************************************************
978 %*                                                                      *
979                    Size
980 %*                                                                      *
981 %************************************************************************
982
983 \begin{code}
984 typeSize :: Type -> Int
985 typeSize (LitTy {})      = 1
986 typeSize (TyVarTy {})    = 1
987 typeSize (AppTy t1 t2)   = typeSize t1 + typeSize t2
988 typeSize (FunTy t1 t2)   = typeSize t1 + typeSize t2
989 typeSize (ForAllTy _ t)  = 1 + typeSize t
990 typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
991
992 varSetElemsKvsFirst :: VarSet -> [TyVar]
993 -- {k1,a,k2,b} --> [k1,k2,a,b]
994 varSetElemsKvsFirst set
995   = kvs ++ tvs
996   where
997     (kvs, tvs) = partition isKindVar (varSetElems set)
998 \end{code}
999
1000
1001 %************************************************************************
1002 %*                                                                      *
1003 \subsection{Type families}
1004 %*                                                                      *
1005 %************************************************************************
1006
1007 \begin{code}
1008 mkFamilyTyConApp :: TyCon -> [Type] -> Type
1009 -- ^ Given a family instance TyCon and its arg types, return the
1010 -- corresponding family type.  E.g:
1011 --
1012 -- > data family T a
1013 -- > data instance T (Maybe b) = MkT b
1014 --
1015 -- Where the instance tycon is :RTL, so:
1016 --
1017 -- > mkFamilyTyConApp :RTL Int  =  T (Maybe Int)
1018 mkFamilyTyConApp tc tys
1019   | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
1020   , let tvs = tyConTyVars tc
1021         fam_subst = ASSERT2( length tvs == length tys, ppr tc <+> ppr tys )
1022                     zipTopTvSubst tvs tys
1023   = mkTyConApp fam_tc (substTys fam_subst fam_tys)
1024   | otherwise
1025   = mkTyConApp tc tys
1026
1027 -- | Get the type on the LHS of a coercion induced by a type/data
1028 -- family instance.
1029 coAxNthLHS :: CoAxiom br -> Int -> Type
1030 coAxNthLHS ax ind =
1031   mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind))
1032
1033 -- | Pretty prints a 'TyCon', using the family instance in case of a
1034 -- representation tycon.  For example:
1035 --
1036 -- > data T [a] = ...
1037 --
1038 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
1039 pprSourceTyCon :: TyCon -> SDoc
1040 pprSourceTyCon tycon
1041   | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
1042   = ppr $ fam_tc `TyConApp` tys        -- can't be FunTyCon
1043   | otherwise
1044   = ppr tycon
1045 \end{code}
1046
1047 %************************************************************************
1048 %*                                                                      *
1049 \subsection{Liftedness}
1050 %*                                                                      *
1051 %************************************************************************
1052
1053 \begin{code}
1054 -- | See "Type#type_classification" for what an unlifted type is
1055 isUnLiftedType :: Type -> Bool
1056         -- isUnLiftedType returns True for forall'd unlifted types:
1057         --      x :: forall a. Int#
1058         -- I found bindings like these were getting floated to the top level.
1059         -- They are pretty bogus types, mind you.  It would be better never to
1060         -- construct them
1061
1062 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
1063 isUnLiftedType (ForAllTy _ ty)      = isUnLiftedType ty
1064 isUnLiftedType (TyConApp tc _)      = isUnLiftedTyCon tc
1065 isUnLiftedType _                    = False
1066
1067 isUnboxedTupleType :: Type -> Bool
1068 isUnboxedTupleType ty = case tyConAppTyCon_maybe ty of
1069                            Just tc -> isUnboxedTupleTyCon tc
1070                            _       -> False
1071
1072 -- | See "Type#type_classification" for what an algebraic type is.
1073 -- Should only be applied to /types/, as opposed to e.g. partially
1074 -- saturated type constructors
1075 isAlgType :: Type -> Bool
1076 isAlgType ty
1077   = case splitTyConApp_maybe ty of
1078       Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1079                             isAlgTyCon tc
1080       _other             -> False
1081
1082 -- | See "Type#type_classification" for what an algebraic type is.
1083 -- Should only be applied to /types/, as opposed to e.g. partially
1084 -- saturated type constructors. Closed type constructors are those
1085 -- with a fixed right hand side, as opposed to e.g. associated types
1086 isClosedAlgType :: Type -> Bool
1087 isClosedAlgType ty
1088   = case splitTyConApp_maybe ty of
1089       Just (tc, ty_args) | isAlgTyCon tc && not (isFamilyTyCon tc)
1090              -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
1091       _other -> False
1092 \end{code}
1093
1094 \begin{code}
1095 -- | Computes whether an argument (or let right hand side) should
1096 -- be computed strictly or lazily, based only on its type.
1097 -- Works just like 'isUnLiftedType', except that it has a special case
1098 -- for dictionaries (i.e. does not work purely on representation types)
1099
1100 -- Since it takes account of class 'PredType's, you might think
1101 -- this function should be in 'TcType', but 'isStrictType' is used by 'DataCon',
1102 -- which is below 'TcType' in the hierarchy, so it's convenient to put it here.
1103 --
1104 -- We may be strict in dictionary types, but only if it
1105 -- has more than one component.
1106 --
1107 -- (Being strict in a single-component dictionary risks
1108 --  poking the dictionary component, which is wrong.)
1109 isStrictType :: Type -> Bool
1110 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
1111 isStrictType (ForAllTy _ ty)   = isStrictType ty
1112 isStrictType (TyConApp tc _)
1113  | isUnLiftedTyCon tc               = True
1114  | isClassTyCon tc, opt_DictsStrict = True
1115 isStrictType _                      = False
1116 \end{code}
1117
1118 \begin{code}
1119 isPrimitiveType :: Type -> Bool
1120 -- ^ Returns true of types that are opaque to Haskell.
1121 -- Most of these are unlifted, but now that we interact with .NET, we
1122 -- may have primtive (foreign-imported) types that are lifted
1123 isPrimitiveType ty = case splitTyConApp_maybe ty of
1124                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1125                                               isPrimTyCon tc
1126                         _                  -> False
1127 \end{code}
1128
1129
1130 %************************************************************************
1131 %*                                                                      *
1132 \subsection{Sequencing on types}
1133 %*                                                                      *
1134 %************************************************************************
1135
1136 \begin{code}
1137 seqType :: Type -> ()
1138 seqType (LitTy n)         = n `seq` ()
1139 seqType (TyVarTy tv)      = tv `seq` ()
1140 seqType (AppTy t1 t2)     = seqType t1 `seq` seqType t2
1141 seqType (FunTy t1 t2)     = seqType t1 `seq` seqType t2
1142 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
1143 seqType (ForAllTy tv ty)  = seqType (tyVarKind tv) `seq` seqType ty
1144
1145 seqTypes :: [Type] -> ()
1146 seqTypes []       = ()
1147 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
1148 \end{code}
1149
1150
1151 %************************************************************************
1152 %*                                                                      *
1153                 Comparision for types
1154         (We don't use instances so that we know where it happens)
1155 %*                                                                      *
1156 %************************************************************************
1157
1158 \begin{code}
1159 eqKind :: Kind -> Kind -> Bool
1160 eqKind = eqType
1161
1162 eqType :: Type -> Type -> Bool
1163 -- ^ Type equality on source types. Does not look through @newtypes@ or
1164 -- 'PredType's, but it does look through type synonyms.
1165 eqType t1 t2 = isEqual $ cmpType t1 t2
1166
1167 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
1168 eqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
1169
1170 eqTypes :: [Type] -> [Type] -> Bool
1171 eqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
1172
1173 eqPred :: PredType -> PredType -> Bool
1174 eqPred = eqType
1175
1176 eqPredX :: RnEnv2 -> PredType -> PredType -> Bool
1177 eqPredX env p1 p2 = isEqual $ cmpTypeX env p1 p2
1178
1179 eqTyVarBndrs :: RnEnv2 -> [TyVar] -> [TyVar] -> Maybe RnEnv2
1180 -- Check that the tyvar lists are the same length
1181 -- and have matching kinds; if so, extend the RnEnv2
1182 -- Returns Nothing if they don't match
1183 eqTyVarBndrs env [] []
1184  = Just env
1185 eqTyVarBndrs env (tv1:tvs1) (tv2:tvs2)
1186  | eqTypeX env (tyVarKind tv1) (tyVarKind tv2)
1187  = eqTyVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
1188 eqTyVarBndrs _ _ _= Nothing
1189 \end{code}
1190
1191 Now here comes the real worker
1192
1193 \begin{code}
1194 cmpType :: Type -> Type -> Ordering
1195 cmpType t1 t2 = cmpTypeX rn_env t1 t2
1196   where
1197     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
1198
1199 cmpTypes :: [Type] -> [Type] -> Ordering
1200 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
1201   where
1202     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
1203
1204 cmpPred :: PredType -> PredType -> Ordering
1205 cmpPred p1 p2 = cmpTypeX rn_env p1 p2
1206   where
1207     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType p1 `unionVarSet` tyVarsOfType p2))
1208
1209 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
1210 cmpTypeX env t1 t2 | Just t1' <- coreView t1 = cmpTypeX env t1' t2
1211                    | Just t2' <- coreView t2 = cmpTypeX env t1 t2'
1212 -- We expand predicate types, because in Core-land we have
1213 -- lots of definitions like
1214 --      fOrdBool :: Ord Bool
1215 --      fOrdBool = D:Ord .. .. ..
1216 -- So the RHS has a data type
1217
1218 cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
1219 cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX env (tyVarKind tv1) (tyVarKind tv2)
1220                                                        `thenCmp` cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
1221 cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1222 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1223 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `cmpTc` tc2) `thenCmp` cmpTypesX env tys1 tys2
1224 cmpTypeX _   (LitTy l1)          (LitTy l2)          = compare l1 l2
1225
1226     -- Deal with the rest: TyVarTy < AppTy < FunTy < LitTy < TyConApp < ForAllTy < PredTy
1227 cmpTypeX _ (AppTy _ _)    (TyVarTy _)    = GT
1228
1229 cmpTypeX _ (FunTy _ _)    (TyVarTy _)    = GT
1230 cmpTypeX _ (FunTy _ _)    (AppTy _ _)    = GT
1231
1232 cmpTypeX _ (LitTy _)      (TyVarTy _)    = GT
1233 cmpTypeX _ (LitTy _)      (AppTy _ _)    = GT
1234 cmpTypeX _ (LitTy _)      (FunTy _ _)    = GT
1235
1236 cmpTypeX _ (TyConApp _ _) (TyVarTy _)    = GT
1237 cmpTypeX _ (TyConApp _ _) (AppTy _ _)    = GT
1238 cmpTypeX _ (TyConApp _ _) (FunTy _ _)    = GT
1239 cmpTypeX _ (TyConApp _ _) (LitTy _)      = GT
1240
1241 cmpTypeX _ (ForAllTy _ _) (TyVarTy _)    = GT
1242 cmpTypeX _ (ForAllTy _ _) (AppTy _ _)    = GT
1243 cmpTypeX _ (ForAllTy _ _) (FunTy _ _)    = GT
1244 cmpTypeX _ (ForAllTy _ _) (LitTy _)      = GT
1245 cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = GT
1246
1247 cmpTypeX _ _              _              = LT
1248
1249 -------------
1250 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1251 cmpTypesX _   []        []        = EQ
1252 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1253 cmpTypesX _   []        _         = LT
1254 cmpTypesX _   _         []        = GT
1255
1256 -------------
1257 cmpTc :: TyCon -> TyCon -> Ordering
1258 -- Here we treat * and Constraint as equal
1259 -- See Note [Kind Constraint and kind *] in Kinds.lhs
1260 --
1261 -- Also we treat OpenTypeKind as equal to either * or #
1262 -- See Note [Comparison with OpenTypeKind]
1263 cmpTc tc1 tc2 
1264   | u1 == openTypeKindTyConKey, isSubOpenTypeKindKey u2 = EQ
1265   | u2 == openTypeKindTyConKey, isSubOpenTypeKindKey u1 = EQ
1266   | otherwise = nu1 `compare` nu2
1267   where
1268     u1  = tyConUnique tc1
1269     nu1 = if u1==constraintKindTyConKey then liftedTypeKindTyConKey else u1
1270     u2  = tyConUnique tc2
1271     nu2 = if u2==constraintKindTyConKey then liftedTypeKindTyConKey else u2
1272 \end{code}
1273
1274 Note [Comparison with OpenTypeKind]
1275 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1276 In PrimOpWrappers we have things like
1277    PrimOpWrappers.mkWeak# = /\ a b c. Prim.mkWeak# a b c
1278 where
1279    Prim.mkWeak# :: forall (a:Open) b c. a -> b -> c 
1280                                      -> State# RealWorld -> (# State# RealWorld, Weak# b #)
1281 Now, eta reduction will turn the definition into
1282      PrimOpWrappers.mkWeak# = Prim.mkWeak#
1283 which is kind-of OK, but now the types aren't really equal.  So HACK HACK
1284 we pretend (in Core) that Open is equal to * or #.  I hate this.
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?