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