(Another) minor refactoring of substitutions
[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, VisibilityFlag(..), KindOrType, PredType, ThetaType,
18 Var, TyVar, isTyVar, TyCoVar, TyBinder,
19
20 -- ** Constructing and deconstructing types
21 mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, repGetTyVar_maybe,
22 getCastedTyVar_maybe, tyVarKind,
23
24 mkAppTy, mkAppTys, splitAppTy, splitAppTys, repSplitAppTys,
25 splitAppTy_maybe, repSplitAppTy_maybe, tcRepSplitAppTy_maybe,
26
27 mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
28 splitFunTys, splitFunTysN,
29 funResultTy, funArgTy,
30
31 mkTyConApp, mkTyConTy,
32 tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
33 tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
34 splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
35 splitListTyConApp_maybe,
36 repSplitTyConApp_maybe,
37
38 mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys,
39 mkVisForAllTys,
40 mkNamedForAllTy,
41 splitForAllTy_maybe, splitForAllTys, splitForAllTy,
42 splitPiTy_maybe, splitPiTys, splitPiTy,
43 splitNamedPiTys,
44 mkPiType, mkPiTypes, mkPiTypesPreferFunTy,
45 piResultTy, piResultTys,
46 applyTys, applyTysD, applyTysX, dropForAlls,
47
48 mkNumLitTy, isNumLitTy,
49 mkStrLitTy, isStrLitTy,
50
51 mkCastTy, mkCoercionTy, splitCastTy_maybe,
52
53 userTypeError_maybe, pprUserTypeErrorTy,
54
55 coAxNthLHS,
56 stripCoercionTy, splitCoercionType_maybe,
57
58 splitPiTysInvisible, filterOutInvisibleTypes,
59 filterOutInvisibleTyVars, partitionInvisibles,
60 synTyConResKind,
61 tyConBinders,
62
63 -- Analyzing types
64 TyCoMapper(..), mapType, mapCoercion,
65
66 -- (Newtypes)
67 newTyConInstRhs,
68
69 -- Pred types
70 mkFamilyTyConApp,
71 isDictLikeTy,
72 mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
73 equalityTyCon,
74 mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
75 mkClassPred,
76 isClassPred, isEqPred, isNomEqPred,
77 isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
78 isCTupleClass,
79
80 -- Deconstructing predicate types
81 PredTree(..), EqRel(..), eqRelRole, classifyPredType,
82 getClassPredTys, getClassPredTys_maybe,
83 getEqPredTys, getEqPredTys_maybe, getEqPredRole,
84 predTypeEqRel,
85
86 -- ** Binders
87 sameVis,
88 mkNamedBinder, mkAnonBinder, isNamedBinder, isAnonBinder,
89 isIdLikeBinder, binderVisibility, binderVar_maybe,
90 binderVar, binderRelevantType_maybe, caseBinder,
91 partitionBinders, partitionBindersIntoBinders,
92 binderType, isVisibleBinder, isInvisibleBinder,
93
94 -- ** Common type constructors
95 funTyCon,
96
97 -- ** Predicates on types
98 allDistinctTyVars,
99 isTyVarTy, isFunTy, isDictTy, isPredTy, isVoidTy, isCoercionTy,
100 isCoercionTy_maybe, isCoercionType, isForAllTy,
101 isPiTy,
102
103 -- (Lifting and boxity)
104 isUnliftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
105 isPrimitiveType, isStrictType,
106 isLevityTy, isLevityVar, isLevityKindedTy,
107 dropLevityArgs,
108 getLevity, getLevityFromKind,
109
110 -- * Main data types representing Kinds
111 Kind,
112
113 -- ** Finding the kind of a type
114 typeKind,
115
116 -- ** Common Kind
117 liftedTypeKind, unliftedTypeKind,
118
119 -- * Type free variables
120 tyCoVarsOfType, tyCoVarsOfTypes, tyCoVarsOfTypeAcc,
121 tyCoVarsOfTypeDSet,
122 coVarsOfType,
123 coVarsOfTypes, closeOverKinds,
124 splitDepVarsOfType, splitDepVarsOfTypes,
125 splitVisVarsOfType, splitVisVarsOfTypes,
126 expandTypeSynonyms,
127 typeSize,
128
129 -- * Well-scoped lists of variables
130 varSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped,
131
132 -- * Type comparison
133 eqType, eqTypeX, eqTypes, cmpType, cmpTypes, cmpTypeX, cmpTypesX, cmpTc,
134 eqVarBndrs,
135
136 -- * Forcing evaluation of types
137 seqType, seqTypes,
138
139 -- * Other views onto Types
140 coreView, coreViewOneStarKind,
141
142 UnaryType, RepType(..), flattenRepType, repType,
143 tyConsOfType,
144
145 -- * Type representation for the code generator
146 typePrimRep, typeRepArity,
147
148 -- * Main type substitution data types
149 TvSubstEnv, -- Representation widely visible
150 TCvSubst(..), -- Representation visible to a few friends
151
152 -- ** Manipulating type substitutions
153 emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
154
155 mkTCvSubst, zipTvSubst, mkTvSubstPrs,
156 notElemTCvSubst,
157 getTvSubstEnv, setTvSubstEnv,
158 zapTCvSubst, getTCvInScope,
159 extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
160 extendTCvSubst, extendCvSubst,
161 extendTvSubst, extendTvSubstList, extendTvSubstAndInScope,
162 isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv,
163 isEmptyTCvSubst, unionTCvSubst,
164
165 -- ** Performing substitution on types and kinds
166 substTy, substTys, substTyWith, substTysWith, substTheta,
167 substTyAddInScope,
168 substTyUnchecked, substTysUnchecked, substThetaUnchecked,
169 substTyWithBindersUnchecked, substTyWithUnchecked,
170 substCoUnchecked, substCoWithUnchecked,
171 substTyVarBndr, substTyVar, substTyVars,
172 cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
173
174 -- * Pretty-printing
175 pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing,
176 pprTvBndr, pprTvBndrs, pprForAll, pprForAllImplicit, pprUserForAll,
177 pprSigmaType,
178 pprTheta, pprThetaArrowTy, pprClassPred,
179 pprKind, pprParendKind, pprSourceTyCon,
180 TyPrec(..), maybeParen,
181 pprTyVar, pprTcAppTy, pprPrefixApp, pprArrowChain,
182
183 -- * Tidying type related things up for printing
184 tidyType, tidyTypes,
185 tidyOpenType, tidyOpenTypes,
186 tidyOpenKind,
187 tidyTyCoVarBndr, tidyTyCoVarBndrs, tidyFreeTyCoVars,
188 tidyOpenTyCoVar, tidyOpenTyCoVars,
189 tidyTyVarOcc,
190 tidyTopType,
191 tidyKind
192 ) where
193
194 #include "HsVersions.h"
195
196 -- We import the representation and primitive functions from TyCoRep.
197 -- Many things are reexported, but not the representation!
198
199 import Kind
200 import TyCoRep
201
202 -- friends:
203 import Var
204 import VarEnv
205 import VarSet
206 import NameEnv
207
208 import Class
209 import TyCon
210 import TysPrim
211 import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind
212 , typeSymbolKind, liftedTypeKind )
213 import PrelNames
214 import CoAxiom
215 import {-# SOURCE #-} Coercion
216
217 -- others
218 import BasicTypes ( Arity, RepArity )
219 import Util
220 import Outputable
221 import FastString
222 import Pair
223 import ListSetOps
224 import Digraph
225
226 import Maybes ( orElse )
227 import Data.Maybe ( isJust, mapMaybe )
228 import Control.Monad ( guard )
229 import Control.Arrow ( first, second )
230
231 -- $type_classification
232 -- #type_classification#
233 --
234 -- Types are one of:
235 --
236 -- [Unboxed] Iff its representation is other than a pointer
237 -- Unboxed types are also unlifted.
238 --
239 -- [Lifted] Iff it has bottom as an element.
240 -- Closures always have lifted types: i.e. any
241 -- let-bound identifier in Core must have a lifted
242 -- type. Operationally, a lifted object is one that
243 -- can be entered.
244 -- Only lifted types may be unified with a type variable.
245 --
246 -- [Algebraic] Iff it is a type with one or more constructors, whether
247 -- declared with @data@ or @newtype@.
248 -- An algebraic type is one that can be deconstructed
249 -- with a case expression. This is /not/ the same as
250 -- lifted types, because we also include unboxed
251 -- tuples in this classification.
252 --
253 -- [Data] Iff it is a type declared with @data@, or a boxed tuple.
254 --
255 -- [Primitive] Iff it is a built-in type that can't be expressed in Haskell.
256 --
257 -- Currently, all primitive types are unlifted, but that's not necessarily
258 -- the case: for example, @Int@ could be primitive.
259 --
260 -- Some primitive types are unboxed, such as @Int#@, whereas some are boxed
261 -- but unlifted (such as @ByteArray#@). The only primitive types that we
262 -- classify as algebraic are the unboxed tuples.
263 --
264 -- Some examples of type classifications that may make this a bit clearer are:
265 --
266 -- @
267 -- Type primitive boxed lifted algebraic
268 -- -----------------------------------------------------------------------------
269 -- Int# Yes No No No
270 -- ByteArray# Yes Yes No No
271 -- (\# a, b \#) Yes No No Yes
272 -- ( a, b ) No Yes Yes Yes
273 -- [a] No Yes Yes Yes
274 -- @
275
276 -- $representation_types
277 -- A /source type/ is a type that is a separate type as far as the type checker is
278 -- concerned, but which has a more low-level representation as far as Core-to-Core
279 -- passes and the rest of the back end is concerned.
280 --
281 -- You don't normally have to worry about this, as the utility functions in
282 -- this module will automatically convert a source into a representation type
283 -- if they are spotted, to the best of it's abilities. If you don't want this
284 -- to happen, use the equivalent functions from the "TcType" module.
285
286 {-
287 ************************************************************************
288 * *
289 Type representation
290 * *
291 ************************************************************************
292 -}
293
294 {-# INLINE coreView #-}
295 coreView :: Type -> Maybe Type
296 -- ^ This function Strips off the /top layer only/ of a type synonym
297 -- application (if any) its underlying representation type.
298 -- Returns Nothing if there is nothing to look through.
299 --
300 -- By being non-recursive and inlined, this case analysis gets efficiently
301 -- joined onto the case analysis that the caller is already doing
302 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
303 = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
304 -- The free vars of 'rhs' should all be bound by 'tenv', so it's
305 -- ok to use 'substTy' here.
306 -- See also Note [The substitution invariant] in TyCoRep.
307 -- Its important to use mkAppTys, rather than (foldl AppTy),
308 -- because the function part might well return a
309 -- partially-applied type constructor; indeed, usually will!
310 coreView _ = Nothing
311
312 -- | Like 'coreView', but it also "expands" @Constraint@ to become
313 -- @TYPE Lifted@.
314 coreViewOneStarKind :: Type -> Maybe Type
315 coreViewOneStarKind ty
316 | Just ty' <- coreView ty = Just ty'
317 | TyConApp tc [] <- ty
318 , isStarKindSynonymTyCon tc = Just liftedTypeKind
319 | otherwise = Nothing
320
321 -----------------------------------------------
322 expandTypeSynonyms :: Type -> Type
323 -- ^ Expand out all type synonyms. Actually, it'd suffice to expand out
324 -- just the ones that discard type variables (e.g. type Funny a = Int)
325 -- But we don't know which those are currently, so we just expand all.
326 --
327 -- 'expandTypeSynonyms' only expands out type synonyms mentioned in the type,
328 -- not in the kinds of any TyCon or TyVar mentioned in the type.
329 expandTypeSynonyms ty
330 = go (mkEmptyTCvSubst (mkTyCoInScopeSet [ty] [])) ty
331 where
332 go subst (TyConApp tc tys)
333 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
334 = let subst' = unionTCvSubst subst (mkTvSubstPrs tenv) in
335 go subst' (mkAppTys rhs tys')
336 | otherwise
337 = TyConApp tc (map (go subst) tys)
338 go _ (LitTy l) = LitTy l
339 go subst (TyVarTy tv) = substTyVar subst tv
340 go subst (AppTy t1 t2) = mkAppTy (go subst t1) (go subst t2)
341 go subst (ForAllTy (Anon arg) res)
342 = mkFunTy (go subst arg) (go subst res)
343 go subst (ForAllTy (Named tv vis) t)
344 = let (subst', tv') = substTyVarBndrCallback go subst tv in
345 ForAllTy (Named tv' vis) (go subst' t)
346 go subst (CastTy ty co) = mkCastTy (go subst ty) (go_co subst co)
347 go subst (CoercionTy co) = mkCoercionTy (go_co subst co)
348
349 go_co subst (Refl r ty)
350 = mkReflCo r (go subst ty)
351 -- NB: coercions are always expanded upon creation
352 go_co subst (TyConAppCo r tc args)
353 = mkTyConAppCo r tc (map (go_co subst) args)
354 go_co subst (AppCo co arg)
355 = mkAppCo (go_co subst co) (go_co subst arg)
356 go_co subst (ForAllCo tv kind_co co)
357 = let (subst', tv', kind_co') = go_cobndr subst tv kind_co in
358 mkForAllCo tv' kind_co' (go_co subst' co)
359 go_co subst (CoVarCo cv)
360 = substCoVar subst cv
361 go_co subst (AxiomInstCo ax ind args)
362 = mkAxiomInstCo ax ind (map (go_co subst) args)
363 go_co subst (UnivCo p r t1 t2)
364 = mkUnivCo (go_prov subst p) r (go subst t1) (go subst t2)
365 go_co subst (SymCo co)
366 = mkSymCo (go_co subst co)
367 go_co subst (TransCo co1 co2)
368 = mkTransCo (go_co subst co1) (go_co subst co2)
369 go_co subst (NthCo n co)
370 = mkNthCo n (go_co subst co)
371 go_co subst (LRCo lr co)
372 = mkLRCo lr (go_co subst co)
373 go_co subst (InstCo co arg)
374 = mkInstCo (go_co subst co) (go_co subst arg)
375 go_co subst (CoherenceCo co1 co2)
376 = mkCoherenceCo (go_co subst co1) (go_co subst co2)
377 go_co subst (KindCo co)
378 = mkKindCo (go_co subst co)
379 go_co subst (SubCo co)
380 = mkSubCo (go_co subst co)
381 go_co subst (AxiomRuleCo ax cs) = AxiomRuleCo ax (map (go_co subst) cs)
382
383 go_prov _ UnsafeCoerceProv = UnsafeCoerceProv
384 go_prov subst (PhantomProv co) = PhantomProv (go_co subst co)
385 go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
386 go_prov _ p@(PluginProv _) = p
387 go_prov _ (HoleProv h) = pprPanic "expandTypeSynonyms hit a hole" (ppr h)
388
389 -- the "False" and "const" are to accommodate the type of
390 -- substForAllCoBndrCallback, which is general enough to
391 -- handle coercion optimization (which sometimes swaps the
392 -- order of a coercion)
393 go_cobndr subst = substForAllCoBndrCallback False (go_co subst) subst
394
395 {-
396 ************************************************************************
397 * *
398 Analyzing types
399 * *
400 ************************************************************************
401
402 These functions do a map-like operation over types, performing some operation
403 on all variables and binding sites. Primarily used for zonking.
404
405 Note [Efficiency for mapCoercion ForAllCo case]
406 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
407 As noted in Note [Forall coercions] in TyCoRep, a ForAllCo is a bit redundant.
408 It stores a TyVar and a Coercion, where the kind of the TyVar always matches
409 the left-hand kind of the coercion. This is convenient lots of the time, but
410 not when mapping a function over a coercion.
411
412 The problem is that tcm_tybinder will affect the TyVar's kind and
413 mapCoercion will affect the Coercion, and we hope that the results will be
414 the same. Even if they are the same (which should generally happen with
415 correct algorithms), then there is an efficiency issue. In particular,
416 this problem seems to make what should be a linear algorithm into a potentially
417 exponential one. But it's only going to be bad in the case where there's
418 lots of foralls in the kinds of other foralls. Like this:
419
420 forall a : (forall b : (forall c : ...). ...). ...
421
422 This construction seems unlikely. So we'll do the inefficient, easy way
423 for now.
424
425 Note [Specialising mappers]
426 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
427 These INLINABLE pragmas are indispensable. mapType/mapCoercion are used
428 to implement zonking, and it's vital that they get specialised to the TcM
429 monad. This specialisation happens automatically (that is, without a
430 SPECIALISE pragma) as long as the definitions are INLINABLE. For example,
431 this one change made a 20% allocation difference in perf/compiler/T5030.
432
433 -}
434
435 -- | This describes how a "map" operation over a type/coercion should behave
436 data TyCoMapper env m
437 = TyCoMapper
438 { tcm_smart :: Bool -- ^ Should the new type be created with smart
439 -- constructors?
440 , tcm_tyvar :: env -> TyVar -> m Type
441 , tcm_covar :: env -> CoVar -> m Coercion
442 , tcm_hole :: env -> CoercionHole -> Role
443 -> Type -> Type -> m Coercion
444 -- ^ What to do with coercion holes. See Note [Coercion holes] in
445 -- TyCoRep.
446
447 , tcm_tybinder :: env -> TyVar -> VisibilityFlag -> m (env, TyVar)
448 -- ^ The returned env is used in the extended scope
449 }
450
451 {-# INLINABLE mapType #-} -- See Note [Specialising mappers]
452 mapType :: Monad m => TyCoMapper env m -> env -> Type -> m Type
453 mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
454 , tcm_tybinder = tybinder })
455 env ty
456 = go ty
457 where
458 go (TyVarTy tv) = tyvar env tv
459 go (AppTy t1 t2) = mkappty <$> go t1 <*> go t2
460 go (TyConApp tc tys) = mktyconapp tc <$> mapM go tys
461 go (ForAllTy (Anon arg) res) = mkfunty <$> go arg <*> go res
462 go (ForAllTy (Named tv vis) inner)
463 = do { (env', tv') <- tybinder env tv vis
464 ; inner' <- mapType mapper env' inner
465 ; return $ ForAllTy (Named tv' vis) inner' }
466 go ty@(LitTy {}) = return ty
467 go (CastTy ty co) = mkcastty <$> go ty <*> mapCoercion mapper env co
468 go (CoercionTy co) = CoercionTy <$> mapCoercion mapper env co
469
470 (mktyconapp, mkappty, mkcastty, mkfunty)
471 | smart = (mkTyConApp, mkAppTy, mkCastTy, mkFunTy)
472 | otherwise = (TyConApp, AppTy, CastTy, ForAllTy . Anon)
473
474 {-# INLINABLE mapCoercion #-} -- See Note [Specialising mappers]
475 mapCoercion :: Monad m
476 => TyCoMapper env m -> env -> Coercion -> m Coercion
477 mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
478 , tcm_hole = cohole, tcm_tybinder = tybinder })
479 env co
480 = go co
481 where
482 go (Refl r ty) = Refl r <$> mapType mapper env ty
483 go (TyConAppCo r tc args)
484 = mktyconappco r tc <$> mapM go args
485 go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
486 go (ForAllCo tv kind_co co)
487 = do { kind_co' <- go kind_co
488 ; (env', tv') <- tybinder env tv Invisible
489 ; co' <- mapCoercion mapper env' co
490 ; return $ mkforallco tv' kind_co' co' }
491 -- See Note [Efficiency for mapCoercion ForAllCo case]
492 go (CoVarCo cv) = covar env cv
493 go (AxiomInstCo ax i args)
494 = mkaxiominstco ax i <$> mapM go args
495 go (UnivCo (HoleProv hole) r t1 t2)
496 = cohole env hole r t1 t2
497 go (UnivCo p r t1 t2)
498 = mkunivco <$> go_prov p <*> pure r
499 <*> mapType mapper env t1 <*> mapType mapper env t2
500 go (SymCo co) = mksymco <$> go co
501 go (TransCo c1 c2) = mktransco <$> go c1 <*> go c2
502 go (AxiomRuleCo r cos) = AxiomRuleCo r <$> mapM go cos
503 go (NthCo i co) = mknthco i <$> go co
504 go (LRCo lr co) = mklrco lr <$> go co
505 go (InstCo co arg) = mkinstco <$> go co <*> go arg
506 go (CoherenceCo c1 c2) = mkcoherenceco <$> go c1 <*> go c2
507 go (KindCo co) = mkkindco <$> go co
508 go (SubCo co) = mksubco <$> go co
509
510 go_prov UnsafeCoerceProv = return UnsafeCoerceProv
511 go_prov (PhantomProv co) = PhantomProv <$> go co
512 go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co
513 go_prov p@(PluginProv _) = return p
514 go_prov (HoleProv _) = panic "mapCoercion"
515
516 ( mktyconappco, mkappco, mkaxiominstco, mkunivco
517 , mksymco, mktransco, mknthco, mklrco, mkinstco, mkcoherenceco
518 , mkkindco, mksubco, mkforallco)
519 | smart
520 = ( mkTyConAppCo, mkAppCo, mkAxiomInstCo, mkUnivCo
521 , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo, mkCoherenceCo
522 , mkKindCo, mkSubCo, mkForAllCo )
523 | otherwise
524 = ( TyConAppCo, AppCo, AxiomInstCo, UnivCo
525 , SymCo, TransCo, NthCo, LRCo, InstCo, CoherenceCo
526 , KindCo, SubCo, ForAllCo )
527
528 {-
529 ************************************************************************
530 * *
531 \subsection{Constructor-specific functions}
532 * *
533 ************************************************************************
534
535
536 ---------------------------------------------------------------------
537 TyVarTy
538 ~~~~~~~
539 -}
540
541 -- | Attempts to obtain the type variable underlying a 'Type', and panics with the
542 -- given message if this is not a type variable type. See also 'getTyVar_maybe'
543 getTyVar :: String -> Type -> TyVar
544 getTyVar msg ty = case getTyVar_maybe ty of
545 Just tv -> tv
546 Nothing -> panic ("getTyVar: " ++ msg)
547
548 isTyVarTy :: Type -> Bool
549 isTyVarTy ty = isJust (getTyVar_maybe ty)
550
551 -- | Attempts to obtain the type variable underlying a 'Type'
552 getTyVar_maybe :: Type -> Maybe TyVar
553 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
554 | otherwise = repGetTyVar_maybe ty
555
556 -- | If the type is a tyvar, possibly under a cast, returns it, along
557 -- with the coercion. Thus, the co is :: kind tv ~R kind type
558 getCastedTyVar_maybe :: Type -> Maybe (TyVar, Coercion)
559 getCastedTyVar_maybe ty | Just ty' <- coreView ty = getCastedTyVar_maybe ty'
560 getCastedTyVar_maybe (CastTy (TyVarTy tv) co) = Just (tv, co)
561 getCastedTyVar_maybe (TyVarTy tv)
562 = Just (tv, mkReflCo Nominal (tyVarKind tv))
563 getCastedTyVar_maybe _ = Nothing
564
565 -- | Attempts to obtain the type variable underlying a 'Type', without
566 -- any expansion
567 repGetTyVar_maybe :: Type -> Maybe TyVar
568 repGetTyVar_maybe (TyVarTy tv) = Just tv
569 repGetTyVar_maybe _ = Nothing
570
571 allDistinctTyVars :: [KindOrType] -> Bool
572 allDistinctTyVars tkvs = go emptyVarSet tkvs
573 where
574 go _ [] = True
575 go so_far (ty : tys)
576 = case getTyVar_maybe ty of
577 Nothing -> False
578 Just tv | tv `elemVarSet` so_far -> False
579 | otherwise -> go (so_far `extendVarSet` tv) tys
580
581 {-
582 ---------------------------------------------------------------------
583 AppTy
584 ~~~~~
585 We need to be pretty careful with AppTy to make sure we obey the
586 invariant that a TyConApp is always visibly so. mkAppTy maintains the
587 invariant: use it.
588
589 Note [Decomposing fat arrow c=>t]
590 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
591 Can we unify (a b) with (Eq a => ty)? If we do so, we end up with
592 a partial application like ((=>) Eq a) which doesn't make sense in
593 source Haskell. In constrast, we *can* unify (a b) with (t1 -> t2).
594 Here's an example (Trac #9858) of how you might do it:
595 i :: (Typeable a, Typeable b) => Proxy (a b) -> TypeRep
596 i p = typeRep p
597
598 j = i (Proxy :: Proxy (Eq Int => Int))
599 The type (Proxy (Eq Int => Int)) is only accepted with -XImpredicativeTypes,
600 but suppose we want that. But then in the call to 'i', we end
601 up decomposing (Eq Int => Int), and we definitely don't want that.
602
603 This really only applies to the type checker; in Core, '=>' and '->'
604 are the same, as are 'Constraint' and '*'. But for now I've put
605 the test in repSplitAppTy_maybe, which applies throughout, because
606 the other calls to splitAppTy are in Unify, which is also used by
607 the type checker (e.g. when matching type-function equations).
608
609 -}
610
611 -- | Applies a type to another, as in e.g. @k a@
612 mkAppTy :: Type -> Type -> Type
613 mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
614 mkAppTy ty1 ty2 = AppTy ty1 ty2
615 -- Note that the TyConApp could be an
616 -- under-saturated type synonym. GHC allows that; e.g.
617 -- type Foo k = k a -> k a
618 -- type Id x = x
619 -- foo :: Foo Id -> Foo Id
620 --
621 -- Here Id is partially applied in the type sig for Foo,
622 -- but once the type synonyms are expanded all is well
623
624 mkAppTys :: Type -> [Type] -> Type
625 mkAppTys ty1 [] = ty1
626 mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
627 mkAppTys ty1 tys2 = foldl AppTy ty1 tys2
628
629 -------------
630 splitAppTy_maybe :: Type -> Maybe (Type, Type)
631 -- ^ Attempt to take a type application apart, whether it is a
632 -- function, type constructor, or plain type application. Note
633 -- that type family applications are NEVER unsaturated by this!
634 splitAppTy_maybe ty | Just ty' <- coreView ty
635 = splitAppTy_maybe ty'
636 splitAppTy_maybe ty = repSplitAppTy_maybe ty
637
638 -------------
639 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
640 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
641 -- any Core view stuff is already done
642 repSplitAppTy_maybe (ForAllTy (Anon ty1) ty2)
643 = Just (TyConApp funTyCon [ty1], ty2)
644 repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
645 repSplitAppTy_maybe (TyConApp tc tys)
646 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
647 , Just (tys', ty') <- snocView tys
648 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
649 repSplitAppTy_maybe _other = Nothing
650
651 -- this one doesn't braek apart (c => t).
652 -- See Note [Decomposing fat arrow c=>t]
653 -- Defined here to avoid module loops between Unify and TcType.
654 tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
655 -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
656 -- any coreView stuff is already done. Refuses to look through (c => t)
657 tcRepSplitAppTy_maybe (ForAllTy (Anon ty1) ty2)
658 | isConstraintKind (typeKind ty1) = Nothing -- See Note [Decomposing fat arrow c=>t]
659 | otherwise = Just (TyConApp funTyCon [ty1], ty2)
660 tcRepSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
661 tcRepSplitAppTy_maybe (TyConApp tc tys)
662 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
663 , Just (tys', ty') <- snocView tys
664 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
665 tcRepSplitAppTy_maybe _other = Nothing
666 -------------
667 splitAppTy :: Type -> (Type, Type)
668 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
669 -- and panics if this is not possible
670 splitAppTy ty = case splitAppTy_maybe ty of
671 Just pr -> pr
672 Nothing -> panic "splitAppTy"
673
674 -------------
675 splitAppTys :: Type -> (Type, [Type])
676 -- ^ Recursively splits a type as far as is possible, leaving a residual
677 -- type being applied to and the type arguments applied to it. Never fails,
678 -- even if that means returning an empty list of type applications.
679 splitAppTys ty = split ty ty []
680 where
681 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
682 split _ (AppTy ty arg) args = split ty ty (arg:args)
683 split _ (TyConApp tc tc_args) args
684 = let -- keep type families saturated
685 n | mightBeUnsaturatedTyCon tc = 0
686 | otherwise = tyConArity tc
687 (tc_args1, tc_args2) = splitAt n tc_args
688 in
689 (TyConApp tc tc_args1, tc_args2 ++ args)
690 split _ (ForAllTy (Anon ty1) ty2) args = ASSERT( null args )
691 (TyConApp funTyCon [], [ty1,ty2])
692 split orig_ty _ args = (orig_ty, args)
693
694 -- | Like 'splitAppTys', but doesn't look through type synonyms
695 repSplitAppTys :: Type -> (Type, [Type])
696 repSplitAppTys ty = split ty []
697 where
698 split (AppTy ty arg) args = split ty (arg:args)
699 split (TyConApp tc tc_args) args
700 = let n | mightBeUnsaturatedTyCon tc = 0
701 | otherwise = tyConArity tc
702 (tc_args1, tc_args2) = splitAt n tc_args
703 in
704 (TyConApp tc tc_args1, tc_args2 ++ args)
705 split (ForAllTy (Anon ty1) ty2) args = ASSERT( null args )
706 (TyConApp funTyCon [], [ty1, ty2])
707 split ty args = (ty, args)
708
709 {-
710 LitTy
711 ~~~~~
712 -}
713
714 mkNumLitTy :: Integer -> Type
715 mkNumLitTy n = LitTy (NumTyLit n)
716
717 -- | Is this a numeric literal. We also look through type synonyms.
718 isNumLitTy :: Type -> Maybe Integer
719 isNumLitTy ty | Just ty1 <- coreView ty = isNumLitTy ty1
720 isNumLitTy (LitTy (NumTyLit n)) = Just n
721 isNumLitTy _ = Nothing
722
723 mkStrLitTy :: FastString -> Type
724 mkStrLitTy s = LitTy (StrTyLit s)
725
726 -- | Is this a symbol literal. We also look through type synonyms.
727 isStrLitTy :: Type -> Maybe FastString
728 isStrLitTy ty | Just ty1 <- coreView ty = isStrLitTy ty1
729 isStrLitTy (LitTy (StrTyLit s)) = Just s
730 isStrLitTy _ = Nothing
731
732
733 -- | Is this type a custom user error?
734 -- If so, give us the kind and the error message.
735 userTypeError_maybe :: Type -> Maybe Type
736 userTypeError_maybe t
737 = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t
738 -- There may be more than 2 arguments, if the type error is
739 -- used as a type constructor (e.g. at kind `Type -> Type`).
740
741 ; guard (tyConName tc == errorMessageTypeErrorFamName)
742 ; return msg }
743
744 -- | Render a type corresponding to a user type error into a SDoc.
745 pprUserTypeErrorTy :: Type -> SDoc
746 pprUserTypeErrorTy ty =
747 case splitTyConApp_maybe ty of
748
749 -- Text "Something"
750 Just (tc,[txt])
751 | tyConName tc == typeErrorTextDataConName
752 , Just str <- isStrLitTy txt -> ftext str
753
754 -- ShowType t
755 Just (tc,[_k,t])
756 | tyConName tc == typeErrorShowTypeDataConName -> ppr t
757
758 -- t1 :<>: t2
759 Just (tc,[t1,t2])
760 | tyConName tc == typeErrorAppendDataConName ->
761 pprUserTypeErrorTy t1 <> pprUserTypeErrorTy t2
762
763 -- t1 :$$: t2
764 Just (tc,[t1,t2])
765 | tyConName tc == typeErrorVAppendDataConName ->
766 pprUserTypeErrorTy t1 $$ pprUserTypeErrorTy t2
767
768 -- An uneavaluated type function
769 _ -> ppr ty
770
771
772
773
774 {-
775 ---------------------------------------------------------------------
776 FunTy
777 ~~~~~
778
779 Function types are represented with (ForAllTy (Anon ...) ...)
780 -}
781
782 isFunTy :: Type -> Bool
783 isFunTy ty = isJust (splitFunTy_maybe ty)
784
785 splitFunTy :: Type -> (Type, Type)
786 -- ^ Attempts to extract the argument and result types from a type, and
787 -- panics if that is not possible. See also 'splitFunTy_maybe'
788 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
789 splitFunTy (ForAllTy (Anon arg) res) = (arg, res)
790 splitFunTy other = pprPanic "splitFunTy" (ppr other)
791
792 splitFunTy_maybe :: Type -> Maybe (Type, Type)
793 -- ^ Attempts to extract the argument and result types from a type
794 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
795 splitFunTy_maybe (ForAllTy (Anon arg) res) = Just (arg, res)
796 splitFunTy_maybe _ = Nothing
797
798 splitFunTys :: Type -> ([Type], Type)
799 splitFunTys ty = split [] ty ty
800 where
801 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
802 split args _ (ForAllTy (Anon arg) res) = split (arg:args) res res
803 split args orig_ty _ = (reverse args, orig_ty)
804
805 splitFunTysN :: Int -> Type -> ([Type], Type)
806 -- ^ Split off exactly the given number argument types, and panics if that is not possible
807 splitFunTysN 0 ty = ([], ty)
808 splitFunTysN n ty = ASSERT2( isFunTy ty, int n <+> ppr ty )
809 case splitFunTy ty of { (arg, res) ->
810 case splitFunTysN (n-1) res of { (args, res) ->
811 (arg:args, res) }}
812
813 funResultTy :: Type -> Type
814 -- ^ Extract the function result type and panic if that is not possible
815 funResultTy ty = piResultTy ty (pprPanic "funResultTy" (ppr ty))
816
817 -- | Essentially 'funResultTy' on kinds handling pi-types too
818 piResultTy :: Type -> Type -> Type
819 piResultTy ty arg | Just ty' <- coreView ty = piResultTy ty' arg
820 piResultTy (ForAllTy (Anon _) res) _ = res
821 piResultTy (ForAllTy (Named tv _) res) arg = substTyWithUnchecked [tv] [arg] res
822 piResultTy ty arg = pprPanic "piResultTy"
823 (ppr ty $$ ppr arg)
824
825 -- | Fold 'piResultTy' over many types
826 piResultTys :: Type -> [Type] -> Type
827 piResultTys = foldl piResultTy
828
829 funArgTy :: Type -> Type
830 -- ^ Extract the function argument type and panic if that is not possible
831 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
832 funArgTy (ForAllTy (Anon arg) _res) = arg
833 funArgTy ty = pprPanic "funArgTy" (ppr ty)
834
835 {-
836 ---------------------------------------------------------------------
837 TyConApp
838 ~~~~~~~~
839 -}
840
841 -- | A key function: builds a 'TyConApp' or 'FunTy' as appropriate to
842 -- its arguments. Applies its arguments to the constructor from left to right.
843 mkTyConApp :: TyCon -> [Type] -> Type
844 mkTyConApp tycon tys
845 | isFunTyCon tycon, [ty1,ty2] <- tys
846 = ForAllTy (Anon ty1) ty2
847
848 | otherwise
849 = TyConApp tycon tys
850
851 -- splitTyConApp "looks through" synonyms, because they don't
852 -- mean a distinct type, but all other type-constructor applications
853 -- including functions are returned as Just ..
854
855 -- | Retrieve the tycon heading this type, if there is one. Does /not/
856 -- look through synonyms.
857 tyConAppTyConPicky_maybe :: Type -> Maybe TyCon
858 tyConAppTyConPicky_maybe (TyConApp tc _) = Just tc
859 tyConAppTyConPicky_maybe (ForAllTy (Anon _) _) = Just funTyCon
860 tyConAppTyConPicky_maybe _ = Nothing
861
862
863 -- | The same as @fst . splitTyConApp@
864 tyConAppTyCon_maybe :: Type -> Maybe TyCon
865 tyConAppTyCon_maybe ty | Just ty' <- coreView ty = tyConAppTyCon_maybe ty'
866 tyConAppTyCon_maybe (TyConApp tc _) = Just tc
867 tyConAppTyCon_maybe (ForAllTy (Anon _) _) = Just funTyCon
868 tyConAppTyCon_maybe _ = Nothing
869
870 tyConAppTyCon :: Type -> TyCon
871 tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr ty)
872
873 -- | The same as @snd . splitTyConApp@
874 tyConAppArgs_maybe :: Type -> Maybe [Type]
875 tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty'
876 tyConAppArgs_maybe (TyConApp _ tys) = Just tys
877 tyConAppArgs_maybe (ForAllTy (Anon arg) res) = Just [arg,res]
878 tyConAppArgs_maybe _ = Nothing
879
880 tyConAppArgs :: Type -> [Type]
881 tyConAppArgs ty = tyConAppArgs_maybe ty `orElse` pprPanic "tyConAppArgs" (ppr ty)
882
883 tyConAppArgN :: Int -> Type -> Type
884 -- Executing Nth
885 tyConAppArgN n ty
886 = case tyConAppArgs_maybe ty of
887 Just tys -> ASSERT2( n < length tys, ppr n <+> ppr tys ) tys `getNth` n
888 Nothing -> pprPanic "tyConAppArgN" (ppr n <+> ppr ty)
889
890 -- | Attempts to tease a type apart into a type constructor and the application
891 -- of a number of arguments to that constructor. Panics if that is not possible.
892 -- See also 'splitTyConApp_maybe'
893 splitTyConApp :: Type -> (TyCon, [Type])
894 splitTyConApp ty = case splitTyConApp_maybe ty of
895 Just stuff -> stuff
896 Nothing -> pprPanic "splitTyConApp" (ppr ty)
897
898 -- | Attempts to tease a type apart into a type constructor and the application
899 -- of a number of arguments to that constructor
900 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
901 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
902 splitTyConApp_maybe ty = repSplitTyConApp_maybe ty
903
904 -- | Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
905 -- assumes the synonyms have already been dealt with.
906 repSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
907 repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
908 repSplitTyConApp_maybe (ForAllTy (Anon arg) res) = Just (funTyCon, [arg,res])
909 repSplitTyConApp_maybe _ = Nothing
910
911 -- | Attempts to tease a list type apart and gives the type of the elements if
912 -- successful (looks through type synonyms)
913 splitListTyConApp_maybe :: Type -> Maybe Type
914 splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
915 Just (tc,[e]) | tc == listTyCon -> Just e
916 _other -> Nothing
917
918 -- | What is the role assigned to the next parameter of this type? Usually,
919 -- this will be 'Nominal', but if the type is a 'TyConApp', we may be able to
920 -- do better. The type does *not* have to be well-kinded when applied for this
921 -- to work!
922 nextRole :: Type -> Role
923 nextRole ty
924 | Just (tc, tys) <- splitTyConApp_maybe ty
925 , let num_tys = length tys
926 , num_tys < tyConArity tc
927 = tyConRoles tc `getNth` num_tys
928
929 | otherwise
930 = Nominal
931
932 newTyConInstRhs :: TyCon -> [Type] -> Type
933 -- ^ Unwrap one 'layer' of newtype on a type constructor and its
934 -- arguments, using an eta-reduced version of the @newtype@ if possible.
935 -- This requires tys to have at least @newTyConInstArity tycon@ elements.
936 newTyConInstRhs tycon tys
937 = ASSERT2( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs )
938 applyTysX tvs rhs tys
939 where
940 (tvs, rhs) = newTyConEtadRhs tycon
941
942 {-
943 ---------------------------------------------------------------------
944 CastTy
945 ~~~~~~
946 A casted type has its *kind* casted into something new.
947
948 Note [Weird typing rule for ForAllTy]
949 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
950
951 Here is the (truncated) typing rule for the dependent ForAllTy:
952
953 inner : kind
954 ------------------------------------
955 ForAllTy (Named tv vis) inner : kind
956
957 Note that neither the inner type nor for ForAllTy itself have to have
958 kind *! But, it means that we should push any kind casts through the
959 ForAllTy. The only trouble is avoiding capture.
960
961 -}
962
963 splitCastTy_maybe :: Type -> Maybe (Type, Coercion)
964 splitCastTy_maybe ty | Just ty' <- coreView ty = splitCastTy_maybe ty'
965 splitCastTy_maybe (CastTy ty co) = Just (ty, co)
966 splitCastTy_maybe _ = Nothing
967
968 -- | Make a 'CastTy'. The Coercion must be nominal. This function looks
969 -- at the entire structure of the type and coercion in an attempt to
970 -- maintain representation invariance (that is, any two types that are `eqType`
971 -- look the same). Be very wary of calling this in a loop.
972 mkCastTy :: Type -> Coercion -> Type
973 -- Running example:
974 -- T :: forall k1. k1 -> forall k2. k2 -> Bool -> Maybe k1 -> *
975 -- co :: * ~R X (maybe X is a newtype around *)
976 -- ty = T Nat 3 Symbol "foo" True (Just 2)
977 --
978 -- We wish to "push" the cast down as far as possible. See also
979 -- Note [Pushing down casts] in TyCoRep. Here is where we end
980 -- up:
981 --
982 -- (T Nat 3 Symbol |> <Symbol> -> <Bool> -> <Maybe Nat> -> co)
983 -- "foo" True (Just 2)
984 --
985 mkCastTy ty co | isReflexiveCo co = ty
986 -- NB: Do the slow check here. This is important to keep the splitXXX
987 -- functions working properly. Otherwise, we may end up with something
988 -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
989 -- fails under splitFunTy_maybe. This happened with the cheaper check
990 -- in test dependent/should_compile/dynamic-paper.
991
992 mkCastTy (CastTy ty co1) co2 = mkCastTy ty (co1 `mkTransCo` co2)
993 -- See Note [Weird typing rule for ForAllTy]
994 mkCastTy (ForAllTy (Named tv vis) inner_ty) co
995 = -- have to make sure that pushing the co in doesn't capture the bound var
996 let fvs = tyCoVarsOfCo co
997 empty_subst = mkEmptyTCvSubst (mkInScopeSet fvs)
998 (subst, tv') = substTyVarBndr empty_subst tv
999 in
1000 ForAllTy (Named tv' vis) (substTy subst inner_ty `mkCastTy` co)
1001 mkCastTy ty co = -- NB: don't check if the coercion "from" type matches here;
1002 -- there may be unzonked variables about
1003 let result = split_apps [] ty co in
1004 ASSERT2( CastTy ty co `eqType` result
1005 , ppr ty <+> dcolon <+> ppr (typeKind ty) $$
1006 ppr co <+> dcolon <+> ppr (coercionKind co) $$
1007 ppr result <+> dcolon <+> ppr (typeKind result) )
1008 result
1009 where
1010 -- split_apps breaks apart any type applications, so we can see how far down
1011 -- to push the cast
1012 split_apps args (AppTy t1 t2) co
1013 = split_apps (t2:args) t1 co
1014 split_apps args (TyConApp tc tc_args) co
1015 | mightBeUnsaturatedTyCon tc
1016 = affix_co (tyConKind tc) (mkTyConTy tc) (tc_args `chkAppend` args) co
1017 | otherwise -- not decomposable... but it may still be oversaturated
1018 = let (non_decomp_args, decomp_args) = splitAt (tyConArity tc) tc_args
1019 saturated_tc = mkTyConApp tc non_decomp_args
1020 in
1021 affix_co (typeKind saturated_tc) saturated_tc (decomp_args `chkAppend` args) co
1022
1023 split_apps args (ForAllTy (Anon arg) res) co
1024 = affix_co (tyConKind funTyCon) (mkTyConTy funTyCon)
1025 (arg : res : args) co
1026 split_apps args ty co
1027 = affix_co (typeKind ty) ty args co
1028
1029 -- having broken everything apart, this figures out the point at which there
1030 -- are no more dependent quantifications, and puts the cast there
1031 affix_co _ ty [] co = no_double_casts ty co
1032 affix_co kind ty args co
1033 -- if kind contains any dependent quantifications, we can't push.
1034 -- apply arguments until it doesn't
1035 = let (bndrs, _inner_ki) = splitPiTys kind
1036 (no_dep_bndrs, some_dep_bndrs) = spanEnd isAnonBinder bndrs
1037 (some_dep_args, rest_args) = splitAtList some_dep_bndrs args
1038 dep_subst = zipTyBinderSubst some_dep_bndrs some_dep_args
1039 used_no_dep_bndrs = takeList rest_args no_dep_bndrs
1040 rest_arg_tys = substTys dep_subst (map binderType used_no_dep_bndrs)
1041 co' = mkFunCos Nominal
1042 (map (mkReflCo Nominal) rest_arg_tys)
1043 co
1044 in
1045 ((ty `mkAppTys` some_dep_args) `no_double_casts` co') `mkAppTys` rest_args
1046
1047 no_double_casts (CastTy ty co1) co2 = CastTy ty (co1 `mkTransCo` co2)
1048 no_double_casts ty co = CastTy ty co
1049
1050 {-
1051 --------------------------------------------------------------------
1052 CoercionTy
1053 ~~~~~~~~~~
1054 CoercionTy allows us to inject coercions into types. A CoercionTy
1055 should appear only in the right-hand side of an application.
1056 -}
1057
1058 mkCoercionTy :: Coercion -> Type
1059 mkCoercionTy = CoercionTy
1060
1061 isCoercionTy :: Type -> Bool
1062 isCoercionTy (CoercionTy _) = True
1063 isCoercionTy _ = False
1064
1065 isCoercionTy_maybe :: Type -> Maybe Coercion
1066 isCoercionTy_maybe (CoercionTy co) = Just co
1067 isCoercionTy_maybe _ = Nothing
1068
1069 stripCoercionTy :: Type -> Coercion
1070 stripCoercionTy (CoercionTy co) = co
1071 stripCoercionTy ty = pprPanic "stripCoercionTy" (ppr ty)
1072
1073 {-
1074 ---------------------------------------------------------------------
1075 SynTy
1076 ~~~~~
1077
1078 Notes on type synonyms
1079 ~~~~~~~~~~~~~~~~~~~~~~
1080 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
1081 to return type synonyms wherever possible. Thus
1082
1083 type Foo a = a -> a
1084
1085 we want
1086 splitFunTys (a -> Foo a) = ([a], Foo a)
1087 not ([a], a -> a)
1088
1089 The reason is that we then get better (shorter) type signatures in
1090 interfaces. Notably this plays a role in tcTySigs in TcBinds.hs.
1091
1092
1093 Representation types
1094 ~~~~~~~~~~~~~~~~~~~~
1095
1096 Note [Nullary unboxed tuple]
1097 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1098 We represent the nullary unboxed tuple as the unary (but void) type
1099 Void#. The reason for this is that the ReprArity is never
1100 less than the Arity (as it would otherwise be for a function type like
1101 (# #) -> Int).
1102
1103 As a result, ReprArity is always strictly positive if Arity is. This
1104 is important because it allows us to distinguish at runtime between a
1105 thunk and a function takes a nullary unboxed tuple as an argument!
1106 -}
1107
1108 type UnaryType = Type
1109
1110 data RepType = UbxTupleRep [UnaryType] -- INVARIANT: never an empty list (see Note [Nullary unboxed tuple])
1111 | UnaryRep UnaryType
1112
1113 instance Outputable RepType where
1114 ppr (UbxTupleRep tys) = text "UbxTupleRep" <+> ppr tys
1115 ppr (UnaryRep ty) = text "UnaryRep" <+> ppr ty
1116
1117 flattenRepType :: RepType -> [UnaryType]
1118 flattenRepType (UbxTupleRep tys) = tys
1119 flattenRepType (UnaryRep ty) = [ty]
1120
1121 -- | Looks through:
1122 --
1123 -- 1. For-alls
1124 -- 2. Synonyms
1125 -- 3. Predicates
1126 -- 4. All newtypes, including recursive ones, but not newtype families
1127 -- 5. Casts
1128 --
1129 -- It's useful in the back end of the compiler.
1130 repType :: Type -> RepType
1131 repType ty
1132 = go initRecTc ty
1133 where
1134 go :: RecTcChecker -> Type -> RepType
1135 go rec_nts ty -- Expand predicates and synonyms
1136 | Just ty' <- coreView ty
1137 = go rec_nts ty'
1138
1139 go rec_nts (ForAllTy (Named {}) ty2) -- Drop type foralls
1140 = go rec_nts ty2
1141
1142 go rec_nts (TyConApp tc tys) -- Expand newtypes
1143 | isNewTyCon tc
1144 , tys `lengthAtLeast` tyConArity tc
1145 , Just rec_nts' <- checkRecTc rec_nts tc -- See Note [Expanding newtypes] in TyCon
1146 = go rec_nts' (newTyConInstRhs tc tys)
1147
1148 | isUnboxedTupleTyCon tc
1149 = if null tys
1150 then UnaryRep voidPrimTy -- See Note [Nullary unboxed tuple]
1151 else UbxTupleRep (concatMap (flattenRepType . go rec_nts) non_levity_tys)
1152 where
1153 -- See Note [Unboxed tuple levity vars] in TyCon
1154 non_levity_tys = dropLevityArgs tys
1155
1156 go rec_nts (CastTy ty _)
1157 = go rec_nts ty
1158
1159 go _ ty@(CoercionTy _)
1160 = pprPanic "repType" (ppr ty)
1161
1162 go _ ty = UnaryRep ty
1163
1164 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
1165 -- of inspecting the type directly.
1166
1167 -- | Discovers the primitive representation of a more abstract 'UnaryType'
1168 typePrimRep :: UnaryType -> PrimRep
1169 typePrimRep ty
1170 = case repType ty of
1171 UbxTupleRep _ -> pprPanic "typePrimRep: UbxTupleRep" (ppr ty)
1172 UnaryRep rep -> go rep
1173 where go (TyConApp tc _) = tyConPrimRep tc
1174 go (ForAllTy _ _) = PtrRep
1175 go (AppTy _ _) = PtrRep -- See Note [AppTy rep]
1176 go (TyVarTy _) = PtrRep
1177 go (CastTy ty _) = go ty
1178 go _ = pprPanic "typePrimRep: UnaryRep" (ppr ty)
1179
1180 typeRepArity :: Arity -> Type -> RepArity
1181 typeRepArity 0 _ = 0
1182 typeRepArity n ty = case repType ty of
1183 UnaryRep (ForAllTy bndr ty) -> length (flattenRepType (repType (binderType bndr))) + typeRepArity (n - 1) ty
1184 _ -> pprPanic "typeRepArity: arity greater than type can handle" (ppr (n, ty, repType ty))
1185
1186 isVoidTy :: Type -> Bool
1187 -- True if the type has zero width
1188 isVoidTy ty = case repType ty of
1189 UnaryRep (TyConApp tc _) -> isVoidRep (tyConPrimRep tc)
1190 _ -> False
1191
1192 {-
1193 Note [AppTy rep]
1194 ~~~~~~~~~~~~~~~~
1195 Types of the form 'f a' must be of kind *, not #, so we are guaranteed
1196 that they are represented by pointers. The reason is that f must have
1197 kind (kk -> kk) and kk cannot be unlifted; see Note [The kind invariant]
1198 in TyCoRep.
1199
1200 ---------------------------------------------------------------------
1201 ForAllTy
1202 ~~~~~~~~
1203 -}
1204
1205 mkForAllTy :: TyBinder -> Type -> Type
1206 mkForAllTy = ForAllTy
1207
1208 -- | Make a dependent forall.
1209 mkNamedForAllTy :: TyVar -> VisibilityFlag -> Type -> Type
1210 mkNamedForAllTy tv vis = ASSERT( isTyVar tv )
1211 ForAllTy (Named tv vis)
1212
1213 -- | Wraps foralls over the type using the provided 'TyVar's from left to right
1214 mkForAllTys :: [TyBinder] -> Type -> Type
1215 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
1216
1217 -- | Like mkForAllTys, but assumes all variables are dependent and invisible,
1218 -- a common case
1219 mkInvForAllTys :: [TyVar] -> Type -> Type
1220 mkInvForAllTys tvs = ASSERT( all isTyVar tvs )
1221 mkForAllTys (map (flip Named Invisible) tvs)
1222
1223 -- | Like mkForAllTys, but assumes all variables are dependent and specified,
1224 -- a common case
1225 mkSpecForAllTys :: [TyVar] -> Type -> Type
1226 mkSpecForAllTys tvs = ASSERT( all isTyVar tvs )
1227 mkForAllTys (map (flip Named Specified) tvs)
1228
1229 -- | Like mkForAllTys, but assumes all variables are dependent and visible
1230 mkVisForAllTys :: [TyVar] -> Type -> Type
1231 mkVisForAllTys tvs = ASSERT( all isTyVar tvs )
1232 mkForAllTys (map (flip Named Visible) tvs)
1233
1234 mkPiType :: Var -> Type -> Type
1235 -- ^ Makes a @(->)@ type or an implicit forall type, depending
1236 -- on whether it is given a type variable or a term variable.
1237 -- This is used, for example, when producing the type of a lambda.
1238 -- Always uses Invisible binders.
1239 mkPiTypes :: [Var] -> Type -> Type
1240 -- ^ 'mkPiType' for multiple type or value arguments
1241
1242 mkPiType v ty
1243 | isTyVar v = mkForAllTy (Named v Invisible) ty
1244 | otherwise = mkForAllTy (Anon (varType v)) ty
1245
1246 mkPiTypes vs ty = foldr mkPiType ty vs
1247
1248 -- | Given a list of type-level vars, makes ForAllTys, preferring
1249 -- anonymous binders if the variable is, in fact, not dependent.
1250 -- All binders are /visible/.
1251 mkPiTypesPreferFunTy :: [TyVar] -> Type -> Type
1252 mkPiTypesPreferFunTy vars inner_ty = fst $ go vars inner_ty
1253 where
1254 go :: [TyVar] -> Type -> (Type, VarSet) -- also returns the free vars
1255 go [] ty = (ty, tyCoVarsOfType ty)
1256 go (v:vs) ty | v `elemVarSet` fvs
1257 = ( mkForAllTy (Named v Visible) qty
1258 , fvs `delVarSet` v `unionVarSet` kind_vars )
1259 | otherwise
1260 = ( mkForAllTy (Anon (tyVarKind v)) qty
1261 , fvs `unionVarSet` kind_vars )
1262 where
1263 (qty, fvs) = go vs ty
1264 kind_vars = tyCoVarsOfType $ tyVarKind v
1265
1266 -- | Take a ForAllTy apart, returning the list of tyvars and the result type.
1267 -- This always succeeds, even if it returns only an empty list. Note that the
1268 -- result type returned may have free variables that were bound by a forall.
1269 splitForAllTys :: Type -> ([TyVar], Type)
1270 splitForAllTys ty = split ty ty []
1271 where
1272 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
1273 split _ (ForAllTy (Named tv _) ty) tvs = split ty ty (tv:tvs)
1274 split orig_ty _ tvs = (reverse tvs, orig_ty)
1275
1276 -- | Split off all TyBinders to a type, splitting both proper foralls
1277 -- and functions
1278 splitPiTys :: Type -> ([TyBinder], Type)
1279 splitPiTys ty = split ty ty []
1280 where
1281 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1282 split _ (ForAllTy b res) bs = split res res (b:bs)
1283 split orig_ty _ bs = (reverse bs, orig_ty)
1284
1285 -- | Like 'splitPiTys' but split off only /named/ binders.
1286 splitNamedPiTys :: Type -> ([TyBinder], Type)
1287 splitNamedPiTys ty = split ty ty []
1288 where
1289 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1290 split _ (ForAllTy b@(Named {}) res) bs = split res res (b:bs)
1291 split orig_ty _ bs = (reverse bs, orig_ty)
1292
1293 -- | Checks whether this is a proper forall (with a named binder)
1294 isForAllTy :: Type -> Bool
1295 isForAllTy (ForAllTy (Named {}) _) = True
1296 isForAllTy _ = False
1297
1298 -- | Is this a function or forall?
1299 isPiTy :: Type -> Bool
1300 isPiTy (ForAllTy {}) = True
1301 isPiTy _ = False
1302
1303 -- | Take a forall type apart, or panics if that is not possible.
1304 splitForAllTy :: Type -> (TyVar, Type)
1305 splitForAllTy ty
1306 | Just answer <- splitForAllTy_maybe ty = answer
1307 | otherwise = pprPanic "splitForAllTy" (ppr ty)
1308
1309 -- | Attempts to take a forall type apart, but only if it's a proper forall,
1310 -- with a named binder
1311 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
1312 splitForAllTy_maybe ty = splitFAT_m ty
1313 where
1314 splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
1315 splitFAT_m (ForAllTy (Named tv _) ty) = Just (tv, ty)
1316 splitFAT_m _ = Nothing
1317
1318 -- | Attempts to take a forall type apart; works with proper foralls and
1319 -- functions
1320 splitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
1321 splitPiTy_maybe ty = go ty
1322 where
1323 go ty | Just ty' <- coreView ty = go ty'
1324 go (ForAllTy bndr ty) = Just (bndr, ty)
1325 go _ = Nothing
1326
1327 -- | Takes a forall type apart, or panics
1328 splitPiTy :: Type -> (TyBinder, Type)
1329 splitPiTy ty
1330 | Just answer <- splitPiTy_maybe ty = answer
1331 | otherwise = pprPanic "splitPiTy" (ppr ty)
1332
1333 -- | Drops all non-anonymous ForAllTys
1334 dropForAlls :: Type -> Type
1335 dropForAlls ty | Just ty' <- coreView ty = dropForAlls ty'
1336 | otherwise = go ty
1337 where
1338 go (ForAllTy (Named {}) res) = go res
1339 go res = res
1340
1341 -- | Given a tycon and its arguments, filters out any invisible arguments
1342 filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
1343 filterOutInvisibleTypes tc tys = snd $ partitionInvisibles tc id tys
1344
1345 -- | Like 'filterOutInvisibles', but works on 'TyVar's
1346 filterOutInvisibleTyVars :: TyCon -> [TyVar] -> [TyVar]
1347 filterOutInvisibleTyVars tc tvs = snd $ partitionInvisibles tc mkTyVarTy tvs
1348
1349 -- | Given a tycon and a list of things (which correspond to arguments),
1350 -- partitions the things into the invisible ones and the visible ones.
1351 -- The callback function is necessary for this scenario:
1352 --
1353 -- > T :: forall k. k -> k
1354 -- > partitionInvisibles T [forall m. m -> m -> m, S, R, Q]
1355 --
1356 -- After substituting, we get
1357 --
1358 -- > T (forall m. m -> m -> m) :: (forall m. m -> m -> m) -> forall n. n -> n -> n
1359 --
1360 -- Thus, the first argument is invisible, @S@ is visible, @R@ is invisible again,
1361 -- and @Q@ is visible.
1362 --
1363 -- If you're absolutely sure that your tycon's kind doesn't end in a variable,
1364 -- it's OK if the callback function panics, as that's the only time it's
1365 -- consulted.
1366 partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
1367 partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
1368 where
1369 go _ _ [] = ([], [])
1370 go subst (ForAllTy bndr res_ki) (x:xs)
1371 | isVisibleBinder bndr = second (x :) (go subst' res_ki xs)
1372 | otherwise = first (x :) (go subst' res_ki xs)
1373 where
1374 subst' = extendTvSubstBinder subst bndr (get_ty x)
1375 go subst (TyVarTy tv) xs
1376 | Just ki <- lookupTyVar subst tv = go subst ki xs
1377 go _ _ xs = ([], xs) -- something is ill-kinded. But this can happen
1378 -- when printing errors. Assume everything is visible.
1379
1380 -- like splitPiTys, but returns only *invisible* binders, including constraints
1381 splitPiTysInvisible :: Type -> ([TyBinder], Type)
1382 splitPiTysInvisible ty = split ty ty []
1383 where
1384 split orig_ty ty bndrs
1385 | Just ty' <- coreView ty = split orig_ty ty' bndrs
1386 split _ (ForAllTy bndr ty) bndrs
1387 | isInvisibleBinder bndr
1388 = split ty ty (bndr:bndrs)
1389
1390 split orig_ty _ bndrs
1391 = (reverse bndrs, orig_ty)
1392
1393 tyConBinders :: TyCon -> [TyBinder]
1394 tyConBinders = fst . splitPiTys . tyConKind
1395
1396 {-
1397 applyTys
1398 ~~~~~~~~~~~~~~~~~
1399 -}
1400
1401 applyTys :: Type -> [KindOrType] -> Type
1402 -- ^ This function is interesting because:
1403 --
1404 -- 1. The function may have more for-alls than there are args
1405 --
1406 -- 2. Less obviously, it may have fewer for-alls
1407 --
1408 -- For case 2. think of:
1409 --
1410 -- > applyTys (forall a.a) [forall b.b, Int]
1411 --
1412 -- This really can happen, but only (I think) in situations involving
1413 -- undefined. For example:
1414 -- undefined :: forall a. a
1415 -- Term: undefined @(forall b. b->b) @Int
1416 -- This term should have type (Int -> Int), but notice that
1417 -- there are more type args than foralls in 'undefined's type.
1418
1419 -- If you edit this function, you may need to update the GHC formalism
1420 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
1421 applyTys ty args = applyTysD empty ty args
1422
1423 applyTysD :: SDoc -> Type -> [Type] -> Type -- Debug version
1424 applyTysD doc orig_fun_ty arg_tys
1425 | null arg_tys
1426 = orig_fun_ty
1427
1428 | n_bndrs == n_args -- The vastly common case
1429 = substTyWithBindersUnchecked bndrs arg_tys rho_ty
1430
1431 | n_bndrs > n_args -- Too many for-alls
1432 = substTyWithBindersUnchecked (take n_args bndrs) arg_tys
1433 (mkForAllTys (drop n_args bndrs) rho_ty)
1434
1435 | otherwise -- Too many type args
1436 = ASSERT2( n_bndrs > 0, doc $$ ppr orig_fun_ty $$ ppr arg_tys ) -- Zero case gives infinite loop!
1437 applyTysD doc (substTyWithBinders bndrs (take n_bndrs arg_tys) rho_ty)
1438 (drop n_bndrs arg_tys)
1439 where
1440 (bndrs, rho_ty) = splitPiTys orig_fun_ty
1441 n_bndrs = length bndrs
1442 n_args = length arg_tys
1443
1444 applyTysX :: [TyVar] -> Type -> [Type] -> Type
1445 -- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
1446 applyTysX tvs body_ty arg_tys
1447 = ASSERT2( length arg_tys >= n_tvs, ppr tvs $$ ppr body_ty $$ ppr arg_tys )
1448 mkAppTys (substTyWithUnchecked tvs (take n_tvs arg_tys) body_ty)
1449 (drop n_tvs arg_tys)
1450 where
1451 n_tvs = length tvs
1452
1453 {-
1454 %************************************************************************
1455 %* *
1456 TyBinders
1457 %* *
1458 %************************************************************************
1459 -}
1460
1461 -- | Make a named binder
1462 mkNamedBinder :: VisibilityFlag -> Var -> TyBinder
1463 mkNamedBinder vis var = Named var vis
1464
1465 -- | Make an anonymous binder
1466 mkAnonBinder :: Type -> TyBinder
1467 mkAnonBinder = Anon
1468
1469 -- | Does this binder bind a variable that is /not/ erased? Returns
1470 -- 'True' for anonymous binders.
1471 isIdLikeBinder :: TyBinder -> Bool
1472 isIdLikeBinder (Named {}) = False
1473 isIdLikeBinder (Anon {}) = True
1474
1475 -- | Does this type, when used to the left of an arrow, require
1476 -- a visible argument? This checks to see if the kind of the type
1477 -- is constraint.
1478 isVisibleType :: Type -> Bool
1479 isVisibleType = not . isPredTy
1480
1481 binderVisibility :: TyBinder -> VisibilityFlag
1482 binderVisibility (Named _ vis) = vis
1483 binderVisibility (Anon ty)
1484 | isVisibleType ty = Visible
1485 | otherwise = Invisible
1486
1487 -- | Extract a bound variable in a binder, if any
1488 binderVar_maybe :: TyBinder -> Maybe Var
1489 binderVar_maybe (Named v _) = Just v
1490 binderVar_maybe (Anon {}) = Nothing
1491
1492 -- | Extract a bound variable in a binder, or panics
1493 binderVar :: String -- ^ printed if there is a panic
1494 -> TyBinder -> Var
1495 binderVar _ (Named v _) = v
1496 binderVar e (Anon t) = pprPanic ("binderVar (" ++ e ++ ")") (ppr t)
1497
1498 -- | Extract a relevant type, if there is one.
1499 binderRelevantType_maybe :: TyBinder -> Maybe Type
1500 binderRelevantType_maybe (Named {}) = Nothing
1501 binderRelevantType_maybe (Anon ty) = Just ty
1502
1503 -- | Like 'maybe', but for binders.
1504 caseBinder :: TyBinder -- ^ binder to scrutinize
1505 -> (TyVar -> a) -- ^ named case
1506 -> (Type -> a) -- ^ anonymous case
1507 -> a
1508 caseBinder (Named v _) f _ = f v
1509 caseBinder (Anon t) _ d = d t
1510
1511 -- | Break apart a list of binders into tyvars and anonymous types.
1512 partitionBinders :: [TyBinder] -> ([TyVar], [Type])
1513 partitionBinders = partitionWith named_or_anon
1514 where
1515 named_or_anon bndr = caseBinder bndr Left Right
1516
1517 -- | Break apart a list of binders into a list of named binders and
1518 -- a list of anonymous types.
1519 partitionBindersIntoBinders :: [TyBinder] -> ([TyBinder], [Type])
1520 partitionBindersIntoBinders = partitionWith named_or_anon
1521 where
1522 named_or_anon bndr = caseBinder bndr (\_ -> Left bndr) Right
1523
1524 {-
1525 %************************************************************************
1526 %* *
1527 Pred
1528 * *
1529 ************************************************************************
1530
1531 Predicates on PredType
1532
1533 Note [isPredTy complications]
1534 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1535 You would think that we could define
1536 isPredTy ty = isConstraintKind (typeKind ty)
1537 But there are a number of complications:
1538
1539 * isPredTy is used when printing types, which can happen in debug
1540 printing during type checking of not-fully-zonked types. So it's
1541 not cool to say isConstraintKind (typeKind ty) because, absent
1542 zonking, the type might be ill-kinded, and typeKind crashes. Hence the
1543 rather tiresome story here
1544
1545 * isPredTy must return "True" to *unlifted* coercions, such as (t1 ~# t2)
1546 and (t1 ~R# t2), which are not of kind Constraint! Currently they are
1547 of kind #.
1548
1549 * If we do form the type '(C a => C [a]) => blah', then we'd like to
1550 print it as such. But that means that isPredTy must return True for
1551 (C a => C [a]). Admittedly that type is illegal in Haskell, but we
1552 want to print it nicely in error messages.
1553 -}
1554
1555 -- | Is the type suitable to classify a given/wanted in the typechecker?
1556 isPredTy :: Type -> Bool
1557 -- See Note [isPredTy complications]
1558 isPredTy ty = go ty []
1559 where
1560 go :: Type -> [KindOrType] -> Bool
1561 go (AppTy ty1 ty2) args = go ty1 (ty2 : args)
1562 go (TyVarTy tv) args = go_k (tyVarKind tv) args
1563 go (TyConApp tc tys) args = ASSERT( null args ) -- TyConApp invariant
1564 go_tc tc tys
1565 go (ForAllTy (Anon arg) res) []
1566 | isPredTy arg = isPredTy res -- (Eq a => C a)
1567 | otherwise = False -- (Int -> Bool)
1568 go (ForAllTy (Named {}) ty) [] = go ty []
1569 go _ _ = False
1570
1571 go_tc :: TyCon -> [KindOrType] -> Bool
1572 go_tc tc args
1573 | tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1574 = length args == 4 -- ~# and ~R# sadly have result kind #
1575 -- not Contraint; but we still want
1576 -- isPredTy to reply True.
1577 | otherwise = go_k (tyConKind tc) args
1578
1579 go_k :: Kind -> [KindOrType] -> Bool
1580 -- True <=> ('k' applied to 'kts') = Constraint
1581 go_k k args = isConstraintKind (applyTys k args)
1582
1583 isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool
1584 isClassPred ty = case tyConAppTyCon_maybe ty of
1585 Just tyCon | isClassTyCon tyCon -> True
1586 _ -> False
1587 isEqPred ty = case tyConAppTyCon_maybe ty of
1588 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1589 || tyCon `hasKey` eqReprPrimTyConKey
1590 _ -> False
1591
1592 isNomEqPred ty = case tyConAppTyCon_maybe ty of
1593 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1594 _ -> False
1595
1596 isIPPred ty = case tyConAppTyCon_maybe ty of
1597 Just tc -> isIPTyCon tc
1598 _ -> False
1599
1600 isIPTyCon :: TyCon -> Bool
1601 isIPTyCon tc = tc `hasKey` ipClassKey
1602 -- Class and its corresponding TyCon have the same Unique
1603
1604 isIPClass :: Class -> Bool
1605 isIPClass cls = cls `hasKey` ipClassKey
1606
1607 isCTupleClass :: Class -> Bool
1608 isCTupleClass cls = isTupleTyCon (classTyCon cls)
1609
1610 isIPPred_maybe :: Type -> Maybe (FastString, Type)
1611 isIPPred_maybe ty =
1612 do (tc,[t1,t2]) <- splitTyConApp_maybe ty
1613 guard (isIPTyCon tc)
1614 x <- isStrLitTy t1
1615 return (x,t2)
1616
1617 {-
1618 Make PredTypes
1619
1620 --------------------- Equality types ---------------------------------
1621 -}
1622
1623 -- | Makes a lifted equality predicate at the given role
1624 mkPrimEqPredRole :: Role -> Type -> Type -> PredType
1625 mkPrimEqPredRole Nominal = mkPrimEqPred
1626 mkPrimEqPredRole Representational = mkReprPrimEqPred
1627 mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
1628
1629 -- | Creates a primitive type equality predicate.
1630 -- Invariant: the types are not Coercions
1631 mkPrimEqPred :: Type -> Type -> Type
1632 mkPrimEqPred ty1 ty2
1633 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1634 where
1635 k1 = typeKind ty1
1636 k2 = typeKind ty2
1637
1638 -- | Creates a primite type equality predicate with explicit kinds
1639 mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1640 mkHeteroPrimEqPred k1 k2 ty1 ty2 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1641
1642 -- | Creates a primitive representational type equality predicate
1643 -- with explicit kinds
1644 mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1645 mkHeteroReprPrimEqPred k1 k2 ty1 ty2
1646 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1647
1648 -- | Try to split up a coercion type into the types that it coerces
1649 splitCoercionType_maybe :: Type -> Maybe (Type, Type)
1650 splitCoercionType_maybe ty
1651 = do { (tc, [_, _, ty1, ty2]) <- splitTyConApp_maybe ty
1652 ; guard $ tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1653 ; return (ty1, ty2) }
1654
1655 mkReprPrimEqPred :: Type -> Type -> Type
1656 mkReprPrimEqPred ty1 ty2
1657 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1658 where
1659 k1 = typeKind ty1
1660 k2 = typeKind ty2
1661
1662 equalityTyCon :: Role -> TyCon
1663 equalityTyCon Nominal = eqPrimTyCon
1664 equalityTyCon Representational = eqReprPrimTyCon
1665 equalityTyCon Phantom = eqPhantPrimTyCon
1666
1667 -- --------------------- Dictionary types ---------------------------------
1668
1669 mkClassPred :: Class -> [Type] -> PredType
1670 mkClassPred clas tys = TyConApp (classTyCon clas) tys
1671
1672 isDictTy :: Type -> Bool
1673 isDictTy = isClassPred
1674
1675 isDictLikeTy :: Type -> Bool
1676 -- Note [Dictionary-like types]
1677 isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
1678 isDictLikeTy ty = case splitTyConApp_maybe ty of
1679 Just (tc, tys) | isClassTyCon tc -> True
1680 | isTupleTyCon tc -> all isDictLikeTy tys
1681 _other -> False
1682
1683 {-
1684 Note [Dictionary-like types]
1685 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1686 Being "dictionary-like" means either a dictionary type or a tuple thereof.
1687 In GHC 6.10 we build implication constraints which construct such tuples,
1688 and if we land up with a binding
1689 t :: (C [a], Eq [a])
1690 t = blah
1691 then we want to treat t as cheap under "-fdicts-cheap" for example.
1692 (Implication constraints are normally inlined, but sadly not if the
1693 occurrence is itself inside an INLINE function! Until we revise the
1694 handling of implication constraints, that is.) This turned out to
1695 be important in getting good arities in DPH code. Example:
1696
1697 class C a
1698 class D a where { foo :: a -> a }
1699 instance C a => D (Maybe a) where { foo x = x }
1700
1701 bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
1702 {-# INLINE bar #-}
1703 bar x y = (foo (Just x), foo (Just y))
1704
1705 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
1706 we ended up with something like
1707 bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
1708 in \x,y. <blah>)
1709
1710 This is all a bit ad-hoc; eg it relies on knowing that implication
1711 constraints build tuples.
1712
1713
1714 Decomposing PredType
1715 -}
1716
1717 -- | A choice of equality relation. This is separate from the type 'Role'
1718 -- because 'Phantom' does not define a (non-trivial) equality relation.
1719 data EqRel = NomEq | ReprEq
1720 deriving (Eq, Ord)
1721
1722 instance Outputable EqRel where
1723 ppr NomEq = text "nominal equality"
1724 ppr ReprEq = text "representational equality"
1725
1726 eqRelRole :: EqRel -> Role
1727 eqRelRole NomEq = Nominal
1728 eqRelRole ReprEq = Representational
1729
1730 data PredTree = ClassPred Class [Type]
1731 | EqPred EqRel Type Type
1732 | IrredPred PredType
1733
1734 classifyPredType :: PredType -> PredTree
1735 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
1736 Just (tc, [_, _, ty1, ty2])
1737 | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
1738 | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
1739 Just (tc, tys)
1740 | Just clas <- tyConClass_maybe tc -> ClassPred clas tys
1741 _ -> IrredPred ev_ty
1742
1743 getClassPredTys :: PredType -> (Class, [Type])
1744 getClassPredTys ty = case getClassPredTys_maybe ty of
1745 Just (clas, tys) -> (clas, tys)
1746 Nothing -> pprPanic "getClassPredTys" (ppr ty)
1747
1748 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
1749 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
1750 Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
1751 _ -> Nothing
1752
1753 getEqPredTys :: PredType -> (Type, Type)
1754 getEqPredTys ty
1755 = case splitTyConApp_maybe ty of
1756 Just (tc, [_, _, ty1, ty2])
1757 | tc `hasKey` eqPrimTyConKey
1758 || tc `hasKey` eqReprPrimTyConKey
1759 -> (ty1, ty2)
1760 _ -> pprPanic "getEqPredTys" (ppr ty)
1761
1762 getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
1763 getEqPredTys_maybe ty
1764 = case splitTyConApp_maybe ty of
1765 Just (tc, [_, _, ty1, ty2])
1766 | tc `hasKey` eqPrimTyConKey -> Just (Nominal, ty1, ty2)
1767 | tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2)
1768 _ -> Nothing
1769
1770 getEqPredRole :: PredType -> Role
1771 getEqPredRole ty = eqRelRole (predTypeEqRel ty)
1772
1773 -- | Get the equality relation relevant for a pred type.
1774 predTypeEqRel :: PredType -> EqRel
1775 predTypeEqRel ty
1776 | Just (tc, _) <- splitTyConApp_maybe ty
1777 , tc `hasKey` eqReprPrimTyConKey
1778 = ReprEq
1779 | otherwise
1780 = NomEq
1781
1782 {-
1783 %************************************************************************
1784 %* *
1785 Size
1786 * *
1787 ************************************************************************
1788 -}
1789
1790 -- NB: This function does not respect `eqType`, in that two types that
1791 -- are `eqType` may return different sizes. This is OK, because this
1792 -- function is used only in reporting, not decision-making.
1793 typeSize :: Type -> Int
1794 typeSize (LitTy {}) = 1
1795 typeSize (TyVarTy {}) = 1
1796 typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2
1797 typeSize (ForAllTy b t) = typeSize (binderType b) + typeSize t
1798 typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
1799 typeSize (CastTy ty co) = typeSize ty + coercionSize co
1800 typeSize (CoercionTy co) = coercionSize co
1801
1802 {-
1803 %************************************************************************
1804 %* *
1805 Well-scoped tyvars
1806 * *
1807 ************************************************************************
1808 -}
1809
1810 -- | Do a topological sort on a list of tyvars. This is a deterministic
1811 -- sorting operation (that is, doesn't depend on Uniques).
1812 toposortTyVars :: [TyVar] -> [TyVar]
1813 toposortTyVars tvs = reverse $
1814 [ tv | (tv, _, _) <- topologicalSortG $
1815 graphFromEdgedVertices nodes ]
1816 where
1817 var_ids :: VarEnv Int
1818 var_ids = mkVarEnv (zip tvs [1..])
1819
1820 nodes = [ ( tv
1821 , lookupVarEnv_NF var_ids tv
1822 , mapMaybe (lookupVarEnv var_ids)
1823 (tyCoVarsOfTypeList (tyVarKind tv)) )
1824 | tv <- tvs ]
1825
1826 -- | Extract a well-scoped list of variables from a set of variables.
1827 varSetElemsWellScoped :: VarSet -> [Var]
1828 varSetElemsWellScoped = toposortTyVars . varSetElems
1829
1830 -- | Get the free vars of a type in scoped order
1831 tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
1832 tyCoVarsOfTypeWellScoped = toposortTyVars . tyCoVarsOfTypeList
1833
1834 {-
1835 ************************************************************************
1836 * *
1837 \subsection{Type families}
1838 * *
1839 ************************************************************************
1840 -}
1841
1842 mkFamilyTyConApp :: TyCon -> [Type] -> Type
1843 -- ^ Given a family instance TyCon and its arg types, return the
1844 -- corresponding family type. E.g:
1845 --
1846 -- > data family T a
1847 -- > data instance T (Maybe b) = MkT b
1848 --
1849 -- Where the instance tycon is :RTL, so:
1850 --
1851 -- > mkFamilyTyConApp :RTL Int = T (Maybe Int)
1852 mkFamilyTyConApp tc tys
1853 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
1854 , let tvs = tyConTyVars tc
1855 fam_subst = ASSERT2( length tvs == length tys, ppr tc <+> ppr tys )
1856 zipTvSubst tvs tys
1857 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
1858 | otherwise
1859 = mkTyConApp tc tys
1860
1861 -- | Get the type on the LHS of a coercion induced by a type/data
1862 -- family instance.
1863 coAxNthLHS :: CoAxiom br -> Int -> Type
1864 coAxNthLHS ax ind =
1865 mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind))
1866
1867 -- | Pretty prints a 'TyCon', using the family instance in case of a
1868 -- representation tycon. For example:
1869 --
1870 -- > data T [a] = ...
1871 --
1872 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
1873 pprSourceTyCon :: TyCon -> SDoc
1874 pprSourceTyCon tycon
1875 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
1876 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
1877 | otherwise
1878 = ppr tycon
1879
1880 {-
1881 ************************************************************************
1882 * *
1883 \subsection{Liftedness}
1884 * *
1885 ************************************************************************
1886 -}
1887
1888 -- | See "Type#type_classification" for what an unlifted type is
1889 isUnliftedType :: Type -> Bool
1890 -- isUnliftedType returns True for forall'd unlifted types:
1891 -- x :: forall a. Int#
1892 -- I found bindings like these were getting floated to the top level.
1893 -- They are pretty bogus types, mind you. It would be better never to
1894 -- construct them
1895
1896 isUnliftedType ty | Just ty' <- coreView ty = isUnliftedType ty'
1897 isUnliftedType (ForAllTy (Named {}) ty) = isUnliftedType ty
1898 isUnliftedType (TyConApp tc _) = isUnliftedTyCon tc
1899 isUnliftedType _ = False
1900
1901 -- | Extract the levity classifier of a type. Panics if this is not possible.
1902 getLevity :: String -- ^ Printed in case of an error
1903 -> Type -> Type
1904 getLevity err ty = getLevityFromKind err (typeKind ty)
1905
1906 -- | Extract the levity classifier of a type from its kind.
1907 -- For example, getLevityFromKind * = Lifted; getLevityFromKind # = Unlifted.
1908 -- Panics if this is not possible.
1909 getLevityFromKind :: String -- ^ Printed in case of an error
1910 -> Type -> Type
1911 getLevityFromKind err = go
1912 where
1913 go k | Just k' <- coreViewOneStarKind k = go k'
1914 go k
1915 | Just (tc, [arg]) <- splitTyConApp_maybe k
1916 , tc `hasKey` tYPETyConKey
1917 = arg
1918 go k = pprPanic "getLevity" (text err $$
1919 ppr k <+> dcolon <+> ppr (typeKind k))
1920
1921 isUnboxedTupleType :: Type -> Bool
1922 isUnboxedTupleType ty = case tyConAppTyCon_maybe ty of
1923 Just tc -> isUnboxedTupleTyCon tc
1924 _ -> False
1925
1926 -- | See "Type#type_classification" for what an algebraic type is.
1927 -- Should only be applied to /types/, as opposed to e.g. partially
1928 -- saturated type constructors
1929 isAlgType :: Type -> Bool
1930 isAlgType ty
1931 = case splitTyConApp_maybe ty of
1932 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1933 isAlgTyCon tc
1934 _other -> False
1935
1936 -- | See "Type#type_classification" for what an algebraic type is.
1937 -- Should only be applied to /types/, as opposed to e.g. partially
1938 -- saturated type constructors. Closed type constructors are those
1939 -- with a fixed right hand side, as opposed to e.g. associated types
1940 isClosedAlgType :: Type -> Bool
1941 isClosedAlgType ty
1942 = case splitTyConApp_maybe ty of
1943 Just (tc, ty_args) | isAlgTyCon tc && not (isFamilyTyCon tc)
1944 -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
1945 _other -> False
1946
1947 -- | Computes whether an argument (or let right hand side) should
1948 -- be computed strictly or lazily, based only on its type.
1949 -- Currently, it's just 'isUnliftedType'.
1950
1951 isStrictType :: Type -> Bool
1952 isStrictType = isUnliftedType
1953
1954 isPrimitiveType :: Type -> Bool
1955 -- ^ Returns true of types that are opaque to Haskell.
1956 isPrimitiveType ty = case splitTyConApp_maybe ty of
1957 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1958 isPrimTyCon tc
1959 _ -> False
1960
1961 {-
1962 ************************************************************************
1963 * *
1964 \subsection{Sequencing on types}
1965 * *
1966 ************************************************************************
1967 -}
1968
1969 seqType :: Type -> ()
1970 seqType (LitTy n) = n `seq` ()
1971 seqType (TyVarTy tv) = tv `seq` ()
1972 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
1973 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
1974 seqType (ForAllTy bndr ty) = seqType (binderType bndr) `seq` seqType ty
1975 seqType (CastTy ty co) = seqType ty `seq` seqCo co
1976 seqType (CoercionTy co) = seqCo co
1977
1978 seqTypes :: [Type] -> ()
1979 seqTypes [] = ()
1980 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
1981
1982 {-
1983 ************************************************************************
1984 * *
1985 Comparison for types
1986 (We don't use instances so that we know where it happens)
1987 * *
1988 ************************************************************************
1989
1990 Note [Equality on AppTys]
1991 ~~~~~~~~~~~~~~~~~~~~~~~~~
1992 In our cast-ignoring equality, we want to say that the following two
1993 are equal:
1994
1995 (Maybe |> co) (Int |> co') ~? Maybe Int
1996
1997 But the left is an AppTy while the right is a TyConApp. The solution is
1998 to use repSplitAppTy_maybe to break up the TyConApp into its pieces and
1999 then continue. Easy to do, but also easy to forget to do.
2000
2001 -}
2002
2003 eqType :: Type -> Type -> Bool
2004 -- ^ Type equality on source types. Does not look through @newtypes@ or
2005 -- 'PredType's, but it does look through type synonyms.
2006 -- This first checks that the kinds of the types are equal and then
2007 -- checks whether the types are equal, ignoring casts and coercions.
2008 -- (The kind check is a recursive call, but since all kinds have type
2009 -- @Type@, there is no need to check the types of kinds.)
2010 -- See also Note [Non-trivial definitional equality] in TyCoRep.
2011 eqType t1 t2 = isEqual $ cmpType t1 t2
2012
2013 -- | Compare types with respect to a (presumably) non-empty 'RnEnv2'.
2014 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
2015 eqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
2016
2017 -- | Type equality on lists of types, looking through type synonyms
2018 -- but not newtypes.
2019 eqTypes :: [Type] -> [Type] -> Bool
2020 eqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
2021
2022 eqVarBndrs :: RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
2023 -- Check that the var lists are the same length
2024 -- and have matching kinds; if so, extend the RnEnv2
2025 -- Returns Nothing if they don't match
2026 eqVarBndrs env [] []
2027 = Just env
2028 eqVarBndrs env (tv1:tvs1) (tv2:tvs2)
2029 | eqTypeX env (tyVarKind tv1) (tyVarKind tv2)
2030 = eqVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
2031 eqVarBndrs _ _ _= Nothing
2032
2033 -- Now here comes the real worker
2034
2035 cmpType :: Type -> Type -> Ordering
2036 cmpType t1 t2
2037 -- we know k1 and k2 have the same kind, because they both have kind *.
2038 = cmpTypeX rn_env t1 t2
2039 where
2040 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes [t1, t2]))
2041
2042 cmpTypes :: [Type] -> [Type] -> Ordering
2043 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
2044 where
2045 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes (ts1 ++ ts2)))
2046
2047 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
2048 -- See Note [Non-trivial definitional equality] in TyCoRep
2049 cmpTypeX env orig_t1 orig_t2 = go env k1 k2 `thenCmp` go env orig_t1 orig_t2
2050 where
2051 k1 = typeKind orig_t1
2052 k2 = typeKind orig_t2
2053
2054 go env t1 t2 | Just t1' <- coreViewOneStarKind t1 = go env t1' t2
2055 go env t1 t2 | Just t2' <- coreViewOneStarKind t2 = go env t1 t2'
2056
2057 go env (TyVarTy tv1) (TyVarTy tv2)
2058 = rnOccL env tv1 `compare` rnOccR env tv2
2059 go env (ForAllTy (Named tv1 _) t1) (ForAllTy (Named tv2 _) t2)
2060 = go env (tyVarKind tv1) (tyVarKind tv2)
2061 `thenCmp` go (rnBndr2 env tv1 tv2) t1 t2
2062 -- See Note [Equality on AppTys]
2063 go env (AppTy s1 t1) ty2
2064 | Just (s2, t2) <- repSplitAppTy_maybe ty2
2065 = go env s1 s2 `thenCmp` go env t1 t2
2066 go env ty1 (AppTy s2 t2)
2067 | Just (s1, t1) <- repSplitAppTy_maybe ty1
2068 = go env s1 s2 `thenCmp` go env t1 t2
2069 go env (ForAllTy (Anon s1) t1) (ForAllTy (Anon s2) t2)
2070 = go env s1 s2 `thenCmp` go env t1 t2
2071 go env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2072 = (tc1 `cmpTc` tc2) `thenCmp` gos env tys1 tys2
2073 go _ (LitTy l1) (LitTy l2) = compare l1 l2
2074 go env (CastTy t1 _) t2 = go env t1 t2
2075 go env t1 (CastTy t2 _) = go env t1 t2
2076 go _ (CoercionTy {}) (CoercionTy {}) = EQ
2077
2078 -- Deal with the rest: TyVarTy < CoercionTy < AppTy < LitTy < TyConApp < ForAllTy
2079 go _ ty1 ty2
2080 = (get_rank ty1) `compare` (get_rank ty2)
2081 where get_rank :: Type -> Int
2082 get_rank (CastTy {})
2083 = pprPanic "cmpTypeX.get_rank" (ppr [ty1,ty2])
2084 get_rank (TyVarTy {}) = 0
2085 get_rank (CoercionTy {}) = 1
2086 get_rank (AppTy {}) = 3
2087 get_rank (LitTy {}) = 4
2088 get_rank (TyConApp {}) = 5
2089 get_rank (ForAllTy (Anon {}) _) = 6
2090 get_rank (ForAllTy (Named {}) _) = 7
2091
2092 gos _ [] [] = EQ
2093 gos _ [] _ = LT
2094 gos _ _ [] = GT
2095 gos env (ty1:tys1) (ty2:tys2) = go env ty1 ty2 `thenCmp` gos env tys1 tys2
2096
2097 -------------
2098 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
2099 cmpTypesX _ [] [] = EQ
2100 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
2101 cmpTypesX _ [] _ = LT
2102 cmpTypesX _ _ [] = GT
2103
2104 -------------
2105 -- | Compare two 'TyCon's. NB: This should /never/ see the "star synonyms",
2106 -- as recognized by Kind.isStarKindSynonymTyCon. See Note
2107 -- [Kind Constraint and kind *] in Kind.
2108 cmpTc :: TyCon -> TyCon -> Ordering
2109 cmpTc tc1 tc2
2110 = ASSERT( not (isStarKindSynonymTyCon tc1) && not (isStarKindSynonymTyCon tc2) )
2111 u1 `compare` u2
2112 where
2113 u1 = tyConUnique tc1
2114 u2 = tyConUnique tc2
2115
2116 {-
2117 ************************************************************************
2118 * *
2119 The kind of a type
2120 * *
2121 ************************************************************************
2122 -}
2123
2124 typeKind :: Type -> Kind
2125 typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
2126 typeKind (AppTy fun arg) = piResultTy (typeKind fun) arg
2127 typeKind (LitTy l) = typeLiteralKind l
2128 typeKind (ForAllTy (Anon _) _) = liftedTypeKind
2129 typeKind (ForAllTy _ ty) = typeKind ty
2130 typeKind (TyVarTy tyvar) = tyVarKind tyvar
2131 typeKind (CastTy _ty co) = pSnd $ coercionKind co
2132 typeKind (CoercionTy co) = coercionType co
2133
2134 typeLiteralKind :: TyLit -> Kind
2135 typeLiteralKind l =
2136 case l of
2137 NumTyLit _ -> typeNatKind
2138 StrTyLit _ -> typeSymbolKind
2139
2140 -- | Print a tyvar with its kind
2141 pprTyVar :: TyVar -> SDoc
2142 pprTyVar tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
2143
2144 {-
2145 %************************************************************************
2146 %* *
2147 Miscellaneous functions
2148 %* *
2149 %************************************************************************
2150
2151 -}
2152 -- | All type constructors occurring in the type; looking through type
2153 -- synonyms, but not newtypes.
2154 -- When it finds a Class, it returns the class TyCon.
2155 tyConsOfType :: Type -> NameEnv TyCon
2156 tyConsOfType ty
2157 = go ty
2158 where
2159 go :: Type -> NameEnv TyCon -- The NameEnv does duplicate elim
2160 go ty | Just ty' <- coreView ty = go ty'
2161 go (TyVarTy {}) = emptyNameEnv
2162 go (LitTy {}) = emptyNameEnv
2163 go (TyConApp tc tys) = go_tc tc `plusNameEnv` go_s tys
2164 go (AppTy a b) = go a `plusNameEnv` go b
2165 go (ForAllTy (Anon a) b) = go a `plusNameEnv` go b `plusNameEnv` go_tc funTyCon
2166 go (ForAllTy (Named tv _) ty) = go ty `plusNameEnv` go (tyVarKind tv)
2167 go (CastTy ty co) = go ty `plusNameEnv` go_co co
2168 go (CoercionTy co) = go_co co
2169
2170 go_co (Refl _ ty) = go ty
2171 go_co (TyConAppCo _ tc args) = go_tc tc `plusNameEnv` go_cos args
2172 go_co (AppCo co arg) = go_co co `plusNameEnv` go_co arg
2173 go_co (ForAllCo _ kind_co co) = go_co kind_co `plusNameEnv` go_co co
2174 go_co (CoVarCo {}) = emptyNameEnv
2175 go_co (AxiomInstCo ax _ args) = go_ax ax `plusNameEnv` go_cos args
2176 go_co (UnivCo p _ t1 t2) = go_prov p `plusNameEnv` go t1 `plusNameEnv` go t2
2177 go_co (SymCo co) = go_co co
2178 go_co (TransCo co1 co2) = go_co co1 `plusNameEnv` go_co co2
2179 go_co (NthCo _ co) = go_co co
2180 go_co (LRCo _ co) = go_co co
2181 go_co (InstCo co arg) = go_co co `plusNameEnv` go_co arg
2182 go_co (CoherenceCo co1 co2) = go_co co1 `plusNameEnv` go_co co2
2183 go_co (KindCo co) = go_co co
2184 go_co (SubCo co) = go_co co
2185 go_co (AxiomRuleCo _ cs) = go_cos cs
2186
2187 go_prov UnsafeCoerceProv = emptyNameEnv
2188 go_prov (PhantomProv co) = go_co co
2189 go_prov (ProofIrrelProv co) = go_co co
2190 go_prov (PluginProv _) = emptyNameEnv
2191 go_prov (HoleProv h) = pprPanic "tyConsOfType hit a hole" (ppr h)
2192
2193 go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
2194 go_cos cos = foldr (plusNameEnv . go_co) emptyNameEnv cos
2195
2196 go_tc tc = unitNameEnv (tyConName tc) tc
2197 go_ax ax = go_tc $ coAxiomTyCon ax
2198
2199 -- | Find the result 'Kind' of a type synonym,
2200 -- after applying it to its 'arity' number of type variables
2201 -- Actually this function works fine on data types too,
2202 -- but they'd always return '*', so we never need to ask
2203 synTyConResKind :: TyCon -> Kind
2204 synTyConResKind tycon = piResultTys (tyConKind tycon) (mkTyVarTys (tyConTyVars tycon))
2205
2206 -- | Retrieve the free variables in this type, splitting them based
2207 -- on whether the variable was used in a dependent context. It's possible
2208 -- for a variable to be reported twice, if it's used both dependently
2209 -- and non-dependently. (This isn't the most precise analysis, because
2210 -- it's used in the typechecking knot. It might list some dependent
2211 -- variables as also non-dependent.)
2212 splitDepVarsOfType :: Type -> Pair TyCoVarSet
2213 splitDepVarsOfType = go
2214 where
2215 go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv)
2216 (unitVarSet tv)
2217 go (AppTy t1 t2) = go t1 `mappend` go t2
2218 go (TyConApp _ tys) = foldMap go tys
2219 go (ForAllTy (Anon arg) res) = go arg `mappend` go res
2220 go (ForAllTy (Named tv _) ty)
2221 = let Pair kvs tvs = go ty in
2222 Pair (kvs `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv))
2223 (tvs `delVarSet` tv)
2224 go (LitTy {}) = mempty
2225 go (CastTy ty co) = go ty `mappend` Pair (tyCoVarsOfCo co)
2226 emptyVarSet
2227 go (CoercionTy co) = go_co co
2228
2229 go_co co = let Pair ty1 ty2 = coercionKind co in
2230 go ty1 `mappend` go ty2 -- NB: the Pairs separate along different
2231 -- dimensions here. Be careful!
2232
2233 -- | Like 'splitDepVarsOfType', but over a list of types
2234 splitDepVarsOfTypes :: [Type] -> Pair TyCoVarSet
2235 splitDepVarsOfTypes = foldMap splitDepVarsOfType
2236
2237 -- | Retrieve the free variables in this type, splitting them based
2238 -- on whether they are used visibly or invisibly. Invisible ones come
2239 -- first.
2240 splitVisVarsOfType :: Type -> Pair TyCoVarSet
2241 splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
2242 where
2243 Pair invis_vars1 vis_vars = go orig_ty
2244 invis_vars = invis_vars1 `minusVarSet` vis_vars
2245
2246 go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv)
2247 go (AppTy t1 t2) = go t1 `mappend` go t2
2248 go (TyConApp tc tys) = go_tc tc tys
2249 go (ForAllTy (Anon t1) t2) = go t1 `mappend` go t2
2250 go (ForAllTy (Named tv _) ty)
2251 = ((`delVarSet` tv) <$> go ty) `mappend`
2252 (invisible (tyCoVarsOfType $ tyVarKind tv))
2253 go (LitTy {}) = mempty
2254 go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co)
2255 go (CoercionTy co) = invisible $ tyCoVarsOfCo co
2256
2257 invisible vs = Pair vs emptyVarSet
2258
2259 go_tc tc tys = let (invis, vis) = partitionInvisibles tc id tys in
2260 invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis
2261
2262 splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
2263 splitVisVarsOfTypes = foldMap splitVisVarsOfType