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