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