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