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