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