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