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