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