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