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