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