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