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