s/Invisible/Inferred/g s/Visible/Required/g
[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 #-}
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, TyBinder, TyVarBinder,
19
20 -- ** Constructing and deconstructing types
21 mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, repGetTyVar_maybe,
22 getCastedTyVar_maybe, tyVarKind,
23
24 mkAppTy, mkAppTys, splitAppTy, splitAppTys, repSplitAppTys,
25 splitAppTy_maybe, repSplitAppTy_maybe, tcRepSplitAppTy_maybe,
26
27 mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
28 splitFunTys, funResultTy, funArgTy,
29
30 mkTyConApp, mkTyConTy,
31 tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
32 tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
33 splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
34 splitListTyConApp_maybe,
35 repSplitTyConApp_maybe,
36
37 mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys,
38 mkVisForAllTys, mkInvForAllTy,
39 splitForAllTys, splitForAllTyVarBndrs,
40 splitForAllTy_maybe, splitForAllTy,
41 splitPiTy_maybe, splitPiTy, splitPiTys,
42 mkPiTy, mkPiTys, mkTyConBindersPreferAnon,
43 mkLamType, mkLamTypes,
44 piResultTy, piResultTys,
45 applyTysX, dropForAlls,
46
47 mkNumLitTy, isNumLitTy,
48 mkStrLitTy, isStrLitTy,
49
50 mkCastTy, mkCoercionTy, splitCastTy_maybe,
51
52 userTypeError_maybe, pprUserTypeErrorTy,
53
54 coAxNthLHS,
55 stripCoercionTy, splitCoercionType_maybe,
56
57 splitPiTysInvisible, filterOutInvisibleTypes,
58 filterOutInvisibleTyVars, partitionInvisibles,
59 synTyConResKind,
60
61 -- Analyzing types
62 TyCoMapper(..), mapType, mapCoercion,
63
64 -- (Newtypes)
65 newTyConInstRhs,
66
67 -- Pred types
68 mkFamilyTyConApp,
69 isDictLikeTy,
70 mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
71 equalityTyCon,
72 mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
73 mkClassPred,
74 isClassPred, isEqPred, isNomEqPred,
75 isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
76 isCTupleClass,
77
78 -- Deconstructing predicate types
79 PredTree(..), EqRel(..), eqRelRole, classifyPredType,
80 getClassPredTys, getClassPredTys_maybe,
81 getEqPredTys, getEqPredTys_maybe, getEqPredRole,
82 predTypeEqRel,
83
84 -- ** Binders
85 sameVis,
86 mkTyVarBinder, mkTyVarBinders,
87 mkAnonBinder,
88 isAnonTyBinder, isNamedTyBinder,
89 binderVar, binderVars, binderKind, binderArgFlag,
90 tyBinderType,
91 binderRelevantType_maybe, caseBinder,
92 isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder, isInvisibleBinder,
93 tyConBindersTyBinders,
94
95 -- ** Common type constructors
96 funTyCon,
97
98 -- ** Predicates on types
99 isTyVarTy, isFunTy, isDictTy, isPredTy, isVoidTy, isCoercionTy,
100 isCoercionTy_maybe, isCoercionType, isForAllTy,
101 isPiTy,
102
103 -- (Lifting and boxity)
104 isUnliftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
105 isPrimitiveType, isStrictType,
106 isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
107 dropRuntimeRepArgs,
108 getRuntimeRep, getRuntimeRepFromKind,
109
110 -- * Main data types representing Kinds
111 Kind,
112
113 -- ** Finding the kind of a type
114 typeKind,
115
116 -- ** Common Kind
117 liftedTypeKind,
118
119 -- * Type free variables
120 tyCoFVsOfType, tyCoFVsBndr,
121 tyCoVarsOfType, tyCoVarsOfTypes,
122 tyCoVarsOfTypeDSet,
123 coVarsOfType,
124 coVarsOfTypes, closeOverKinds, closeOverKindsList,
125 splitVisVarsOfType, splitVisVarsOfTypes,
126 expandTypeSynonyms,
127 typeSize,
128
129 -- * Well-scoped lists of variables
130 dVarSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped,
131 tyCoVarsOfTypesWellScoped,
132
133 -- * Type comparison
134 eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX,
135 nonDetCmpTypesX, nonDetCmpTc,
136 eqVarBndrs,
137
138 -- * Forcing evaluation of types
139 seqType, seqTypes,
140
141 -- * Other views onto Types
142 coreView, coreViewOneStarKind,
143
144 UnaryType, RepType(..), flattenRepType, repType,
145 tyConsOfType,
146
147 -- * Type representation for the code generator
148 typePrimRep, typeRepArity, tyConPrimRep,
149
150 -- * Main type substitution data types
151 TvSubstEnv, -- Representation widely visible
152 TCvSubst(..), -- Representation visible to a few friends
153
154 -- ** Manipulating type substitutions
155 emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
156
157 mkTCvSubst, zipTvSubst, mkTvSubstPrs,
158 notElemTCvSubst,
159 getTvSubstEnv, setTvSubstEnv,
160 zapTCvSubst, getTCvInScope, getTCvSubstRangeFVs,
161 extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
162 extendTCvSubst, extendCvSubst,
163 extendTvSubst, extendTvSubstList, extendTvSubstAndInScope,
164 extendTvSubstWithClone,
165 isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv,
166 isEmptyTCvSubst, unionTCvSubst,
167
168 -- ** Performing substitution on types and kinds
169 substTy, substTys, substTyWith, substTysWith, substTheta,
170 substTyAddInScope,
171 substTyUnchecked, substTysUnchecked, substThetaUnchecked,
172 substTyWithUnchecked,
173 substCoUnchecked, substCoWithUnchecked,
174 substTyVarBndr, substTyVar, substTyVars,
175 cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
176
177 -- * Pretty-printing
178 pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprShortTyThing,
179 pprTvBndr, pprTvBndrs, pprForAll, pprForAllImplicit, pprUserForAll,
180 pprSigmaType, ppSuggestExplicitKinds,
181 pprTheta, pprThetaArrowTy, pprClassPred,
182 pprKind, pprParendKind, pprSourceTyCon,
183 TyPrec(..), maybeParen,
184 pprTyVar, pprTcAppTy, pprPrefixApp, pprArrowChain,
185
186 -- * Tidying type related things up for printing
187 tidyType, tidyTypes,
188 tidyOpenType, tidyOpenTypes,
189 tidyOpenKind,
190 tidyTyCoVarBndr, tidyTyCoVarBndrs, tidyFreeTyCoVars,
191 tidyOpenTyCoVar, tidyOpenTyCoVars,
192 tidyTyVarOcc,
193 tidyTopType,
194 tidyKind,
195 tidyTyVarBinder, tidyTyVarBinders
196 ) where
197
198 #include "HsVersions.h"
199
200 -- We import the representation and primitive functions from TyCoRep.
201 -- Many things are reexported, but not the representation!
202
203 import Kind
204 import TyCoRep
205
206 -- friends:
207 import Var
208 import VarEnv
209 import VarSet
210 import NameEnv
211
212 import Class
213 import TyCon
214 import TysPrim
215 import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind
216 , typeSymbolKind, liftedTypeKind )
217 import PrelNames
218 import CoAxiom
219 import {-# SOURCE #-} Coercion
220
221 -- others
222 import BasicTypes ( Arity, RepArity )
223 import Util
224 import Outputable
225 import FastString
226 import Pair
227 import ListSetOps
228 import Digraph
229 import Unique ( nonDetCmpUnique )
230
231 import Maybes ( orElse )
232 import Data.Maybe ( isJust, mapMaybe )
233 import Control.Monad ( guard )
234 import Control.Arrow ( first, second )
235
236 -- $type_classification
237 -- #type_classification#
238 --
239 -- Types are one of:
240 --
241 -- [Unboxed] Iff its representation is other than a pointer
242 -- Unboxed types are also unlifted.
243 --
244 -- [Lifted] Iff it has bottom as an element.
245 -- Closures always have lifted types: i.e. any
246 -- let-bound identifier in Core must have a lifted
247 -- type. Operationally, a lifted object is one that
248 -- can be entered.
249 -- Only lifted types may be unified with a type variable.
250 --
251 -- [Algebraic] Iff it is a type with one or more constructors, whether
252 -- declared with @data@ or @newtype@.
253 -- An algebraic type is one that can be deconstructed
254 -- with a case expression. This is /not/ the same as
255 -- lifted types, because we also include unboxed
256 -- tuples in this classification.
257 --
258 -- [Data] Iff it is a type declared with @data@, or a boxed tuple.
259 --
260 -- [Primitive] Iff it is a built-in type that can't be expressed in Haskell.
261 --
262 -- Currently, all primitive types are unlifted, but that's not necessarily
263 -- the case: for example, @Int@ could be primitive.
264 --
265 -- Some primitive types are unboxed, such as @Int#@, whereas some are boxed
266 -- but unlifted (such as @ByteArray#@). The only primitive types that we
267 -- classify as algebraic are the unboxed tuples.
268 --
269 -- Some examples of type classifications that may make this a bit clearer are:
270 --
271 -- @
272 -- Type primitive boxed lifted algebraic
273 -- -----------------------------------------------------------------------------
274 -- Int# Yes No No No
275 -- ByteArray# Yes Yes No No
276 -- (\# a, b \#) Yes No No Yes
277 -- ( a, b ) No Yes Yes Yes
278 -- [a] No Yes Yes Yes
279 -- @
280
281 -- $representation_types
282 -- A /source type/ is a type that is a separate type as far as the type checker is
283 -- concerned, but which has a more low-level representation as far as Core-to-Core
284 -- passes and the rest of the back end is concerned.
285 --
286 -- You don't normally have to worry about this, as the utility functions in
287 -- this module will automatically convert a source into a representation type
288 -- if they are spotted, to the best of it's abilities. If you don't want this
289 -- to happen, use the equivalent functions from the "TcType" module.
290
291 {-
292 ************************************************************************
293 * *
294 Type representation
295 * *
296 ************************************************************************
297 -}
298
299 {-# INLINE coreView #-}
300 coreView :: Type -> Maybe Type
301 -- ^ This function Strips off the /top layer only/ of a type synonym
302 -- application (if any) its underlying representation type.
303 -- Returns Nothing if there is nothing to look through.
304 --
305 -- By being non-recursive and inlined, this case analysis gets efficiently
306 -- joined onto the case analysis that the caller is already doing
307 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
308 = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
309 -- The free vars of 'rhs' should all be bound by 'tenv', so it's
310 -- ok to use 'substTy' here.
311 -- See also Note [The substitution invariant] in TyCoRep.
312 -- Its important to use mkAppTys, rather than (foldl AppTy),
313 -- because the function part might well return a
314 -- partially-applied type constructor; indeed, usually will!
315 coreView _ = Nothing
316
317 -- | Like 'coreView', but it also "expands" @Constraint@ to become
318 -- @TYPE PtrRepLifted@.
319 {-# INLINE coreViewOneStarKind #-}
320 coreViewOneStarKind :: Type -> Maybe Type
321 coreViewOneStarKind ty
322 | Just ty' <- coreView ty = Just ty'
323 | TyConApp tc [] <- ty
324 , isStarKindSynonymTyCon tc = Just liftedTypeKind
325 | otherwise = Nothing
326
327 -----------------------------------------------
328 expandTypeSynonyms :: Type -> Type
329 -- ^ Expand out all type synonyms. Actually, it'd suffice to expand out
330 -- just the ones that discard type variables (e.g. type Funny a = Int)
331 -- But we don't know which those are currently, so we just expand all.
332 --
333 -- 'expandTypeSynonyms' only expands out type synonyms mentioned in the type,
334 -- not in the kinds of any TyCon or TyVar mentioned in the type.
335 expandTypeSynonyms ty
336 = go (mkEmptyTCvSubst in_scope) ty
337 where
338 in_scope = mkInScopeSet (tyCoVarsOfType ty)
339
340 go subst (TyConApp tc tys)
341 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc expanded_tys
342 = let subst' = mkTvSubst in_scope (mkVarEnv tenv)
343 -- Make a fresh substitution; rhs has nothing to
344 -- do with anything that has happened so far
345 -- NB: if you make changes here, be sure to build an
346 -- /idempotent/ substitution, even in the nested case
347 -- type T a b = a -> b
348 -- type S x y = T y x
349 -- (Trac #11665)
350 in mkAppTys (go subst' rhs) tys'
351 | otherwise
352 = TyConApp tc expanded_tys
353 where
354 expanded_tys = (map (go subst) tys)
355
356 go _ (LitTy l) = LitTy l
357 go subst (TyVarTy tv) = substTyVar subst tv
358 go subst (AppTy t1 t2) = mkAppTy (go subst t1) (go subst t2)
359 go subst (FunTy arg res)
360 = mkFunTy (go subst arg) (go subst res)
361 go subst (ForAllTy (TvBndr tv vis) t)
362 = let (subst', tv') = substTyVarBndrCallback go subst tv in
363 ForAllTy (TvBndr tv' vis) (go subst' t)
364 go subst (CastTy ty co) = mkCastTy (go subst ty) (go_co subst co)
365 go subst (CoercionTy co) = mkCoercionTy (go_co subst co)
366
367 go_co subst (Refl r ty)
368 = mkReflCo r (go subst ty)
369 -- NB: coercions are always expanded upon creation
370 go_co subst (TyConAppCo r tc args)
371 = mkTyConAppCo r tc (map (go_co subst) args)
372 go_co subst (AppCo co arg)
373 = mkAppCo (go_co subst co) (go_co subst arg)
374 go_co subst (ForAllCo tv kind_co co)
375 = let (subst', tv', kind_co') = go_cobndr subst tv kind_co in
376 mkForAllCo tv' kind_co' (go_co subst' co)
377 go_co subst (CoVarCo cv)
378 = substCoVar subst cv
379 go_co subst (AxiomInstCo ax ind args)
380 = mkAxiomInstCo ax ind (map (go_co subst) args)
381 go_co subst (UnivCo p r t1 t2)
382 = mkUnivCo (go_prov subst p) r (go subst t1) (go subst t2)
383 go_co subst (SymCo co)
384 = mkSymCo (go_co subst co)
385 go_co subst (TransCo co1 co2)
386 = mkTransCo (go_co subst co1) (go_co subst co2)
387 go_co subst (NthCo n co)
388 = mkNthCo n (go_co subst co)
389 go_co subst (LRCo lr co)
390 = mkLRCo lr (go_co subst co)
391 go_co subst (InstCo co arg)
392 = mkInstCo (go_co subst co) (go_co subst arg)
393 go_co subst (CoherenceCo co1 co2)
394 = mkCoherenceCo (go_co subst co1) (go_co subst co2)
395 go_co subst (KindCo co)
396 = mkKindCo (go_co subst co)
397 go_co subst (SubCo co)
398 = mkSubCo (go_co subst co)
399 go_co subst (AxiomRuleCo ax cs) = AxiomRuleCo ax (map (go_co subst) cs)
400
401 go_prov _ UnsafeCoerceProv = UnsafeCoerceProv
402 go_prov subst (PhantomProv co) = PhantomProv (go_co subst co)
403 go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
404 go_prov _ p@(PluginProv _) = p
405 go_prov _ (HoleProv h) = pprPanic "expandTypeSynonyms hit a hole" (ppr h)
406
407 -- the "False" and "const" are to accommodate the type of
408 -- substForAllCoBndrCallback, which is general enough to
409 -- handle coercion optimization (which sometimes swaps the
410 -- order of a coercion)
411 go_cobndr subst = substForAllCoBndrCallback False (go_co subst) subst
412
413 {-
414 ************************************************************************
415 * *
416 Analyzing types
417 * *
418 ************************************************************************
419
420 These functions do a map-like operation over types, performing some operation
421 on all variables and binding sites. Primarily used for zonking.
422
423 Note [Efficiency for mapCoercion ForAllCo case]
424 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
425 As noted in Note [Forall coercions] in TyCoRep, a ForAllCo is a bit redundant.
426 It stores a TyVar and a Coercion, where the kind of the TyVar always matches
427 the left-hand kind of the coercion. This is convenient lots of the time, but
428 not when mapping a function over a coercion.
429
430 The problem is that tcm_tybinder will affect the TyVar's kind and
431 mapCoercion will affect the Coercion, and we hope that the results will be
432 the same. Even if they are the same (which should generally happen with
433 correct algorithms), then there is an efficiency issue. In particular,
434 this problem seems to make what should be a linear algorithm into a potentially
435 exponential one. But it's only going to be bad in the case where there's
436 lots of foralls in the kinds of other foralls. Like this:
437
438 forall a : (forall b : (forall c : ...). ...). ...
439
440 This construction seems unlikely. So we'll do the inefficient, easy way
441 for now.
442
443 Note [Specialising mappers]
444 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
445 These INLINABLE pragmas are indispensable. mapType/mapCoercion are used
446 to implement zonking, and it's vital that they get specialised to the TcM
447 monad. This specialisation happens automatically (that is, without a
448 SPECIALISE pragma) as long as the definitions are INLINABLE. For example,
449 this one change made a 20% allocation difference in perf/compiler/T5030.
450
451 -}
452
453 -- | This describes how a "map" operation over a type/coercion should behave
454 data TyCoMapper env m
455 = TyCoMapper
456 { tcm_smart :: Bool -- ^ Should the new type be created with smart
457 -- constructors?
458 , tcm_tyvar :: env -> TyVar -> m Type
459 , tcm_covar :: env -> CoVar -> m Coercion
460 , tcm_hole :: env -> CoercionHole -> Role
461 -> Type -> Type -> m Coercion
462 -- ^ What to do with coercion holes. See Note [Coercion holes] in
463 -- TyCoRep.
464
465 , tcm_tybinder :: env -> TyVar -> ArgFlag -> m (env, TyVar)
466 -- ^ The returned env is used in the extended scope
467 }
468
469 {-# INLINABLE mapType #-} -- See Note [Specialising mappers]
470 mapType :: Monad m => TyCoMapper env m -> env -> Type -> m Type
471 mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
472 , tcm_tybinder = tybinder })
473 env ty
474 = go ty
475 where
476 go (TyVarTy tv) = tyvar env tv
477 go (AppTy t1 t2) = mkappty <$> go t1 <*> go t2
478 go t@(TyConApp _ []) = return t -- avoid allocation in this exceedingly
479 -- common case (mostly, for *)
480 go (TyConApp tc tys) = mktyconapp tc <$> mapM go tys
481 go (FunTy arg res) = FunTy <$> go arg <*> go res
482 go (ForAllTy (TvBndr tv vis) inner)
483 = do { (env', tv') <- tybinder env tv vis
484 ; inner' <- mapType mapper env' inner
485 ; return $ ForAllTy (TvBndr tv' vis) inner' }
486 go ty@(LitTy {}) = return ty
487 go (CastTy ty co) = mkcastty <$> go ty <*> mapCoercion mapper env co
488 go (CoercionTy co) = CoercionTy <$> mapCoercion mapper env co
489
490 (mktyconapp, mkappty, mkcastty)
491 | smart = (mkTyConApp, mkAppTy, mkCastTy)
492 | otherwise = (TyConApp, AppTy, CastTy)
493
494 {-# INLINABLE mapCoercion #-} -- See Note [Specialising mappers]
495 mapCoercion :: Monad m
496 => TyCoMapper env m -> env -> Coercion -> m Coercion
497 mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
498 , tcm_hole = cohole, tcm_tybinder = tybinder })
499 env co
500 = go co
501 where
502 go (Refl r ty) = Refl r <$> mapType mapper env ty
503 go (TyConAppCo r tc args)
504 = mktyconappco r tc <$> mapM go args
505 go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
506 go (ForAllCo tv kind_co co)
507 = do { kind_co' <- go kind_co
508 ; (env', tv') <- tybinder env tv Inferred
509 ; co' <- mapCoercion mapper env' co
510 ; return $ mkforallco tv' kind_co' co' }
511 -- See Note [Efficiency for mapCoercion ForAllCo case]
512 go (CoVarCo cv) = covar env cv
513 go (AxiomInstCo ax i args)
514 = mkaxiominstco ax i <$> mapM go args
515 go (UnivCo (HoleProv hole) r t1 t2)
516 = cohole env hole r t1 t2
517 go (UnivCo p r t1 t2)
518 = mkunivco <$> go_prov p <*> pure r
519 <*> mapType mapper env t1 <*> mapType mapper env t2
520 go (SymCo co) = mksymco <$> go co
521 go (TransCo c1 c2) = mktransco <$> go c1 <*> go c2
522 go (AxiomRuleCo r cos) = AxiomRuleCo r <$> mapM go cos
523 go (NthCo i co) = mknthco i <$> go co
524 go (LRCo lr co) = mklrco lr <$> go co
525 go (InstCo co arg) = mkinstco <$> go co <*> go arg
526 go (CoherenceCo c1 c2) = mkcoherenceco <$> go c1 <*> go c2
527 go (KindCo co) = mkkindco <$> go co
528 go (SubCo co) = mksubco <$> go co
529
530 go_prov UnsafeCoerceProv = return UnsafeCoerceProv
531 go_prov (PhantomProv co) = PhantomProv <$> go co
532 go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co
533 go_prov p@(PluginProv _) = return p
534 go_prov (HoleProv _) = panic "mapCoercion"
535
536 ( mktyconappco, mkappco, mkaxiominstco, mkunivco
537 , mksymco, mktransco, mknthco, mklrco, mkinstco, mkcoherenceco
538 , mkkindco, mksubco, mkforallco)
539 | smart
540 = ( mkTyConAppCo, mkAppCo, mkAxiomInstCo, mkUnivCo
541 , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo, mkCoherenceCo
542 , mkKindCo, mkSubCo, mkForAllCo )
543 | otherwise
544 = ( TyConAppCo, AppCo, AxiomInstCo, UnivCo
545 , SymCo, TransCo, NthCo, LRCo, InstCo, CoherenceCo
546 , KindCo, SubCo, ForAllCo )
547
548 {-
549 ************************************************************************
550 * *
551 \subsection{Constructor-specific functions}
552 * *
553 ************************************************************************
554
555
556 ---------------------------------------------------------------------
557 TyVarTy
558 ~~~~~~~
559 -}
560
561 -- | Attempts to obtain the type variable underlying a 'Type', and panics with the
562 -- given message if this is not a type variable type. See also 'getTyVar_maybe'
563 getTyVar :: String -> Type -> TyVar
564 getTyVar msg ty = case getTyVar_maybe ty of
565 Just tv -> tv
566 Nothing -> panic ("getTyVar: " ++ msg)
567
568 isTyVarTy :: Type -> Bool
569 isTyVarTy ty = isJust (getTyVar_maybe ty)
570
571 -- | Attempts to obtain the type variable underlying a 'Type'
572 getTyVar_maybe :: Type -> Maybe TyVar
573 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
574 | otherwise = repGetTyVar_maybe ty
575
576 -- | If the type is a tyvar, possibly under a cast, returns it, along
577 -- with the coercion. Thus, the co is :: kind tv ~R kind type
578 getCastedTyVar_maybe :: Type -> Maybe (TyVar, Coercion)
579 getCastedTyVar_maybe ty | Just ty' <- coreView ty = getCastedTyVar_maybe ty'
580 getCastedTyVar_maybe (CastTy (TyVarTy tv) co) = Just (tv, co)
581 getCastedTyVar_maybe (TyVarTy tv)
582 = Just (tv, mkReflCo Nominal (tyVarKind tv))
583 getCastedTyVar_maybe _ = Nothing
584
585 -- | Attempts to obtain the type variable underlying a 'Type', without
586 -- any expansion
587 repGetTyVar_maybe :: Type -> Maybe TyVar
588 repGetTyVar_maybe (TyVarTy tv) = Just tv
589 repGetTyVar_maybe _ = Nothing
590
591 {-
592 ---------------------------------------------------------------------
593 AppTy
594 ~~~~~
595 We need to be pretty careful with AppTy to make sure we obey the
596 invariant that a TyConApp is always visibly so. mkAppTy maintains the
597 invariant: use it.
598
599 Note [Decomposing fat arrow c=>t]
600 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
601 Can we unify (a b) with (Eq a => ty)? If we do so, we end up with
602 a partial application like ((=>) Eq a) which doesn't make sense in
603 source Haskell. In constrast, we *can* unify (a b) with (t1 -> t2).
604 Here's an example (Trac #9858) of how you might do it:
605 i :: (Typeable a, Typeable b) => Proxy (a b) -> TypeRep
606 i p = typeRep p
607
608 j = i (Proxy :: Proxy (Eq Int => Int))
609 The type (Proxy (Eq Int => Int)) is only accepted with -XImpredicativeTypes,
610 but suppose we want that. But then in the call to 'i', we end
611 up decomposing (Eq Int => Int), and we definitely don't want that.
612
613 This really only applies to the type checker; in Core, '=>' and '->'
614 are the same, as are 'Constraint' and '*'. But for now I've put
615 the test in repSplitAppTy_maybe, which applies throughout, because
616 the other calls to splitAppTy are in Unify, which is also used by
617 the type checker (e.g. when matching type-function equations).
618
619 -}
620
621 -- | Applies a type to another, as in e.g. @k a@
622 mkAppTy :: Type -> Type -> Type
623 mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
624 mkAppTy ty1 ty2 = AppTy ty1 ty2
625 -- Note that the TyConApp could be an
626 -- under-saturated type synonym. GHC allows that; e.g.
627 -- type Foo k = k a -> k a
628 -- type Id x = x
629 -- foo :: Foo Id -> Foo Id
630 --
631 -- Here Id is partially applied in the type sig for Foo,
632 -- but once the type synonyms are expanded all is well
633
634 mkAppTys :: Type -> [Type] -> Type
635 mkAppTys ty1 [] = ty1
636 mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
637 mkAppTys ty1 tys2 = foldl AppTy ty1 tys2
638
639 -------------
640 splitAppTy_maybe :: Type -> Maybe (Type, Type)
641 -- ^ Attempt to take a type application apart, whether it is a
642 -- function, type constructor, or plain type application. Note
643 -- that type family applications are NEVER unsaturated by this!
644 splitAppTy_maybe ty | Just ty' <- coreView ty
645 = splitAppTy_maybe ty'
646 splitAppTy_maybe ty = repSplitAppTy_maybe ty
647
648 -------------
649 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
650 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
651 -- any Core view stuff is already done
652 repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
653 repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
654 repSplitAppTy_maybe (TyConApp tc tys)
655 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
656 , Just (tys', ty') <- snocView tys
657 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
658 repSplitAppTy_maybe _other = Nothing
659
660 -- this one doesn't braek apart (c => t).
661 -- See Note [Decomposing fat arrow c=>t]
662 -- Defined here to avoid module loops between Unify and TcType.
663 tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
664 -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
665 -- any coreView stuff is already done. Refuses to look through (c => t)
666 tcRepSplitAppTy_maybe (FunTy ty1 ty2)
667 | isConstraintKind (typeKind ty1) = Nothing -- See Note [Decomposing fat arrow c=>t]
668 | otherwise = Just (TyConApp funTyCon [ty1], ty2)
669 tcRepSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
670 tcRepSplitAppTy_maybe (TyConApp tc tys)
671 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
672 , Just (tys', ty') <- snocView tys
673 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
674 tcRepSplitAppTy_maybe _other = Nothing
675 -------------
676 splitAppTy :: Type -> (Type, Type)
677 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
678 -- and panics if this is not possible
679 splitAppTy ty = case splitAppTy_maybe ty of
680 Just pr -> pr
681 Nothing -> panic "splitAppTy"
682
683 -------------
684 splitAppTys :: Type -> (Type, [Type])
685 -- ^ Recursively splits a type as far as is possible, leaving a residual
686 -- type being applied to and the type arguments applied to it. Never fails,
687 -- even if that means returning an empty list of type applications.
688 splitAppTys ty = split ty ty []
689 where
690 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
691 split _ (AppTy ty arg) args = split ty ty (arg:args)
692 split _ (TyConApp tc tc_args) args
693 = let -- keep type families saturated
694 n | mightBeUnsaturatedTyCon tc = 0
695 | otherwise = tyConArity tc
696 (tc_args1, tc_args2) = splitAt n tc_args
697 in
698 (TyConApp tc tc_args1, tc_args2 ++ args)
699 split _ (FunTy ty1 ty2) args = ASSERT( null args )
700 (TyConApp funTyCon [], [ty1,ty2])
701 split orig_ty _ args = (orig_ty, args)
702
703 -- | Like 'splitAppTys', but doesn't look through type synonyms
704 repSplitAppTys :: Type -> (Type, [Type])
705 repSplitAppTys ty = split ty []
706 where
707 split (AppTy ty arg) args = split ty (arg:args)
708 split (TyConApp tc tc_args) args
709 = let n | mightBeUnsaturatedTyCon tc = 0
710 | otherwise = tyConArity tc
711 (tc_args1, tc_args2) = splitAt n tc_args
712 in
713 (TyConApp tc tc_args1, tc_args2 ++ args)
714 split (FunTy ty1 ty2) args = ASSERT( null args )
715 (TyConApp funTyCon [], [ty1, ty2])
716 split ty args = (ty, args)
717
718 {-
719 LitTy
720 ~~~~~
721 -}
722
723 mkNumLitTy :: Integer -> Type
724 mkNumLitTy n = LitTy (NumTyLit n)
725
726 -- | Is this a numeric literal. We also look through type synonyms.
727 isNumLitTy :: Type -> Maybe Integer
728 isNumLitTy ty | Just ty1 <- coreView ty = isNumLitTy ty1
729 isNumLitTy (LitTy (NumTyLit n)) = Just n
730 isNumLitTy _ = Nothing
731
732 mkStrLitTy :: FastString -> Type
733 mkStrLitTy s = LitTy (StrTyLit s)
734
735 -- | Is this a symbol literal. We also look through type synonyms.
736 isStrLitTy :: Type -> Maybe FastString
737 isStrLitTy ty | Just ty1 <- coreView ty = isStrLitTy ty1
738 isStrLitTy (LitTy (StrTyLit s)) = Just s
739 isStrLitTy _ = Nothing
740
741
742 -- | Is this type a custom user error?
743 -- If so, give us the kind and the error message.
744 userTypeError_maybe :: Type -> Maybe Type
745 userTypeError_maybe t
746 = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t
747 -- There may be more than 2 arguments, if the type error is
748 -- used as a type constructor (e.g. at kind `Type -> Type`).
749
750 ; guard (tyConName tc == errorMessageTypeErrorFamName)
751 ; return msg }
752
753 -- | Render a type corresponding to a user type error into a SDoc.
754 pprUserTypeErrorTy :: Type -> SDoc
755 pprUserTypeErrorTy ty =
756 case splitTyConApp_maybe ty of
757
758 -- Text "Something"
759 Just (tc,[txt])
760 | tyConName tc == typeErrorTextDataConName
761 , Just str <- isStrLitTy txt -> ftext str
762
763 -- ShowType t
764 Just (tc,[_k,t])
765 | tyConName tc == typeErrorShowTypeDataConName -> ppr t
766
767 -- t1 :<>: t2
768 Just (tc,[t1,t2])
769 | tyConName tc == typeErrorAppendDataConName ->
770 pprUserTypeErrorTy t1 <> pprUserTypeErrorTy t2
771
772 -- t1 :$$: t2
773 Just (tc,[t1,t2])
774 | tyConName tc == typeErrorVAppendDataConName ->
775 pprUserTypeErrorTy t1 $$ pprUserTypeErrorTy t2
776
777 -- An uneavaluated type function
778 _ -> ppr ty
779
780
781
782
783 {-
784 ---------------------------------------------------------------------
785 FunTy
786 ~~~~~
787 -}
788
789 isFunTy :: Type -> Bool
790 isFunTy ty = isJust (splitFunTy_maybe ty)
791
792 splitFunTy :: Type -> (Type, Type)
793 -- ^ Attempts to extract the argument and result types from a type, and
794 -- panics if that is not possible. See also 'splitFunTy_maybe'
795 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
796 splitFunTy (FunTy arg res) = (arg, res)
797 splitFunTy other = pprPanic "splitFunTy" (ppr other)
798
799 splitFunTy_maybe :: Type -> Maybe (Type, Type)
800 -- ^ Attempts to extract the argument and result types from a type
801 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
802 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
803 splitFunTy_maybe _ = Nothing
804
805 splitFunTys :: Type -> ([Type], Type)
806 splitFunTys ty = split [] ty ty
807 where
808 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
809 split args _ (FunTy arg res) = split (arg:args) res res
810 split args orig_ty _ = (reverse args, orig_ty)
811
812 funResultTy :: Type -> Type
813 -- ^ Extract the function result type and panic if that is not possible
814 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
815 funResultTy (FunTy _ res) = res
816 funResultTy ty = pprPanic "funResultTy" (ppr ty)
817
818 funArgTy :: Type -> Type
819 -- ^ Extract the function argument type and panic if that is not possible
820 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
821 funArgTy (FunTy arg _res) = arg
822 funArgTy ty = pprPanic "funArgTy" (ppr ty)
823
824 piResultTy :: Type -> Type -> Type
825 piResultTy ty arg = case piResultTy_maybe ty arg of
826 Just res -> res
827 Nothing -> pprPanic "piResultTy" (ppr ty $$ ppr arg)
828
829 piResultTy_maybe :: Type -> Type -> Maybe Type
830
831 -- ^ Just like 'piResultTys' but for a single argument
832 -- Try not to iterate 'piResultTy', because it's inefficient to substitute
833 -- one variable at a time; instead use 'piResultTys"
834 piResultTy_maybe ty arg
835 | Just ty' <- coreView ty = piResultTy_maybe ty' arg
836
837 | FunTy _ res <- ty
838 = Just res
839
840 | ForAllTy (TvBndr tv _) res <- ty
841 = let empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
842 tyCoVarsOfTypes [arg,res]
843 in Just (substTy (extendTvSubst empty_subst tv arg) res)
844
845 | otherwise
846 = Nothing
847
848 -- | (piResultTys f_ty [ty1, .., tyn]) gives the type of (f ty1 .. tyn)
849 -- where f :: f_ty
850 -- 'piResultTys' is interesting because:
851 -- 1. 'f_ty' may have more for-alls than there are args
852 -- 2. Less obviously, it may have fewer for-alls
853 -- For case 2. think of:
854 -- piResultTys (forall a.a) [forall b.b, Int]
855 -- This really can happen, but only (I think) in situations involving
856 -- undefined. For example:
857 -- undefined :: forall a. a
858 -- Term: undefined @(forall b. b->b) @Int
859 -- This term should have type (Int -> Int), but notice that
860 -- there are more type args than foralls in 'undefined's type.
861
862 -- If you edit this function, you may need to update the GHC formalism
863 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
864
865 -- This is a heavily used function (e.g. from typeKind),
866 -- so we pay attention to efficiency, especially in the special case
867 -- where there are no for-alls so we are just dropping arrows from
868 -- a function type/kind.
869 piResultTys :: Type -> [Type] -> Type
870 piResultTys ty [] = ty
871 piResultTys ty orig_args@(arg:args)
872 | Just ty' <- coreView ty
873 = piResultTys ty' orig_args
874
875 | FunTy _ res <- ty
876 = piResultTys res args
877
878 | ForAllTy (TvBndr tv _) res <- ty
879 = go (extendVarEnv emptyTvSubstEnv tv arg) res args
880
881 | otherwise
882 = pprPanic "piResultTys1" (ppr ty $$ ppr orig_args)
883 where
884 in_scope = mkInScopeSet (tyCoVarsOfTypes (ty:orig_args))
885
886 go :: TvSubstEnv -> Type -> [Type] -> Type
887 go tv_env ty [] = substTy (mkTvSubst in_scope tv_env) ty
888
889 go tv_env ty all_args@(arg:args)
890 | Just ty' <- coreView ty
891 = go tv_env ty' all_args
892
893 | FunTy _ res <- ty
894 = go tv_env res args
895
896 | ForAllTy (TvBndr tv _) res <- ty
897 = go (extendVarEnv tv_env tv arg) res args
898
899 | TyVarTy tv <- ty
900 , Just ty' <- lookupVarEnv tv_env tv
901 -- Deals with piResultTys (forall a. a) [forall b.b, Int]
902 = piResultTys ty' all_args
903
904 | otherwise
905 = pprPanic "piResultTys2" (ppr ty $$ ppr orig_args $$ ppr all_args)
906
907 applyTysX :: [TyVar] -> Type -> [Type] -> Type
908 -- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
909 -- Assumes that (/\tvs. body_ty) is closed
910 applyTysX tvs body_ty arg_tys
911 = ASSERT2( length arg_tys >= n_tvs, pp_stuff )
912 ASSERT2( tyCoVarsOfType body_ty `subVarSet` mkVarSet tvs, pp_stuff )
913 mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
914 (drop n_tvs arg_tys)
915 where
916 pp_stuff = vcat [ppr tvs, ppr body_ty, ppr arg_tys]
917 n_tvs = length tvs
918
919 {-
920 ---------------------------------------------------------------------
921 TyConApp
922 ~~~~~~~~
923 -}
924
925 -- | A key function: builds a 'TyConApp' or 'FunTy' as appropriate to
926 -- its arguments. Applies its arguments to the constructor from left to right.
927 mkTyConApp :: TyCon -> [Type] -> Type
928 mkTyConApp tycon tys
929 | isFunTyCon tycon, [ty1,ty2] <- tys
930 = FunTy ty1 ty2
931
932 | otherwise
933 = TyConApp tycon tys
934
935 -- splitTyConApp "looks through" synonyms, because they don't
936 -- mean a distinct type, but all other type-constructor applications
937 -- including functions are returned as Just ..
938
939 -- | Retrieve the tycon heading this type, if there is one. Does /not/
940 -- look through synonyms.
941 tyConAppTyConPicky_maybe :: Type -> Maybe TyCon
942 tyConAppTyConPicky_maybe (TyConApp tc _) = Just tc
943 tyConAppTyConPicky_maybe (FunTy {}) = Just funTyCon
944 tyConAppTyConPicky_maybe _ = Nothing
945
946
947 -- | The same as @fst . splitTyConApp@
948 tyConAppTyCon_maybe :: Type -> Maybe TyCon
949 tyConAppTyCon_maybe ty | Just ty' <- coreView ty = tyConAppTyCon_maybe ty'
950 tyConAppTyCon_maybe (TyConApp tc _) = Just tc
951 tyConAppTyCon_maybe (FunTy {}) = Just funTyCon
952 tyConAppTyCon_maybe _ = Nothing
953
954 tyConAppTyCon :: Type -> TyCon
955 tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr ty)
956
957 -- | The same as @snd . splitTyConApp@
958 tyConAppArgs_maybe :: Type -> Maybe [Type]
959 tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty'
960 tyConAppArgs_maybe (TyConApp _ tys) = Just tys
961 tyConAppArgs_maybe (FunTy arg res) = Just [arg,res]
962 tyConAppArgs_maybe _ = Nothing
963
964 tyConAppArgs :: Type -> [Type]
965 tyConAppArgs ty = tyConAppArgs_maybe ty `orElse` pprPanic "tyConAppArgs" (ppr ty)
966
967 tyConAppArgN :: Int -> Type -> Type
968 -- Executing Nth
969 tyConAppArgN n ty
970 = case tyConAppArgs_maybe ty of
971 Just tys -> ASSERT2( n < length tys, ppr n <+> ppr tys ) tys `getNth` n
972 Nothing -> pprPanic "tyConAppArgN" (ppr n <+> ppr ty)
973
974 -- | Attempts to tease a type apart into a type constructor and the application
975 -- of a number of arguments to that constructor. Panics if that is not possible.
976 -- See also 'splitTyConApp_maybe'
977 splitTyConApp :: Type -> (TyCon, [Type])
978 splitTyConApp ty = case splitTyConApp_maybe ty of
979 Just stuff -> stuff
980 Nothing -> pprPanic "splitTyConApp" (ppr ty)
981
982 -- | Attempts to tease a type apart into a type constructor and the application
983 -- of a number of arguments to that constructor
984 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
985 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
986 splitTyConApp_maybe ty = repSplitTyConApp_maybe ty
987
988 -- | Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
989 -- assumes the synonyms have already been dealt with.
990 repSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
991 repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
992 repSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
993 repSplitTyConApp_maybe _ = Nothing
994
995 -- | Attempts to tease a list type apart and gives the type of the elements if
996 -- successful (looks through type synonyms)
997 splitListTyConApp_maybe :: Type -> Maybe Type
998 splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
999 Just (tc,[e]) | tc == listTyCon -> Just e
1000 _other -> Nothing
1001
1002 -- | What is the role assigned to the next parameter of this type? Usually,
1003 -- this will be 'Nominal', but if the type is a 'TyConApp', we may be able to
1004 -- do better. The type does *not* have to be well-kinded when applied for this
1005 -- to work!
1006 nextRole :: Type -> Role
1007 nextRole ty
1008 | Just (tc, tys) <- splitTyConApp_maybe ty
1009 , let num_tys = length tys
1010 , num_tys < tyConArity tc
1011 = tyConRoles tc `getNth` num_tys
1012
1013 | otherwise
1014 = Nominal
1015
1016 newTyConInstRhs :: TyCon -> [Type] -> Type
1017 -- ^ Unwrap one 'layer' of newtype on a type constructor and its
1018 -- arguments, using an eta-reduced version of the @newtype@ if possible.
1019 -- This requires tys to have at least @newTyConInstArity tycon@ elements.
1020 newTyConInstRhs tycon tys
1021 = ASSERT2( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs )
1022 applyTysX tvs rhs tys
1023 where
1024 (tvs, rhs) = newTyConEtadRhs tycon
1025
1026 {-
1027 ---------------------------------------------------------------------
1028 CastTy
1029 ~~~~~~
1030 A casted type has its *kind* casted into something new.
1031
1032 Note [Weird typing rule for ForAllTy]
1033 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1034
1035 Here is the (truncated) typing rule for the dependent ForAllTy:
1036
1037 inner : kind
1038 ------------------------------------
1039 ForAllTy (Named tv vis) inner : kind
1040
1041 Note that neither the inner type nor for ForAllTy itself have to have
1042 kind *! But, it means that we should push any kind casts through the
1043 ForAllTy. The only trouble is avoiding capture.
1044
1045 -}
1046
1047 splitCastTy_maybe :: Type -> Maybe (Type, Coercion)
1048 splitCastTy_maybe ty | Just ty' <- coreView ty = splitCastTy_maybe ty'
1049 splitCastTy_maybe (CastTy ty co) = Just (ty, co)
1050 splitCastTy_maybe _ = Nothing
1051
1052 -- | Make a 'CastTy'. The Coercion must be nominal. This function looks
1053 -- at the entire structure of the type and coercion in an attempt to
1054 -- maintain representation invariance (that is, any two types that are `eqType`
1055 -- look the same). Be very wary of calling this in a loop.
1056 mkCastTy :: Type -> Coercion -> Type
1057 -- Running example:
1058 -- T :: forall k1. k1 -> forall k2. k2 -> Bool -> Maybe k1 -> *
1059 -- co :: * ~R X (maybe X is a newtype around *)
1060 -- ty = T Nat 3 Symbol "foo" True (Just 2)
1061 --
1062 -- We wish to "push" the cast down as far as possible. See also
1063 -- Note [Pushing down casts] in TyCoRep. Here is where we end
1064 -- up:
1065 --
1066 -- (T Nat 3 Symbol |> <Symbol> -> <Bool> -> <Maybe Nat> -> co)
1067 -- "foo" True (Just 2)
1068 --
1069 mkCastTy ty co | isReflexiveCo co = ty
1070 -- NB: Do the slow check here. This is important to keep the splitXXX
1071 -- functions working properly. Otherwise, we may end up with something
1072 -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
1073 -- fails under splitFunTy_maybe. This happened with the cheaper check
1074 -- in test dependent/should_compile/dynamic-paper.
1075
1076 mkCastTy (CastTy ty co1) co2 = mkCastTy ty (co1 `mkTransCo` co2)
1077
1078 mkCastTy outer_ty@(ForAllTy (TvBndr tv vis) inner_ty) co
1079 = ForAllTy (TvBndr tv' vis) (substTy subst inner_ty `mkCastTy` co)
1080 where
1081 -- See Note [Weird typing rule for ForAllTy]
1082 -- have to make sure that pushing the co in doesn't capture the bound var
1083 fvs = tyCoVarsOfCo co `unionVarSet` tyCoVarsOfType outer_ty
1084 empty_subst = mkEmptyTCvSubst (mkInScopeSet fvs)
1085 (subst, tv') = substTyVarBndr empty_subst tv
1086
1087 mkCastTy ty co = -- NB: don't check if the coercion "from" type matches here;
1088 -- there may be unzonked variables about
1089 let result = split_apps [] ty co in
1090 ASSERT2( CastTy ty co `eqType` result
1091 , ppr ty <+> dcolon <+> ppr (typeKind ty) $$
1092 ppr co <+> dcolon <+> ppr (coercionKind co) $$
1093 ppr result <+> dcolon <+> ppr (typeKind result) )
1094 result
1095 where
1096 -- split_apps breaks apart any type applications, so we can see how far down
1097 -- to push the cast
1098 split_apps args (AppTy t1 t2) co
1099 = split_apps (t2:args) t1 co
1100 split_apps args (TyConApp tc tc_args) co
1101 | mightBeUnsaturatedTyCon tc
1102 = affix_co (tyConTyBinders tc) (mkTyConTy tc) (tc_args `chkAppend` args) co
1103 | otherwise -- not decomposable... but it may still be oversaturated
1104 = let (non_decomp_args, decomp_args) = splitAt (tyConArity tc) tc_args
1105 saturated_tc = mkTyConApp tc non_decomp_args
1106 in
1107 affix_co (fst $ splitPiTys $ typeKind saturated_tc)
1108 saturated_tc (decomp_args `chkAppend` args) co
1109
1110 split_apps args (FunTy arg res) co
1111 = affix_co (tyConTyBinders funTyCon) (mkTyConTy funTyCon)
1112 (arg : res : args) co
1113 split_apps args ty co
1114 = affix_co (fst $ splitPiTys $ typeKind ty)
1115 ty args co
1116
1117 -- Having broken everything apart, this figures out the point at which there
1118 -- are no more dependent quantifications, and puts the cast there
1119 affix_co _ ty [] co
1120 = no_double_casts ty co
1121 affix_co bndrs ty args co
1122 -- if kind contains any dependent quantifications, we can't push.
1123 -- apply arguments until it doesn't
1124 = let (no_dep_bndrs, some_dep_bndrs) = spanEnd isAnonTyBinder bndrs
1125 (some_dep_args, rest_args) = splitAtList some_dep_bndrs args
1126 dep_subst = zipTyBinderSubst some_dep_bndrs some_dep_args
1127 used_no_dep_bndrs = takeList rest_args no_dep_bndrs
1128 rest_arg_tys = substTys dep_subst (map tyBinderType used_no_dep_bndrs)
1129 co' = mkFunCos Nominal
1130 (map (mkReflCo Nominal) rest_arg_tys)
1131 co
1132 in
1133 ((ty `mkAppTys` some_dep_args) `no_double_casts` co') `mkAppTys` rest_args
1134
1135 no_double_casts (CastTy ty co1) co2 = CastTy ty (co1 `mkTransCo` co2)
1136 no_double_casts ty co = CastTy ty co
1137
1138 tyConTyBinders :: TyCon -> [TyBinder]
1139 -- Return the tyConBinders in TyBinder form
1140 tyConTyBinders tycon = tyConBindersTyBinders (tyConBinders tycon)
1141
1142 tyConBindersTyBinders :: [TyConBinder] -> [TyBinder]
1143 -- Return the tyConBinders in TyBinder form
1144 tyConBindersTyBinders = map to_tyb
1145 where
1146 to_tyb (TvBndr tv (NamedTCB vis)) = Named (TvBndr tv vis)
1147 to_tyb (TvBndr tv AnonTCB) = Anon (tyVarKind tv)
1148
1149 {-
1150 --------------------------------------------------------------------
1151 CoercionTy
1152 ~~~~~~~~~~
1153 CoercionTy allows us to inject coercions into types. A CoercionTy
1154 should appear only in the right-hand side of an application.
1155 -}
1156
1157 mkCoercionTy :: Coercion -> Type
1158 mkCoercionTy = CoercionTy
1159
1160 isCoercionTy :: Type -> Bool
1161 isCoercionTy (CoercionTy _) = True
1162 isCoercionTy _ = False
1163
1164 isCoercionTy_maybe :: Type -> Maybe Coercion
1165 isCoercionTy_maybe (CoercionTy co) = Just co
1166 isCoercionTy_maybe _ = Nothing
1167
1168 stripCoercionTy :: Type -> Coercion
1169 stripCoercionTy (CoercionTy co) = co
1170 stripCoercionTy ty = pprPanic "stripCoercionTy" (ppr ty)
1171
1172 {-
1173 ---------------------------------------------------------------------
1174 SynTy
1175 ~~~~~
1176
1177 Notes on type synonyms
1178 ~~~~~~~~~~~~~~~~~~~~~~
1179 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
1180 to return type synonyms wherever possible. Thus
1181
1182 type Foo a = a -> a
1183
1184 we want
1185 splitFunTys (a -> Foo a) = ([a], Foo a)
1186 not ([a], a -> a)
1187
1188 The reason is that we then get better (shorter) type signatures in
1189 interfaces. Notably this plays a role in tcTySigs in TcBinds.hs.
1190
1191
1192 ---------------------------------------------------------------------
1193 ForAllTy
1194 ~~~~~~~~
1195 -}
1196
1197 -- | Make a dependent forall.
1198 mkInvForAllTy :: TyVar -> Type -> Type
1199 mkInvForAllTy tv ty = ASSERT( isTyVar tv )
1200 ForAllTy (TvBndr tv Inferred) ty
1201
1202 -- | Like mkForAllTys, but assumes all variables are dependent and invisible,
1203 -- a common case
1204 mkInvForAllTys :: [TyVar] -> Type -> Type
1205 mkInvForAllTys tvs ty = ASSERT( all isTyVar tvs )
1206 foldr mkInvForAllTy ty tvs
1207
1208 -- | Like mkForAllTys, but assumes all variables are dependent and specified,
1209 -- a common case
1210 mkSpecForAllTys :: [TyVar] -> Type -> Type
1211 mkSpecForAllTys tvs = ASSERT( all isTyVar tvs )
1212 mkForAllTys [ TvBndr tv Specified | tv <- tvs ]
1213
1214 -- | Like mkForAllTys, but assumes all variables are dependent and visible
1215 mkVisForAllTys :: [TyVar] -> Type -> Type
1216 mkVisForAllTys tvs = ASSERT( all isTyVar tvs )
1217 mkForAllTys [ TvBndr tv Required | tv <- tvs ]
1218
1219 mkLamType :: Var -> Type -> Type
1220 -- ^ Makes a @(->)@ type or an implicit forall type, depending
1221 -- on whether it is given a type variable or a term variable.
1222 -- This is used, for example, when producing the type of a lambda.
1223 -- Always uses Inferred binders.
1224 mkLamTypes :: [Var] -> Type -> Type
1225 -- ^ 'mkLamType' for multiple type or value arguments
1226
1227 mkLamType v ty
1228 | isTyVar v = ForAllTy (TvBndr v Inferred) ty
1229 | otherwise = FunTy (varType v) ty
1230
1231 mkLamTypes vs ty = foldr mkLamType ty vs
1232
1233 -- | Given a list of type-level vars and a result type, makes TyBinders, preferring
1234 -- anonymous binders if the variable is, in fact, not dependent.
1235 -- All binders are /visible/.
1236 mkTyConBindersPreferAnon :: [TyVar] -> Type -> [TyConBinder]
1237 mkTyConBindersPreferAnon vars inner_ty = fst (go vars)
1238 where
1239 go :: [TyVar] -> ([TyConBinder], VarSet) -- also returns the free vars
1240 go [] = ([], tyCoVarsOfType inner_ty)
1241 go (v:vs) | v `elemVarSet` fvs
1242 = ( TvBndr v (NamedTCB Required) : binders
1243 , fvs `delVarSet` v `unionVarSet` kind_vars )
1244 | otherwise
1245 = ( TvBndr v AnonTCB : binders
1246 , fvs `unionVarSet` kind_vars )
1247 where
1248 (binders, fvs) = go vs
1249 kind_vars = tyCoVarsOfType $ tyVarKind v
1250
1251 -- | Take a ForAllTy apart, returning the list of tyvars and the result type.
1252 -- This always succeeds, even if it returns only an empty list. Note that the
1253 -- result type returned may have free variables that were bound by a forall.
1254 splitForAllTys :: Type -> ([TyVar], Type)
1255 splitForAllTys ty = split ty ty []
1256 where
1257 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
1258 split _ (ForAllTy (TvBndr tv _) ty) tvs = split ty ty (tv:tvs)
1259 split orig_ty _ tvs = (reverse tvs, orig_ty)
1260
1261 -- | Like 'splitPiTys' but split off only /named/ binders.
1262 splitForAllTyVarBndrs :: Type -> ([TyVarBinder], Type)
1263 splitForAllTyVarBndrs ty = split ty ty []
1264 where
1265 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1266 split _ (ForAllTy b res) bs = split res res (b:bs)
1267 split orig_ty _ bs = (reverse bs, orig_ty)
1268
1269 -- | Checks whether this is a proper forall (with a named binder)
1270 isForAllTy :: Type -> Bool
1271 isForAllTy (ForAllTy {}) = True
1272 isForAllTy _ = False
1273
1274 -- | Is this a function or forall?
1275 isPiTy :: Type -> Bool
1276 isPiTy (ForAllTy {}) = True
1277 isPiTy (FunTy {}) = True
1278 isPiTy _ = False
1279
1280 -- | Take a forall type apart, or panics if that is not possible.
1281 splitForAllTy :: Type -> (TyVar, Type)
1282 splitForAllTy ty
1283 | Just answer <- splitForAllTy_maybe ty = answer
1284 | otherwise = pprPanic "splitForAllTy" (ppr ty)
1285
1286 -- | Drops all ForAllTys
1287 dropForAlls :: Type -> Type
1288 dropForAlls ty = go ty
1289 where
1290 go ty | Just ty' <- coreView ty = go ty'
1291 go (ForAllTy _ res) = go res
1292 go res = res
1293
1294 -- | Attempts to take a forall type apart, but only if it's a proper forall,
1295 -- with a named binder
1296 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
1297 splitForAllTy_maybe ty = go ty
1298 where
1299 go ty | Just ty' <- coreView ty = go ty'
1300 go (ForAllTy (TvBndr tv _) ty) = Just (tv, ty)
1301 go _ = Nothing
1302
1303 -- | Attempts to take a forall type apart; works with proper foralls and
1304 -- functions
1305 splitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
1306 splitPiTy_maybe ty = go ty
1307 where
1308 go ty | Just ty' <- coreView ty = go ty'
1309 go (ForAllTy bndr ty) = Just (Named bndr, ty)
1310 go (FunTy arg res) = Just (Anon arg, res)
1311 go _ = Nothing
1312
1313 -- | Takes a forall type apart, or panics
1314 splitPiTy :: Type -> (TyBinder, Type)
1315 splitPiTy ty
1316 | Just answer <- splitPiTy_maybe ty = answer
1317 | otherwise = pprPanic "splitPiTy" (ppr ty)
1318
1319 -- | Split off all TyBinders to a type, splitting both proper foralls
1320 -- and functions
1321 splitPiTys :: Type -> ([TyBinder], Type)
1322 splitPiTys ty = split ty ty []
1323 where
1324 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1325 split _ (ForAllTy b res) bs = split res res (Named b : bs)
1326 split _ (FunTy arg res) bs = split res res (Anon arg : bs)
1327 split orig_ty _ bs = (reverse bs, orig_ty)
1328
1329 -- Like splitPiTys, but returns only *invisible* binders, including constraints
1330 -- Stops at the first visible binder
1331 splitPiTysInvisible :: Type -> ([TyBinder], Type)
1332 splitPiTysInvisible ty = split ty ty []
1333 where
1334 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1335 split _ (ForAllTy b@(TvBndr _ vis) res) bs
1336 | isInvisibleArgFlag vis = split res res (Named b : bs)
1337 split _ (FunTy arg res) bs
1338 | isPredTy arg = split res res (Anon arg : bs)
1339 split orig_ty _ bs = (reverse bs, orig_ty)
1340
1341 -- | Given a tycon and its arguments, filters out any invisible arguments
1342 filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
1343 filterOutInvisibleTypes tc tys = snd $ partitionInvisibles tc id tys
1344
1345 -- | Like 'filterOutInvisibles', but works on 'TyVar's
1346 filterOutInvisibleTyVars :: TyCon -> [TyVar] -> [TyVar]
1347 filterOutInvisibleTyVars tc tvs = snd $ partitionInvisibles tc mkTyVarTy tvs
1348
1349 -- | Given a tycon and a list of things (which correspond to arguments),
1350 -- partitions the things into
1351 -- Inferred or Specified ones and
1352 -- Required ones
1353 -- The callback function is necessary for this scenario:
1354 --
1355 -- > T :: forall k. k -> k
1356 -- > partitionInvisibles T [forall m. m -> m -> m, S, R, Q]
1357 --
1358 -- After substituting, we get
1359 --
1360 -- > T (forall m. m -> m -> m) :: (forall m. m -> m -> m) -> forall n. n -> n -> n
1361 --
1362 -- Thus, the first argument is invisible, @S@ is visible, @R@ is invisible again,
1363 -- and @Q@ is visible.
1364 --
1365 -- If you're absolutely sure that your tycon's kind doesn't end in a variable,
1366 -- it's OK if the callback function panics, as that's the only time it's
1367 -- consulted.
1368 partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
1369 partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
1370 where
1371 go _ _ [] = ([], [])
1372 go subst (ForAllTy (TvBndr tv vis) res_ki) (x:xs)
1373 | isVisibleArgFlag vis = second (x :) (go subst' res_ki xs)
1374 | otherwise = first (x :) (go subst' res_ki xs)
1375 where
1376 subst' = extendTvSubst subst tv (get_ty x)
1377 go subst (TyVarTy tv) xs
1378 | Just ki <- lookupTyVar subst tv = go subst ki xs
1379 go _ _ xs = ([], xs) -- something is ill-kinded. But this can happen
1380 -- when printing errors. Assume everything is visible.
1381
1382
1383 {-
1384 %************************************************************************
1385 %* *
1386 TyBinders
1387 %* *
1388 %************************************************************************
1389 -}
1390
1391 -- | Make a named binder
1392 mkTyVarBinder :: ArgFlag -> Var -> TyVarBinder
1393 mkTyVarBinder vis var = TvBndr var vis
1394
1395 -- | Make many named binders
1396 mkTyVarBinders :: ArgFlag -> [TyVar] -> [TyVarBinder]
1397 mkTyVarBinders vis = map (mkTyVarBinder vis)
1398
1399 -- | Make an anonymous binder
1400 mkAnonBinder :: Type -> TyBinder
1401 mkAnonBinder = Anon
1402
1403 -- | Does this binder bind a variable that is /not/ erased? Returns
1404 -- 'True' for anonymous binders.
1405 isAnonTyBinder :: TyBinder -> Bool
1406 isAnonTyBinder (Named {}) = False
1407 isAnonTyBinder (Anon {}) = True
1408
1409 isNamedTyBinder :: TyBinder -> Bool
1410 isNamedTyBinder (Named {}) = True
1411 isNamedTyBinder (Anon {}) = False
1412
1413 tyBinderType :: TyBinder -> Type
1414 -- Barely used
1415 tyBinderType (Named tvb) = binderKind tvb
1416 tyBinderType (Anon ty) = ty
1417
1418 -- | Extract a relevant type, if there is one.
1419 binderRelevantType_maybe :: TyBinder -> Maybe Type
1420 binderRelevantType_maybe (Named {}) = Nothing
1421 binderRelevantType_maybe (Anon ty) = Just ty
1422
1423 -- | Like 'maybe', but for binders.
1424 caseBinder :: TyBinder -- ^ binder to scrutinize
1425 -> (TyVarBinder -> a) -- ^ named case
1426 -> (Type -> a) -- ^ anonymous case
1427 -> a
1428 caseBinder (Named v) f _ = f v
1429 caseBinder (Anon t) _ d = d t
1430
1431 -- | Create a TCvSubst combining the binders and types provided.
1432 -- NB: It is specifically OK if the lists are of different lengths.
1433 -- Barely used
1434 zipTyBinderSubst :: [TyBinder] -> [Type] -> TCvSubst
1435 zipTyBinderSubst bndrs tys
1436 = mkTvSubstPrs [ (tv, ty) | (Named (TvBndr tv _), ty) <- zip bndrs tys ]
1437
1438 {-
1439 %************************************************************************
1440 %* *
1441 Pred
1442 * *
1443 ************************************************************************
1444
1445 Predicates on PredType
1446
1447 Note [isPredTy complications]
1448 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1449 You would think that we could define
1450 isPredTy ty = isConstraintKind (typeKind ty)
1451 But there are a number of complications:
1452
1453 * isPredTy is used when printing types, which can happen in debug
1454 printing during type checking of not-fully-zonked types. So it's
1455 not cool to say isConstraintKind (typeKind ty) because, absent
1456 zonking, the type might be ill-kinded, and typeKind crashes. Hence the
1457 rather tiresome story here
1458
1459 * isPredTy must return "True" to *unlifted* coercions, such as (t1 ~# t2)
1460 and (t1 ~R# t2), which are not of kind Constraint! Currently they are
1461 of kind #.
1462
1463 * If we do form the type '(C a => C [a]) => blah', then we'd like to
1464 print it as such. But that means that isPredTy must return True for
1465 (C a => C [a]). Admittedly that type is illegal in Haskell, but we
1466 want to print it nicely in error messages.
1467 -}
1468
1469 -- | Is the type suitable to classify a given/wanted in the typechecker?
1470 isPredTy :: Type -> Bool
1471 -- See Note [isPredTy complications]
1472 isPredTy ty = go ty []
1473 where
1474 go :: Type -> [KindOrType] -> Bool
1475 go (AppTy ty1 ty2) args = go ty1 (ty2 : args)
1476 go (TyVarTy tv) args = go_k (tyVarKind tv) args
1477 go (TyConApp tc tys) args = ASSERT( null args ) -- TyConApp invariant
1478 go_tc tc tys
1479 go (FunTy arg res) []
1480 | isPredTy arg = isPredTy res -- (Eq a => C a)
1481 | otherwise = False -- (Int -> Bool)
1482 go (ForAllTy _ ty) [] = go ty []
1483 go (CastTy _ co) args = go_k (pSnd (coercionKind co)) args
1484 go _ _ = False
1485
1486 go_tc :: TyCon -> [KindOrType] -> Bool
1487 go_tc tc args
1488 | tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1489 = length args == 4 -- ~# and ~R# sadly have result kind #
1490 -- not Contraint; but we still want
1491 -- isPredTy to reply True.
1492 | otherwise = go_k (tyConKind tc) args
1493
1494 go_k :: Kind -> [KindOrType] -> Bool
1495 -- True <=> ('k' applied to 'kts') = Constraint
1496 go_k k [] = isConstraintKind k
1497 go_k k (arg:args) = case piResultTy_maybe k arg of
1498 Just k' -> go_k k' args
1499 Nothing -> pprTrace "isPredTy" (ppr ty)
1500 False
1501 -- This last case should not happen; but it does if we
1502 -- we call isPredTy during kind checking, especially if
1503 -- there is actually a kind error. Example that showed
1504 -- this up: polykinds/T11399
1505
1506 isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool
1507 isClassPred ty = case tyConAppTyCon_maybe ty of
1508 Just tyCon | isClassTyCon tyCon -> True
1509 _ -> False
1510 isEqPred ty = case tyConAppTyCon_maybe ty of
1511 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1512 || tyCon `hasKey` eqReprPrimTyConKey
1513 _ -> False
1514
1515 isNomEqPred ty = case tyConAppTyCon_maybe ty of
1516 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1517 _ -> False
1518
1519 isIPPred ty = case tyConAppTyCon_maybe ty of
1520 Just tc -> isIPTyCon tc
1521 _ -> False
1522
1523 isIPTyCon :: TyCon -> Bool
1524 isIPTyCon tc = tc `hasKey` ipClassKey
1525 -- Class and its corresponding TyCon have the same Unique
1526
1527 isIPClass :: Class -> Bool
1528 isIPClass cls = cls `hasKey` ipClassKey
1529
1530 isCTupleClass :: Class -> Bool
1531 isCTupleClass cls = isTupleTyCon (classTyCon cls)
1532
1533 isIPPred_maybe :: Type -> Maybe (FastString, Type)
1534 isIPPred_maybe ty =
1535 do (tc,[t1,t2]) <- splitTyConApp_maybe ty
1536 guard (isIPTyCon tc)
1537 x <- isStrLitTy t1
1538 return (x,t2)
1539
1540 {-
1541 Make PredTypes
1542
1543 --------------------- Equality types ---------------------------------
1544 -}
1545
1546 -- | Makes a lifted equality predicate at the given role
1547 mkPrimEqPredRole :: Role -> Type -> Type -> PredType
1548 mkPrimEqPredRole Nominal = mkPrimEqPred
1549 mkPrimEqPredRole Representational = mkReprPrimEqPred
1550 mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
1551
1552 -- | Creates a primitive type equality predicate.
1553 -- Invariant: the types are not Coercions
1554 mkPrimEqPred :: Type -> Type -> Type
1555 mkPrimEqPred ty1 ty2
1556 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1557 where
1558 k1 = typeKind ty1
1559 k2 = typeKind ty2
1560
1561 -- | Creates a primite type equality predicate with explicit kinds
1562 mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1563 mkHeteroPrimEqPred k1 k2 ty1 ty2 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1564
1565 -- | Creates a primitive representational type equality predicate
1566 -- with explicit kinds
1567 mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1568 mkHeteroReprPrimEqPred k1 k2 ty1 ty2
1569 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1570
1571 -- | Try to split up a coercion type into the types that it coerces
1572 splitCoercionType_maybe :: Type -> Maybe (Type, Type)
1573 splitCoercionType_maybe ty
1574 = do { (tc, [_, _, ty1, ty2]) <- splitTyConApp_maybe ty
1575 ; guard $ tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1576 ; return (ty1, ty2) }
1577
1578 mkReprPrimEqPred :: Type -> Type -> Type
1579 mkReprPrimEqPred ty1 ty2
1580 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1581 where
1582 k1 = typeKind ty1
1583 k2 = typeKind ty2
1584
1585 equalityTyCon :: Role -> TyCon
1586 equalityTyCon Nominal = eqPrimTyCon
1587 equalityTyCon Representational = eqReprPrimTyCon
1588 equalityTyCon Phantom = eqPhantPrimTyCon
1589
1590 -- --------------------- Dictionary types ---------------------------------
1591
1592 mkClassPred :: Class -> [Type] -> PredType
1593 mkClassPred clas tys = TyConApp (classTyCon clas) tys
1594
1595 isDictTy :: Type -> Bool
1596 isDictTy = isClassPred
1597
1598 isDictLikeTy :: Type -> Bool
1599 -- Note [Dictionary-like types]
1600 isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
1601 isDictLikeTy ty = case splitTyConApp_maybe ty of
1602 Just (tc, tys) | isClassTyCon tc -> True
1603 | isTupleTyCon tc -> all isDictLikeTy tys
1604 _other -> False
1605
1606 {-
1607 Note [Dictionary-like types]
1608 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1609 Being "dictionary-like" means either a dictionary type or a tuple thereof.
1610 In GHC 6.10 we build implication constraints which construct such tuples,
1611 and if we land up with a binding
1612 t :: (C [a], Eq [a])
1613 t = blah
1614 then we want to treat t as cheap under "-fdicts-cheap" for example.
1615 (Implication constraints are normally inlined, but sadly not if the
1616 occurrence is itself inside an INLINE function! Until we revise the
1617 handling of implication constraints, that is.) This turned out to
1618 be important in getting good arities in DPH code. Example:
1619
1620 class C a
1621 class D a where { foo :: a -> a }
1622 instance C a => D (Maybe a) where { foo x = x }
1623
1624 bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
1625 {-# INLINE bar #-}
1626 bar x y = (foo (Just x), foo (Just y))
1627
1628 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
1629 we ended up with something like
1630 bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
1631 in \x,y. <blah>)
1632
1633 This is all a bit ad-hoc; eg it relies on knowing that implication
1634 constraints build tuples.
1635
1636
1637 Decomposing PredType
1638 -}
1639
1640 -- | A choice of equality relation. This is separate from the type 'Role'
1641 -- because 'Phantom' does not define a (non-trivial) equality relation.
1642 data EqRel = NomEq | ReprEq
1643 deriving (Eq, Ord)
1644
1645 instance Outputable EqRel where
1646 ppr NomEq = text "nominal equality"
1647 ppr ReprEq = text "representational equality"
1648
1649 eqRelRole :: EqRel -> Role
1650 eqRelRole NomEq = Nominal
1651 eqRelRole ReprEq = Representational
1652
1653 data PredTree = ClassPred Class [Type]
1654 | EqPred EqRel Type Type
1655 | IrredPred PredType
1656
1657 classifyPredType :: PredType -> PredTree
1658 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
1659 Just (tc, [_, _, ty1, ty2])
1660 | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
1661 | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
1662 Just (tc, tys)
1663 | Just clas <- tyConClass_maybe tc -> ClassPred clas tys
1664 _ -> IrredPred ev_ty
1665
1666 getClassPredTys :: PredType -> (Class, [Type])
1667 getClassPredTys ty = case getClassPredTys_maybe ty of
1668 Just (clas, tys) -> (clas, tys)
1669 Nothing -> pprPanic "getClassPredTys" (ppr ty)
1670
1671 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
1672 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
1673 Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
1674 _ -> Nothing
1675
1676 getEqPredTys :: PredType -> (Type, Type)
1677 getEqPredTys ty
1678 = case splitTyConApp_maybe ty of
1679 Just (tc, [_, _, ty1, ty2])
1680 | tc `hasKey` eqPrimTyConKey
1681 || tc `hasKey` eqReprPrimTyConKey
1682 -> (ty1, ty2)
1683 _ -> pprPanic "getEqPredTys" (ppr ty)
1684
1685 getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
1686 getEqPredTys_maybe ty
1687 = case splitTyConApp_maybe ty of
1688 Just (tc, [_, _, ty1, ty2])
1689 | tc `hasKey` eqPrimTyConKey -> Just (Nominal, ty1, ty2)
1690 | tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2)
1691 _ -> Nothing
1692
1693 getEqPredRole :: PredType -> Role
1694 getEqPredRole ty = eqRelRole (predTypeEqRel ty)
1695
1696 -- | Get the equality relation relevant for a pred type.
1697 predTypeEqRel :: PredType -> EqRel
1698 predTypeEqRel ty
1699 | Just (tc, _) <- splitTyConApp_maybe ty
1700 , tc `hasKey` eqReprPrimTyConKey
1701 = ReprEq
1702 | otherwise
1703 = NomEq
1704
1705 {-
1706 %************************************************************************
1707 %* *
1708 Size
1709 * *
1710 ************************************************************************
1711 -}
1712
1713 -- NB: This function does not respect `eqType`, in that two types that
1714 -- are `eqType` may return different sizes. This is OK, because this
1715 -- function is used only in reporting, not decision-making.
1716 typeSize :: Type -> Int
1717 typeSize (LitTy {}) = 1
1718 typeSize (TyVarTy {}) = 1
1719 typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2
1720 typeSize (FunTy t1 t2) = typeSize t1 + typeSize t2
1721 typeSize (ForAllTy (TvBndr tv _) t) = typeSize (tyVarKind tv) + typeSize t
1722 typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
1723 typeSize (CastTy ty co) = typeSize ty + coercionSize co
1724 typeSize (CoercionTy co) = coercionSize co
1725
1726
1727 {- **********************************************************************
1728 * *
1729 Representation types
1730 * *
1731 ********************************************************************** -}
1732
1733 type UnaryType = Type
1734
1735 data RepType
1736 = UbxTupleRep [UnaryType] -- Represented by multiple values
1737 -- Can be zero, one, or more
1738 | UnaryRep UnaryType -- Represented by a single value
1739
1740 instance Outputable RepType where
1741 ppr (UbxTupleRep tys) = text "UbxTupleRep" <+> ppr tys
1742 ppr (UnaryRep ty) = text "UnaryRep" <+> ppr ty
1743
1744 flattenRepType :: RepType -> [UnaryType]
1745 flattenRepType (UbxTupleRep tys) = tys
1746 flattenRepType (UnaryRep ty) = [ty]
1747
1748 -- | 'repType' figure out how a type will be represented
1749 -- at runtime. It looks through
1750 --
1751 -- 1. For-alls
1752 -- 2. Synonyms
1753 -- 3. Predicates
1754 -- 4. All newtypes, including recursive ones, but not newtype families
1755 -- 5. Casts
1756 --
1757 repType :: Type -> RepType
1758 repType ty
1759 = go initRecTc ty
1760 where
1761 go :: RecTcChecker -> Type -> RepType
1762 go rec_nts ty -- Expand predicates and synonyms
1763 | Just ty' <- coreView ty
1764 = go rec_nts ty'
1765
1766 go rec_nts (ForAllTy _ ty2) -- Drop type foralls
1767 = go rec_nts ty2
1768
1769 go rec_nts (TyConApp tc tys) -- Expand newtypes
1770 | isNewTyCon tc
1771 , tys `lengthAtLeast` tyConArity tc
1772 , Just rec_nts' <- checkRecTc rec_nts tc -- See Note [Expanding newtypes] in TyCon
1773 = go rec_nts' (newTyConInstRhs tc tys)
1774
1775 | isUnboxedTupleTyCon tc
1776 = UbxTupleRep (concatMap (flattenRepType . go rec_nts) non_rr_tys)
1777 where
1778 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
1779 non_rr_tys = dropRuntimeRepArgs tys
1780
1781 go rec_nts (CastTy ty _)
1782 = go rec_nts ty
1783
1784 go _ ty@(CoercionTy _)
1785 = pprPanic "repType" (ppr ty)
1786
1787 go _ ty = UnaryRep ty
1788
1789 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
1790 -- of inspecting the type directly.
1791
1792 -- | Discovers the primitive representation of a more abstract 'UnaryType'
1793 typePrimRep :: UnaryType -> PrimRep
1794 typePrimRep ty = kindPrimRep (typeKind ty)
1795
1796 -- | Find the primitive representation of a 'TyCon'. Defined here to
1797 -- avoid module loops. Call this only on unlifted tycons.
1798 tyConPrimRep :: TyCon -> PrimRep
1799 tyConPrimRep tc = kindPrimRep res_kind
1800 where
1801 res_kind = tyConResKind tc
1802
1803 -- | Take a kind (of shape @TYPE rr@) and produce the 'PrimRep' of values
1804 -- of types of this kind.
1805 kindPrimRep :: Kind -> PrimRep
1806 kindPrimRep ki | Just ki' <- coreViewOneStarKind ki = kindPrimRep ki'
1807 kindPrimRep (TyConApp typ [runtime_rep])
1808 = ASSERT( typ `hasKey` tYPETyConKey )
1809 go runtime_rep
1810 where
1811 go rr | Just rr' <- coreView rr = go rr'
1812 go (TyConApp rr_dc args)
1813 | RuntimeRep fun <- tyConRuntimeRepInfo rr_dc
1814 = fun args
1815 go rr = pprPanic "kindPrimRep.go" (ppr rr)
1816 kindPrimRep ki = WARN( True
1817 , text "kindPrimRep defaulting to PtrRep on" <+> ppr ki )
1818 PtrRep -- this can happen legitimately for, e.g., Any
1819
1820 typeRepArity :: Arity -> Type -> RepArity
1821 typeRepArity 0 _ = 0
1822 typeRepArity n ty = case repType ty of
1823 UnaryRep (FunTy arg res) -> length (flattenRepType (repType arg)) + typeRepArity (n - 1) res
1824 _ -> pprPanic "typeRepArity: arity greater than type can handle" (ppr (n, ty, repType ty))
1825
1826 isVoidTy :: Type -> Bool
1827 -- True if the type has zero width
1828 isVoidTy ty = case repType ty of
1829 UnaryRep (TyConApp tc _) -> isUnliftedTyCon tc &&
1830 isVoidRep (tyConPrimRep tc)
1831 _ -> False
1832
1833
1834 {-
1835 %************************************************************************
1836 %* *
1837 Well-scoped tyvars
1838 * *
1839 ************************************************************************
1840 -}
1841
1842 -- | Do a topological sort on a list of tyvars,
1843 -- so that binders occur before occurrences
1844 -- E.g. given [ a::k, k::*, b::k ]
1845 -- it'll return a well-scoped list [ k::*, a::k, b::k ]
1846 --
1847 -- This is a deterministic sorting operation
1848 -- (that is, doesn't depend on Uniques).
1849 toposortTyVars :: [TyVar] -> [TyVar]
1850 toposortTyVars tvs = reverse $
1851 [ tv | (tv, _, _) <- topologicalSortG $
1852 graphFromEdgedVerticesOrd nodes ]
1853 where
1854 var_ids :: VarEnv Int
1855 var_ids = mkVarEnv (zip tvs [1..])
1856
1857 nodes = [ ( tv
1858 , lookupVarEnv_NF var_ids tv
1859 , mapMaybe (lookupVarEnv var_ids)
1860 (tyCoVarsOfTypeList (tyVarKind tv)) )
1861 | tv <- tvs ]
1862
1863 -- | Extract a well-scoped list of variables from a deterministic set of
1864 -- variables. The result is deterministic.
1865 -- NB: There used to exist varSetElemsWellScoped :: VarSet -> [Var] which
1866 -- took a non-deterministic set and produced a non-deterministic
1867 -- well-scoped list. If you care about the list being well-scoped you also
1868 -- most likely care about it being in deterministic order.
1869 dVarSetElemsWellScoped :: DVarSet -> [Var]
1870 dVarSetElemsWellScoped = toposortTyVars . dVarSetElems
1871
1872 -- | Get the free vars of a type in scoped order
1873 tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
1874 tyCoVarsOfTypeWellScoped = toposortTyVars . tyCoVarsOfTypeList
1875
1876 -- | Get the free vars of types in scoped order
1877 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
1878 tyCoVarsOfTypesWellScoped = toposortTyVars . tyCoVarsOfTypesList
1879
1880 {-
1881 ************************************************************************
1882 * *
1883 \subsection{Type families}
1884 * *
1885 ************************************************************************
1886 -}
1887
1888 mkFamilyTyConApp :: TyCon -> [Type] -> Type
1889 -- ^ Given a family instance TyCon and its arg types, return the
1890 -- corresponding family type. E.g:
1891 --
1892 -- > data family T a
1893 -- > data instance T (Maybe b) = MkT b
1894 --
1895 -- Where the instance tycon is :RTL, so:
1896 --
1897 -- > mkFamilyTyConApp :RTL Int = T (Maybe Int)
1898 mkFamilyTyConApp tc tys
1899 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
1900 , let tvs = tyConTyVars tc
1901 fam_subst = ASSERT2( length tvs == length tys, ppr tc <+> ppr tys )
1902 zipTvSubst tvs tys
1903 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
1904 | otherwise
1905 = mkTyConApp tc tys
1906
1907 -- | Get the type on the LHS of a coercion induced by a type/data
1908 -- family instance.
1909 coAxNthLHS :: CoAxiom br -> Int -> Type
1910 coAxNthLHS ax ind =
1911 mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind))
1912
1913 -- | Pretty prints a 'TyCon', using the family instance in case of a
1914 -- representation tycon. For example:
1915 --
1916 -- > data T [a] = ...
1917 --
1918 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
1919 pprSourceTyCon :: TyCon -> SDoc
1920 pprSourceTyCon tycon
1921 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
1922 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
1923 | otherwise
1924 = ppr tycon
1925
1926 {-
1927 ************************************************************************
1928 * *
1929 \subsection{Liftedness}
1930 * *
1931 ************************************************************************
1932 -}
1933
1934 -- | See "Type#type_classification" for what an unlifted type is
1935 isUnliftedType :: Type -> Bool
1936 -- isUnliftedType returns True for forall'd unlifted types:
1937 -- x :: forall a. Int#
1938 -- I found bindings like these were getting floated to the top level.
1939 -- They are pretty bogus types, mind you. It would be better never to
1940 -- construct them
1941
1942 isUnliftedType ty | Just ty' <- coreView ty = isUnliftedType ty'
1943 isUnliftedType (ForAllTy _ ty) = isUnliftedType ty
1944 isUnliftedType (TyConApp tc _) = isUnliftedTyCon tc
1945 isUnliftedType _ = False
1946
1947 -- | Extract the RuntimeRep classifier of a type. Panics if this is not possible.
1948 getRuntimeRep :: String -- ^ Printed in case of an error
1949 -> Type -> Type
1950 getRuntimeRep err ty = getRuntimeRepFromKind err (typeKind ty)
1951
1952 -- | Extract the RuntimeRep classifier of a type from its kind.
1953 -- For example, getRuntimeRepFromKind * = PtrRepLifted;
1954 -- getRuntimeRepFromKind # = PtrRepUnlifted.
1955 -- Panics if this is not possible.
1956 getRuntimeRepFromKind :: String -- ^ Printed in case of an error
1957 -> Type -> Type
1958 getRuntimeRepFromKind err = go
1959 where
1960 go k | Just k' <- coreViewOneStarKind k = go k'
1961 go k
1962 | Just (tc, [arg]) <- splitTyConApp_maybe k
1963 , tc `hasKey` tYPETyConKey
1964 = arg
1965 go k = pprPanic "getRuntimeRep" (text err $$
1966 ppr k <+> dcolon <+> ppr (typeKind k))
1967
1968 isUnboxedTupleType :: Type -> Bool
1969 isUnboxedTupleType ty = case tyConAppTyCon_maybe ty of
1970 Just tc -> isUnboxedTupleTyCon tc
1971 _ -> False
1972
1973 -- | See "Type#type_classification" for what an algebraic type is.
1974 -- Should only be applied to /types/, as opposed to e.g. partially
1975 -- saturated type constructors
1976 isAlgType :: Type -> Bool
1977 isAlgType ty
1978 = case splitTyConApp_maybe ty of
1979 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1980 isAlgTyCon tc
1981 _other -> False
1982
1983 -- | See "Type#type_classification" for what an algebraic type is.
1984 -- Should only be applied to /types/, as opposed to e.g. partially
1985 -- saturated type constructors. Closed type constructors are those
1986 -- with a fixed right hand side, as opposed to e.g. associated types
1987 isClosedAlgType :: Type -> Bool
1988 isClosedAlgType ty
1989 = case splitTyConApp_maybe ty of
1990 Just (tc, ty_args) | isAlgTyCon tc && not (isFamilyTyCon tc)
1991 -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
1992 _other -> False
1993
1994 -- | Computes whether an argument (or let right hand side) should
1995 -- be computed strictly or lazily, based only on its type.
1996 -- Currently, it's just 'isUnliftedType'.
1997
1998 isStrictType :: Type -> Bool
1999 isStrictType = isUnliftedType
2000
2001 isPrimitiveType :: Type -> Bool
2002 -- ^ Returns true of types that are opaque to Haskell.
2003 isPrimitiveType ty = case splitTyConApp_maybe ty of
2004 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
2005 isPrimTyCon tc
2006 _ -> False
2007
2008 {-
2009 ************************************************************************
2010 * *
2011 \subsection{Sequencing on types}
2012 * *
2013 ************************************************************************
2014 -}
2015
2016 seqType :: Type -> ()
2017 seqType (LitTy n) = n `seq` ()
2018 seqType (TyVarTy tv) = tv `seq` ()
2019 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
2020 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
2021 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
2022 seqType (ForAllTy (TvBndr tv _) ty) = seqType (tyVarKind tv) `seq` seqType ty
2023 seqType (CastTy ty co) = seqType ty `seq` seqCo co
2024 seqType (CoercionTy co) = seqCo co
2025
2026 seqTypes :: [Type] -> ()
2027 seqTypes [] = ()
2028 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
2029
2030 {-
2031 ************************************************************************
2032 * *
2033 Comparison for types
2034 (We don't use instances so that we know where it happens)
2035 * *
2036 ************************************************************************
2037
2038 Note [Equality on AppTys]
2039 ~~~~~~~~~~~~~~~~~~~~~~~~~
2040 In our cast-ignoring equality, we want to say that the following two
2041 are equal:
2042
2043 (Maybe |> co) (Int |> co') ~? Maybe Int
2044
2045 But the left is an AppTy while the right is a TyConApp. The solution is
2046 to use repSplitAppTy_maybe to break up the TyConApp into its pieces and
2047 then continue. Easy to do, but also easy to forget to do.
2048
2049 -}
2050
2051 eqType :: Type -> Type -> Bool
2052 -- ^ Type equality on source types. Does not look through @newtypes@ or
2053 -- 'PredType's, but it does look through type synonyms.
2054 -- This first checks that the kinds of the types are equal and then
2055 -- checks whether the types are equal, ignoring casts and coercions.
2056 -- (The kind check is a recursive call, but since all kinds have type
2057 -- @Type@, there is no need to check the types of kinds.)
2058 -- See also Note [Non-trivial definitional equality] in TyCoRep.
2059 eqType t1 t2 = isEqual $ nonDetCmpType t1 t2
2060 -- It's OK to use nonDetCmpType here and eqType is deterministic,
2061 -- nonDetCmpType does equality deterministically
2062
2063 -- | Compare types with respect to a (presumably) non-empty 'RnEnv2'.
2064 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
2065 eqTypeX env t1 t2 = isEqual $ nonDetCmpTypeX env t1 t2
2066 -- It's OK to use nonDetCmpType here and eqTypeX is deterministic,
2067 -- nonDetCmpTypeX does equality deterministically
2068
2069 -- | Type equality on lists of types, looking through type synonyms
2070 -- but not newtypes.
2071 eqTypes :: [Type] -> [Type] -> Bool
2072 eqTypes tys1 tys2 = isEqual $ nonDetCmpTypes tys1 tys2
2073 -- It's OK to use nonDetCmpType here and eqTypes is deterministic,
2074 -- nonDetCmpTypes does equality deterministically
2075
2076 eqVarBndrs :: RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
2077 -- Check that the var lists are the same length
2078 -- and have matching kinds; if so, extend the RnEnv2
2079 -- Returns Nothing if they don't match
2080 eqVarBndrs env [] []
2081 = Just env
2082 eqVarBndrs env (tv1:tvs1) (tv2:tvs2)
2083 | eqTypeX env (tyVarKind tv1) (tyVarKind tv2)
2084 = eqVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
2085 eqVarBndrs _ _ _= Nothing
2086
2087 -- Now here comes the real worker
2088
2089 {-
2090 Note [nonDetCmpType nondeterminism]
2091 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2092 nonDetCmpType is implemented in terms of nonDetCmpTypeX. nonDetCmpTypeX
2093 uses nonDetCmpTc which compares TyCons by their Unique value. Using Uniques for
2094 ordering leads to nondeterminism. We hit the same problem in the TyVarTy case,
2095 comparing type variables is nondeterministic, note the call to nonDetCmpVar in
2096 nonDetCmpTypeX.
2097 See Note [Unique Determinism] for more details.
2098 -}
2099
2100 nonDetCmpType :: Type -> Type -> Ordering
2101 nonDetCmpType t1 t2
2102 -- we know k1 and k2 have the same kind, because they both have kind *.
2103 = nonDetCmpTypeX rn_env t1 t2
2104 where
2105 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes [t1, t2]))
2106
2107 nonDetCmpTypes :: [Type] -> [Type] -> Ordering
2108 nonDetCmpTypes ts1 ts2 = nonDetCmpTypesX rn_env ts1 ts2
2109 where
2110 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes (ts1 ++ ts2)))
2111
2112 -- | An ordering relation between two 'Type's (known below as @t1 :: k1@
2113 -- and @t2 :: k2@)
2114 data TypeOrdering = TLT -- ^ @t1 < t2@
2115 | TEQ -- ^ @t1 ~ t2@ and there are no casts in either,
2116 -- therefore we can conclude @k1 ~ k2@
2117 | TEQX -- ^ @t1 ~ t2@ yet one of the types contains a cast so
2118 -- they may differ in kind.
2119 | TGT -- ^ @t1 > t2@
2120 deriving (Eq, Ord, Enum, Bounded)
2121
2122 nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
2123 -- See Note [Non-trivial definitional equality] in TyCoRep
2124 nonDetCmpTypeX env orig_t1 orig_t2 =
2125 case go env orig_t1 orig_t2 of
2126 -- If there are casts then we also need to do a comparison of the kinds of
2127 -- the types being compared
2128 TEQX -> toOrdering $ go env k1 k2
2129 ty_ordering -> toOrdering ty_ordering
2130 where
2131 k1 = typeKind orig_t1
2132 k2 = typeKind orig_t2
2133
2134 toOrdering :: TypeOrdering -> Ordering
2135 toOrdering TLT = LT
2136 toOrdering TEQ = EQ
2137 toOrdering TEQX = EQ
2138 toOrdering TGT = GT
2139
2140 liftOrdering :: Ordering -> TypeOrdering
2141 liftOrdering LT = TLT
2142 liftOrdering EQ = TEQ
2143 liftOrdering GT = TGT
2144
2145 thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering
2146 thenCmpTy TEQ rel = rel
2147 thenCmpTy TEQX rel = hasCast rel
2148 thenCmpTy rel _ = rel
2149
2150 hasCast :: TypeOrdering -> TypeOrdering
2151 hasCast TEQ = TEQX
2152 hasCast rel = rel
2153
2154 -- Returns both the resulting ordering relation between the two types
2155 -- and whether either contains a cast.
2156 go :: RnEnv2 -> Type -> Type -> TypeOrdering
2157 go env t1 t2
2158 | Just t1' <- coreViewOneStarKind t1 = go env t1' t2
2159 | Just t2' <- coreViewOneStarKind t2 = go env t1 t2'
2160
2161 go env (TyVarTy tv1) (TyVarTy tv2)
2162 = liftOrdering $ rnOccL env tv1 `nonDetCmpVar` rnOccR env tv2
2163 go env (ForAllTy (TvBndr tv1 _) t1) (ForAllTy (TvBndr tv2 _) t2)
2164 = go env (tyVarKind tv1) (tyVarKind tv2)
2165 `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2
2166 -- See Note [Equality on AppTys]
2167 go env (AppTy s1 t1) ty2
2168 | Just (s2, t2) <- repSplitAppTy_maybe ty2
2169 = go env s1 s2 `thenCmpTy` go env t1 t2
2170 go env ty1 (AppTy s2 t2)
2171 | Just (s1, t1) <- repSplitAppTy_maybe ty1
2172 = go env s1 s2 `thenCmpTy` go env t1 t2
2173 go env (FunTy s1 t1) (FunTy s2 t2)
2174 = go env s1 s2 `thenCmpTy` go env t1 t2
2175 go env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2176 = liftOrdering (tc1 `nonDetCmpTc` tc2) `thenCmpTy` gos env tys1 tys2
2177 go _ (LitTy l1) (LitTy l2) = liftOrdering (compare l1 l2)
2178 go env (CastTy t1 _) t2 = hasCast $ go env t1 t2
2179 go env t1 (CastTy t2 _) = hasCast $ go env t1 t2
2180 go _ (CoercionTy {}) (CoercionTy {}) = TEQ
2181
2182 -- Deal with the rest: TyVarTy < CoercionTy < AppTy < LitTy < TyConApp < ForAllTy
2183 go _ ty1 ty2
2184 = liftOrdering $ (get_rank ty1) `compare` (get_rank ty2)
2185 where get_rank :: Type -> Int
2186 get_rank (CastTy {})
2187 = pprPanic "nonDetCmpTypeX.get_rank" (ppr [ty1,ty2])
2188 get_rank (TyVarTy {}) = 0
2189 get_rank (CoercionTy {}) = 1
2190 get_rank (AppTy {}) = 3
2191 get_rank (LitTy {}) = 4
2192 get_rank (TyConApp {}) = 5
2193 get_rank (FunTy {}) = 6
2194 get_rank (ForAllTy {}) = 7
2195
2196 gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering
2197 gos _ [] [] = TEQ
2198 gos _ [] _ = TLT
2199 gos _ _ [] = TGT
2200 gos env (ty1:tys1) (ty2:tys2) = go env ty1 ty2 `thenCmpTy` gos env tys1 tys2
2201
2202 -------------
2203 nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
2204 nonDetCmpTypesX _ [] [] = EQ
2205 nonDetCmpTypesX env (t1:tys1) (t2:tys2) = nonDetCmpTypeX env t1 t2
2206 `thenCmp` nonDetCmpTypesX env tys1 tys2
2207 nonDetCmpTypesX _ [] _ = LT
2208 nonDetCmpTypesX _ _ [] = GT
2209
2210 -------------
2211 -- | Compare two 'TyCon's. NB: This should /never/ see the "star synonyms",
2212 -- as recognized by Kind.isStarKindSynonymTyCon. See Note
2213 -- [Kind Constraint and kind *] in Kind.
2214 -- See Note [nonDetCmpType nondeterminism]
2215 nonDetCmpTc :: TyCon -> TyCon -> Ordering
2216 nonDetCmpTc tc1 tc2
2217 = ASSERT( not (isStarKindSynonymTyCon tc1) && not (isStarKindSynonymTyCon tc2) )
2218 u1 `nonDetCmpUnique` u2
2219 where
2220 u1 = tyConUnique tc1
2221 u2 = tyConUnique tc2
2222
2223 {-
2224 ************************************************************************
2225 * *
2226 The kind of a type
2227 * *
2228 ************************************************************************
2229 -}
2230
2231 typeKind :: Type -> Kind
2232 typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
2233 typeKind (AppTy fun arg) = piResultTy (typeKind fun) arg
2234 typeKind (LitTy l) = typeLiteralKind l
2235 typeKind (FunTy {}) = liftedTypeKind
2236 typeKind (ForAllTy _ ty) = typeKind ty
2237 typeKind (TyVarTy tyvar) = tyVarKind tyvar
2238 typeKind (CastTy _ty co) = pSnd $ coercionKind co
2239 typeKind (CoercionTy co) = coercionType co
2240
2241 typeLiteralKind :: TyLit -> Kind
2242 typeLiteralKind l =
2243 case l of
2244 NumTyLit _ -> typeNatKind
2245 StrTyLit _ -> typeSymbolKind
2246
2247 -- | Print a tyvar with its kind
2248 pprTyVar :: TyVar -> SDoc
2249 pprTyVar tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
2250
2251 {-
2252 %************************************************************************
2253 %* *
2254 Miscellaneous functions
2255 %* *
2256 %************************************************************************
2257
2258 -}
2259 -- | All type constructors occurring in the type; looking through type
2260 -- synonyms, but not newtypes.
2261 -- When it finds a Class, it returns the class TyCon.
2262 tyConsOfType :: Type -> NameEnv TyCon
2263 tyConsOfType ty
2264 = go ty
2265 where
2266 go :: Type -> NameEnv TyCon -- The NameEnv does duplicate elim
2267 go ty | Just ty' <- coreView ty = go ty'
2268 go (TyVarTy {}) = emptyNameEnv
2269 go (LitTy {}) = emptyNameEnv
2270 go (TyConApp tc tys) = go_tc tc `plusNameEnv` go_s tys
2271 go (AppTy a b) = go a `plusNameEnv` go b
2272 go (FunTy a b) = go a `plusNameEnv` go b `plusNameEnv` go_tc funTyCon
2273 go (ForAllTy (TvBndr tv _) ty) = go ty `plusNameEnv` go (tyVarKind tv)
2274 go (CastTy ty co) = go ty `plusNameEnv` go_co co
2275 go (CoercionTy co) = go_co co
2276
2277 go_co (Refl _ ty) = go ty
2278 go_co (TyConAppCo _ tc args) = go_tc tc `plusNameEnv` go_cos args
2279 go_co (AppCo co arg) = go_co co `plusNameEnv` go_co arg
2280 go_co (ForAllCo _ kind_co co) = go_co kind_co `plusNameEnv` go_co co
2281 go_co (CoVarCo {}) = emptyNameEnv
2282 go_co (AxiomInstCo ax _ args) = go_ax ax `plusNameEnv` go_cos args
2283 go_co (UnivCo p _ t1 t2) = go_prov p `plusNameEnv` go t1 `plusNameEnv` go t2
2284 go_co (SymCo co) = go_co co
2285 go_co (TransCo co1 co2) = go_co co1 `plusNameEnv` go_co co2
2286 go_co (NthCo _ co) = go_co co
2287 go_co (LRCo _ co) = go_co co
2288 go_co (InstCo co arg) = go_co co `plusNameEnv` go_co arg
2289 go_co (CoherenceCo co1 co2) = go_co co1 `plusNameEnv` go_co co2
2290 go_co (KindCo co) = go_co co
2291 go_co (SubCo co) = go_co co
2292 go_co (AxiomRuleCo _ cs) = go_cos cs
2293
2294 go_prov UnsafeCoerceProv = emptyNameEnv
2295 go_prov (PhantomProv co) = go_co co
2296 go_prov (ProofIrrelProv co) = go_co co
2297 go_prov (PluginProv _) = emptyNameEnv
2298 go_prov (HoleProv _) = emptyNameEnv
2299 -- this last case can happen from the tyConsOfType used from
2300 -- checkTauTvUpdate
2301
2302 go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
2303 go_cos cos = foldr (plusNameEnv . go_co) emptyNameEnv cos
2304
2305 go_tc tc = unitNameEnv (tyConName tc) tc
2306 go_ax ax = go_tc $ coAxiomTyCon ax
2307
2308 -- | Find the result 'Kind' of a type synonym,
2309 -- after applying it to its 'arity' number of type variables
2310 -- Actually this function works fine on data types too,
2311 -- but they'd always return '*', so we never need to ask
2312 synTyConResKind :: TyCon -> Kind
2313 synTyConResKind tycon = piResultTys (tyConKind tycon) (mkTyVarTys (tyConTyVars tycon))
2314
2315 -- | Retrieve the free variables in this type, splitting them based
2316 -- on whether they are used visibly or invisibly. Invisible ones come
2317 -- first.
2318 splitVisVarsOfType :: Type -> Pair TyCoVarSet
2319 splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
2320 where
2321 Pair invis_vars1 vis_vars = go orig_ty
2322 invis_vars = invis_vars1 `minusVarSet` vis_vars
2323
2324 go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv)
2325 go (AppTy t1 t2) = go t1 `mappend` go t2
2326 go (TyConApp tc tys) = go_tc tc tys
2327 go (FunTy t1 t2) = go t1 `mappend` go t2
2328 go (ForAllTy (TvBndr tv _) ty)
2329 = ((`delVarSet` tv) <$> go ty) `mappend`
2330 (invisible (tyCoVarsOfType $ tyVarKind tv))
2331 go (LitTy {}) = mempty
2332 go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co)
2333 go (CoercionTy co) = invisible $ tyCoVarsOfCo co
2334
2335 invisible vs = Pair vs emptyVarSet
2336
2337 go_tc tc tys = let (invis, vis) = partitionInvisibles tc id tys in
2338 invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis
2339
2340 splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
2341 splitVisVarsOfTypes = foldMap splitVisVarsOfType