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