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