Fix a nasty bug in piResultTys
[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, FlexibleContexts #-}
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, ArgFlag(..), KindOrType, PredType, ThetaType,
18 Var, TyVar, isTyVar, TyCoVar, TyBinder, TyVarBinder,
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, funResultTy, funArgTy,
29
30 mkTyConApp, mkTyConTy,
31 tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
32 tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
33 splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
34 tcRepSplitTyConApp_maybe, tcSplitTyConApp_maybe,
35 splitListTyConApp_maybe,
36 repSplitTyConApp_maybe,
37
38 mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys,
39 mkVisForAllTys, mkInvForAllTy,
40 splitForAllTys, splitForAllTyVarBndrs,
41 splitForAllTy_maybe, splitForAllTy,
42 splitPiTy_maybe, splitPiTy, splitPiTys,
43 mkPiTy, mkPiTys, mkTyConBindersPreferAnon,
44 mkLamType, mkLamTypes,
45 piResultTy, piResultTys,
46 applyTysX, dropForAlls,
47
48 mkNumLitTy, isNumLitTy,
49 mkStrLitTy, isStrLitTy,
50
51 getRuntimeRep_maybe, getRuntimeRepFromKind_maybe,
52
53 mkCastTy, mkCoercionTy, splitCastTy_maybe,
54
55 userTypeError_maybe, pprUserTypeErrorTy,
56
57 coAxNthLHS,
58 stripCoercionTy, splitCoercionType_maybe,
59
60 splitPiTysInvisible, filterOutInvisibleTypes,
61 partitionInvisibles,
62 synTyConResKind,
63
64 modifyJoinResTy, setJoinResTy,
65
66 -- Analyzing types
67 TyCoMapper(..), mapType, mapCoercion,
68
69 -- (Newtypes)
70 newTyConInstRhs,
71
72 -- Pred types
73 mkFamilyTyConApp,
74 isDictLikeTy,
75 mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
76 equalityTyCon,
77 mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
78 mkClassPred,
79 isClassPred, isEqPred, isNomEqPred,
80 isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
81 isCTupleClass,
82
83 -- Deconstructing predicate types
84 PredTree(..), EqRel(..), eqRelRole, classifyPredType,
85 getClassPredTys, getClassPredTys_maybe,
86 getEqPredTys, getEqPredTys_maybe, getEqPredRole,
87 predTypeEqRel,
88
89 -- ** Binders
90 sameVis,
91 mkTyVarBinder, mkTyVarBinders,
92 mkAnonBinder,
93 isAnonTyBinder, isNamedTyBinder,
94 binderVar, binderVars, binderKind, binderArgFlag,
95 tyBinderType, tyBinderVar_maybe,
96 binderRelevantType_maybe, caseBinder,
97 isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder, isInvisibleBinder,
98 tyConBindersTyBinders,
99
100 -- ** Common type constructors
101 funTyCon,
102
103 -- ** Predicates on types
104 isTyVarTy, isFunTy, isDictTy, isPredTy, isCoercionTy,
105 isCoercionTy_maybe, isCoercionType, isForAllTy,
106 isPiTy, isTauTy, isFamFreeTy,
107
108 isValidJoinPointType,
109
110 -- (Lifting and boxity)
111 isLiftedType_maybe, isUnliftedType, isUnboxedTupleType, isUnboxedSumType,
112 isAlgType, isDataFamilyAppType,
113 isPrimitiveType, isStrictType,
114 isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
115 dropRuntimeRepArgs,
116 getRuntimeRep, getRuntimeRepFromKind,
117
118 -- * Main data types representing Kinds
119 Kind,
120
121 -- ** Finding the kind of a type
122 typeKind, isTypeLevPoly, resultIsLevPoly,
123
124 -- ** Common Kind
125 liftedTypeKind,
126
127 -- * Type free variables
128 tyCoFVsOfType, tyCoFVsBndr,
129 tyCoVarsOfType, tyCoVarsOfTypes,
130 tyCoVarsOfTypeDSet,
131 coVarsOfType,
132 coVarsOfTypes, closeOverKinds, closeOverKindsList,
133 noFreeVarsOfType,
134 splitVisVarsOfType, splitVisVarsOfTypes,
135 expandTypeSynonyms,
136 typeSize, occCheckExpand,
137
138 -- * Well-scoped lists of variables
139 dVarSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped,
140 tyCoVarsOfTypesWellScoped,
141
142 -- * Type comparison
143 eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX,
144 nonDetCmpTypesX, nonDetCmpTc,
145 eqVarBndrs,
146
147 -- * Forcing evaluation of types
148 seqType, seqTypes,
149
150 -- * Other views onto Types
151 coreView, tcView,
152
153 tyConsOfType,
154
155 -- * Main type substitution data types
156 TvSubstEnv, -- Representation widely visible
157 TCvSubst(..), -- Representation visible to a few friends
158
159 -- ** Manipulating type substitutions
160 emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
161
162 mkTCvSubst, zipTvSubst, mkTvSubstPrs,
163 notElemTCvSubst,
164 getTvSubstEnv, setTvSubstEnv,
165 zapTCvSubst, getTCvInScope, getTCvSubstRangeFVs,
166 extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
167 extendTCvSubst, extendCvSubst,
168 extendTvSubst, extendTvSubstBinderAndInScope,
169 extendTvSubstList, extendTvSubstAndInScope,
170 extendTvSubstWithClone,
171 isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv,
172 isEmptyTCvSubst, unionTCvSubst,
173
174 -- ** Performing substitution on types and kinds
175 substTy, substTys, substTyWith, substTysWith, substTheta,
176 substTyAddInScope,
177 substTyUnchecked, substTysUnchecked, substThetaUnchecked,
178 substTyWithUnchecked,
179 substCoUnchecked, substCoWithUnchecked,
180 substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars,
181 cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
182
183 -- * Pretty-printing
184 pprType, pprParendType, pprPrecType,
185 pprTypeApp, pprTyThingCategory, pprShortTyThing,
186 pprTvBndr, pprTvBndrs, pprForAll, pprUserForAll,
187 pprSigmaType, ppSuggestExplicitKinds,
188 pprTheta, pprThetaArrowTy, pprClassPred,
189 pprKind, pprParendKind, pprSourceTyCon,
190 PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
191 pprTyVar, pprTyVars,
192 pprWithTYPE,
193
194 -- * Tidying type related things up for printing
195 tidyType, tidyTypes,
196 tidyOpenType, tidyOpenTypes,
197 tidyOpenKind,
198 tidyTyCoVarBndr, tidyTyCoVarBndrs, tidyFreeTyCoVars,
199 tidyOpenTyCoVar, tidyOpenTyCoVars,
200 tidyTyVarOcc,
201 tidyTopType,
202 tidyKind,
203 tidyTyVarBinder, tidyTyVarBinders
204 ) where
205
206 #include "HsVersions.h"
207
208 import GhcPrelude
209
210 import BasicTypes
211
212 -- We import the representation and primitive functions from TyCoRep.
213 -- Many things are reexported, but not the representation!
214
215 import Kind
216 import TyCoRep
217
218 -- friends:
219 import Var
220 import VarEnv
221 import VarSet
222 import UniqSet
223
224 import Class
225 import TyCon
226 import TysPrim
227 import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind
228 , typeSymbolKind, liftedTypeKind )
229 import PrelNames
230 import CoAxiom
231 import {-# SOURCE #-} Coercion
232
233 -- others
234 import Util
235 import Outputable
236 import FastString
237 import Pair
238 import DynFlags ( gopt_set, GeneralFlag(Opt_PrintExplicitRuntimeReps) )
239 import ListSetOps
240 import Digraph
241 import Unique ( nonDetCmpUnique )
242
243 import Maybes ( orElse )
244 import Data.Maybe ( isJust, mapMaybe )
245 import Control.Monad ( guard )
246 import Control.Arrow ( first, second )
247
248 -- $type_classification
249 -- #type_classification#
250 --
251 -- Types are one of:
252 --
253 -- [Unboxed] Iff its representation is other than a pointer
254 -- Unboxed types are also unlifted.
255 --
256 -- [Lifted] Iff it has bottom as an element.
257 -- Closures always have lifted types: i.e. any
258 -- let-bound identifier in Core must have a lifted
259 -- type. Operationally, a lifted object is one that
260 -- can be entered.
261 -- Only lifted types may be unified with a type variable.
262 --
263 -- [Algebraic] Iff it is a type with one or more constructors, whether
264 -- declared with @data@ or @newtype@.
265 -- An algebraic type is one that can be deconstructed
266 -- with a case expression. This is /not/ the same as
267 -- lifted types, because we also include unboxed
268 -- tuples in this classification.
269 --
270 -- [Data] Iff it is a type declared with @data@, or a boxed tuple.
271 --
272 -- [Primitive] Iff it is a built-in type that can't be expressed in Haskell.
273 --
274 -- Currently, all primitive types are unlifted, but that's not necessarily
275 -- the case: for example, @Int@ could be primitive.
276 --
277 -- Some primitive types are unboxed, such as @Int#@, whereas some are boxed
278 -- but unlifted (such as @ByteArray#@). The only primitive types that we
279 -- classify as algebraic are the unboxed tuples.
280 --
281 -- Some examples of type classifications that may make this a bit clearer are:
282 --
283 -- @
284 -- Type primitive boxed lifted algebraic
285 -- -----------------------------------------------------------------------------
286 -- Int# Yes No No No
287 -- ByteArray# Yes Yes No No
288 -- (\# a, b \#) Yes No No Yes
289 -- (\# a | b \#) Yes No No Yes
290 -- ( a, b ) No Yes Yes Yes
291 -- [a] No Yes Yes Yes
292 -- @
293
294 -- $representation_types
295 -- A /source type/ is a type that is a separate type as far as the type checker is
296 -- concerned, but which has a more low-level representation as far as Core-to-Core
297 -- passes and the rest of the back end is concerned.
298 --
299 -- You don't normally have to worry about this, as the utility functions in
300 -- this module will automatically convert a source into a representation type
301 -- if they are spotted, to the best of it's abilities. If you don't want this
302 -- to happen, use the equivalent functions from the "TcType" module.
303
304 {-
305 ************************************************************************
306 * *
307 Type representation
308 * *
309 ************************************************************************
310
311 Note [coreView vs tcView]
312 ~~~~~~~~~~~~~~~~~~~~~~~~~
313 So far as the typechecker is concerned, 'Constraint' and 'TYPE LiftedRep' are distinct kinds.
314
315 But in Core these two are treated as identical.
316
317 We implement this by making 'coreView' convert 'Constraint' to 'TYPE LiftedRep' on the fly.
318 The function tcView (used in the type checker) does not do this.
319
320 See also Trac #11715, which tracks removing this inconsistency.
321
322 -}
323
324 {-# INLINE coreView #-}
325 coreView :: Type -> Maybe Type
326 -- ^ This function Strips off the /top layer only/ of a type synonym
327 -- application (if any) its underlying representation type.
328 -- Returns Nothing if there is nothing to look through.
329 -- This function considers 'Constraint' to be a synonym of @TYPE LiftedRep@.
330 --
331 -- By being non-recursive and inlined, this case analysis gets efficiently
332 -- joined onto the case analysis that the caller is already doing
333 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
334 = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
335 -- The free vars of 'rhs' should all be bound by 'tenv', so it's
336 -- ok to use 'substTy' here.
337 -- See also Note [The substitution invariant] in TyCoRep.
338 -- Its important to use mkAppTys, rather than (foldl AppTy),
339 -- because the function part might well return a
340 -- partially-applied type constructor; indeed, usually will!
341
342 coreView (TyConApp tc []) -- At the Core level, Constraint = Type
343 | isConstraintKindCon tc
344 = Just liftedTypeKind
345
346 coreView _ = Nothing
347
348 -- | Gives the typechecker view of a type. This unwraps synonyms but
349 -- leaves 'Constraint' alone. c.f. coreView, which turns Constraint into
350 -- TYPE LiftedRep. Returns Nothing if no unwrapping happens.
351 -- See also Note [coreView vs tcView] in Type.
352 {-# INLINE tcView #-}
353 tcView :: Type -> Maybe Type
354 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
355 = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
356 -- The free vars of 'rhs' should all be bound by 'tenv', so it's
357 -- ok to use 'substTy' here.
358 -- See also Note [The substitution invariant] in TyCoRep.
359 -- Its important to use mkAppTys, rather than (foldl AppTy),
360 -- because the function part might well return a
361 -- partially-applied type constructor; indeed, usually will!
362 tcView _ = Nothing
363
364 -----------------------------------------------
365 expandTypeSynonyms :: Type -> Type
366 -- ^ Expand out all type synonyms. Actually, it'd suffice to expand out
367 -- just the ones that discard type variables (e.g. type Funny a = Int)
368 -- But we don't know which those are currently, so we just expand all.
369 --
370 -- 'expandTypeSynonyms' only expands out type synonyms mentioned in the type,
371 -- not in the kinds of any TyCon or TyVar mentioned in the type.
372 --
373 -- Keep this synchronized with 'synonymTyConsOfType'
374 expandTypeSynonyms ty
375 = go (mkEmptyTCvSubst in_scope) ty
376 where
377 in_scope = mkInScopeSet (tyCoVarsOfType ty)
378
379 go subst (TyConApp tc tys)
380 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc expanded_tys
381 = let subst' = mkTvSubst in_scope (mkVarEnv tenv)
382 -- Make a fresh substitution; rhs has nothing to
383 -- do with anything that has happened so far
384 -- NB: if you make changes here, be sure to build an
385 -- /idempotent/ substitution, even in the nested case
386 -- type T a b = a -> b
387 -- type S x y = T y x
388 -- (Trac #11665)
389 in mkAppTys (go subst' rhs) tys'
390 | otherwise
391 = TyConApp tc expanded_tys
392 where
393 expanded_tys = (map (go subst) tys)
394
395 go _ (LitTy l) = LitTy l
396 go subst (TyVarTy tv) = substTyVar subst tv
397 go subst (AppTy t1 t2) = mkAppTy (go subst t1) (go subst t2)
398 go subst (FunTy arg res)
399 = mkFunTy (go subst arg) (go subst res)
400 go subst (ForAllTy (TvBndr tv vis) t)
401 = let (subst', tv') = substTyVarBndrUsing go subst tv in
402 ForAllTy (TvBndr tv' vis) (go subst' t)
403 go subst (CastTy ty co) = mkCastTy (go subst ty) (go_co subst co)
404 go subst (CoercionTy co) = mkCoercionTy (go_co subst co)
405
406 go_mco _ MRefl = MRefl
407 go_mco subst (MCo co) = MCo (go_co subst co)
408
409 go_co subst (Refl ty)
410 = mkNomReflCo (go subst ty)
411 go_co subst (GRefl r ty mco)
412 = mkGReflCo r (go subst ty) (go_mco subst mco)
413 -- NB: coercions are always expanded upon creation
414 go_co subst (TyConAppCo r tc args)
415 = mkTyConAppCo r tc (map (go_co subst) args)
416 go_co subst (AppCo co arg)
417 = mkAppCo (go_co subst co) (go_co subst arg)
418 go_co subst (ForAllCo tv kind_co co)
419 = let (subst', tv', kind_co') = go_cobndr subst tv kind_co in
420 mkForAllCo tv' kind_co' (go_co subst' co)
421 go_co subst (FunCo r co1 co2)
422 = mkFunCo r (go_co subst co1) (go_co subst co2)
423 go_co subst (CoVarCo cv)
424 = substCoVar subst cv
425 go_co subst (AxiomInstCo ax ind args)
426 = mkAxiomInstCo ax ind (map (go_co subst) args)
427 go_co subst (UnivCo p r t1 t2)
428 = mkUnivCo (go_prov subst p) r (go subst t1) (go subst t2)
429 go_co subst (SymCo co)
430 = mkSymCo (go_co subst co)
431 go_co subst (TransCo co1 co2)
432 = mkTransCo (go_co subst co1) (go_co subst co2)
433 go_co subst (NthCo r n co)
434 = mkNthCo r n (go_co subst co)
435 go_co subst (LRCo lr co)
436 = mkLRCo lr (go_co subst co)
437 go_co subst (InstCo co arg)
438 = mkInstCo (go_co subst co) (go_co subst arg)
439 go_co subst (KindCo co)
440 = mkKindCo (go_co subst co)
441 go_co subst (SubCo co)
442 = mkSubCo (go_co subst co)
443 go_co subst (AxiomRuleCo ax cs)
444 = AxiomRuleCo ax (map (go_co subst) cs)
445 go_co _ (HoleCo h)
446 = pprPanic "expandTypeSynonyms hit a hole" (ppr h)
447
448 go_prov _ UnsafeCoerceProv = UnsafeCoerceProv
449 go_prov subst (PhantomProv co) = PhantomProv (go_co subst co)
450 go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
451 go_prov _ p@(PluginProv _) = p
452
453 -- the "False" and "const" are to accommodate the type of
454 -- substForAllCoBndrUsing, which is general enough to
455 -- handle coercion optimization (which sometimes swaps the
456 -- order of a coercion)
457 go_cobndr subst = substForAllCoBndrUsing False (go_co subst) subst
458
459 {-
460 ************************************************************************
461 * *
462 Analyzing types
463 * *
464 ************************************************************************
465
466 These functions do a map-like operation over types, performing some operation
467 on all variables and binding sites. Primarily used for zonking.
468
469 Note [Efficiency for mapCoercion ForAllCo case]
470 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
471 As noted in Note [Forall coercions] in TyCoRep, a ForAllCo is a bit redundant.
472 It stores a TyVar and a Coercion, where the kind of the TyVar always matches
473 the left-hand kind of the coercion. This is convenient lots of the time, but
474 not when mapping a function over a coercion.
475
476 The problem is that tcm_tybinder will affect the TyVar's kind and
477 mapCoercion will affect the Coercion, and we hope that the results will be
478 the same. Even if they are the same (which should generally happen with
479 correct algorithms), then there is an efficiency issue. In particular,
480 this problem seems to make what should be a linear algorithm into a potentially
481 exponential one. But it's only going to be bad in the case where there's
482 lots of foralls in the kinds of other foralls. Like this:
483
484 forall a : (forall b : (forall c : ...). ...). ...
485
486 This construction seems unlikely. So we'll do the inefficient, easy way
487 for now.
488
489 Note [Specialising mappers]
490 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
491 These INLINABLE pragmas are indispensable. mapType/mapCoercion are used
492 to implement zonking, and it's vital that they get specialised to the TcM
493 monad. This specialisation happens automatically (that is, without a
494 SPECIALISE pragma) as long as the definitions are INLINABLE. For example,
495 this one change made a 20% allocation difference in perf/compiler/T5030.
496
497 -}
498
499 -- | This describes how a "map" operation over a type/coercion should behave
500 data TyCoMapper env m
501 = TyCoMapper
502 { tcm_smart :: Bool -- ^ Should the new type be created with smart
503 -- constructors?
504 , tcm_tyvar :: env -> TyVar -> m Type
505 , tcm_covar :: env -> CoVar -> m Coercion
506 , tcm_hole :: env -> CoercionHole -> m Coercion
507 -- ^ What to do with coercion holes.
508 -- See Note [Coercion holes] in TyCoRep.
509
510 , tcm_tybinder :: env -> TyVar -> ArgFlag -> m (env, TyVar)
511 -- ^ The returned env is used in the extended scope
512 }
513
514 {-# INLINABLE mapType #-} -- See Note [Specialising mappers]
515 mapType :: Monad m => TyCoMapper env m -> env -> Type -> m Type
516 mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
517 , tcm_tybinder = tybinder })
518 env ty
519 = go ty
520 where
521 go (TyVarTy tv) = tyvar env tv
522 go (AppTy t1 t2) = mkappty <$> go t1 <*> go t2
523 go t@(TyConApp _ []) = return t -- avoid allocation in this exceedingly
524 -- common case (mostly, for *)
525 go (TyConApp tc tys) = mktyconapp tc <$> mapM go tys
526 go (FunTy arg res) = FunTy <$> go arg <*> go res
527 go (ForAllTy (TvBndr tv vis) inner)
528 = do { (env', tv') <- tybinder env tv vis
529 ; inner' <- mapType mapper env' inner
530 ; return $ ForAllTy (TvBndr tv' vis) inner' }
531 go ty@(LitTy {}) = return ty
532 go (CastTy ty co) = mkcastty <$> go ty <*> mapCoercion mapper env co
533 go (CoercionTy co) = CoercionTy <$> mapCoercion mapper env co
534
535 (mktyconapp, mkappty, mkcastty)
536 | smart = (mkTyConApp, mkAppTy, mkCastTy)
537 | otherwise = (TyConApp, AppTy, CastTy)
538
539 {-# INLINABLE mapCoercion #-} -- See Note [Specialising mappers]
540 mapCoercion :: Monad m
541 => TyCoMapper env m -> env -> Coercion -> m Coercion
542 mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
543 , tcm_hole = cohole, tcm_tybinder = tybinder })
544 env co
545 = go co
546 where
547 go_mco MRefl = return MRefl
548 go_mco (MCo co) = MCo <$> (go co)
549
550 go (Refl ty) = Refl <$> mapType mapper env ty
551 go (GRefl r ty mco) = mkgreflco r <$> mapType mapper env ty <*> (go_mco mco)
552 go (TyConAppCo r tc args)
553 = mktyconappco r tc <$> mapM go args
554 go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
555 go (ForAllCo tv kind_co co)
556 = do { kind_co' <- go kind_co
557 ; (env', tv') <- tybinder env tv Inferred
558 ; co' <- mapCoercion mapper env' co
559 ; return $ mkforallco tv' kind_co' co' }
560 -- See Note [Efficiency for mapCoercion ForAllCo case]
561 go (FunCo r c1 c2) = mkFunCo r <$> go c1 <*> go c2
562 go (CoVarCo cv) = covar env cv
563 go (AxiomInstCo ax i args)
564 = mkaxiominstco ax i <$> mapM go args
565 go (HoleCo hole) = cohole env hole
566 go (UnivCo p r t1 t2)
567 = mkunivco <$> go_prov p <*> pure r
568 <*> mapType mapper env t1 <*> mapType mapper env t2
569 go (SymCo co) = mksymco <$> go co
570 go (TransCo c1 c2) = mktransco <$> go c1 <*> go c2
571 go (AxiomRuleCo r cos) = AxiomRuleCo r <$> mapM go cos
572 go (NthCo r i co) = mknthco r i <$> go co
573 go (LRCo lr co) = mklrco lr <$> go co
574 go (InstCo co arg) = mkinstco <$> go co <*> go arg
575 go (KindCo co) = mkkindco <$> go co
576 go (SubCo co) = mksubco <$> go co
577
578 go_prov UnsafeCoerceProv = return UnsafeCoerceProv
579 go_prov (PhantomProv co) = PhantomProv <$> go co
580 go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co
581 go_prov p@(PluginProv _) = return p
582
583 ( mktyconappco, mkappco, mkaxiominstco, mkunivco
584 , mksymco, mktransco, mknthco, mklrco, mkinstco
585 , mkkindco, mksubco, mkforallco, mkgreflco)
586 | smart
587 = ( mkTyConAppCo, mkAppCo, mkAxiomInstCo, mkUnivCo
588 , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo
589 , mkKindCo, mkSubCo, mkForAllCo, mkGReflCo )
590 | otherwise
591 = ( TyConAppCo, AppCo, AxiomInstCo, UnivCo
592 , SymCo, TransCo, NthCo, LRCo, InstCo
593 , KindCo, SubCo, ForAllCo, GRefl )
594
595 {-
596 ************************************************************************
597 * *
598 \subsection{Constructor-specific functions}
599 * *
600 ************************************************************************
601
602
603 ---------------------------------------------------------------------
604 TyVarTy
605 ~~~~~~~
606 -}
607
608 -- | Attempts to obtain the type variable underlying a 'Type', and panics with the
609 -- given message if this is not a type variable type. See also 'getTyVar_maybe'
610 getTyVar :: String -> Type -> TyVar
611 getTyVar msg ty = case getTyVar_maybe ty of
612 Just tv -> tv
613 Nothing -> panic ("getTyVar: " ++ msg)
614
615 isTyVarTy :: Type -> Bool
616 isTyVarTy ty = isJust (getTyVar_maybe ty)
617
618 -- | Attempts to obtain the type variable underlying a 'Type'
619 getTyVar_maybe :: Type -> Maybe TyVar
620 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
621 | otherwise = repGetTyVar_maybe ty
622
623 -- | If the type is a tyvar, possibly under a cast, returns it, along
624 -- with the coercion. Thus, the co is :: kind tv ~N kind type
625 getCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN)
626 getCastedTyVar_maybe ty | Just ty' <- coreView ty = getCastedTyVar_maybe ty'
627 getCastedTyVar_maybe (CastTy (TyVarTy tv) co) = Just (tv, co)
628 getCastedTyVar_maybe (TyVarTy tv)
629 = Just (tv, mkReflCo Nominal (tyVarKind tv))
630 getCastedTyVar_maybe _ = Nothing
631
632 -- | Attempts to obtain the type variable underlying a 'Type', without
633 -- any expansion
634 repGetTyVar_maybe :: Type -> Maybe TyVar
635 repGetTyVar_maybe (TyVarTy tv) = Just tv
636 repGetTyVar_maybe _ = Nothing
637
638 {-
639 ---------------------------------------------------------------------
640 AppTy
641 ~~~~~
642 We need to be pretty careful with AppTy to make sure we obey the
643 invariant that a TyConApp is always visibly so. mkAppTy maintains the
644 invariant: use it.
645
646 Note [Decomposing fat arrow c=>t]
647 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
648 Can we unify (a b) with (Eq a => ty)? If we do so, we end up with
649 a partial application like ((=>) Eq a) which doesn't make sense in
650 source Haskell. In contrast, we *can* unify (a b) with (t1 -> t2).
651 Here's an example (Trac #9858) of how you might do it:
652 i :: (Typeable a, Typeable b) => Proxy (a b) -> TypeRep
653 i p = typeRep p
654
655 j = i (Proxy :: Proxy (Eq Int => Int))
656 The type (Proxy (Eq Int => Int)) is only accepted with -XImpredicativeTypes,
657 but suppose we want that. But then in the call to 'i', we end
658 up decomposing (Eq Int => Int), and we definitely don't want that.
659
660 This really only applies to the type checker; in Core, '=>' and '->'
661 are the same, as are 'Constraint' and '*'. But for now I've put
662 the test in repSplitAppTy_maybe, which applies throughout, because
663 the other calls to splitAppTy are in Unify, which is also used by
664 the type checker (e.g. when matching type-function equations).
665
666 -}
667
668 -- | Applies a type to another, as in e.g. @k a@
669 mkAppTy :: Type -> Type -> Type
670 -- See Note [Respecting definitional equality], invariant (EQ1).
671 mkAppTy (CastTy fun_ty co) arg_ty
672 | ([arg_co], res_co) <- decomposePiCos co (coercionKind co) [arg_ty]
673 = (fun_ty `mkAppTy` (arg_ty `mkCastTy` arg_co)) `mkCastTy` res_co
674
675 mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
676 mkAppTy ty1 ty2 = AppTy ty1 ty2
677 -- Note that the TyConApp could be an
678 -- under-saturated type synonym. GHC allows that; e.g.
679 -- type Foo k = k a -> k a
680 -- type Id x = x
681 -- foo :: Foo Id -> Foo Id
682 --
683 -- Here Id is partially applied in the type sig for Foo,
684 -- but once the type synonyms are expanded all is well
685
686 mkAppTys :: Type -> [Type] -> Type
687 mkAppTys ty1 [] = ty1
688 mkAppTys (CastTy fun_ty co) arg_tys -- much more efficient then nested mkAppTy
689 -- Why do this? See (EQ1) of
690 -- Note [Respecting definitional equality]
691 -- in TyCoRep
692 = foldl AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers
693 where
694 (arg_cos, res_co) = decomposePiCos co (coercionKind co) arg_tys
695 (args_to_cast, leftovers) = splitAtList arg_cos arg_tys
696 casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos
697 mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
698 mkAppTys ty1 tys2 = foldl AppTy ty1 tys2
699
700 -------------
701 splitAppTy_maybe :: Type -> Maybe (Type, Type)
702 -- ^ Attempt to take a type application apart, whether it is a
703 -- function, type constructor, or plain type application. Note
704 -- that type family applications are NEVER unsaturated by this!
705 splitAppTy_maybe ty | Just ty' <- coreView ty
706 = splitAppTy_maybe ty'
707 splitAppTy_maybe ty = repSplitAppTy_maybe ty
708
709 -------------
710 repSplitAppTy_maybe :: HasDebugCallStack => Type -> Maybe (Type,Type)
711 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
712 -- any Core view stuff is already done
713 repSplitAppTy_maybe (FunTy ty1 ty2)
714 = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
715 where
716 rep1 = getRuntimeRep ty1
717 rep2 = getRuntimeRep ty2
718
719 repSplitAppTy_maybe (AppTy ty1 ty2)
720 = Just (ty1, ty2)
721
722 repSplitAppTy_maybe (TyConApp tc tys)
723 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
724 , Just (tys', ty') <- snocView tys
725 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
726
727 repSplitAppTy_maybe _other = Nothing
728
729 -- this one doesn't braek apart (c => t).
730 -- See Note [Decomposing fat arrow c=>t]
731 -- Defined here to avoid module loops between Unify and TcType.
732 tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
733 -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
734 -- any coreView stuff is already done. Refuses to look through (c => t)
735 tcRepSplitAppTy_maybe (FunTy ty1 ty2)
736 | isConstraintKind (typeKind ty1)
737 = Nothing -- See Note [Decomposing fat arrow c=>t]
738
739 | otherwise
740 = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
741 where
742 rep1 = getRuntimeRep ty1
743 rep2 = getRuntimeRep ty2
744
745 tcRepSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
746 tcRepSplitAppTy_maybe (TyConApp tc tys)
747 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
748 , Just (tys', ty') <- snocView tys
749 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
750 tcRepSplitAppTy_maybe _other = Nothing
751
752 -- | Split a type constructor application into its type constructor and
753 -- applied types. Note that this may fail in the case of a 'FunTy' with an
754 -- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind
755 -- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your
756 -- type before using this function.
757 --
758 -- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'.
759 tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
760 -- Defined here to avoid module loops between Unify and TcType.
761 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
762 tcSplitTyConApp_maybe ty = tcRepSplitTyConApp_maybe ty
763
764 -- | Like 'tcSplitTyConApp_maybe' but doesn't look through type synonyms.
765 tcRepSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
766 -- Defined here to avoid module loops between Unify and TcType.
767 tcRepSplitTyConApp_maybe (TyConApp tc tys)
768 = Just (tc, tys)
769
770 tcRepSplitTyConApp_maybe (FunTy arg res)
771 = Just (funTyCon, [arg_rep, res_rep, arg, res])
772 where
773 arg_rep = getRuntimeRep arg
774 res_rep = getRuntimeRep res
775
776 tcRepSplitTyConApp_maybe _
777 = Nothing
778
779 -------------
780 splitAppTy :: Type -> (Type, Type)
781 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
782 -- and panics if this is not possible
783 splitAppTy ty = case splitAppTy_maybe ty of
784 Just pr -> pr
785 Nothing -> panic "splitAppTy"
786
787 -------------
788 splitAppTys :: Type -> (Type, [Type])
789 -- ^ Recursively splits a type as far as is possible, leaving a residual
790 -- type being applied to and the type arguments applied to it. Never fails,
791 -- even if that means returning an empty list of type applications.
792 splitAppTys ty = split ty ty []
793 where
794 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
795 split _ (AppTy ty arg) args = split ty ty (arg:args)
796 split _ (TyConApp tc tc_args) args
797 = let -- keep type families saturated
798 n | mightBeUnsaturatedTyCon tc = 0
799 | otherwise = tyConArity tc
800 (tc_args1, tc_args2) = splitAt n tc_args
801 in
802 (TyConApp tc tc_args1, tc_args2 ++ args)
803 split _ (FunTy ty1 ty2) args
804 = ASSERT( null args )
805 (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
806 where
807 rep1 = getRuntimeRep ty1
808 rep2 = getRuntimeRep ty2
809
810 split orig_ty _ args = (orig_ty, args)
811
812 -- | Like 'splitAppTys', but doesn't look through type synonyms
813 repSplitAppTys :: HasDebugCallStack => Type -> (Type, [Type])
814 repSplitAppTys ty = split ty []
815 where
816 split (AppTy ty arg) args = split ty (arg:args)
817 split (TyConApp tc tc_args) args
818 = let n | mightBeUnsaturatedTyCon tc = 0
819 | otherwise = tyConArity tc
820 (tc_args1, tc_args2) = splitAt n tc_args
821 in
822 (TyConApp tc tc_args1, tc_args2 ++ args)
823 split (FunTy ty1 ty2) args
824 = ASSERT( null args )
825 (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
826 where
827 rep1 = getRuntimeRep ty1
828 rep2 = getRuntimeRep ty2
829
830 split ty args = (ty, args)
831
832 {-
833 LitTy
834 ~~~~~
835 -}
836
837 mkNumLitTy :: Integer -> Type
838 mkNumLitTy n = LitTy (NumTyLit n)
839
840 -- | Is this a numeric literal. We also look through type synonyms.
841 isNumLitTy :: Type -> Maybe Integer
842 isNumLitTy ty | Just ty1 <- coreView ty = isNumLitTy ty1
843 isNumLitTy (LitTy (NumTyLit n)) = Just n
844 isNumLitTy _ = Nothing
845
846 mkStrLitTy :: FastString -> Type
847 mkStrLitTy s = LitTy (StrTyLit s)
848
849 -- | Is this a symbol literal. We also look through type synonyms.
850 isStrLitTy :: Type -> Maybe FastString
851 isStrLitTy ty | Just ty1 <- coreView ty = isStrLitTy ty1
852 isStrLitTy (LitTy (StrTyLit s)) = Just s
853 isStrLitTy _ = Nothing
854
855
856 -- | Is this type a custom user error?
857 -- If so, give us the kind and the error message.
858 userTypeError_maybe :: Type -> Maybe Type
859 userTypeError_maybe t
860 = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t
861 -- There may be more than 2 arguments, if the type error is
862 -- used as a type constructor (e.g. at kind `Type -> Type`).
863
864 ; guard (tyConName tc == errorMessageTypeErrorFamName)
865 ; return msg }
866
867 -- | Render a type corresponding to a user type error into a SDoc.
868 pprUserTypeErrorTy :: Type -> SDoc
869 pprUserTypeErrorTy ty =
870 case splitTyConApp_maybe ty of
871
872 -- Text "Something"
873 Just (tc,[txt])
874 | tyConName tc == typeErrorTextDataConName
875 , Just str <- isStrLitTy txt -> ftext str
876
877 -- ShowType t
878 Just (tc,[_k,t])
879 | tyConName tc == typeErrorShowTypeDataConName -> ppr t
880
881 -- t1 :<>: t2
882 Just (tc,[t1,t2])
883 | tyConName tc == typeErrorAppendDataConName ->
884 pprUserTypeErrorTy t1 <> pprUserTypeErrorTy t2
885
886 -- t1 :$$: t2
887 Just (tc,[t1,t2])
888 | tyConName tc == typeErrorVAppendDataConName ->
889 pprUserTypeErrorTy t1 $$ pprUserTypeErrorTy t2
890
891 -- An unevaluated type function
892 _ -> ppr ty
893
894
895
896
897 {-
898 ---------------------------------------------------------------------
899 FunTy
900 ~~~~~
901
902 Note [Representation of function types]
903 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
904
905 Functions (e.g. Int -> Char) are can be thought of as being applications
906 of funTyCon (known in Haskell surface syntax as (->)),
907
908 (->) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
909 (a :: TYPE r1) (b :: TYPE r2).
910 a -> b -> Type
911
912 However, for efficiency's sake we represent saturated applications of (->)
913 with FunTy. For instance, the type,
914
915 (->) r1 r2 a b
916
917 is equivalent to,
918
919 FunTy (Anon a) b
920
921 Note how the RuntimeReps are implied in the FunTy representation. For this
922 reason we must be careful when recontructing the TyConApp representation (see,
923 for instance, splitTyConApp_maybe).
924
925 In the compiler we maintain the invariant that all saturated applications of
926 (->) are represented with FunTy.
927
928 See #11714.
929 -}
930
931 isFunTy :: Type -> Bool
932 isFunTy ty = isJust (splitFunTy_maybe ty)
933
934 splitFunTy :: Type -> (Type, Type)
935 -- ^ Attempts to extract the argument and result types from a type, and
936 -- panics if that is not possible. See also 'splitFunTy_maybe'
937 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
938 splitFunTy (FunTy arg res) = (arg, res)
939 splitFunTy other = pprPanic "splitFunTy" (ppr other)
940
941 splitFunTy_maybe :: Type -> Maybe (Type, Type)
942 -- ^ Attempts to extract the argument and result types from a type
943 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
944 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
945 splitFunTy_maybe _ = Nothing
946
947 splitFunTys :: Type -> ([Type], Type)
948 splitFunTys ty = split [] ty ty
949 where
950 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
951 split args _ (FunTy arg res) = split (arg:args) res res
952 split args orig_ty _ = (reverse args, orig_ty)
953
954 funResultTy :: Type -> Type
955 -- ^ Extract the function result type and panic if that is not possible
956 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
957 funResultTy (FunTy _ res) = res
958 funResultTy ty = pprPanic "funResultTy" (ppr ty)
959
960 funArgTy :: Type -> Type
961 -- ^ Extract the function argument type and panic if that is not possible
962 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
963 funArgTy (FunTy arg _res) = arg
964 funArgTy ty = pprPanic "funArgTy" (ppr ty)
965
966 piResultTy :: HasDebugCallStack => Type -> Type -> Type
967 piResultTy ty arg = case piResultTy_maybe ty arg of
968 Just res -> res
969 Nothing -> pprPanic "piResultTy" (ppr ty $$ ppr arg)
970
971 piResultTy_maybe :: Type -> Type -> Maybe Type
972
973 -- ^ Just like 'piResultTys' but for a single argument
974 -- Try not to iterate 'piResultTy', because it's inefficient to substitute
975 -- one variable at a time; instead use 'piResultTys"
976 piResultTy_maybe ty arg
977 | Just ty' <- coreView ty = piResultTy_maybe ty' arg
978
979 | FunTy _ res <- ty
980 = Just res
981
982 | ForAllTy (TvBndr tv _) res <- ty
983 = let empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
984 tyCoVarsOfTypes [arg,res]
985 in Just (substTy (extendTvSubst empty_subst tv arg) res)
986
987 | otherwise
988 = Nothing
989
990 -- | (piResultTys f_ty [ty1, .., tyn]) gives the type of (f ty1 .. tyn)
991 -- where f :: f_ty
992 -- 'piResultTys' is interesting because:
993 -- 1. 'f_ty' may have more for-alls than there are args
994 -- 2. Less obviously, it may have fewer for-alls
995 -- For case 2. think of:
996 -- piResultTys (forall a.a) [forall b.b, Int]
997 -- This really can happen, but only (I think) in situations involving
998 -- undefined. For example:
999 -- undefined :: forall a. a
1000 -- Term: undefined @(forall b. b->b) @Int
1001 -- This term should have type (Int -> Int), but notice that
1002 -- there are more type args than foralls in 'undefined's type.
1003
1004 -- If you edit this function, you may need to update the GHC formalism
1005 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
1006
1007 -- This is a heavily used function (e.g. from typeKind),
1008 -- so we pay attention to efficiency, especially in the special case
1009 -- where there are no for-alls so we are just dropping arrows from
1010 -- a function type/kind.
1011 piResultTys :: HasDebugCallStack => Type -> [Type] -> Type
1012 piResultTys ty [] = ty
1013 piResultTys ty orig_args@(arg:args)
1014 | Just ty' <- coreView ty
1015 = piResultTys ty' orig_args
1016
1017 | FunTy _ res <- ty
1018 = piResultTys res args
1019
1020 | ForAllTy (TvBndr tv _) res <- ty
1021 = go (extendVarEnv emptyTvSubstEnv tv arg) res args
1022
1023 | otherwise
1024 = pprPanic "piResultTys1" (ppr ty $$ ppr orig_args)
1025 where
1026 in_scope = mkInScopeSet (tyCoVarsOfTypes (ty:orig_args))
1027
1028 go :: TvSubstEnv -> Type -> [Type] -> Type
1029 go tv_env ty [] = substTy (mkTvSubst in_scope tv_env) ty
1030
1031 go tv_env ty all_args@(arg:args)
1032 | Just ty' <- coreView ty
1033 = go tv_env ty' all_args
1034
1035 | FunTy _ res <- ty
1036 = go tv_env res args
1037
1038 | ForAllTy (TvBndr tv _) res <- ty
1039 = go (extendVarEnv tv_env tv arg) res args
1040
1041 | otherwise -- See Note [Care with kind instantiation]
1042 = ASSERT2( not (isEmptyVarEnv tv_env)
1043 , ppr ty $$ ppr orig_args $$ ppr all_args )
1044 go emptyTvSubstEnv
1045 (substTy (mkTvSubst in_scope tv_env) ty)
1046 all_args
1047
1048 applyTysX :: [TyVar] -> Type -> [Type] -> Type
1049 -- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
1050 -- Assumes that (/\tvs. body_ty) is closed
1051 applyTysX tvs body_ty arg_tys
1052 = ASSERT2( arg_tys `lengthAtLeast` n_tvs, pp_stuff )
1053 ASSERT2( tyCoVarsOfType body_ty `subVarSet` mkVarSet tvs, pp_stuff )
1054 mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
1055 (drop n_tvs arg_tys)
1056 where
1057 pp_stuff = vcat [ppr tvs, ppr body_ty, ppr arg_tys]
1058 n_tvs = length tvs
1059
1060
1061
1062 {- Note [Care with kind instantiation]
1063 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1064 Suppose we have
1065 T :: forall k. k
1066 and we are finding the kind of
1067 T (forall b. b -> b) * Int
1068 Then
1069 T (forall b. b->b) :: k[ k :-> forall b. b->b]
1070 :: forall b. b -> b
1071 So
1072 T (forall b. b->b) * :: (b -> b)[ b :-> *]
1073 :: * -> *
1074
1075 In other words wwe must intantiate the forall!
1076
1077 Similarly (Trac #154218)
1078 S :: forall k f. k -> f k
1079 and we are finding the kind of
1080 S * (* ->) Int Bool
1081 We have
1082 S * (* ->) :: (k -> f k)[ k :-> *, f :-> (* ->)]
1083 :: * -> * -> *
1084 So again we must instantiate.
1085
1086 The same thing happens in ToIface.toIfaceAppArgsX.
1087
1088
1089 ---------------------------------------------------------------------
1090 TyConApp
1091 ~~~~~~~~
1092 -}
1093
1094 -- | A key function: builds a 'TyConApp' or 'FunTy' as appropriate to
1095 -- its arguments. Applies its arguments to the constructor from left to right.
1096 mkTyConApp :: TyCon -> [Type] -> Type
1097 mkTyConApp tycon tys
1098 | isFunTyCon tycon
1099 , [_rep1,_rep2,ty1,ty2] <- tys
1100 = FunTy ty1 ty2
1101
1102 | otherwise
1103 = TyConApp tycon tys
1104
1105 -- splitTyConApp "looks through" synonyms, because they don't
1106 -- mean a distinct type, but all other type-constructor applications
1107 -- including functions are returned as Just ..
1108
1109 -- | Retrieve the tycon heading this type, if there is one. Does /not/
1110 -- look through synonyms.
1111 tyConAppTyConPicky_maybe :: Type -> Maybe TyCon
1112 tyConAppTyConPicky_maybe (TyConApp tc _) = Just tc
1113 tyConAppTyConPicky_maybe (FunTy {}) = Just funTyCon
1114 tyConAppTyConPicky_maybe _ = Nothing
1115
1116
1117 -- | The same as @fst . splitTyConApp@
1118 tyConAppTyCon_maybe :: Type -> Maybe TyCon
1119 tyConAppTyCon_maybe ty | Just ty' <- coreView ty = tyConAppTyCon_maybe ty'
1120 tyConAppTyCon_maybe (TyConApp tc _) = Just tc
1121 tyConAppTyCon_maybe (FunTy {}) = Just funTyCon
1122 tyConAppTyCon_maybe _ = Nothing
1123
1124 tyConAppTyCon :: Type -> TyCon
1125 tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr ty)
1126
1127 -- | The same as @snd . splitTyConApp@
1128 tyConAppArgs_maybe :: Type -> Maybe [Type]
1129 tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty'
1130 tyConAppArgs_maybe (TyConApp _ tys) = Just tys
1131 tyConAppArgs_maybe (FunTy arg res)
1132 | Just rep1 <- getRuntimeRep_maybe arg
1133 , Just rep2 <- getRuntimeRep_maybe res
1134 = Just [rep1, rep2, arg, res]
1135 tyConAppArgs_maybe _ = Nothing
1136
1137 tyConAppArgs :: Type -> [Type]
1138 tyConAppArgs ty = tyConAppArgs_maybe ty `orElse` pprPanic "tyConAppArgs" (ppr ty)
1139
1140 tyConAppArgN :: Int -> Type -> Type
1141 -- Executing Nth
1142 tyConAppArgN n ty
1143 = case tyConAppArgs_maybe ty of
1144 Just tys -> ASSERT2( tys `lengthExceeds` n, ppr n <+> ppr tys ) tys `getNth` n
1145 Nothing -> pprPanic "tyConAppArgN" (ppr n <+> ppr ty)
1146
1147 -- | Attempts to tease a type apart into a type constructor and the application
1148 -- of a number of arguments to that constructor. Panics if that is not possible.
1149 -- See also 'splitTyConApp_maybe'
1150 splitTyConApp :: Type -> (TyCon, [Type])
1151 splitTyConApp ty = case splitTyConApp_maybe ty of
1152 Just stuff -> stuff
1153 Nothing -> pprPanic "splitTyConApp" (ppr ty)
1154
1155 -- | Attempts to tease a type apart into a type constructor and the application
1156 -- of a number of arguments to that constructor
1157 splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
1158 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
1159 splitTyConApp_maybe ty = repSplitTyConApp_maybe ty
1160
1161 -- | Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
1162 -- assumes the synonyms have already been dealt with.
1163 repSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
1164 repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
1165 repSplitTyConApp_maybe (FunTy arg res)
1166 | Just arg_rep <- getRuntimeRep_maybe arg
1167 , Just res_rep <- getRuntimeRep_maybe res
1168 = Just (funTyCon, [arg_rep, res_rep, arg, res])
1169 repSplitTyConApp_maybe _ = Nothing
1170
1171 -- | Attempts to tease a list type apart and gives the type of the elements if
1172 -- successful (looks through type synonyms)
1173 splitListTyConApp_maybe :: Type -> Maybe Type
1174 splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
1175 Just (tc,[e]) | tc == listTyCon -> Just e
1176 _other -> Nothing
1177
1178 nextRole :: Type -> Role
1179 nextRole ty
1180 | Just (tc, tys) <- splitTyConApp_maybe ty
1181 , let num_tys = length tys
1182 , num_tys < tyConArity tc
1183 = tyConRoles tc `getNth` num_tys
1184
1185 | otherwise
1186 = Nominal
1187
1188 newTyConInstRhs :: TyCon -> [Type] -> Type
1189 -- ^ Unwrap one 'layer' of newtype on a type constructor and its
1190 -- arguments, using an eta-reduced version of the @newtype@ if possible.
1191 -- This requires tys to have at least @newTyConInstArity tycon@ elements.
1192 newTyConInstRhs tycon tys
1193 = ASSERT2( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs )
1194 applyTysX tvs rhs tys
1195 where
1196 (tvs, rhs) = newTyConEtadRhs tycon
1197
1198 {-
1199 ---------------------------------------------------------------------
1200 CastTy
1201 ~~~~~~
1202 A casted type has its *kind* casted into something new.
1203
1204 -}
1205
1206 splitCastTy_maybe :: Type -> Maybe (Type, Coercion)
1207 splitCastTy_maybe ty | Just ty' <- coreView ty = splitCastTy_maybe ty'
1208 splitCastTy_maybe (CastTy ty co) = Just (ty, co)
1209 splitCastTy_maybe _ = Nothing
1210
1211 -- | Make a 'CastTy'. The Coercion must be nominal. Checks the
1212 -- Coercion for reflexivity, dropping it if it's reflexive.
1213 -- See Note [Respecting definitional equality] in TyCoRep
1214 mkCastTy :: Type -> Coercion -> Type
1215 mkCastTy ty co | isReflexiveCo co = ty -- (EQ2) from the Note
1216 -- NB: Do the slow check here. This is important to keep the splitXXX
1217 -- functions working properly. Otherwise, we may end up with something
1218 -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
1219 -- fails under splitFunTy_maybe. This happened with the cheaper check
1220 -- in test dependent/should_compile/dynamic-paper.
1221
1222 mkCastTy (CastTy ty co1) co2 = mkCastTy ty (co1 `mkTransCo` co2) -- (EQ3) from the Note
1223 -- call mkCastTy again for the reflexivity check
1224 mkCastTy ty co = CastTy ty co
1225
1226 tyConBindersTyBinders :: [TyConBinder] -> [TyBinder]
1227 -- Return the tyConBinders in TyBinder form
1228 tyConBindersTyBinders = map to_tyb
1229 where
1230 to_tyb (TvBndr tv (NamedTCB vis)) = Named (TvBndr tv vis)
1231 to_tyb (TvBndr tv AnonTCB) = Anon (tyVarKind tv)
1232
1233 {-
1234 --------------------------------------------------------------------
1235 CoercionTy
1236 ~~~~~~~~~~
1237 CoercionTy allows us to inject coercions into types. A CoercionTy
1238 should appear only in the right-hand side of an application.
1239 -}
1240
1241 mkCoercionTy :: Coercion -> Type
1242 mkCoercionTy = CoercionTy
1243
1244 isCoercionTy :: Type -> Bool
1245 isCoercionTy (CoercionTy _) = True
1246 isCoercionTy _ = False
1247
1248 isCoercionTy_maybe :: Type -> Maybe Coercion
1249 isCoercionTy_maybe (CoercionTy co) = Just co
1250 isCoercionTy_maybe _ = Nothing
1251
1252 stripCoercionTy :: Type -> Coercion
1253 stripCoercionTy (CoercionTy co) = co
1254 stripCoercionTy ty = pprPanic "stripCoercionTy" (ppr ty)
1255
1256 {-
1257 ---------------------------------------------------------------------
1258 SynTy
1259 ~~~~~
1260
1261 Notes on type synonyms
1262 ~~~~~~~~~~~~~~~~~~~~~~
1263 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
1264 to return type synonyms wherever possible. Thus
1265
1266 type Foo a = a -> a
1267
1268 we want
1269 splitFunTys (a -> Foo a) = ([a], Foo a)
1270 not ([a], a -> a)
1271
1272 The reason is that we then get better (shorter) type signatures in
1273 interfaces. Notably this plays a role in tcTySigs in TcBinds.hs.
1274
1275
1276 ---------------------------------------------------------------------
1277 ForAllTy
1278 ~~~~~~~~
1279 -}
1280
1281 -- | Make a dependent forall over an Inferred (as opposed to Specified)
1282 -- variable
1283 mkInvForAllTy :: TyVar -> Type -> Type
1284 mkInvForAllTy tv ty = ASSERT( isTyVar tv )
1285 ForAllTy (TvBndr tv Inferred) ty
1286
1287 -- | Like mkForAllTys, but assumes all variables are dependent and Inferred,
1288 -- a common case
1289 mkInvForAllTys :: [TyVar] -> Type -> Type
1290 mkInvForAllTys tvs ty = ASSERT( all isTyVar tvs )
1291 foldr mkInvForAllTy ty tvs
1292
1293 -- | Like mkForAllTys, but assumes all variables are dependent and specified,
1294 -- a common case
1295 mkSpecForAllTys :: [TyVar] -> Type -> Type
1296 mkSpecForAllTys tvs = ASSERT( all isTyVar tvs )
1297 mkForAllTys [ TvBndr tv Specified | tv <- tvs ]
1298
1299 -- | Like mkForAllTys, but assumes all variables are dependent and visible
1300 mkVisForAllTys :: [TyVar] -> Type -> Type
1301 mkVisForAllTys tvs = ASSERT( all isTyVar tvs )
1302 mkForAllTys [ TvBndr tv Required | tv <- tvs ]
1303
1304 mkLamType :: Var -> Type -> Type
1305 -- ^ Makes a @(->)@ type or an implicit forall type, depending
1306 -- on whether it is given a type variable or a term variable.
1307 -- This is used, for example, when producing the type of a lambda.
1308 -- Always uses Inferred binders.
1309 mkLamTypes :: [Var] -> Type -> Type
1310 -- ^ 'mkLamType' for multiple type or value arguments
1311
1312 mkLamType v ty
1313 | isTyVar v = ForAllTy (TvBndr v Inferred) ty
1314 | otherwise = FunTy (varType v) ty
1315
1316 mkLamTypes vs ty = foldr mkLamType ty vs
1317
1318 -- | Given a list of type-level vars and a result kind,
1319 -- makes TyBinders, preferring anonymous binders
1320 -- if the variable is, in fact, not dependent.
1321 -- e.g. mkTyConBindersPreferAnon [(k:*),(b:k),(c:k)] (k->k)
1322 -- We want (k:*) Named, (a;k) Anon, (c:k) Anon
1323 --
1324 -- All binders are /visible/.
1325 mkTyConBindersPreferAnon :: [TyVar] -> Type -> [TyConBinder]
1326 mkTyConBindersPreferAnon vars inner_ty = fst (go vars)
1327 where
1328 go :: [TyVar] -> ([TyConBinder], VarSet) -- also returns the free vars
1329 go [] = ([], tyCoVarsOfType inner_ty)
1330 go (v:vs) | v `elemVarSet` fvs
1331 = ( TvBndr v (NamedTCB Required) : binders
1332 , fvs `delVarSet` v `unionVarSet` kind_vars )
1333 | otherwise
1334 = ( TvBndr v AnonTCB : binders
1335 , fvs `unionVarSet` kind_vars )
1336 where
1337 (binders, fvs) = go vs
1338 kind_vars = tyCoVarsOfType $ tyVarKind v
1339
1340 -- | Take a ForAllTy apart, returning the list of tyvars and the result type.
1341 -- This always succeeds, even if it returns only an empty list. Note that the
1342 -- result type returned may have free variables that were bound by a forall.
1343 splitForAllTys :: Type -> ([TyVar], Type)
1344 splitForAllTys ty = split ty ty []
1345 where
1346 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
1347 split _ (ForAllTy (TvBndr tv _) ty) tvs = split ty ty (tv:tvs)
1348 split orig_ty _ tvs = (reverse tvs, orig_ty)
1349
1350 -- | Like 'splitPiTys' but split off only /named/ binders.
1351 splitForAllTyVarBndrs :: Type -> ([TyVarBinder], Type)
1352 splitForAllTyVarBndrs ty = split ty ty []
1353 where
1354 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1355 split _ (ForAllTy b res) bs = split res res (b:bs)
1356 split orig_ty _ bs = (reverse bs, orig_ty)
1357 {-# INLINE splitForAllTyVarBndrs #-}
1358
1359 -- | Checks whether this is a proper forall (with a named binder)
1360 isForAllTy :: Type -> Bool
1361 isForAllTy ty | Just ty' <- coreView ty = isForAllTy ty'
1362 isForAllTy (ForAllTy {}) = True
1363 isForAllTy _ = False
1364
1365 -- | Is this a function or forall?
1366 isPiTy :: Type -> Bool
1367 isPiTy ty | Just ty' <- coreView ty = isForAllTy ty'
1368 isPiTy (ForAllTy {}) = True
1369 isPiTy (FunTy {}) = True
1370 isPiTy _ = False
1371
1372 -- | Take a forall type apart, or panics if that is not possible.
1373 splitForAllTy :: Type -> (TyVar, Type)
1374 splitForAllTy ty
1375 | Just answer <- splitForAllTy_maybe ty = answer
1376 | otherwise = pprPanic "splitForAllTy" (ppr ty)
1377
1378 -- | Drops all ForAllTys
1379 dropForAlls :: Type -> Type
1380 dropForAlls ty = go ty
1381 where
1382 go ty | Just ty' <- coreView ty = go ty'
1383 go (ForAllTy _ res) = go res
1384 go res = res
1385
1386 -- | Attempts to take a forall type apart, but only if it's a proper forall,
1387 -- with a named binder
1388 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
1389 splitForAllTy_maybe ty = go ty
1390 where
1391 go ty | Just ty' <- coreView ty = go ty'
1392 go (ForAllTy (TvBndr tv _) ty) = Just (tv, ty)
1393 go _ = Nothing
1394
1395 -- | Attempts to take a forall type apart; works with proper foralls and
1396 -- functions
1397 splitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
1398 splitPiTy_maybe ty = go ty
1399 where
1400 go ty | Just ty' <- coreView ty = go ty'
1401 go (ForAllTy bndr ty) = Just (Named bndr, ty)
1402 go (FunTy arg res) = Just (Anon arg, res)
1403 go _ = Nothing
1404
1405 -- | Takes a forall type apart, or panics
1406 splitPiTy :: Type -> (TyBinder, Type)
1407 splitPiTy ty
1408 | Just answer <- splitPiTy_maybe ty = answer
1409 | otherwise = pprPanic "splitPiTy" (ppr ty)
1410
1411 -- | Split off all TyBinders to a type, splitting both proper foralls
1412 -- and functions
1413 splitPiTys :: Type -> ([TyBinder], Type)
1414 splitPiTys ty = split ty ty
1415 where
1416 split orig_ty ty | Just ty' <- coreView ty = split orig_ty ty'
1417 split _ (ForAllTy b res) = let (bs, ty) = split res res
1418 in (Named b : bs, ty)
1419 split _ (FunTy arg res) = let (bs, ty) = split res res
1420 in (Anon arg : bs, ty)
1421 split orig_ty _ = ([], orig_ty)
1422
1423 -- Like splitPiTys, but returns only *invisible* binders, including constraints
1424 -- Stops at the first visible binder
1425 splitPiTysInvisible :: Type -> ([TyBinder], Type)
1426 splitPiTysInvisible ty = split ty ty []
1427 where
1428 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1429 split _ (ForAllTy b@(TvBndr _ vis) res) bs
1430 | isInvisibleArgFlag vis = split res res (Named b : bs)
1431 split _ (FunTy arg res) bs
1432 | isPredTy arg = split res res (Anon arg : bs)
1433 split orig_ty _ bs = (reverse bs, orig_ty)
1434
1435 -- | Given a tycon and its arguments, filters out any invisible arguments
1436 filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
1437 filterOutInvisibleTypes tc tys = snd $ partitionInvisibles tc id tys
1438
1439 -- | Given a tycon and a list of things (which correspond to arguments),
1440 -- partitions the things into
1441 -- Inferred or Specified ones and
1442 -- Required ones
1443 -- The callback function is necessary for this scenario:
1444 --
1445 -- > T :: forall k. k -> k
1446 -- > partitionInvisibles T [forall m. m -> m -> m, S, R, Q]
1447 --
1448 -- After substituting, we get
1449 --
1450 -- > T (forall m. m -> m -> m) :: (forall m. m -> m -> m) -> forall n. n -> n -> n
1451 --
1452 -- Thus, the first argument is invisible, @S@ is visible, @R@ is invisible again,
1453 -- and @Q@ is visible.
1454 --
1455 -- If you're absolutely sure that your tycon's kind doesn't end in a variable,
1456 -- it's OK if the callback function panics, as that's the only time it's
1457 -- consulted.
1458 partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
1459 partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
1460 where
1461 go _ _ [] = ([], [])
1462 go subst (ForAllTy (TvBndr tv vis) res_ki) (x:xs)
1463 | isVisibleArgFlag vis = second (x :) (go subst' res_ki xs)
1464 | otherwise = first (x :) (go subst' res_ki xs)
1465 where
1466 subst' = extendTvSubst subst tv (get_ty x)
1467 go subst (TyVarTy tv) xs
1468 | Just ki <- lookupTyVar subst tv = go subst ki xs
1469 go _ _ xs = ([], xs) -- something is ill-kinded. But this can happen
1470 -- when printing errors. Assume everything is visible.
1471
1472 -- @isTauTy@ tests if a type has no foralls
1473 isTauTy :: Type -> Bool
1474 isTauTy ty | Just ty' <- coreView ty = isTauTy ty'
1475 isTauTy (TyVarTy _) = True
1476 isTauTy (LitTy {}) = True
1477 isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
1478 isTauTy (AppTy a b) = isTauTy a && isTauTy b
1479 isTauTy (FunTy a b) = isTauTy a && isTauTy b
1480 isTauTy (ForAllTy {}) = False
1481 isTauTy (CastTy ty _) = isTauTy ty
1482 isTauTy (CoercionTy _) = False -- Not sure about this
1483
1484 {-
1485 %************************************************************************
1486 %* *
1487 TyBinders
1488 %* *
1489 %************************************************************************
1490 -}
1491
1492 -- | Make an anonymous binder
1493 mkAnonBinder :: Type -> TyBinder
1494 mkAnonBinder = Anon
1495
1496 -- | Does this binder bind a variable that is /not/ erased? Returns
1497 -- 'True' for anonymous binders.
1498 isAnonTyBinder :: TyBinder -> Bool
1499 isAnonTyBinder (Named {}) = False
1500 isAnonTyBinder (Anon {}) = True
1501
1502 isNamedTyBinder :: TyBinder -> Bool
1503 isNamedTyBinder (Named {}) = True
1504 isNamedTyBinder (Anon {}) = False
1505
1506 tyBinderVar_maybe :: TyBinder -> Maybe TyVar
1507 tyBinderVar_maybe (Named tv) = Just $ binderVar tv
1508 tyBinderVar_maybe _ = Nothing
1509
1510 tyBinderType :: TyBinder -> Type
1511 -- Barely used
1512 tyBinderType (Named tvb) = binderKind tvb
1513 tyBinderType (Anon ty) = ty
1514
1515 -- | Extract a relevant type, if there is one.
1516 binderRelevantType_maybe :: TyBinder -> Maybe Type
1517 binderRelevantType_maybe (Named {}) = Nothing
1518 binderRelevantType_maybe (Anon ty) = Just ty
1519
1520 -- | Like 'maybe', but for binders.
1521 caseBinder :: TyBinder -- ^ binder to scrutinize
1522 -> (TyVarBinder -> a) -- ^ named case
1523 -> (Type -> a) -- ^ anonymous case
1524 -> a
1525 caseBinder (Named v) f _ = f v
1526 caseBinder (Anon t) _ d = d t
1527
1528
1529 {-
1530 %************************************************************************
1531 %* *
1532 Pred
1533 * *
1534 ************************************************************************
1535
1536 Predicates on PredType
1537
1538 Note [isPredTy complications]
1539 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1540 You would think that we could define
1541 isPredTy ty = isConstraintKind (typeKind ty)
1542 But there are a number of complications:
1543
1544 * isPredTy is used when printing types, which can happen in debug
1545 printing during type checking of not-fully-zonked types. So it's
1546 not cool to say isConstraintKind (typeKind ty) because, absent
1547 zonking, the type might be ill-kinded, and typeKind crashes. Hence the
1548 rather tiresome story here
1549
1550 * isPredTy must return "True" to *unlifted* coercions, such as (t1 ~# t2)
1551 and (t1 ~R# t2), which are not of kind Constraint! Currently they are
1552 of kind #.
1553
1554 * If we do form the type '(C a => C [a]) => blah', then we'd like to
1555 print it as such. But that means that isPredTy must return True for
1556 (C a => C [a]). Admittedly that type is illegal in Haskell, but we
1557 want to print it nicely in error messages.
1558 -}
1559
1560 -- | Is the type suitable to classify a given/wanted in the typechecker?
1561 isPredTy :: Type -> Bool
1562 -- See Note [isPredTy complications]
1563 isPredTy ty = go ty []
1564 where
1565 go :: Type -> [KindOrType] -> Bool
1566 go (AppTy ty1 ty2) args = go ty1 (ty2 : args)
1567 go (TyVarTy tv) args = go_k (tyVarKind tv) args
1568 go (TyConApp tc tys) args = ASSERT( null args ) -- TyConApp invariant
1569 go_tc tc tys
1570 go (FunTy arg res) []
1571 | isPredTy arg = isPredTy res -- (Eq a => C a)
1572 | otherwise = False -- (Int -> Bool)
1573 go (ForAllTy _ ty) [] = go ty []
1574 go (CastTy _ co) args = go_k (pSnd (coercionKind co)) args
1575 go _ _ = False
1576
1577 go_tc :: TyCon -> [KindOrType] -> Bool
1578 go_tc tc args
1579 | tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1580 = args `lengthIs` 4 -- ~# and ~R# sadly have result kind #
1581 -- not Constraint; but we still want
1582 -- isPredTy to reply True.
1583 | otherwise = go_k (tyConKind tc) args
1584
1585 go_k :: Kind -> [KindOrType] -> Bool
1586 -- True <=> ('k' applied to 'kts') = Constraint
1587 go_k k [] = isConstraintKind k
1588 go_k k (arg:args) = case piResultTy_maybe k arg of
1589 Just k' -> go_k k' args
1590 Nothing -> WARN( True, text "isPredTy" <+> ppr ty )
1591 False
1592 -- This last case shouldn't happen under most circumstances. It can
1593 -- occur if we call isPredTy during kind checking, especially if one
1594 -- of the following happens:
1595 --
1596 -- 1. There is actually a kind error. Example in which this showed up:
1597 -- polykinds/T11399
1598 --
1599 -- 2. A type constructor application appears to be oversaturated. An
1600 -- example of this occurred in GHC Trac #13187:
1601 --
1602 -- {-# LANGUAGE PolyKinds #-}
1603 -- type Const a b = b
1604 -- f :: Const Int (,) Bool Char -> Char
1605 --
1606 -- We call isPredTy (Const k1 k2 Int (,) Bool Char
1607 -- where k1,k2 are unification variables that have been
1608 -- unified to *, and (*->*->*) resp, /but not zonked/.
1609 -- This shows that isPredTy can report a false negative
1610 -- if a constraint is similarly oversaturated, but
1611 -- it's hard to do better than isPredTy currently does without
1612 -- zonking, so we punt on such cases for now. This only happens
1613 -- during debug-printing, so it doesn't matter.
1614
1615 isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool
1616 isClassPred ty = case tyConAppTyCon_maybe ty of
1617 Just tyCon | isClassTyCon tyCon -> True
1618 _ -> False
1619 isEqPred ty = case tyConAppTyCon_maybe ty of
1620 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1621 || tyCon `hasKey` eqReprPrimTyConKey
1622 _ -> False
1623
1624 isNomEqPred ty = case tyConAppTyCon_maybe ty of
1625 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1626 _ -> False
1627
1628 isIPPred ty = case tyConAppTyCon_maybe ty of
1629 Just tc -> isIPTyCon tc
1630 _ -> False
1631
1632 isIPTyCon :: TyCon -> Bool
1633 isIPTyCon tc = tc `hasKey` ipClassKey
1634 -- Class and its corresponding TyCon have the same Unique
1635
1636 isIPClass :: Class -> Bool
1637 isIPClass cls = cls `hasKey` ipClassKey
1638
1639 isCTupleClass :: Class -> Bool
1640 isCTupleClass cls = isTupleTyCon (classTyCon cls)
1641
1642 isIPPred_maybe :: Type -> Maybe (FastString, Type)
1643 isIPPred_maybe ty =
1644 do (tc,[t1,t2]) <- splitTyConApp_maybe ty
1645 guard (isIPTyCon tc)
1646 x <- isStrLitTy t1
1647 return (x,t2)
1648
1649 {-
1650 Make PredTypes
1651
1652 --------------------- Equality types ---------------------------------
1653 -}
1654
1655 -- | Makes a lifted equality predicate at the given role
1656 mkPrimEqPredRole :: Role -> Type -> Type -> PredType
1657 mkPrimEqPredRole Nominal = mkPrimEqPred
1658 mkPrimEqPredRole Representational = mkReprPrimEqPred
1659 mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
1660
1661 -- | Creates a primitive type equality predicate.
1662 -- Invariant: the types are not Coercions
1663 mkPrimEqPred :: Type -> Type -> Type
1664 mkPrimEqPred ty1 ty2
1665 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1666 where
1667 k1 = typeKind ty1
1668 k2 = typeKind ty2
1669
1670 -- | Creates a primite type equality predicate with explicit kinds
1671 mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1672 mkHeteroPrimEqPred k1 k2 ty1 ty2 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1673
1674 -- | Creates a primitive representational type equality predicate
1675 -- with explicit kinds
1676 mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1677 mkHeteroReprPrimEqPred k1 k2 ty1 ty2
1678 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1679
1680 -- | Try to split up a coercion type into the types that it coerces
1681 splitCoercionType_maybe :: Type -> Maybe (Type, Type)
1682 splitCoercionType_maybe ty
1683 = do { (tc, [_, _, ty1, ty2]) <- splitTyConApp_maybe ty
1684 ; guard $ tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1685 ; return (ty1, ty2) }
1686
1687 mkReprPrimEqPred :: Type -> Type -> Type
1688 mkReprPrimEqPred ty1 ty2
1689 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1690 where
1691 k1 = typeKind ty1
1692 k2 = typeKind ty2
1693
1694 equalityTyCon :: Role -> TyCon
1695 equalityTyCon Nominal = eqPrimTyCon
1696 equalityTyCon Representational = eqReprPrimTyCon
1697 equalityTyCon Phantom = eqPhantPrimTyCon
1698
1699 -- --------------------- Dictionary types ---------------------------------
1700
1701 mkClassPred :: Class -> [Type] -> PredType
1702 mkClassPred clas tys = TyConApp (classTyCon clas) tys
1703
1704 isDictTy :: Type -> Bool
1705 isDictTy = isClassPred
1706
1707 isDictLikeTy :: Type -> Bool
1708 -- Note [Dictionary-like types]
1709 isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
1710 isDictLikeTy ty = case splitTyConApp_maybe ty of
1711 Just (tc, tys) | isClassTyCon tc -> True
1712 | isTupleTyCon tc -> all isDictLikeTy tys
1713 _other -> False
1714
1715 {-
1716 Note [Dictionary-like types]
1717 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1718 Being "dictionary-like" means either a dictionary type or a tuple thereof.
1719 In GHC 6.10 we build implication constraints which construct such tuples,
1720 and if we land up with a binding
1721 t :: (C [a], Eq [a])
1722 t = blah
1723 then we want to treat t as cheap under "-fdicts-cheap" for example.
1724 (Implication constraints are normally inlined, but sadly not if the
1725 occurrence is itself inside an INLINE function! Until we revise the
1726 handling of implication constraints, that is.) This turned out to
1727 be important in getting good arities in DPH code. Example:
1728
1729 class C a
1730 class D a where { foo :: a -> a }
1731 instance C a => D (Maybe a) where { foo x = x }
1732
1733 bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
1734 {-# INLINE bar #-}
1735 bar x y = (foo (Just x), foo (Just y))
1736
1737 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
1738 we ended up with something like
1739 bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
1740 in \x,y. <blah>)
1741
1742 This is all a bit ad-hoc; eg it relies on knowing that implication
1743 constraints build tuples.
1744
1745
1746 Decomposing PredType
1747 -}
1748
1749 -- | A choice of equality relation. This is separate from the type 'Role'
1750 -- because 'Phantom' does not define a (non-trivial) equality relation.
1751 data EqRel = NomEq | ReprEq
1752 deriving (Eq, Ord)
1753
1754 instance Outputable EqRel where
1755 ppr NomEq = text "nominal equality"
1756 ppr ReprEq = text "representational equality"
1757
1758 eqRelRole :: EqRel -> Role
1759 eqRelRole NomEq = Nominal
1760 eqRelRole ReprEq = Representational
1761
1762 data PredTree
1763 = ClassPred Class [Type]
1764 | EqPred EqRel Type Type
1765 | IrredPred PredType
1766 | ForAllPred [TyVarBinder] [PredType] PredType
1767 -- ForAllPred: see Note [Quantified constraints] in TcCanonical
1768 -- NB: There is no TuplePred case
1769 -- Tuple predicates like (Eq a, Ord b) are just treated
1770 -- as ClassPred, as if we had a tuple class with two superclasses
1771 -- class (c1, c2) => (%,%) c1 c2
1772
1773 classifyPredType :: PredType -> PredTree
1774 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
1775 Just (tc, [_, _, ty1, ty2])
1776 | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
1777 | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
1778
1779 Just (tc, tys)
1780 | Just clas <- tyConClass_maybe tc
1781 -> ClassPred clas tys
1782
1783 _ | (tvs, rho) <- splitForAllTyVarBndrs ev_ty
1784 , (theta, pred) <- splitFunTys rho
1785 , not (null tvs && null theta)
1786 -> ForAllPred tvs theta pred
1787
1788 | otherwise
1789 -> IrredPred ev_ty
1790
1791 getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type])
1792 getClassPredTys ty = case getClassPredTys_maybe ty of
1793 Just (clas, tys) -> (clas, tys)
1794 Nothing -> pprPanic "getClassPredTys" (ppr ty)
1795
1796 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
1797 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
1798 Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
1799 _ -> Nothing
1800
1801 getEqPredTys :: PredType -> (Type, Type)
1802 getEqPredTys ty
1803 = case splitTyConApp_maybe ty of
1804 Just (tc, [_, _, ty1, ty2])
1805 | tc `hasKey` eqPrimTyConKey
1806 || tc `hasKey` eqReprPrimTyConKey
1807 -> (ty1, ty2)
1808 _ -> pprPanic "getEqPredTys" (ppr ty)
1809
1810 getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
1811 getEqPredTys_maybe ty
1812 = case splitTyConApp_maybe ty of
1813 Just (tc, [_, _, ty1, ty2])
1814 | tc `hasKey` eqPrimTyConKey -> Just (Nominal, ty1, ty2)
1815 | tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2)
1816 _ -> Nothing
1817
1818 getEqPredRole :: PredType -> Role
1819 getEqPredRole ty = eqRelRole (predTypeEqRel ty)
1820
1821 -- | Get the equality relation relevant for a pred type.
1822 predTypeEqRel :: PredType -> EqRel
1823 predTypeEqRel ty
1824 | Just (tc, _) <- splitTyConApp_maybe ty
1825 , tc `hasKey` eqReprPrimTyConKey
1826 = ReprEq
1827 | otherwise
1828 = NomEq
1829
1830 {-
1831 %************************************************************************
1832 %* *
1833 Well-scoped tyvars
1834 * *
1835 ************************************************************************
1836 -}
1837
1838 -- | Do a topological sort on a list of tyvars,
1839 -- so that binders occur before occurrences
1840 -- E.g. given [ a::k, k::*, b::k ]
1841 -- it'll return a well-scoped list [ k::*, a::k, b::k ]
1842 --
1843 -- This is a deterministic sorting operation
1844 -- (that is, doesn't depend on Uniques).
1845 --
1846 -- It is also meant to be stable: that is, variables should not
1847 -- be reordered unnecessarily. The implementation of this
1848 -- has been observed to be stable, though it is not proven to
1849 -- be so. See also Note [Ordering of implicit variables] in HsTypes
1850 toposortTyVars :: [TyCoVar] -> [TyCoVar]
1851 toposortTyVars tvs = reverse $
1852 [ node_payload node | node <- topologicalSortG $
1853 graphFromEdgedVerticesOrd nodes ]
1854 where
1855 var_ids :: VarEnv Int
1856 var_ids = mkVarEnv (zip tvs [1..])
1857
1858 nodes :: [ Node Int TyVar ]
1859 nodes = [ DigraphNode
1860 tv
1861 (lookupVarEnv_NF var_ids tv)
1862 (mapMaybe (lookupVarEnv var_ids)
1863 (tyCoVarsOfTypeList (tyVarKind tv)))
1864 | tv <- tvs ]
1865
1866 -- | Extract a well-scoped list of variables from a deterministic set of
1867 -- variables. The result is deterministic.
1868 -- NB: There used to exist varSetElemsWellScoped :: VarSet -> [Var] which
1869 -- took a non-deterministic set and produced a non-deterministic
1870 -- well-scoped list. If you care about the list being well-scoped you also
1871 -- most likely care about it being in deterministic order.
1872 dVarSetElemsWellScoped :: DVarSet -> [Var]
1873 dVarSetElemsWellScoped = toposortTyVars . dVarSetElems
1874
1875 -- | Get the free vars of a type in scoped order
1876 tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
1877 tyCoVarsOfTypeWellScoped = toposortTyVars . tyCoVarsOfTypeList
1878
1879 -- | Get the free vars of types in scoped order
1880 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
1881 tyCoVarsOfTypesWellScoped = toposortTyVars . tyCoVarsOfTypesList
1882
1883 {-
1884 ************************************************************************
1885 * *
1886 \subsection{Type families}
1887 * *
1888 ************************************************************************
1889 -}
1890
1891 mkFamilyTyConApp :: TyCon -> [Type] -> Type
1892 -- ^ Given a family instance TyCon and its arg types, return the
1893 -- corresponding family type. E.g:
1894 --
1895 -- > data family T a
1896 -- > data instance T (Maybe b) = MkT b
1897 --
1898 -- Where the instance tycon is :RTL, so:
1899 --
1900 -- > mkFamilyTyConApp :RTL Int = T (Maybe Int)
1901 mkFamilyTyConApp tc tys
1902 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
1903 , let tvs = tyConTyVars tc
1904 fam_subst = ASSERT2( tvs `equalLength` tys, ppr tc <+> ppr tys )
1905 zipTvSubst tvs tys
1906 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
1907 | otherwise
1908 = mkTyConApp tc tys
1909
1910 -- | Get the type on the LHS of a coercion induced by a type/data
1911 -- family instance.
1912 coAxNthLHS :: CoAxiom br -> Int -> Type
1913 coAxNthLHS ax ind =
1914 mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind))
1915
1916 -- | Pretty prints a 'TyCon', using the family instance in case of a
1917 -- representation tycon. For example:
1918 --
1919 -- > data T [a] = ...
1920 --
1921 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
1922 pprSourceTyCon :: TyCon -> SDoc
1923 pprSourceTyCon tycon
1924 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
1925 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
1926 | otherwise
1927 = ppr tycon
1928
1929 -- @isTauTy@ tests if a type has no foralls
1930 isFamFreeTy :: Type -> Bool
1931 isFamFreeTy ty | Just ty' <- coreView ty = isFamFreeTy ty'
1932 isFamFreeTy (TyVarTy _) = True
1933 isFamFreeTy (LitTy {}) = True
1934 isFamFreeTy (TyConApp tc tys) = all isFamFreeTy tys && isFamFreeTyCon tc
1935 isFamFreeTy (AppTy a b) = isFamFreeTy a && isFamFreeTy b
1936 isFamFreeTy (FunTy a b) = isFamFreeTy a && isFamFreeTy b
1937 isFamFreeTy (ForAllTy _ ty) = isFamFreeTy ty
1938 isFamFreeTy (CastTy ty _) = isFamFreeTy ty
1939 isFamFreeTy (CoercionTy _) = False -- Not sure about this
1940
1941 {-
1942 ************************************************************************
1943 * *
1944 \subsection{Liftedness}
1945 * *
1946 ************************************************************************
1947 -}
1948
1949 -- | Returns Just True if this type is surely lifted, Just False
1950 -- if it is surely unlifted, Nothing if we can't be sure (i.e., it is
1951 -- levity polymorphic), and panics if the kind does not have the shape
1952 -- TYPE r.
1953 isLiftedType_maybe :: HasDebugCallStack => Type -> Maybe Bool
1954 isLiftedType_maybe ty = go (getRuntimeRep ty)
1955 where
1956 go rr | Just rr' <- coreView rr = go rr'
1957 go (TyConApp lifted_rep [])
1958 | lifted_rep `hasKey` liftedRepDataConKey = Just True
1959 go (TyConApp {}) = Just False -- everything else is unlifted
1960 go _ = Nothing -- levity polymorphic
1961
1962 -- | See "Type#type_classification" for what an unlifted type is.
1963 -- Panics on levity polymorphic types.
1964 isUnliftedType :: HasDebugCallStack => Type -> Bool
1965 -- isUnliftedType returns True for forall'd unlifted types:
1966 -- x :: forall a. Int#
1967 -- I found bindings like these were getting floated to the top level.
1968 -- They are pretty bogus types, mind you. It would be better never to
1969 -- construct them
1970 isUnliftedType ty
1971 = not (isLiftedType_maybe ty `orElse`
1972 pprPanic "isUnliftedType" (ppr ty <+> dcolon <+> ppr (typeKind ty)))
1973
1974 -- | Is this a type of kind RuntimeRep? (e.g. LiftedRep)
1975 isRuntimeRepKindedTy :: Type -> Bool
1976 isRuntimeRepKindedTy = isRuntimeRepTy . typeKind
1977
1978 -- | Drops prefix of RuntimeRep constructors in 'TyConApp's. Useful for e.g.
1979 -- dropping 'LiftedRep arguments of unboxed tuple TyCon applications:
1980 --
1981 -- dropRuntimeRepArgs [ 'LiftedRep, 'IntRep
1982 -- , String, Int# ] == [String, Int#]
1983 --
1984 dropRuntimeRepArgs :: [Type] -> [Type]
1985 dropRuntimeRepArgs = dropWhile isRuntimeRepKindedTy
1986
1987 -- | Extract the RuntimeRep classifier of a type. For instance,
1988 -- @getRuntimeRep_maybe Int = LiftedRep@. Returns 'Nothing' if this is not
1989 -- possible.
1990 getRuntimeRep_maybe :: HasDebugCallStack
1991 => Type -> Maybe Type
1992 getRuntimeRep_maybe = getRuntimeRepFromKind_maybe . typeKind
1993
1994 -- | Extract the RuntimeRep classifier of a type. For instance,
1995 -- @getRuntimeRep_maybe Int = LiftedRep@. Panics if this is not possible.
1996 getRuntimeRep :: HasDebugCallStack => Type -> Type
1997 getRuntimeRep ty
1998 = case getRuntimeRep_maybe ty of
1999 Just r -> r
2000 Nothing -> pprPanic "getRuntimeRep" (ppr ty <+> dcolon <+> ppr (typeKind ty))
2001
2002 -- | Extract the RuntimeRep classifier of a type from its kind. For example,
2003 -- @getRuntimeRepFromKind * = LiftedRep@; Panics if this is not possible.
2004 getRuntimeRepFromKind :: HasDebugCallStack
2005 => Type -> Type
2006 getRuntimeRepFromKind k =
2007 case getRuntimeRepFromKind_maybe k of
2008 Just r -> r
2009 Nothing -> pprPanic "getRuntimeRepFromKind"
2010 (ppr k <+> dcolon <+> ppr (typeKind k))
2011
2012 -- | Extract the RuntimeRep classifier of a type from its kind. For example,
2013 -- @getRuntimeRepFromKind * = LiftedRep@; Returns 'Nothing' if this is not
2014 -- possible.
2015 getRuntimeRepFromKind_maybe :: HasDebugCallStack
2016 => Type -> Maybe Type
2017 getRuntimeRepFromKind_maybe = go
2018 where
2019 go k | Just k' <- coreView k = go k'
2020 go k
2021 | Just (_tc, [arg]) <- splitTyConApp_maybe k
2022 = ASSERT2( _tc `hasKey` tYPETyConKey, ppr k )
2023 Just arg
2024 go _ = Nothing
2025
2026 isUnboxedTupleType :: Type -> Bool
2027 isUnboxedTupleType ty
2028 = tyConAppTyCon (getRuntimeRep ty) `hasKey` tupleRepDataConKey
2029 -- NB: Do not use typePrimRep, as that can't tell the difference between
2030 -- unboxed tuples and unboxed sums
2031
2032
2033 isUnboxedSumType :: Type -> Bool
2034 isUnboxedSumType ty
2035 = tyConAppTyCon (getRuntimeRep ty) `hasKey` sumRepDataConKey
2036
2037 -- | See "Type#type_classification" for what an algebraic type is.
2038 -- Should only be applied to /types/, as opposed to e.g. partially
2039 -- saturated type constructors
2040 isAlgType :: Type -> Bool
2041 isAlgType ty
2042 = case splitTyConApp_maybe ty of
2043 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
2044 isAlgTyCon tc
2045 _other -> False
2046
2047 -- | Check whether a type is a data family type
2048 isDataFamilyAppType :: Type -> Bool
2049 isDataFamilyAppType ty = case tyConAppTyCon_maybe ty of
2050 Just tc -> isDataFamilyTyCon tc
2051 _ -> False
2052
2053 -- | Computes whether an argument (or let right hand side) should
2054 -- be computed strictly or lazily, based only on its type.
2055 -- Currently, it's just 'isUnliftedType'. Panics on levity-polymorphic types.
2056 isStrictType :: HasDebugCallStack => Type -> Bool
2057 isStrictType = isUnliftedType
2058
2059 isPrimitiveType :: Type -> Bool
2060 -- ^ Returns true of types that are opaque to Haskell.
2061 isPrimitiveType ty = case splitTyConApp_maybe ty of
2062 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
2063 isPrimTyCon tc
2064 _ -> False
2065
2066 {-
2067 ************************************************************************
2068 * *
2069 \subsection{Join points}
2070 * *
2071 ************************************************************************
2072 -}
2073
2074 -- | Determine whether a type could be the type of a join point of given total
2075 -- arity, according to the polymorphism rule. A join point cannot be polymorphic
2076 -- in its return type, since given
2077 -- join j @a @b x y z = e1 in e2,
2078 -- the types of e1 and e2 must be the same, and a and b are not in scope for e2.
2079 -- (See Note [The polymorphism rule of join points] in CoreSyn.) Returns False
2080 -- also if the type simply doesn't have enough arguments.
2081 --
2082 -- Note that we need to know how many arguments (type *and* value) the putative
2083 -- join point takes; for instance, if
2084 -- j :: forall a. a -> Int
2085 -- then j could be a binary join point returning an Int, but it could *not* be a
2086 -- unary join point returning a -> Int.
2087 --
2088 -- TODO: See Note [Excess polymorphism and join points]
2089 isValidJoinPointType :: JoinArity -> Type -> Bool
2090 isValidJoinPointType arity ty
2091 = valid_under emptyVarSet arity ty
2092 where
2093 valid_under tvs arity ty
2094 | arity == 0
2095 = isEmptyVarSet (tvs `intersectVarSet` tyCoVarsOfType ty)
2096 | Just (t, ty') <- splitForAllTy_maybe ty
2097 = valid_under (tvs `extendVarSet` t) (arity-1) ty'
2098 | Just (_, res_ty) <- splitFunTy_maybe ty
2099 = valid_under tvs (arity-1) res_ty
2100 | otherwise
2101 = False
2102
2103 {- Note [Excess polymorphism and join points]
2104 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2105 In principle, if a function would be a join point except that it fails
2106 the polymorphism rule (see Note [The polymorphism rule of join points] in
2107 CoreSyn), it can still be made a join point with some effort. This is because
2108 all tail calls must return the same type (they return to the same context!), and
2109 thus if the return type depends on an argument, that argument must always be the
2110 same.
2111
2112 For instance, consider:
2113
2114 let f :: forall a. a -> Char -> [a]
2115 f @a x c = ... f @a y 'a' ...
2116 in ... f @Int 1 'b' ... f @Int 2 'c' ...
2117
2118 (where the calls are tail calls). `f` fails the polymorphism rule because its
2119 return type is [a], where [a] is bound. But since the type argument is always
2120 'Int', we can rewrite it as:
2121
2122 let f' :: Int -> Char -> [Int]
2123 f' x c = ... f' y 'a' ...
2124 in ... f' 1 'b' ... f 2 'c' ...
2125
2126 and now we can make f' a join point:
2127
2128 join f' :: Int -> Char -> [Int]
2129 f' x c = ... jump f' y 'a' ...
2130 in ... jump f' 1 'b' ... jump f' 2 'c' ...
2131
2132 It's not clear that this comes up often, however. TODO: Measure how often and
2133 add this analysis if necessary. See Trac #14620.
2134
2135
2136 ************************************************************************
2137 * *
2138 \subsection{Sequencing on types}
2139 * *
2140 ************************************************************************
2141 -}
2142
2143 seqType :: Type -> ()
2144 seqType (LitTy n) = n `seq` ()
2145 seqType (TyVarTy tv) = tv `seq` ()
2146 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
2147 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
2148 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
2149 seqType (ForAllTy (TvBndr tv _) ty) = seqType (tyVarKind tv) `seq` seqType ty
2150 seqType (CastTy ty co) = seqType ty `seq` seqCo co
2151 seqType (CoercionTy co) = seqCo co
2152
2153 seqTypes :: [Type] -> ()
2154 seqTypes [] = ()
2155 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
2156
2157 {-
2158 ************************************************************************
2159 * *
2160 Comparison for types
2161 (We don't use instances so that we know where it happens)
2162 * *
2163 ************************************************************************
2164
2165 Note [Equality on AppTys]
2166 ~~~~~~~~~~~~~~~~~~~~~~~~~
2167 In our cast-ignoring equality, we want to say that the following two
2168 are equal:
2169
2170 (Maybe |> co) (Int |> co') ~? Maybe Int
2171
2172 But the left is an AppTy while the right is a TyConApp. The solution is
2173 to use repSplitAppTy_maybe to break up the TyConApp into its pieces and
2174 then continue. Easy to do, but also easy to forget to do.
2175
2176 -}
2177
2178 eqType :: Type -> Type -> Bool
2179 -- ^ Type equality on source types. Does not look through @newtypes@ or
2180 -- 'PredType's, but it does look through type synonyms.
2181 -- This first checks that the kinds of the types are equal and then
2182 -- checks whether the types are equal, ignoring casts and coercions.
2183 -- (The kind check is a recursive call, but since all kinds have type
2184 -- @Type@, there is no need to check the types of kinds.)
2185 -- See also Note [Non-trivial definitional equality] in TyCoRep.
2186 eqType t1 t2 = isEqual $ nonDetCmpType t1 t2
2187 -- It's OK to use nonDetCmpType here and eqType is deterministic,
2188 -- nonDetCmpType does equality deterministically
2189
2190 -- | Compare types with respect to a (presumably) non-empty 'RnEnv2'.
2191 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
2192 eqTypeX env t1 t2 = isEqual $ nonDetCmpTypeX env t1 t2
2193 -- It's OK to use nonDetCmpType here and eqTypeX is deterministic,
2194 -- nonDetCmpTypeX does equality deterministically
2195
2196 -- | Type equality on lists of types, looking through type synonyms
2197 -- but not newtypes.
2198 eqTypes :: [Type] -> [Type] -> Bool
2199 eqTypes tys1 tys2 = isEqual $ nonDetCmpTypes tys1 tys2
2200 -- It's OK to use nonDetCmpType here and eqTypes is deterministic,
2201 -- nonDetCmpTypes does equality deterministically
2202
2203 eqVarBndrs :: RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
2204 -- Check that the var lists are the same length
2205 -- and have matching kinds; if so, extend the RnEnv2
2206 -- Returns Nothing if they don't match
2207 eqVarBndrs env [] []
2208 = Just env
2209 eqVarBndrs env (tv1:tvs1) (tv2:tvs2)
2210 | eqTypeX env (tyVarKind tv1) (tyVarKind tv2)
2211 = eqVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
2212 eqVarBndrs _ _ _= Nothing
2213
2214 -- Now here comes the real worker
2215
2216 {-
2217 Note [nonDetCmpType nondeterminism]
2218 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2219 nonDetCmpType is implemented in terms of nonDetCmpTypeX. nonDetCmpTypeX
2220 uses nonDetCmpTc which compares TyCons by their Unique value. Using Uniques for
2221 ordering leads to nondeterminism. We hit the same problem in the TyVarTy case,
2222 comparing type variables is nondeterministic, note the call to nonDetCmpVar in
2223 nonDetCmpTypeX.
2224 See Note [Unique Determinism] for more details.
2225 -}
2226
2227 nonDetCmpType :: Type -> Type -> Ordering
2228 nonDetCmpType t1 t2
2229 -- we know k1 and k2 have the same kind, because they both have kind *.
2230 = nonDetCmpTypeX rn_env t1 t2
2231 where
2232 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes [t1, t2]))
2233
2234 nonDetCmpTypes :: [Type] -> [Type] -> Ordering
2235 nonDetCmpTypes ts1 ts2 = nonDetCmpTypesX rn_env ts1 ts2
2236 where
2237 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes (ts1 ++ ts2)))
2238
2239 -- | An ordering relation between two 'Type's (known below as @t1 :: k1@
2240 -- and @t2 :: k2@)
2241 data TypeOrdering = TLT -- ^ @t1 < t2@
2242 | TEQ -- ^ @t1 ~ t2@ and there are no casts in either,
2243 -- therefore we can conclude @k1 ~ k2@
2244 | TEQX -- ^ @t1 ~ t2@ yet one of the types contains a cast so
2245 -- they may differ in kind.
2246 | TGT -- ^ @t1 > t2@
2247 deriving (Eq, Ord, Enum, Bounded)
2248
2249 nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
2250 -- See Note [Non-trivial definitional equality] in TyCoRep
2251 nonDetCmpTypeX env orig_t1 orig_t2 =
2252 case go env orig_t1 orig_t2 of
2253 -- If there are casts then we also need to do a comparison of the kinds of
2254 -- the types being compared
2255 TEQX -> toOrdering $ go env k1 k2
2256 ty_ordering -> toOrdering ty_ordering
2257 where
2258 k1 = typeKind orig_t1
2259 k2 = typeKind orig_t2
2260
2261 toOrdering :: TypeOrdering -> Ordering
2262 toOrdering TLT = LT
2263 toOrdering TEQ = EQ
2264 toOrdering TEQX = EQ
2265 toOrdering TGT = GT
2266
2267 liftOrdering :: Ordering -> TypeOrdering
2268 liftOrdering LT = TLT
2269 liftOrdering EQ = TEQ
2270 liftOrdering GT = TGT
2271
2272 thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering
2273 thenCmpTy TEQ rel = rel
2274 thenCmpTy TEQX rel = hasCast rel
2275 thenCmpTy rel _ = rel
2276
2277 hasCast :: TypeOrdering -> TypeOrdering
2278 hasCast TEQ = TEQX
2279 hasCast rel = rel
2280
2281 -- Returns both the resulting ordering relation between the two types
2282 -- and whether either contains a cast.
2283 go :: RnEnv2 -> Type -> Type -> TypeOrdering
2284 go env t1 t2
2285 | Just t1' <- coreView t1 = go env t1' t2
2286 | Just t2' <- coreView t2 = go env t1 t2'
2287
2288 go env (TyVarTy tv1) (TyVarTy tv2)
2289 = liftOrdering $ rnOccL env tv1 `nonDetCmpVar` rnOccR env tv2
2290 go env (ForAllTy (TvBndr tv1 _) t1) (ForAllTy (TvBndr tv2 _) t2)
2291 = go env (tyVarKind tv1) (tyVarKind tv2)
2292 `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2
2293 -- See Note [Equality on AppTys]
2294 go env (AppTy s1 t1) ty2
2295 | Just (s2, t2) <- repSplitAppTy_maybe ty2
2296 = go env s1 s2 `thenCmpTy` go env t1 t2
2297 go env ty1 (AppTy s2 t2)
2298 | Just (s1, t1) <- repSplitAppTy_maybe ty1
2299 = go env s1 s2 `thenCmpTy` go env t1 t2
2300 go env (FunTy s1 t1) (FunTy s2 t2)
2301 = go env s1 s2 `thenCmpTy` go env t1 t2
2302 go env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2303 = liftOrdering (tc1 `nonDetCmpTc` tc2) `thenCmpTy` gos env tys1 tys2
2304 go _ (LitTy l1) (LitTy l2) = liftOrdering (compare l1 l2)
2305 go env (CastTy t1 _) t2 = hasCast $ go env t1 t2
2306 go env t1 (CastTy t2 _) = hasCast $ go env t1 t2
2307
2308 go _ (CoercionTy {}) (CoercionTy {}) = TEQ
2309
2310 -- Deal with the rest: TyVarTy < CoercionTy < AppTy < LitTy < TyConApp < ForAllTy
2311 go _ ty1 ty2
2312 = liftOrdering $ (get_rank ty1) `compare` (get_rank ty2)
2313 where get_rank :: Type -> Int
2314 get_rank (CastTy {})
2315 = pprPanic "nonDetCmpTypeX.get_rank" (ppr [ty1,ty2])
2316 get_rank (TyVarTy {}) = 0
2317 get_rank (CoercionTy {}) = 1
2318 get_rank (AppTy {}) = 3
2319 get_rank (LitTy {}) = 4
2320 get_rank (TyConApp {}) = 5
2321 get_rank (FunTy {}) = 6
2322 get_rank (ForAllTy {}) = 7
2323
2324 gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering
2325 gos _ [] [] = TEQ
2326 gos _ [] _ = TLT
2327 gos _ _ [] = TGT
2328 gos env (ty1:tys1) (ty2:tys2) = go env ty1 ty2 `thenCmpTy` gos env tys1 tys2
2329
2330 -------------
2331 nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
2332 nonDetCmpTypesX _ [] [] = EQ
2333 nonDetCmpTypesX env (t1:tys1) (t2:tys2) = nonDetCmpTypeX env t1 t2
2334 `thenCmp`
2335 nonDetCmpTypesX env tys1 tys2
2336 nonDetCmpTypesX _ [] _ = LT
2337 nonDetCmpTypesX _ _ [] = GT
2338
2339 -------------
2340 -- | Compare two 'TyCon's. NB: This should /never/ see 'Constraint' (as
2341 -- recognized by Kind.isConstraintKindCon) which is considered a synonym for
2342 -- 'Type' in Core.
2343 -- See Note [Kind Constraint and kind Type] in Kind.
2344 -- See Note [nonDetCmpType nondeterminism]
2345 nonDetCmpTc :: TyCon -> TyCon -> Ordering
2346 nonDetCmpTc tc1 tc2
2347 = ASSERT( not (isConstraintKindCon tc1) && not (isConstraintKindCon tc2) )
2348 u1 `nonDetCmpUnique` u2
2349 where
2350 u1 = tyConUnique tc1
2351 u2 = tyConUnique tc2
2352
2353 {-
2354 ************************************************************************
2355 * *
2356 The kind of a type
2357 * *
2358 ************************************************************************
2359 -}
2360
2361 typeKind :: HasDebugCallStack => Type -> Kind
2362 typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
2363 typeKind (AppTy fun arg) = typeKind_apps fun [arg]
2364 typeKind (LitTy l) = typeLiteralKind l
2365 typeKind (FunTy {}) = liftedTypeKind
2366 typeKind (TyVarTy tyvar) = tyVarKind tyvar
2367 typeKind (CastTy _ty co) = pSnd $ coercionKind co
2368 typeKind (CoercionTy co) = coercionType co
2369 typeKind ty@(ForAllTy {}) = case occCheckExpand tvs k of
2370 Just k' -> k'
2371 Nothing -> pprPanic "typeKind"
2372 (ppr ty $$ ppr k $$ ppr tvs $$ ppr body)
2373 where
2374 (tvs, body) = splitForAllTys ty
2375 k = typeKind body
2376
2377 typeKind_apps :: HasDebugCallStack => Type -> [Type] -> Kind
2378 -- The sole purpose of the function is to accumulate
2379 -- the type arugments, so we can call piResultTys, rather than
2380 -- a succession of calls to piResultTy (which is asymptotically
2381 -- less efficient as the number of arguments increases)
2382 typeKind_apps (AppTy fun arg) args = typeKind_apps fun (arg:args)
2383 typeKind_apps fun args = piResultTys (typeKind fun) args
2384
2385 --------------------------
2386 typeLiteralKind :: TyLit -> Kind
2387 typeLiteralKind l =
2388 case l of
2389 NumTyLit _ -> typeNatKind
2390 StrTyLit _ -> typeSymbolKind
2391
2392 -- | Returns True if a type is levity polymorphic. Should be the same
2393 -- as (isKindLevPoly . typeKind) but much faster.
2394 -- Precondition: The type has kind (TYPE blah)
2395 isTypeLevPoly :: Type -> Bool
2396 isTypeLevPoly = go
2397 where
2398 go ty@(TyVarTy {}) = check_kind ty
2399 go ty@(AppTy {}) = check_kind ty
2400 go ty@(TyConApp tc _) | not (isTcLevPoly tc) = False
2401 | otherwise = check_kind ty
2402 go (ForAllTy _ ty) = go ty
2403 go (FunTy {}) = False
2404 go (LitTy {}) = False
2405 go ty@(CastTy {}) = check_kind ty
2406 go ty@(CoercionTy {}) = pprPanic "isTypeLevPoly co" (ppr ty)
2407
2408 check_kind = isKindLevPoly . typeKind
2409
2410 -- | Looking past all pi-types, is the end result potentially levity polymorphic?
2411 -- Example: True for (forall r (a :: TYPE r). String -> a)
2412 -- Example: False for (forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). a -> b -> Type)
2413 resultIsLevPoly :: Type -> Bool
2414 resultIsLevPoly = isTypeLevPoly . snd . splitPiTys
2415
2416
2417 {- **********************************************************************
2418 * *
2419 Occurs check expansion
2420 %* *
2421 %********************************************************************* -}
2422
2423 {- Note [Occurs check expansion]
2424 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2425 (occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
2426 of occurrences of tv outside type function arguments, if that is
2427 possible; otherwise, it returns Nothing.
2428
2429 For example, suppose we have
2430 type F a b = [a]
2431 Then
2432 occCheckExpand b (F Int b) = Just [Int]
2433 but
2434 occCheckExpand a (F a Int) = Nothing
2435
2436 We don't promise to do the absolute minimum amount of expanding
2437 necessary, but we try not to do expansions we don't need to. We
2438 prefer doing inner expansions first. For example,
2439 type F a b = (a, Int, a, [a])
2440 type G b = Char
2441 We have
2442 occCheckExpand b (F (G b)) = Just (F Char)
2443 even though we could also expand F to get rid of b.
2444 -}
2445
2446 occCheckExpand :: [Var] -> Type -> Maybe Type
2447 -- See Note [Occurs check expansion]
2448 -- We may have needed to do some type synonym unfolding in order to
2449 -- get rid of the variable (or forall), so we also return the unfolded
2450 -- version of the type, which is guaranteed to be syntactically free
2451 -- of the given type variable. If the type is already syntactically
2452 -- free of the variable, then the same type is returned.
2453 occCheckExpand vs_to_avoid ty
2454 = go (mkVarSet vs_to_avoid, emptyVarEnv) ty
2455 where
2456 go :: (VarSet, VarEnv TyVar) -> Type -> Maybe Type
2457 -- The VarSet is the set of variables we are trying to avoid
2458 -- The VarEnv carries mappings necessary
2459 -- because of kind expansion
2460 go cxt@(as, env) (TyVarTy tv')
2461 | tv' `elemVarSet` as = Nothing
2462 | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
2463 | otherwise = do { tv'' <- go_var cxt tv'
2464 ; return (mkTyVarTy tv'') }
2465
2466 go _ ty@(LitTy {}) = return ty
2467 go cxt (AppTy ty1 ty2) = do { ty1' <- go cxt ty1
2468 ; ty2' <- go cxt ty2
2469 ; return (mkAppTy ty1' ty2') }
2470 go cxt (FunTy ty1 ty2) = do { ty1' <- go cxt ty1
2471 ; ty2' <- go cxt ty2
2472 ; return (mkFunTy ty1' ty2') }
2473 go cxt@(as, env) (ForAllTy (TvBndr tv vis) body_ty)
2474 = do { ki' <- go cxt (tyVarKind tv)
2475 ; let tv' = setTyVarKind tv ki'
2476 env' = extendVarEnv env tv tv'
2477 as' = as `delVarSet` tv
2478 ; body' <- go (as', env') body_ty
2479 ; return (ForAllTy (TvBndr tv' vis) body') }
2480
2481 -- For a type constructor application, first try expanding away the
2482 -- offending variable from the arguments. If that doesn't work, next
2483 -- see if the type constructor is a type synonym, and if so, expand
2484 -- it and try again.
2485 go cxt ty@(TyConApp tc tys)
2486 = case mapM (go cxt) tys of
2487 Just tys' -> return (mkTyConApp tc tys')
2488 Nothing | Just ty' <- tcView ty -> go cxt ty'
2489 | otherwise -> Nothing
2490 -- Failing that, try to expand a synonym
2491
2492 go cxt (CastTy ty co) = do { ty' <- go cxt ty
2493 ; co' <- go_co cxt co
2494 ; return (mkCastTy ty' co') }
2495 go cxt (CoercionTy co) = do { co' <- go_co cxt co
2496 ; return (mkCoercionTy co') }
2497
2498 ------------------
2499 go_var cxt v = do { k' <- go cxt (varType v)
2500 ; return (setVarType v k') }
2501 -- Works for TyVar and CoVar
2502 -- See Note [Occurrence checking: look inside kinds]
2503
2504 ------------------
2505 go_mco _ MRefl = return MRefl
2506 go_mco ctx (MCo co) = MCo <$> go_co ctx co
2507
2508 ------------------
2509 go_co cxt (Refl ty) = do { ty' <- go cxt ty
2510 ; return (mkNomReflCo ty') }
2511 go_co cxt (GRefl r ty mco) = do { mco' <- go_mco cxt mco
2512 ; ty' <- go cxt ty
2513 ; return (mkGReflCo r ty' mco') }
2514 -- Note: Coercions do not contain type synonyms
2515 go_co cxt (TyConAppCo r tc args) = do { args' <- mapM (go_co cxt) args
2516 ; return (mkTyConAppCo r tc args') }
2517 go_co cxt (AppCo co arg) = do { co' <- go_co cxt co
2518 ; arg' <- go_co cxt arg
2519 ; return (mkAppCo co' arg') }
2520 go_co cxt@(as, env) (ForAllCo tv kind_co body_co)
2521 = do { kind_co' <- go_co cxt kind_co
2522 ; let tv' = setTyVarKind tv $
2523 pFst (coercionKind kind_co')
2524 env' = extendVarEnv env tv tv'
2525 as' = as `delVarSet` tv
2526 ; body' <- go_co (as', env') body_co
2527 ; return (ForAllCo tv' kind_co' body') }
2528 go_co cxt (FunCo r co1 co2) = do { co1' <- go_co cxt co1
2529 ; co2' <- go_co cxt co2
2530 ; return (mkFunCo r co1' co2') }
2531 go_co cxt (CoVarCo c) = do { c' <- go_var cxt c
2532 ; return (mkCoVarCo c') }
2533 go_co cxt (HoleCo h) = do { c' <- go_var cxt (ch_co_var h)
2534 ; return (HoleCo (h { ch_co_var = c' })) }
2535 go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args
2536 ; return (mkAxiomInstCo ax ind args') }
2537 go_co cxt (UnivCo p r ty1 ty2) = do { p' <- go_prov cxt p
2538 ; ty1' <- go cxt ty1
2539 ; ty2' <- go cxt ty2
2540 ; return (mkUnivCo p' r ty1' ty2') }
2541 go_co cxt (SymCo co) = do { co' <- go_co cxt co
2542 ; return (mkSymCo co') }
2543 go_co cxt (TransCo co1 co2) = do { co1' <- go_co cxt co1
2544 ; co2' <- go_co cxt co2
2545 ; return (mkTransCo co1' co2') }
2546 go_co cxt (NthCo r n co) = do { co' <- go_co cxt co
2547 ; return (mkNthCo r n co') }
2548 go_co cxt (LRCo lr co) = do { co' <- go_co cxt co
2549 ; return (mkLRCo lr co') }
2550 go_co cxt (InstCo co arg) = do { co' <- go_co cxt co
2551 ; arg' <- go_co cxt arg
2552 ; return (mkInstCo co' arg') }
2553 go_co cxt (KindCo co) = do { co' <- go_co cxt co
2554 ; return (mkKindCo co') }
2555 go_co cxt (SubCo co) = do { co' <- go_co cxt co
2556 ; return (mkSubCo co') }
2557 go_co cxt (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co cxt) cs
2558 ; return (mkAxiomRuleCo ax cs') }
2559
2560 ------------------
2561 go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv
2562 go_prov cxt (PhantomProv co) = PhantomProv <$> go_co cxt co
2563 go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
2564 go_prov _ p@(PluginProv _) = return p
2565
2566
2567 {-
2568 %************************************************************************
2569 %* *
2570 Miscellaneous functions
2571 %* *
2572 %************************************************************************
2573
2574 -}
2575 -- | All type constructors occurring in the type; looking through type
2576 -- synonyms, but not newtypes.
2577 -- When it finds a Class, it returns the class TyCon.
2578 tyConsOfType :: Type -> UniqSet TyCon
2579 tyConsOfType ty
2580 = go ty
2581 where
2582 go :: Type -> UniqSet TyCon -- The UniqSet does duplicate elim
2583 go ty | Just ty' <- coreView ty = go ty'
2584 go (TyVarTy {}) = emptyUniqSet
2585 go (LitTy {}) = emptyUniqSet
2586 go (TyConApp tc tys) = go_tc tc `unionUniqSets` go_s tys
2587 go (AppTy a b) = go a `unionUniqSets` go b
2588 go (FunTy a b) = go a `unionUniqSets` go b `unionUniqSets` go_tc funTyCon
2589 go (ForAllTy (TvBndr tv _) ty) = go ty `unionUniqSets` go (tyVarKind tv)
2590 go (CastTy ty co) = go ty `unionUniqSets` go_co co
2591 go (CoercionTy co) = go_co co
2592
2593 go_co (Refl ty) = go ty
2594 go_co (GRefl _ ty mco) = go ty `unionUniqSets` go_mco mco
2595 go_co (TyConAppCo _ tc args) = go_tc tc `unionUniqSets` go_cos args
2596 go_co (AppCo co arg) = go_co co `unionUniqSets` go_co arg
2597 go_co (ForAllCo _ kind_co co) = go_co kind_co `unionUniqSets` go_co co
2598 go_co (FunCo _ co1 co2) = go_co co1 `unionUniqSets` go_co co2
2599 go_co (AxiomInstCo ax _ args) = go_ax ax `unionUniqSets` go_cos args
2600 go_co (UnivCo p _ t1 t2) = go_prov p `unionUniqSets` go t1 `unionUniqSets` go t2
2601 go_co (CoVarCo {}) = emptyUniqSet
2602 go_co (HoleCo {}) = emptyUniqSet
2603 go_co (SymCo co) = go_co co
2604 go_co (TransCo co1 co2) = go_co co1 `unionUniqSets` go_co co2
2605 go_co (NthCo _ _ co) = go_co co
2606 go_co (LRCo _ co) = go_co co
2607 go_co (InstCo co arg) = go_co co `unionUniqSets` go_co arg
2608 go_co (KindCo co) = go_co co
2609 go_co (SubCo co) = go_co co
2610 go_co (AxiomRuleCo _ cs) = go_cos cs
2611
2612 go_mco MRefl = emptyUniqSet
2613 go_mco (MCo co) = go_co co
2614
2615 go_prov UnsafeCoerceProv = emptyUniqSet
2616 go_prov (PhantomProv co) = go_co co
2617 go_prov (ProofIrrelProv co) = go_co co
2618 go_prov (PluginProv _) = emptyUniqSet
2619 -- this last case can happen from the tyConsOfType used from
2620 -- checkTauTvUpdate
2621
2622 go_s tys = foldr (unionUniqSets . go) emptyUniqSet tys
2623 go_cos cos = foldr (unionUniqSets . go_co) emptyUniqSet cos
2624
2625 go_tc tc = unitUniqSet tc
2626 go_ax ax = go_tc $ coAxiomTyCon ax
2627
2628 -- | Find the result 'Kind' of a type synonym,
2629 -- after applying it to its 'arity' number of type variables
2630 -- Actually this function works fine on data types too,
2631 -- but they'd always return '*', so we never need to ask
2632 synTyConResKind :: TyCon -> Kind
2633 synTyConResKind tycon = piResultTys (tyConKind tycon) (mkTyVarTys (tyConTyVars tycon))
2634
2635 -- | Retrieve the free variables in this type, splitting them based
2636 -- on whether they are used visibly or invisibly. Invisible ones come
2637 -- first.
2638 splitVisVarsOfType :: Type -> Pair TyCoVarSet
2639 splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
2640 where
2641 Pair invis_vars1 vis_vars = go orig_ty
2642 invis_vars = invis_vars1 `minusVarSet` vis_vars
2643
2644 go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv)
2645 go (AppTy t1 t2) = go t1 `mappend` go t2
2646 go (TyConApp tc tys) = go_tc tc tys
2647 go (FunTy t1 t2) = go t1 `mappend` go t2
2648 go (ForAllTy (TvBndr tv _) ty)
2649 = ((`delVarSet` tv) <$> go ty) `mappend`
2650 (invisible (tyCoVarsOfType $ tyVarKind tv))
2651 go (LitTy {}) = mempty
2652 go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co)
2653 go (CoercionTy co) = invisible $ tyCoVarsOfCo co
2654
2655 invisible vs = Pair vs emptyVarSet
2656
2657 go_tc tc tys = let (invis, vis) = partitionInvisibles tc id tys in
2658 invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis
2659
2660 splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
2661 splitVisVarsOfTypes = foldMap splitVisVarsOfType
2662
2663 modifyJoinResTy :: Int -- Number of binders to skip
2664 -> (Type -> Type) -- Function to apply to result type
2665 -> Type -- Type of join point
2666 -> Type -- New type
2667 -- INVARIANT: If any of the first n binders are foralls, those tyvars cannot
2668 -- appear in the original result type. See isValidJoinPointType.
2669 modifyJoinResTy orig_ar f orig_ty
2670 = go orig_ar orig_ty
2671 where
2672 go 0 ty = f ty
2673 go n ty | Just (arg_bndr, res_ty) <- splitPiTy_maybe ty
2674 = mkPiTy arg_bndr (go (n-1) res_ty)
2675 | otherwise
2676 = pprPanic "modifyJoinResTy" (ppr orig_ar <+> ppr orig_ty)
2677
2678 setJoinResTy :: Int -- Number of binders to skip
2679 -> Type -- New result type
2680 -> Type -- Type of join point
2681 -> Type -- New type
2682 -- INVARIANT: Same as for modifyJoinResTy
2683 setJoinResTy ar new_res_ty ty
2684 = modifyJoinResTy ar (const new_res_ty) ty
2685
2686 {-
2687 %************************************************************************
2688 %* *
2689 Pretty-printing
2690 %* *
2691 %************************************************************************
2692
2693 Most pretty-printing is either in TyCoRep or IfaceType.
2694
2695 -}
2696
2697 -- | This variant preserves any use of TYPE in a type, effectively
2698 -- locally setting -fprint-explicit-runtime-reps.
2699 pprWithTYPE :: Type -> SDoc
2700 pprWithTYPE ty = updSDocDynFlags (flip gopt_set Opt_PrintExplicitRuntimeReps) $
2701 ppr ty