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