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