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