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