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