f5f7532075389c7dd3fa1d61533edd7ea3ff292a
[ghc.git] / compiler / typecheck / TcType.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5 \section[TcType]{Types used in the typechecker}
6
7 This module provides the Type interface for front-end parts of the
8 compiler. These parts
9
10 * treat "source types" as opaque:
11 newtypes, and predicates are meaningful.
12 * look through usage types
13
14 The "tc" prefix is for "TypeChecker", because the type checker
15 is the principal client.
16 -}
17
18 {-# LANGUAGE CPP, ScopedTypeVariables, MultiWayIf, FlexibleContexts #-}
19
20 module TcType (
21 --------------------------------
22 -- Types
23 TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
24 TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
25 TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcTyCon,
26
27 ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType,
28
29 SyntaxOpType(..), synKnownType, mkSynFunTys,
30
31 -- TcLevel
32 TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel,
33 strictlyDeeperThan, sameDepthAs,
34 tcTypeLevel, tcTyVarLevel, maxTcLevel,
35 promoteSkolem, promoteSkolemX, promoteSkolemsX,
36 --------------------------------
37 -- MetaDetails
38 UserTypeCtxt(..), pprUserTypeCtxt, isSigMaybe,
39 TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
40 MetaDetails(Flexi, Indirect), MetaInfo(..),
41 isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy,
42 isSigTyVar, isOverlappableTyVar, isTyConableTyVar,
43 isFskTyVar, isFmvTyVar, isFlattenTyVar,
44 isAmbiguousTyVar, metaTyVarRef, metaTyVarInfo,
45 isFlexi, isIndirect, isRuntimeUnkSkol,
46 metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
47 isTouchableMetaTyVar,
48 isFloatedTouchableMetaTyVar,
49 findDupSigTvs, mkTyVarNamePairs,
50
51 --------------------------------
52 -- Builders
53 mkPhiTy, mkInfSigmaTy, mkSpecSigmaTy, mkSigmaTy,
54 mkNakedTyConApp, mkNakedAppTys, mkNakedAppTy,
55 mkNakedCastTy,
56
57 --------------------------------
58 -- Splitters
59 -- These are important because they do not look through newtypes
60 getTyVar,
61 tcSplitForAllTy_maybe,
62 tcSplitForAllTys, tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllTyVarBndrs,
63 tcSplitPhiTy, tcSplitPredFunTy_maybe,
64 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN,
65 tcSplitFunTysN,
66 tcSplitTyConApp, tcSplitTyConApp_maybe,
67 tcRepSplitTyConApp_maybe, tcRepSplitTyConApp_maybe',
68 tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
69 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
70 tcRepGetNumAppTys,
71 tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar, nextRole,
72 tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe,
73
74 ---------------------------------
75 -- Predicates.
76 -- Again, newtypes are opaque
77 eqType, eqTypes, nonDetCmpType, nonDetCmpTypes, eqTypeX,
78 pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck, tcEqTypeVis,
79 isSigmaTy, isRhoTy, isRhoExpTy, isOverloadedTy,
80 isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
81 isIntegerTy, isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred,
82 hasIPPred, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
83 isPredTy, isTyVarClassPred, isTyVarHead, isInsolubleOccursCheck,
84 checkValidClsArgs, hasTyVarHead,
85 isRigidTy,
86
87 ---------------------------------
88 -- Misc type manipulators
89
90 deNoteType,
91 orphNamesOfType, orphNamesOfCo,
92 orphNamesOfTypes, orphNamesOfCoCon,
93 getDFunTyKey,
94 evVarPred_maybe, evVarPred,
95
96 ---------------------------------
97 -- Predicate types
98 mkMinimalBySCs, transSuperClasses,
99 pickQuantifiablePreds, pickCapturedPreds,
100 immSuperClasses,
101 isImprovementPred,
102
103 -- * Finding type instances
104 tcTyFamInsts, isTyFamFree,
105
106 -- * Finding "exact" (non-dead) type variables
107 exactTyCoVarsOfType, exactTyCoVarsOfTypes,
108 candidateQTyVarsOfType, candidateQTyVarsOfTypes, CandidatesQTvs(..),
109 anyRewritableTyVar,
110
111 ---------------------------------
112 -- Foreign import and export
113 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
114 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
115 isFFIExportResultTy, -- :: Type -> Bool
116 isFFIExternalTy, -- :: Type -> Bool
117 isFFIDynTy, -- :: Type -> Type -> Bool
118 isFFIPrimArgumentTy, -- :: DynFlags -> Type -> Bool
119 isFFIPrimResultTy, -- :: DynFlags -> Type -> Bool
120 isFFILabelTy, -- :: Type -> Bool
121 isFFITy, -- :: Type -> Bool
122 isFunPtrTy, -- :: Type -> Bool
123 tcSplitIOType_maybe, -- :: Type -> Maybe Type
124
125 --------------------------------
126 -- Rexported from Kind
127 Kind, typeKind,
128 liftedTypeKind,
129 constraintKind,
130 isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues,
131
132 --------------------------------
133 -- Rexported from Type
134 Type, PredType, ThetaType, TyBinder, ArgFlag(..),
135
136 mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys, mkInvForAllTy,
137 mkFunTy, mkFunTys,
138 mkTyConApp, mkAppTy, mkAppTys,
139 mkTyConTy, mkTyVarTy,
140 mkTyVarTys,
141
142 isClassPred, isEqPred, isNomEqPred, isIPPred,
143 mkClassPred,
144 isDictLikeTy,
145 tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
146 isRuntimeRepVar, isKindLevPoly,
147 isVisibleBinder, isInvisibleBinder,
148
149 -- Type substitutions
150 TCvSubst(..), -- Representation visible to a few friends
151 TvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
152 zipTvSubst,
153 mkTvSubstPrs, notElemTCvSubst, unionTCvSubst,
154 getTvSubstEnv, setTvSubstEnv, getTCvInScope, extendTCvInScope,
155 extendTCvInScopeList, extendTCvInScopeSet, extendTvSubstAndInScope,
156 Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
157 Type.extendTvSubst,
158 isInScope, mkTCvSubst, mkTvSubst, zipTyEnv, zipCoEnv,
159 Type.substTy, substTys, substTyWith, substTyWithCoVars,
160 substTyAddInScope,
161 substTyUnchecked, substTysUnchecked, substThetaUnchecked,
162 substTyWithUnchecked,
163 substCoUnchecked, substCoWithUnchecked,
164 substTheta,
165
166 isUnliftedType, -- Source types are always lifted
167 isUnboxedTupleType, -- Ditto
168 isPrimitiveType,
169
170 tcView, coreView,
171
172 tyCoVarsOfType, tyCoVarsOfTypes, closeOverKinds,
173 tyCoFVsOfType, tyCoFVsOfTypes,
174 tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet, closeOverKindsDSet,
175 tyCoVarsOfTypeList, tyCoVarsOfTypesList,
176 noFreeVarsOfType,
177
178 --------------------------------
179 pprKind, pprParendKind, pprSigmaType,
180 pprType, pprParendType, pprTypeApp, pprTyThingCategory, tyThingCategory,
181 pprTheta, pprParendTheta, pprThetaArrowTy, pprClassPred,
182 pprTvBndr, pprTvBndrs,
183
184 TypeSize, sizeType, sizeTypes, toposortTyVars,
185
186 ---------------------------------
187 -- argument visibility
188 tcTyConVisibilities, isNextTyConArgVisible, isNextArgVisible
189
190 ) where
191
192 #include "HsVersions.h"
193
194 -- friends:
195 import GhcPrelude
196
197 import Kind
198 import TyCoRep
199 import Class
200 import Var
201 import ForeignCall
202 import VarSet
203 import Coercion
204 import Type
205 import RepType
206 import TyCon
207
208 -- others:
209 import DynFlags
210 import CoreFVs
211 import Name -- hiding (varName)
212 -- We use this to make dictionaries for type literals.
213 -- Perhaps there's a better way to do this?
214 import NameSet
215 import VarEnv
216 import PrelNames
217 import TysWiredIn( coercibleClass, unitTyCon, unitTyConKey
218 , listTyCon, constraintKind )
219 import BasicTypes
220 import Util
221 import Maybes
222 import ListSetOps ( getNth, findDupsEq )
223 import Outputable
224 import FastString
225 import ErrUtils( Validity(..), MsgDoc, isValid )
226 import qualified GHC.LanguageExtensions as LangExt
227
228 import Data.List ( mapAccumL )
229 import Data.IORef
230 import Data.List.NonEmpty( NonEmpty(..) )
231 import qualified Data.Semigroup as Semi
232
233 {-
234 ************************************************************************
235 * *
236 Types
237 * *
238 ************************************************************************
239
240 The type checker divides the generic Type world into the
241 following more structured beasts:
242
243 sigma ::= forall tyvars. phi
244 -- A sigma type is a qualified type
245 --
246 -- Note that even if 'tyvars' is empty, theta
247 -- may not be: e.g. (?x::Int) => Int
248
249 -- Note that 'sigma' is in prenex form:
250 -- all the foralls are at the front.
251 -- A 'phi' type has no foralls to the right of
252 -- an arrow
253
254 phi :: theta => rho
255
256 rho ::= sigma -> rho
257 | tau
258
259 -- A 'tau' type has no quantification anywhere
260 -- Note that the args of a type constructor must be taus
261 tau ::= tyvar
262 | tycon tau_1 .. tau_n
263 | tau_1 tau_2
264 | tau_1 -> tau_2
265
266 -- In all cases, a (saturated) type synonym application is legal,
267 -- provided it expands to the required form.
268
269 Note [TcTyVars and TyVars in the typechecker]
270 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
271 The typechecker uses a lot of type variables with special properties,
272 notably being a unification variable with a mutable reference. These
273 use the 'TcTyVar' variant of Var.Var.
274
275 Note, though, that a /bound/ type variable can (and probably should)
276 be a TyVar. E.g
277 forall a. a -> a
278 Here 'a' is really just a deBruijn-number; it certainly does not have
279 a signficant TcLevel (as every TcTyVar does). So a forall-bound type
280 variable should be TyVars; and hence a TyVar can appear free in a TcType.
281
282 The type checker and constraint solver can also encounter /free/ type
283 variables that use the 'TyVar' variant of Var.Var, for a couple of
284 reasons:
285
286 - When typechecking a class decl, say
287 class C (a :: k) where
288 foo :: T a -> Int
289 We have first kind-check the header; fix k and (a:k) to be
290 TyVars, bring 'k' and 'a' into scope, and kind check the
291 signature for 'foo'. In doing so we call solveEqualities to
292 solve any kind equalities in foo's signature. So the solver
293 may see free occurrences of 'k'.
294
295 See calls to tcExtendTyVarEnv for other places that ordinary
296 TyVars are bought into scope, and hence may show up in the types
297 and kinds generated by TcHsType.
298
299 - The pattern-match overlap checker calls the constraint solver,
300 long afer TcTyVars have been zonked away
301
302 It's convenient to simply treat these TyVars as skolem constants,
303 which of course they are. We give them a level number of "outermost",
304 so they behave as global constants. Specifically:
305
306 * Var.tcTyVarDetails succeeds on a TyVar, returning
307 vanillaSkolemTv, as well as on a TcTyVar.
308
309 * tcIsTcTyVar returns True for both TyVar and TcTyVar variants
310 of Var.Var. The "tc" prefix means "a type variable that can be
311 encountered by the typechecker".
312
313 This is a bit of a change from an earlier era when we remoselessly
314 insisted on real TcTyVars in the type checker. But that seems
315 unnecessary (for skolems, TyVars are fine) and it's now very hard
316 to guarantee, with the advent of kind equalities.
317
318 Note [Coercion variables in free variable lists]
319 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
320 There are several places in the GHC codebase where functions like
321 tyCoVarsOfType, tyCoVarsOfCt, et al. are used to compute the free type
322 variables of a type. The "Co" part of these functions' names shouldn't be
323 dismissed, as it is entirely possible that they will include coercion variables
324 in addition to type variables! As a result, there are some places in TcType
325 where we must take care to check that a variable is a _type_ variable (using
326 isTyVar) before calling tcTyVarDetails--a partial function that is not defined
327 for coercion variables--on the variable. Failing to do so led to
328 GHC Trac #12785.
329 -}
330
331 -- See Note [TcTyVars and TyVars in the typechecker]
332 type TcCoVar = CoVar -- Used only during type inference
333 type TcType = Type -- A TcType can have mutable type variables
334 type TcTyCoVar = Var -- Either a TcTyVar or a CoVar
335 -- Invariant on ForAllTy in TcTypes:
336 -- forall a. T
337 -- a cannot occur inside a MutTyVar in T; that is,
338 -- T is "flattened" before quantifying over a
339
340 type TcTyVarBinder = TyVarBinder
341 type TcTyCon = TyCon -- these can be the TcTyCon constructor
342
343 -- These types do not have boxy type variables in them
344 type TcPredType = PredType
345 type TcThetaType = ThetaType
346 type TcSigmaType = TcType
347 type TcRhoType = TcType -- Note [TcRhoType]
348 type TcTauType = TcType
349 type TcKind = Kind
350 type TcTyVarSet = TyVarSet
351 type TcTyCoVarSet = TyCoVarSet
352 type TcDTyVarSet = DTyVarSet
353 type TcDTyCoVarSet = DTyCoVarSet
354
355
356 {- *********************************************************************
357 * *
358 ExpType: an "expected type" in the type checker
359 * *
360 ********************************************************************* -}
361
362 -- | An expected type to check against during type-checking.
363 -- See Note [ExpType] in TcMType, where you'll also find manipulators.
364 data ExpType = Check TcType
365 | Infer !InferResult
366
367 data InferResult
368 = IR { ir_uniq :: Unique -- For debugging only
369 , ir_lvl :: TcLevel -- See Note [TcLevel of ExpType] in TcMType
370 , ir_inst :: Bool -- True <=> deeply instantiate before returning
371 -- i.e. return a RhoType
372 -- False <=> do not instantiate before returning
373 -- i.e. return a SigmaType
374 , ir_ref :: IORef (Maybe TcType) }
375 -- The type that fills in this hole should be a Type,
376 -- that is, its kind should be (TYPE rr) for some rr
377
378 type ExpSigmaType = ExpType
379 type ExpRhoType = ExpType
380
381 instance Outputable ExpType where
382 ppr (Check ty) = text "Check" <> braces (ppr ty)
383 ppr (Infer ir) = ppr ir
384
385 instance Outputable InferResult where
386 ppr (IR { ir_uniq = u, ir_lvl = lvl
387 , ir_inst = inst })
388 = text "Infer" <> braces (ppr u <> comma <> ppr lvl <+> ppr inst)
389
390 -- | Make an 'ExpType' suitable for checking.
391 mkCheckExpType :: TcType -> ExpType
392 mkCheckExpType = Check
393
394
395 {- *********************************************************************
396 * *
397 SyntaxOpType
398 * *
399 ********************************************************************* -}
400
401 -- | What to expect for an argument to a rebindable-syntax operator.
402 -- Quite like 'Type', but allows for holes to be filled in by tcSyntaxOp.
403 -- The callback called from tcSyntaxOp gets a list of types; the meaning
404 -- of these types is determined by a left-to-right depth-first traversal
405 -- of the 'SyntaxOpType' tree. So if you pass in
406 --
407 -- > SynAny `SynFun` (SynList `SynFun` SynType Int) `SynFun` SynAny
408 --
409 -- you'll get three types back: one for the first 'SynAny', the /element/
410 -- type of the list, and one for the last 'SynAny'. You don't get anything
411 -- for the 'SynType', because you've said positively that it should be an
412 -- Int, and so it shall be.
413 --
414 -- This is defined here to avoid defining it in TcExpr.hs-boot.
415 data SyntaxOpType
416 = SynAny -- ^ Any type
417 | SynRho -- ^ A rho type, deeply skolemised or instantiated as appropriate
418 | SynList -- ^ A list type. You get back the element type of the list
419 | SynFun SyntaxOpType SyntaxOpType
420 -- ^ A function.
421 | SynType ExpType -- ^ A known type.
422 infixr 0 `SynFun`
423
424 -- | Like 'SynType' but accepts a regular TcType
425 synKnownType :: TcType -> SyntaxOpType
426 synKnownType = SynType . mkCheckExpType
427
428 -- | Like 'mkFunTys' but for 'SyntaxOpType'
429 mkSynFunTys :: [SyntaxOpType] -> ExpType -> SyntaxOpType
430 mkSynFunTys arg_tys res_ty = foldr SynFun (SynType res_ty) arg_tys
431
432
433 {-
434 Note [TcRhoType]
435 ~~~~~~~~~~~~~~~~
436 A TcRhoType has no foralls or contexts at the top, or to the right of an arrow
437 YES (forall a. a->a) -> Int
438 NO forall a. a -> Int
439 NO Eq a => a -> a
440 NO Int -> forall a. a -> Int
441
442
443 ************************************************************************
444 * *
445 TyVarDetails, MetaDetails, MetaInfo
446 * *
447 ************************************************************************
448
449 TyVarDetails gives extra info about type variables, used during type
450 checking. It's attached to mutable type variables only.
451 It's knot-tied back to Var.hs. There is no reason in principle
452 why Var.hs shouldn't actually have the definition, but it "belongs" here.
453
454 Note [Signature skolems]
455 ~~~~~~~~~~~~~~~~~~~~~~~~
456 A SigTv is a specialised variant of TauTv, with the following invarints:
457
458 * A SigTv can be unified only with a TyVar,
459 not with any other type
460
461 * Its MetaDetails, if filled in, will always be another SigTv
462 or a SkolemTv
463
464 SigTvs are only distinguished to improve error messages.
465 Consider this
466
467 f :: forall a. [a] -> Int
468 f (x::b : xs) = 3
469
470 Here 'b' is a lexically scoped type variable, but it turns out to be
471 the same as the skolem 'a'. So we make them both SigTvs, which can unify
472 with each other.
473
474 Similarly consider
475 data T (a:k1) = MkT (S a)
476 data S (b:k2) = MkS (T b)
477 When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
478 because they end up unifying; we want those SigTvs again.
479
480 SigTvs are used *only* for pattern type signatures.
481
482 Note [TyVars and TcTyVars during type checking]
483 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
484 The Var type has constructors TyVar and TcTyVar. They are used
485 as follows:
486
487 * TcTyVar: used /only/ during type checking. Should never appear
488 afterwards. May contain a mutable field, in the MetaTv case.
489
490 * TyVar: is never seen by the constraint solver, except locally
491 inside a type like (forall a. [a] ->[a]), where 'a' is a TyVar.
492 We instantiate these with TcTyVars before exposing the type
493 to the constraint solver.
494
495 I have swithered about the latter invariant, excluding TyVars from the
496 constraint solver. It's not strictly essential, and indeed
497 (historically but still there) Var.tcTyVarDetails returns
498 vanillaSkolemTv for a TyVar.
499
500 But ultimately I want to seeparate Type from TcType, and in that case
501 we would need to enforce the separation.
502 -}
503
504 -- A TyVarDetails is inside a TyVar
505 -- See Note [TyVars and TcTyVars]
506 data TcTyVarDetails
507 = SkolemTv -- A skolem
508 TcLevel -- Level of the implication that binds it
509 -- See TcUnify Note [Deeper level on the left] for
510 -- how this level number is used
511 Bool -- True <=> this skolem type variable can be overlapped
512 -- when looking up instances
513 -- See Note [Binding when looking up instances] in InstEnv
514
515 | RuntimeUnk -- Stands for an as-yet-unknown type in the GHCi
516 -- interactive context
517
518 | MetaTv { mtv_info :: MetaInfo
519 , mtv_ref :: IORef MetaDetails
520 , mtv_tclvl :: TcLevel } -- See Note [TcLevel and untouchable type variables]
521
522 vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
523 -- See Note [Binding when looking up instances] in InstEnv
524 vanillaSkolemTv = SkolemTv topTcLevel False -- Might be instantiated
525 superSkolemTv = SkolemTv topTcLevel True -- Treat this as a completely distinct type
526 -- The choice of level number here is a bit dodgy, but
527 -- topTcLevel works in the places that vanillaSkolemTv is used
528
529 -----------------------------
530 data MetaDetails
531 = Flexi -- Flexi type variables unify to become Indirects
532 | Indirect TcType
533
534 data MetaInfo
535 = TauTv -- This MetaTv is an ordinary unification variable
536 -- A TauTv is always filled in with a tau-type, which
537 -- never contains any ForAlls.
538
539 | SigTv -- A variant of TauTv, except that it should not be
540 -- unified with a type, only with a type variable
541 -- See Note [Signature skolems]
542
543 | FlatMetaTv -- A flatten meta-tyvar
544 -- It is a meta-tyvar, but it is always untouchable, with level 0
545 -- See Note [The flattening story] in TcFlatten
546
547 | FlatSkolTv -- A flatten skolem tyvar
548 -- Just like FlatMetaTv, but is comletely "owned" by
549 -- its Given CFunEqCan.
550 -- It is filled in /only/ by unflattenGivens
551 -- See Note [The flattening story] in TcFlatten
552
553 instance Outputable MetaDetails where
554 ppr Flexi = text "Flexi"
555 ppr (Indirect ty) = text "Indirect" <+> ppr ty
556
557 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
558 -- For debugging
559 pprTcTyVarDetails (RuntimeUnk {}) = text "rt"
560 pprTcTyVarDetails (SkolemTv lvl True) = text "ssk" <> colon <> ppr lvl
561 pprTcTyVarDetails (SkolemTv lvl False) = text "sk" <> colon <> ppr lvl
562 pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
563 = pp_info <> colon <> ppr tclvl
564 where
565 pp_info = case info of
566 TauTv -> text "tau"
567 SigTv -> text "sig"
568 FlatMetaTv -> text "fmv"
569 FlatSkolTv -> text "fsk"
570
571
572 {- *********************************************************************
573 * *
574 UserTypeCtxt
575 * *
576 ********************************************************************* -}
577
578 -------------------------------------
579 -- UserTypeCtxt describes the origin of the polymorphic type
580 -- in the places where we need to an expression has that type
581
582 data UserTypeCtxt
583 = FunSigCtxt -- Function type signature, when checking the type
584 -- Also used for types in SPECIALISE pragmas
585 Name -- Name of the function
586 Bool -- True <=> report redundant constraints
587 -- This is usually True, but False for
588 -- * Record selectors (not important here)
589 -- * Class and instance methods. Here
590 -- the code may legitimately be more
591 -- polymorphic than the signature
592 -- generated from the class
593 -- declaration
594
595 | InfSigCtxt Name -- Inferred type for function
596 | ExprSigCtxt -- Expression type signature
597 | TypeAppCtxt -- Visible type application
598 | ConArgCtxt Name -- Data constructor argument
599 | TySynCtxt Name -- RHS of a type synonym decl
600 | PatSynCtxt Name -- Type sig for a pattern synonym
601 | PatSigCtxt -- Type sig in pattern
602 -- eg f (x::t) = ...
603 -- or (x::t, y) = e
604 | RuleSigCtxt Name -- LHS of a RULE forall
605 -- RULE "foo" forall (x :: a -> a). f (Just x) = ...
606 | ResSigCtxt -- Result type sig
607 -- f x :: t = ....
608 | ForSigCtxt Name -- Foreign import or export signature
609 | DefaultDeclCtxt -- Types in a default declaration
610 | InstDeclCtxt -- An instance declaration
611 | SpecInstCtxt -- SPECIALISE instance pragma
612 | ThBrackCtxt -- Template Haskell type brackets [t| ... |]
613 | GenSigCtxt -- Higher-rank or impredicative situations
614 -- e.g. (f e) where f has a higher-rank type
615 -- We might want to elaborate this
616 | GhciCtxt -- GHCi command :kind <type>
617
618 | ClassSCCtxt Name -- Superclasses of a class
619 | SigmaCtxt -- Theta part of a normal for-all type
620 -- f :: <S> => a -> a
621 | DataTyCtxt Name -- The "stupid theta" part of a data decl
622 -- data <S> => T a = MkT a
623 | DerivClauseCtxt -- A 'deriving' clause
624 | TyVarBndrKindCtxt Name -- The kind of a type variable being bound
625 | DataKindCtxt Name -- The kind of a data/newtype (instance)
626 | TySynKindCtxt Name -- The kind of the RHS of a type synonym
627 | TyFamResKindCtxt Name -- The result kind of a type family
628
629 {-
630 -- Notes re TySynCtxt
631 -- We allow type synonyms that aren't types; e.g. type List = []
632 --
633 -- If the RHS mentions tyvars that aren't in scope, we'll
634 -- quantify over them:
635 -- e.g. type T = a->a
636 -- will become type T = forall a. a->a
637 --
638 -- With gla-exts that's right, but for H98 we should complain.
639 -}
640
641
642 pprUserTypeCtxt :: UserTypeCtxt -> SDoc
643 pprUserTypeCtxt (FunSigCtxt n _) = text "the type signature for" <+> quotes (ppr n)
644 pprUserTypeCtxt (InfSigCtxt n) = text "the inferred type for" <+> quotes (ppr n)
645 pprUserTypeCtxt (RuleSigCtxt n) = text "a RULE for" <+> quotes (ppr n)
646 pprUserTypeCtxt ExprSigCtxt = text "an expression type signature"
647 pprUserTypeCtxt TypeAppCtxt = text "a type argument"
648 pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c)
649 pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c)
650 pprUserTypeCtxt ThBrackCtxt = text "a Template Haskell quotation [t|...|]"
651 pprUserTypeCtxt PatSigCtxt = text "a pattern type signature"
652 pprUserTypeCtxt ResSigCtxt = text "a result type signature"
653 pprUserTypeCtxt (ForSigCtxt n) = text "the foreign declaration for" <+> quotes (ppr n)
654 pprUserTypeCtxt DefaultDeclCtxt = text "a type in a `default' declaration"
655 pprUserTypeCtxt InstDeclCtxt = text "an instance declaration"
656 pprUserTypeCtxt SpecInstCtxt = text "a SPECIALISE instance pragma"
657 pprUserTypeCtxt GenSigCtxt = text "a type expected by the context"
658 pprUserTypeCtxt GhciCtxt = text "a type in a GHCi command"
659 pprUserTypeCtxt (ClassSCCtxt c) = text "the super-classes of class" <+> quotes (ppr c)
660 pprUserTypeCtxt SigmaCtxt = text "the context of a polymorphic type"
661 pprUserTypeCtxt (DataTyCtxt tc) = text "the context of the data type declaration for" <+> quotes (ppr tc)
662 pprUserTypeCtxt (PatSynCtxt n) = text "the signature for pattern synonym" <+> quotes (ppr n)
663 pprUserTypeCtxt (DerivClauseCtxt) = text "a `deriving' clause"
664 pprUserTypeCtxt (TyVarBndrKindCtxt n) = text "the kind annotation on the type variable" <+> quotes (ppr n)
665 pprUserTypeCtxt (DataKindCtxt n) = text "the kind annotation on the declaration for" <+> quotes (ppr n)
666 pprUserTypeCtxt (TySynKindCtxt n) = text "the kind annotation on the declaration for" <+> quotes (ppr n)
667 pprUserTypeCtxt (TyFamResKindCtxt n) = text "the result kind for" <+> quotes (ppr n)
668
669 isSigMaybe :: UserTypeCtxt -> Maybe Name
670 isSigMaybe (FunSigCtxt n _) = Just n
671 isSigMaybe (ConArgCtxt n) = Just n
672 isSigMaybe (ForSigCtxt n) = Just n
673 isSigMaybe (PatSynCtxt n) = Just n
674 isSigMaybe _ = Nothing
675
676
677 {- *********************************************************************
678 * *
679 Untoucable type variables
680 * *
681 ********************************************************************* -}
682
683 newtype TcLevel = TcLevel Int deriving( Eq, Ord )
684 -- See Note [TcLevel and untouchable type variables] for what this Int is
685 -- See also Note [TcLevel assignment]
686
687 {-
688 Note [TcLevel and untouchable type variables]
689 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
690 * Each unification variable (MetaTv)
691 and each Implication
692 has a level number (of type TcLevel)
693
694 * INVARIANTS. In a tree of Implications,
695
696 (ImplicInv) The level number (ic_tclvl) of an Implication is
697 STRICTLY GREATER THAN that of its parent
698
699 (SkolInv) The level number of the skolems (ic_skols) of an
700 Implication is equal to the level of the implication
701 itself (ic_tclvl)
702
703 (GivenInv) The level number of a unification variable appearing
704 in the 'ic_given' of an implication I should be
705 STRICTLY LESS THAN the ic_tclvl of I
706
707 (WantedInv) The level number of a unification variable appearing
708 in the 'ic_wanted' of an implication I should be
709 LESS THAN OR EQUAL TO the ic_tclvl of I
710 See Note [WantedInv]
711
712 * A unification variable is *touchable* if its level number
713 is EQUAL TO that of its immediate parent implication,
714 and it is a TauTv or SigTv (but /not/ FlatMetaTv or FlatSkolTv
715
716 Note [WantedInv]
717 ~~~~~~~~~~~~~~~~
718 Why is WantedInv important? Consider this implication, where
719 the constraint (C alpha[3]) disobeys WantedInv:
720
721 forall[2] a. blah => (C alpha[3])
722 (forall[3] b. alpha[3] ~ b)
723
724 We can unify alpha:=b in the inner implication, because 'alpha' is
725 touchable; but then 'b' has excaped its scope into the outer implication.
726
727 Note [Skolem escape prevention]
728 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
729 We only unify touchable unification variables. Because of
730 (WantedInv), there can be no occurrences of the variable further out,
731 so the unification can't cause the skolems to escape. Example:
732 data T = forall a. MkT a (a->Int)
733 f x (MkT v f) = length [v,x]
734 We decide (x::alpha), and generate an implication like
735 [1]forall a. (a ~ alpha[0])
736 But we must not unify alpha:=a, because the skolem would escape.
737
738 For the cases where we DO want to unify, we rely on floating the
739 equality. Example (with same T)
740 g x (MkT v f) = x && True
741 We decide (x::alpha), and generate an implication like
742 [1]forall a. (Bool ~ alpha[0])
743 We do NOT unify directly, bur rather float out (if the constraint
744 does not mention 'a') to get
745 (Bool ~ alpha[0]) /\ [1]forall a.()
746 and NOW we can unify alpha.
747
748 The same idea of only unifying touchables solves another problem.
749 Suppose we had
750 (F Int ~ uf[0]) /\ [1](forall a. C a => F Int ~ beta[1])
751 In this example, beta is touchable inside the implication. The
752 first solveSimpleWanteds step leaves 'uf' un-unified. Then we move inside
753 the implication where a new constraint
754 uf ~ beta
755 emerges. If we (wrongly) spontaneously solved it to get uf := beta,
756 the whole implication disappears but when we pop out again we are left with
757 (F Int ~ uf) which will be unified by our final zonking stage and
758 uf will get unified *once more* to (F Int).
759
760 Note [TcLevel assignment]
761 ~~~~~~~~~~~~~~~~~~~~~~~~~
762 We arrange the TcLevels like this
763
764 0 Top level
765 1 First-level implication constraints
766 2 Second-level implication constraints
767 ...etc...
768 -}
769
770 maxTcLevel :: TcLevel -> TcLevel -> TcLevel
771 maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b)
772
773 topTcLevel :: TcLevel
774 -- See Note [TcLevel assignment]
775 topTcLevel = TcLevel 0 -- 0 = outermost level
776
777 isTopTcLevel :: TcLevel -> Bool
778 isTopTcLevel (TcLevel 0) = True
779 isTopTcLevel _ = False
780
781 pushTcLevel :: TcLevel -> TcLevel
782 -- See Note [TcLevel assignment]
783 pushTcLevel (TcLevel us) = TcLevel (us + 1)
784
785 strictlyDeeperThan :: TcLevel -> TcLevel -> Bool
786 strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
787 = tv_tclvl > ctxt_tclvl
788
789 sameDepthAs :: TcLevel -> TcLevel -> Bool
790 sameDepthAs (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
791 = ctxt_tclvl == tv_tclvl -- NB: invariant ctxt_tclvl >= tv_tclvl
792 -- So <= would be equivalent
793
794 checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool
795 -- Checks (WantedInv) from Note [TcLevel and untouchable type variables]
796 checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
797 = ctxt_tclvl >= tv_tclvl
798
799 tcTyVarLevel :: TcTyVar -> TcLevel
800 tcTyVarLevel tv
801 = ASSERT2( tcIsTcTyVar tv, ppr tv )
802 case tcTyVarDetails tv of
803 MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl
804 SkolemTv tv_lvl _ -> tv_lvl
805 RuntimeUnk -> topTcLevel
806
807
808 tcTypeLevel :: TcType -> TcLevel
809 -- Max level of any free var of the type
810 tcTypeLevel ty
811 = foldDVarSet add topTcLevel (tyCoVarsOfTypeDSet ty)
812 where
813 add v lvl
814 | isTcTyVar v = lvl `maxTcLevel` tcTyVarLevel v
815 | otherwise = lvl
816
817 instance Outputable TcLevel where
818 ppr (TcLevel us) = ppr us
819
820 promoteSkolem :: TcLevel -> TcTyVar -> TcTyVar
821 promoteSkolem tclvl skol
822 | tclvl < tcTyVarLevel skol
823 = ASSERT( isTcTyVar skol && isSkolemTyVar skol )
824 setTcTyVarDetails skol (SkolemTv tclvl (isOverlappableTyVar skol))
825
826 | otherwise
827 = skol
828
829 -- | Change the TcLevel in a skolem, extending a substitution
830 promoteSkolemX :: TcLevel -> TCvSubst -> TcTyVar -> (TCvSubst, TcTyVar)
831 promoteSkolemX tclvl subst skol
832 = ASSERT( isTcTyVar skol && isSkolemTyVar skol )
833 (new_subst, new_skol)
834 where
835 new_skol
836 | tclvl < tcTyVarLevel skol
837 = setTcTyVarDetails (updateTyVarKind (substTy subst) skol)
838 (SkolemTv tclvl (isOverlappableTyVar skol))
839 | otherwise
840 = updateTyVarKind (substTy subst) skol
841 new_subst = extendTvSubstWithClone subst skol new_skol
842
843 promoteSkolemsX :: TcLevel -> TCvSubst -> [TcTyVar] -> (TCvSubst, [TcTyVar])
844 promoteSkolemsX tclvl = mapAccumL (promoteSkolemX tclvl)
845
846 {- *********************************************************************
847 * *
848 Finding type family instances
849 * *
850 ************************************************************************
851 -}
852
853 -- | Finds outermost type-family applications occuring in a type,
854 -- after expanding synonyms. In the list (F, tys) that is returned
855 -- we guarantee that tys matches F's arity. For example, given
856 -- type family F a :: * -> * (arity 1)
857 -- calling tcTyFamInsts on (Maybe (F Int Bool) will return
858 -- (F, [Int]), not (F, [Int,Bool])
859 --
860 -- This is important for its use in deciding termination of type
861 -- instances (see Trac #11581). E.g.
862 -- type instance G [Int] = ...(F Int <big type>)...
863 -- we don't need to take <big type> into account when asking if
864 -- the calls on the RHS are smaller than the LHS
865 tcTyFamInsts :: Type -> [(TyCon, [Type])]
866 tcTyFamInsts ty
867 | Just exp_ty <- tcView ty = tcTyFamInsts exp_ty
868 tcTyFamInsts (TyVarTy _) = []
869 tcTyFamInsts (TyConApp tc tys)
870 | isTypeFamilyTyCon tc = [(tc, take (tyConArity tc) tys)]
871 | otherwise = concat (map tcTyFamInsts tys)
872 tcTyFamInsts (LitTy {}) = []
873 tcTyFamInsts (ForAllTy bndr ty) = tcTyFamInsts (binderKind bndr)
874 ++ tcTyFamInsts ty
875 tcTyFamInsts (FunTy ty1 ty2) = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
876 tcTyFamInsts (AppTy ty1 ty2) = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
877 tcTyFamInsts (CastTy ty _) = tcTyFamInsts ty
878 tcTyFamInsts (CoercionTy _) = [] -- don't count tyfams in coercions,
879 -- as they never get normalized, anyway
880
881 isTyFamFree :: Type -> Bool
882 -- ^ Check that a type does not contain any type family applications.
883 isTyFamFree = null . tcTyFamInsts
884
885 {-
886 ************************************************************************
887 * *
888 The "exact" free variables of a type
889 * *
890 ************************************************************************
891
892 Note [Silly type synonym]
893 ~~~~~~~~~~~~~~~~~~~~~~~~~
894 Consider
895 type T a = Int
896 What are the free tyvars of (T x)? Empty, of course!
897 Here's the example that Ralf Laemmel showed me:
898 foo :: (forall a. C u a -> C u a) -> u
899 mappend :: Monoid u => u -> u -> u
900
901 bar :: Monoid u => u
902 bar = foo (\t -> t `mappend` t)
903 We have to generalise at the arg to f, and we don't
904 want to capture the constraint (Monad (C u a)) because
905 it appears to mention a. Pretty silly, but it was useful to him.
906
907 exactTyCoVarsOfType is used by the type checker to figure out exactly
908 which type variables are mentioned in a type. It's also used in the
909 smart-app checking code --- see TcExpr.tcIdApp
910
911 On the other hand, consider a *top-level* definition
912 f = (\x -> x) :: T a -> T a
913 If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
914 if we have an application like (f "x") we get a confusing error message
915 involving Any. So the conclusion is this: when generalising
916 - at top level use tyCoVarsOfType
917 - in nested bindings use exactTyCoVarsOfType
918 See Trac #1813 for example.
919 -}
920
921 exactTyCoVarsOfType :: Type -> TyCoVarSet
922 -- Find the free type variables (of any kind)
923 -- but *expand* type synonyms. See Note [Silly type synonym] above.
924 exactTyCoVarsOfType ty
925 = go ty
926 where
927 go ty | Just ty' <- tcView ty = go ty' -- This is the key line
928 go (TyVarTy tv) = goVar tv
929 go (TyConApp _ tys) = exactTyCoVarsOfTypes tys
930 go (LitTy {}) = emptyVarSet
931 go (AppTy fun arg) = go fun `unionVarSet` go arg
932 go (FunTy arg res) = go arg `unionVarSet` go res
933 go (ForAllTy bndr ty) = delBinderVar (go ty) bndr `unionVarSet` go (binderKind bndr)
934 go (CastTy ty co) = go ty `unionVarSet` goCo co
935 go (CoercionTy co) = goCo co
936
937 goCo (Refl _ ty) = go ty
938 goCo (TyConAppCo _ _ args)= goCos args
939 goCo (AppCo co arg) = goCo co `unionVarSet` goCo arg
940 goCo (ForAllCo tv k_co co)
941 = goCo co `delVarSet` tv `unionVarSet` goCo k_co
942 goCo (FunCo _ co1 co2) = goCo co1 `unionVarSet` goCo co2
943 goCo (CoVarCo v) = goVar v
944 goCo (HoleCo h) = goVar (coHoleCoVar h)
945 goCo (AxiomInstCo _ _ args) = goCos args
946 goCo (UnivCo p _ t1 t2) = goProv p `unionVarSet` go t1 `unionVarSet` go t2
947 goCo (SymCo co) = goCo co
948 goCo (TransCo co1 co2) = goCo co1 `unionVarSet` goCo co2
949 goCo (NthCo _ _ co) = goCo co
950 goCo (LRCo _ co) = goCo co
951 goCo (InstCo co arg) = goCo co `unionVarSet` goCo arg
952 goCo (CoherenceCo c1 c2) = goCo c1 `unionVarSet` goCo c2
953 goCo (KindCo co) = goCo co
954 goCo (SubCo co) = goCo co
955 goCo (AxiomRuleCo _ c) = goCos c
956
957 goCos cos = foldr (unionVarSet . goCo) emptyVarSet cos
958
959 goProv UnsafeCoerceProv = emptyVarSet
960 goProv (PhantomProv kco) = goCo kco
961 goProv (ProofIrrelProv kco) = goCo kco
962 goProv (PluginProv _) = emptyVarSet
963
964 goVar v = unitVarSet v `unionVarSet` go (varType v)
965
966 exactTyCoVarsOfTypes :: [Type] -> TyVarSet
967 exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
968
969 anyRewritableTyVar :: Bool -- Ignore casts and coercions
970 -> EqRel -- Ambient role
971 -> (EqRel -> TcTyVar -> Bool)
972 -> TcType -> Bool
973 -- (anyRewritableTyVar ignore_cos pred ty) returns True
974 -- if the 'pred' returns True of any free TyVar in 'ty'
975 -- Do not look inside casts and coercions if 'ignore_cos' is True
976 -- See Note [anyRewritableTyVar must be role-aware]
977 anyRewritableTyVar ignore_cos role pred ty
978 = go role emptyVarSet ty
979 where
980 go_tv rl bvs tv | tv `elemVarSet` bvs = False
981 | otherwise = pred rl tv
982
983 go rl bvs (TyVarTy tv) = go_tv rl bvs tv
984 go _ _ (LitTy {}) = False
985 go rl bvs (TyConApp tc tys) = go_tc rl bvs tc tys
986 go rl bvs (AppTy fun arg) = go rl bvs fun || go NomEq bvs arg
987 go rl bvs (FunTy arg res) = go rl bvs arg || go rl bvs res
988 go rl bvs (ForAllTy tv ty) = go rl (bvs `extendVarSet` binderVar tv) ty
989 go rl bvs (CastTy ty co) = go rl bvs ty || go_co rl bvs co
990 go rl bvs (CoercionTy co) = go_co rl bvs co -- ToDo: check
991
992 go_tc NomEq bvs _ tys = any (go NomEq bvs) tys
993 go_tc ReprEq bvs tc tys = foldr ((&&) . go_arg bvs) False $
994 (tyConRolesRepresentational tc `zip` tys)
995
996 go_arg bvs (Nominal, ty) = go NomEq bvs ty
997 go_arg bvs (Representational, ty) = go ReprEq bvs ty
998 go_arg _ (Phantom, _) = False -- We never rewrite with phantoms
999
1000 go_co rl bvs co
1001 | ignore_cos = False
1002 | otherwise = anyVarSet (go_tv rl bvs) (tyCoVarsOfCo co)
1003 -- We don't have an equivalent of anyRewritableTyVar for coercions
1004 -- (at least not yet) so take the free vars and test them
1005
1006 {- Note [anyRewritableTyVar must be role-aware]
1007 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1008 anyRewritableTyVar is used during kick-out from the inert set,
1009 to decide if, given a new equality (a ~ ty), we should kick out
1010 a constraint C. Rather than gather free variables and see if 'a'
1011 is among them, we instead pass in a predicate; this is just efficiency.
1012
1013 Moreover, consider
1014 work item: [G] a ~R f b
1015 inert item: [G] b ~R f a
1016 We use anyRewritableTyVar to decide whether to kick out the inert item,
1017 on the grounds that the work item might rewrite it. Well, 'a' is certainly
1018 free in [G] b ~R f a. But because the role of a type variable ('f' in
1019 this case) is nominal, the work item can't actually rewrite the inert item.
1020 Moreover, if we were to kick out the inert item the exact same situation
1021 would re-occur and we end up with an infinite loop in which each kicks
1022 out the other (Trac #14363).
1023 -}
1024
1025 {- *********************************************************************
1026 * *
1027 Type and kind variables in a type
1028 * *
1029 ********************************************************************* -}
1030
1031 data CandidatesQTvs -- See Note [Dependent type variables]
1032 -- See Note [CandidatesQTvs determinism]
1033 = DV { dv_kvs :: DTyCoVarSet -- "kind" variables (dependent)
1034 , dv_tvs :: DTyVarSet -- "type" variables (non-dependent)
1035 -- A variable may appear in both sets
1036 -- E.g. T k (x::k) The first occurrence of k makes it
1037 -- show up in dv_tvs, the second in dv_kvs
1038 -- See Note [Dependent type variables]
1039 }
1040
1041 instance Semi.Semigroup CandidatesQTvs where
1042 (DV { dv_kvs = kv1, dv_tvs = tv1 }) <> (DV { dv_kvs = kv2, dv_tvs = tv2 })
1043 = DV { dv_kvs = kv1 `unionDVarSet` kv2
1044 , dv_tvs = tv1 `unionDVarSet` tv2}
1045
1046 instance Monoid CandidatesQTvs where
1047 mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet }
1048 mappend = (Semi.<>)
1049
1050 instance Outputable CandidatesQTvs where
1051 ppr (DV {dv_kvs = kvs, dv_tvs = tvs })
1052 = text "DV" <+> braces (sep [ text "dv_kvs =" <+> ppr kvs
1053 , text "dv_tvs =" <+> ppr tvs ])
1054
1055 {- Note [Dependent type variables]
1056 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1057 In Haskell type inference we quantify over type variables; but we only
1058 quantify over /kind/ variables when -XPolyKinds is on. Without -XPolyKinds
1059 we default the kind variables to *.
1060
1061 So, to support this defaulting, and only for that reason, when
1062 collecting the free vars of a type, prior to quantifying, we must keep
1063 the type and kind variables separate.
1064
1065 But what does that mean in a system where kind variables /are/ type
1066 variables? It's a fairly arbitrary distinction based on how the
1067 variables appear:
1068
1069 - "Kind variables" appear in the kind of some other free variable
1070 PLUS any free coercion variables
1071
1072 These are the ones we default to * if -XPolyKinds is off
1073
1074 - "Type variables" are all free vars that are not kind variables
1075
1076 E.g. In the type T k (a::k)
1077 'k' is a kind variable, because it occurs in the kind of 'a',
1078 even though it also appears at "top level" of the type
1079 'a' is a type variable, because it doesn't
1080
1081 We gather these variables using a CandidatesQTvs record:
1082 DV { dv_kvs: Variables free in the kind of a free type variable
1083 or of a forall-bound type variable
1084 , dv_tvs: Variables sytactically free in the type }
1085
1086 So: dv_kvs are the kind variables of the type
1087 (dv_tvs - dv_kvs) are the type variable of the type
1088
1089 Note that
1090
1091 * A variable can occur in both.
1092 T k (x::k) The first occurrence of k makes it
1093 show up in dv_tvs, the second in dv_kvs
1094
1095 * We include any coercion variables in the "dependent",
1096 "kind-variable" set because we never quantify over them.
1097
1098 * Both sets are un-ordered, of course.
1099
1100 * The "kind variables" might depend on each other; e.g
1101 (k1 :: k2), (k2 :: *)
1102 The "type variables" do not depend on each other; if
1103 one did, it'd be classified as a kind variable!
1104
1105 Note [CandidatesQTvs determinism and order]
1106 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1107 * Determinism: when we quantify over type variables we decide the
1108 order in which they appear in the final type. Because the order of
1109 type variables in the type can end up in the interface file and
1110 affects some optimizations like worker-wrapper, we want this order to
1111 be deterministic.
1112
1113 To achieve that we use deterministic sets of variables that can be
1114 converted to lists in a deterministic order. For more information
1115 about deterministic sets see Note [Deterministic UniqFM] in UniqDFM.
1116
1117 * Order: as well as being deterministic, we use an
1118 accumulating-parameter style for candidateQTyVarsOfType so that we
1119 add variables one at a time, left to right. That means we tend to
1120 produce the variables in left-to-right order. This is just to make
1121 it bit more predicatable for the programmer.
1122 -}
1123
1124 -- | Worker for 'splitDepVarsOfType'. This might output the same var
1125 -- in both sets, if it's used in both a type and a kind.
1126 -- See Note [CandidatesQTvs determinism and order]
1127 -- See Note [Dependent type variables]
1128 candidateQTyVarsOfType :: Type -> CandidatesQTvs
1129 candidateQTyVarsOfType = split_dvs emptyVarSet mempty
1130
1131 split_dvs :: VarSet -> CandidatesQTvs -> Type -> CandidatesQTvs
1132 split_dvs bound dvs ty
1133 = go dvs ty
1134 where
1135 go dv (AppTy t1 t2) = go (go dv t1) t2
1136 go dv (TyConApp _ tys) = foldl go dv tys
1137 go dv (FunTy arg res) = go (go dv arg) res
1138 go dv (LitTy {}) = dv
1139 go dv (CastTy ty co) = go dv ty `mappend` go_co co
1140 go dv (CoercionTy co) = dv `mappend` go_co co
1141
1142 go dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) (TyVarTy tv)
1143 | tv `elemVarSet` bound
1144 = dv
1145 | otherwise
1146 = DV { dv_kvs = kvs `unionDVarSet`
1147 kill_bound (tyCoVarsOfTypeDSet (tyVarKind tv))
1148 , dv_tvs = tvs `extendDVarSet` tv }
1149
1150 go dv (ForAllTy (TvBndr tv _) ty)
1151 = DV { dv_kvs = kvs `unionDVarSet`
1152 kill_bound (tyCoVarsOfTypeDSet (tyVarKind tv))
1153 , dv_tvs = tvs }
1154 where
1155 DV { dv_kvs = kvs, dv_tvs = tvs } = split_dvs (bound `extendVarSet` tv) dv ty
1156
1157 go_co co = DV { dv_kvs = kill_bound (tyCoVarsOfCoDSet co)
1158 , dv_tvs = emptyDVarSet }
1159
1160 kill_bound free
1161 | isEmptyVarSet bound = free
1162 | otherwise = free `dVarSetMinusVarSet` bound
1163
1164 -- | Like 'splitDepVarsOfType', but over a list of types
1165 candidateQTyVarsOfTypes :: [Type] -> CandidatesQTvs
1166 candidateQTyVarsOfTypes = foldl (split_dvs emptyVarSet) mempty
1167
1168 {-
1169 ************************************************************************
1170 * *
1171 Predicates
1172 * *
1173 ************************************************************************
1174 -}
1175
1176 tcIsTcTyVar :: TcTyVar -> Bool
1177 -- See Note [TcTyVars and TyVars in the typechecker]
1178 tcIsTcTyVar tv = isTyVar tv
1179
1180 isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
1181 isTouchableMetaTyVar ctxt_tclvl tv
1182 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1183 , MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info } <- tcTyVarDetails tv
1184 , not (isFlattenInfo info)
1185 = ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
1186 ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
1187 tv_tclvl `sameDepthAs` ctxt_tclvl
1188
1189 | otherwise = False
1190
1191 isFloatedTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
1192 isFloatedTouchableMetaTyVar ctxt_tclvl tv
1193 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1194 , MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info } <- tcTyVarDetails tv
1195 , not (isFlattenInfo info)
1196 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1197 tv_tclvl `strictlyDeeperThan` ctxt_tclvl
1198
1199 | otherwise = False
1200
1201 isImmutableTyVar :: TyVar -> Bool
1202 isImmutableTyVar tv = isSkolemTyVar tv
1203
1204 isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
1205 isMetaTyVar, isAmbiguousTyVar,
1206 isFmvTyVar, isFskTyVar, isFlattenTyVar :: TcTyVar -> Bool
1207
1208 isTyConableTyVar tv
1209 -- True of a meta-type variable that can be filled in
1210 -- with a type constructor application; in particular,
1211 -- not a SigTv
1212 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1213 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1214 case tcTyVarDetails tv of
1215 MetaTv { mtv_info = SigTv } -> False
1216 _ -> True
1217 | otherwise = True
1218
1219 isFmvTyVar tv
1220 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1221 case tcTyVarDetails tv of
1222 MetaTv { mtv_info = FlatMetaTv } -> True
1223 _ -> False
1224
1225 isFskTyVar tv
1226 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1227 case tcTyVarDetails tv of
1228 MetaTv { mtv_info = FlatSkolTv } -> True
1229 _ -> False
1230
1231 -- | True of both given and wanted flatten-skolems (fak and usk)
1232 isFlattenTyVar tv
1233 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1234 case tcTyVarDetails tv of
1235 MetaTv { mtv_info = info } -> isFlattenInfo info
1236 _ -> False
1237
1238 isSkolemTyVar tv
1239 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1240 case tcTyVarDetails tv of
1241 MetaTv {} -> False
1242 _other -> True
1243
1244 isOverlappableTyVar tv
1245 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1246 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1247 case tcTyVarDetails tv of
1248 SkolemTv _ overlappable -> overlappable
1249 _ -> False
1250 | otherwise = False
1251
1252 isMetaTyVar tv
1253 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1254 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1255 case tcTyVarDetails tv of
1256 MetaTv {} -> True
1257 _ -> False
1258 | otherwise = False
1259
1260 -- isAmbiguousTyVar is used only when reporting type errors
1261 -- It picks out variables that are unbound, namely meta
1262 -- type variables and the RuntimUnk variables created by
1263 -- RtClosureInspect.zonkRTTIType. These are "ambiguous" in
1264 -- the sense that they stand for an as-yet-unknown type
1265 isAmbiguousTyVar tv
1266 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1267 = case tcTyVarDetails tv of
1268 MetaTv {} -> True
1269 RuntimeUnk {} -> True
1270 _ -> False
1271 | otherwise = False
1272
1273 isMetaTyVarTy :: TcType -> Bool
1274 isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
1275 isMetaTyVarTy _ = False
1276
1277 metaTyVarInfo :: TcTyVar -> MetaInfo
1278 metaTyVarInfo tv
1279 = case tcTyVarDetails tv of
1280 MetaTv { mtv_info = info } -> info
1281 _ -> pprPanic "metaTyVarInfo" (ppr tv)
1282
1283 isFlattenInfo :: MetaInfo -> Bool
1284 isFlattenInfo FlatMetaTv = True
1285 isFlattenInfo FlatSkolTv = True
1286 isFlattenInfo _ = False
1287
1288 metaTyVarTcLevel :: TcTyVar -> TcLevel
1289 metaTyVarTcLevel tv
1290 = case tcTyVarDetails tv of
1291 MetaTv { mtv_tclvl = tclvl } -> tclvl
1292 _ -> pprPanic "metaTyVarTcLevel" (ppr tv)
1293
1294 metaTyVarTcLevel_maybe :: TcTyVar -> Maybe TcLevel
1295 metaTyVarTcLevel_maybe tv
1296 = case tcTyVarDetails tv of
1297 MetaTv { mtv_tclvl = tclvl } -> Just tclvl
1298 _ -> Nothing
1299
1300 metaTyVarRef :: TyVar -> IORef MetaDetails
1301 metaTyVarRef tv
1302 = case tcTyVarDetails tv of
1303 MetaTv { mtv_ref = ref } -> ref
1304 _ -> pprPanic "metaTyVarRef" (ppr tv)
1305
1306 setMetaTyVarTcLevel :: TcTyVar -> TcLevel -> TcTyVar
1307 setMetaTyVarTcLevel tv tclvl
1308 = case tcTyVarDetails tv of
1309 details@(MetaTv {}) -> setTcTyVarDetails tv (details { mtv_tclvl = tclvl })
1310 _ -> pprPanic "metaTyVarTcLevel" (ppr tv)
1311
1312 isSigTyVar :: Var -> Bool
1313 isSigTyVar tv
1314 = case tcTyVarDetails tv of
1315 MetaTv { mtv_info = SigTv } -> True
1316 _ -> False
1317
1318 isFlexi, isIndirect :: MetaDetails -> Bool
1319 isFlexi Flexi = True
1320 isFlexi _ = False
1321
1322 isIndirect (Indirect _) = True
1323 isIndirect _ = False
1324
1325 isRuntimeUnkSkol :: TyVar -> Bool
1326 -- Called only in TcErrors; see Note [Runtime skolems] there
1327 isRuntimeUnkSkol x
1328 | RuntimeUnk <- tcTyVarDetails x = True
1329 | otherwise = False
1330
1331 mkTyVarNamePairs :: [TyVar] -> [(Name,TyVar)]
1332 -- Just pair each TyVar with its own name
1333 mkTyVarNamePairs tvs = [(tyVarName tv, tv) | tv <- tvs]
1334
1335 findDupSigTvs :: [(Name,TcTyVar)] -> [(Name,Name)]
1336 -- If we have [...(x1,tv)...(x2,tv)...]
1337 -- return (x1,x2) in the result list
1338 findDupSigTvs prs
1339 = concatMap mk_result_prs $
1340 findDupsEq eq_snd prs
1341 where
1342 eq_snd (_,tv1) (_,tv2) = tv1 == tv2
1343 mk_result_prs ((n1,_) :| xs) = map (\(n2,_) -> (n1,n2)) xs
1344
1345 {-
1346 ************************************************************************
1347 * *
1348 \subsection{Tau, sigma and rho}
1349 * *
1350 ************************************************************************
1351 -}
1352
1353 mkSigmaTy :: [TyVarBinder] -> [PredType] -> Type -> Type
1354 mkSigmaTy bndrs theta tau = mkForAllTys bndrs (mkPhiTy theta tau)
1355
1356 -- | Make a sigma ty where all type variables are 'Inferred'. That is,
1357 -- they cannot be used with visible type application.
1358 mkInfSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
1359 mkInfSigmaTy tyvars theta ty = mkSigmaTy (mkTyVarBinders Inferred tyvars) theta ty
1360
1361 -- | Make a sigma ty where all type variables are "specified". That is,
1362 -- they can be used with visible type application
1363 mkSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
1364 mkSpecSigmaTy tyvars preds ty = mkSigmaTy (mkTyVarBinders Specified tyvars) preds ty
1365
1366 mkPhiTy :: [PredType] -> Type -> Type
1367 mkPhiTy = mkFunTys
1368
1369 ---------------
1370 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
1371 -- construct a dictionary function name
1372 getDFunTyKey ty | Just ty' <- coreView ty = getDFunTyKey ty'
1373 getDFunTyKey (TyVarTy tv) = getOccName tv
1374 getDFunTyKey (TyConApp tc _) = getOccName tc
1375 getDFunTyKey (LitTy x) = getDFunTyLitKey x
1376 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
1377 getDFunTyKey (FunTy _ _) = getOccName funTyCon
1378 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
1379 getDFunTyKey (CastTy ty _) = getDFunTyKey ty
1380 getDFunTyKey t@(CoercionTy _) = pprPanic "getDFunTyKey" (ppr t)
1381
1382 getDFunTyLitKey :: TyLit -> OccName
1383 getDFunTyLitKey (NumTyLit n) = mkOccName Name.varName (show n)
1384 getDFunTyLitKey (StrTyLit n) = mkOccName Name.varName (show n) -- hm
1385
1386 ---------------
1387 mkNakedTyConApp :: TyCon -> [Type] -> Type
1388 -- Builds a TyConApp
1389 -- * without being strict in TyCon,
1390 -- * without satisfying the invariants of TyConApp
1391 -- A subsequent zonking will establish the invariants
1392 -- See Note [Type-checking inside the knot] in TcHsType
1393 mkNakedTyConApp tc tys = TyConApp tc tys
1394
1395 mkNakedAppTys :: Type -> [Type] -> Type
1396 -- See Note [Type-checking inside the knot] in TcHsType
1397 mkNakedAppTys ty1 [] = ty1
1398 mkNakedAppTys (TyConApp tc tys1) tys2 = mkNakedTyConApp tc (tys1 ++ tys2)
1399 mkNakedAppTys ty1 tys2 = foldl AppTy ty1 tys2
1400
1401 mkNakedAppTy :: Type -> Type -> Type
1402 -- See Note [Type-checking inside the knot] in TcHsType
1403 mkNakedAppTy ty1 ty2 = mkNakedAppTys ty1 [ty2]
1404
1405 mkNakedCastTy :: Type -> Coercion -> Type
1406 -- Do /not/ attempt to get rid of the cast altogether,
1407 -- even if it is Refl: see Note [The well-kinded type invariant]
1408 -- Even doing (t |> co1) |> co2 ---> t |> (co1;co2)
1409 -- does not seem worth the bother
1410 --
1411 -- NB: zonking will get rid of these casts, because it uses mkCastTy
1412 --
1413 -- In fact the calls to mkNakedCastTy ar pretty few and far between.
1414 mkNakedCastTy ty co = CastTy ty co
1415
1416 {- Note [The well-kinded type invariant]
1417 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1418 During type inference, we maintain the invariant that
1419
1420 INVARIANT: every type is well-kinded /without/ zonking
1421
1422 and in particular that typeKind does not fail (as it can for
1423 ill-kinded types).
1424
1425 Now suppose we are kind-checking the type (a Int), where (a :: kappa).
1426 Then in tcInferApps we'll run out of binders on a's kind, so
1427 we'll call matchExpectedFunKind, and unify
1428 kappa := kappa1 -> kappa2, with evidence co :: kappa ~ (kappa1 ~ kappa2)
1429 That evidence is actually Refl, but we must not discard the cast to
1430 form the result type
1431 ((a::kappa) (Int::*))
1432 bacause that does not satisfy the invariant, and crashes TypeKind. This
1433 caused Trac #14174 and #14520.
1434
1435 Solution: make mkNakedCastTy use an actual CastTy, without optimising
1436 for Refl. Now everything is well-kinded. The CastTy will be removed
1437 later, when we zonk. Still, it's distressingly delicate.
1438
1439 NB: mkNakedCastTy is only called in two places:
1440 in tcInferApps and in checkExpectedResultKind.
1441 See Note [The tcType invariant] in TcHsType.
1442 -}
1443
1444 {-
1445 ************************************************************************
1446 * *
1447 \subsection{Expanding and splitting}
1448 * *
1449 ************************************************************************
1450
1451 These tcSplit functions are like their non-Tc analogues, but
1452 *) they do not look through newtypes
1453
1454 However, they are non-monadic and do not follow through mutable type
1455 variables. It's up to you to make sure this doesn't matter.
1456 -}
1457
1458 -- | Splits a forall type into a list of 'TyBinder's and the inner type.
1459 -- Always succeeds, even if it returns an empty list.
1460 tcSplitPiTys :: Type -> ([TyBinder], Type)
1461 tcSplitPiTys = splitPiTys
1462
1463 -- | Splits a type into a TyBinder and a body, if possible. Panics otherwise
1464 tcSplitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
1465 tcSplitPiTy_maybe = splitPiTy_maybe
1466
1467 tcSplitForAllTy_maybe :: Type -> Maybe (TyVarBinder, Type)
1468 tcSplitForAllTy_maybe ty | Just ty' <- tcView ty = tcSplitForAllTy_maybe ty'
1469 tcSplitForAllTy_maybe (ForAllTy tv ty) = Just (tv, ty)
1470 tcSplitForAllTy_maybe _ = Nothing
1471
1472 -- | Like 'tcSplitPiTys', but splits off only named binders, returning
1473 -- just the tycovars.
1474 tcSplitForAllTys :: Type -> ([TyVar], Type)
1475 tcSplitForAllTys = splitForAllTys
1476
1477 -- | Like 'tcSplitForAllTys', but splits off only named binders.
1478 tcSplitForAllTyVarBndrs :: Type -> ([TyVarBinder], Type)
1479 tcSplitForAllTyVarBndrs = splitForAllTyVarBndrs
1480
1481 -- | Is this a ForAllTy with a named binder?
1482 tcIsForAllTy :: Type -> Bool
1483 tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
1484 tcIsForAllTy (ForAllTy {}) = True
1485 tcIsForAllTy _ = False
1486
1487 tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
1488 -- Split off the first predicate argument from a type
1489 tcSplitPredFunTy_maybe ty
1490 | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
1491 tcSplitPredFunTy_maybe (FunTy arg res)
1492 | isPredTy arg = Just (arg, res)
1493 tcSplitPredFunTy_maybe _
1494 = Nothing
1495
1496 tcSplitPhiTy :: Type -> (ThetaType, Type)
1497 tcSplitPhiTy ty
1498 = split ty []
1499 where
1500 split ty ts
1501 = case tcSplitPredFunTy_maybe ty of
1502 Just (pred, ty) -> split ty (pred:ts)
1503 Nothing -> (reverse ts, ty)
1504
1505 -- | Split a sigma type into its parts.
1506 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
1507 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
1508 (tvs, rho) -> case tcSplitPhiTy rho of
1509 (theta, tau) -> (tvs, theta, tau)
1510
1511 -- | Split a sigma type into its parts, going underneath as many @ForAllTy@s
1512 -- as possible. For example, given this type synonym:
1513 --
1514 -- @
1515 -- type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
1516 -- @
1517 --
1518 -- if you called @tcSplitSigmaTy@ on this type:
1519 --
1520 -- @
1521 -- forall s t a b. Each s t a b => Traversal s t a b
1522 -- @
1523 --
1524 -- then it would return @([s,t,a,b], [Each s t a b], Traversal s t a b)@. But
1525 -- if you instead called @tcSplitNestedSigmaTys@ on the type, it would return
1526 -- @([s,t,a,b,f], [Each s t a b, Applicative f], (a -> f b) -> s -> f t)@.
1527 tcSplitNestedSigmaTys :: Type -> ([TyVar], ThetaType, Type)
1528 -- NB: This is basically a pure version of deeplyInstantiate (from Inst) that
1529 -- doesn't compute an HsWrapper.
1530 tcSplitNestedSigmaTys ty
1531 -- If there's a forall, split it apart and try splitting the rho type
1532 -- underneath it.
1533 | Just (arg_tys, tvs1, theta1, rho1) <- tcDeepSplitSigmaTy_maybe ty
1534 = let (tvs2, theta2, rho2) = tcSplitNestedSigmaTys rho1
1535 in (tvs1 ++ tvs2, theta1 ++ theta2, mkFunTys arg_tys rho2)
1536 -- If there's no forall, we're done.
1537 | otherwise = ([], [], ty)
1538
1539 -----------------------
1540 tcDeepSplitSigmaTy_maybe
1541 :: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType)
1542 -- Looks for a *non-trivial* quantified type, under zero or more function arrows
1543 -- By "non-trivial" we mean either tyvars or constraints are non-empty
1544
1545 tcDeepSplitSigmaTy_maybe ty
1546 | Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty
1547 , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty
1548 = Just (arg_ty:arg_tys, tvs, theta, rho)
1549
1550 | (tvs, theta, rho) <- tcSplitSigmaTy ty
1551 , not (null tvs && null theta)
1552 = Just ([], tvs, theta, rho)
1553
1554 | otherwise = Nothing
1555
1556 -----------------------
1557 tcTyConAppTyCon :: Type -> TyCon
1558 tcTyConAppTyCon ty
1559 = case tcTyConAppTyCon_maybe ty of
1560 Just tc -> tc
1561 Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
1562
1563 -- | Like 'tcRepSplitTyConApp_maybe', but only returns the 'TyCon'.
1564 tcTyConAppTyCon_maybe :: Type -> Maybe TyCon
1565 tcTyConAppTyCon_maybe ty
1566 | Just ty' <- tcView ty = tcTyConAppTyCon_maybe ty'
1567 tcTyConAppTyCon_maybe (TyConApp tc _)
1568 = Just tc
1569 tcTyConAppTyCon_maybe (FunTy _ _)
1570 = Just funTyCon
1571 tcTyConAppTyCon_maybe _
1572 = Nothing
1573
1574 tcTyConAppArgs :: Type -> [Type]
1575 tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
1576 Just (_, args) -> args
1577 Nothing -> pprPanic "tcTyConAppArgs" (pprType ty)
1578
1579 tcSplitTyConApp :: Type -> (TyCon, [Type])
1580 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
1581 Just stuff -> stuff
1582 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
1583
1584 -- | Like 'tcRepSplitTyConApp_maybe', but returns 'Nothing' if,
1585 --
1586 -- 1. the type is structurally not a type constructor application, or
1587 --
1588 -- 2. the type is a function type (e.g. application of 'funTyCon'), but we
1589 -- currently don't even enough information to fully determine its RuntimeRep
1590 -- variables. For instance, @FunTy (a :: k) Int@.
1591 --
1592 -- By contrast 'tcRepSplitTyConApp_maybe' panics in the second case.
1593 --
1594 -- The behavior here is needed during canonicalization; see Note [FunTy and
1595 -- decomposing tycon applications] in TcCanonical for details.
1596 tcRepSplitTyConApp_maybe' :: HasCallStack => Type -> Maybe (TyCon, [Type])
1597 tcRepSplitTyConApp_maybe' (TyConApp tc tys) = Just (tc, tys)
1598 tcRepSplitTyConApp_maybe' (FunTy arg res)
1599 | Just arg_rep <- getRuntimeRep_maybe arg
1600 , Just res_rep <- getRuntimeRep_maybe res
1601 = Just (funTyCon, [arg_rep, res_rep, arg, res])
1602 tcRepSplitTyConApp_maybe' _ = Nothing
1603
1604
1605 -----------------------
1606 tcSplitFunTys :: Type -> ([Type], Type)
1607 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
1608 Nothing -> ([], ty)
1609 Just (arg,res) -> (arg:args, res')
1610 where
1611 (args,res') = tcSplitFunTys res
1612
1613 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
1614 tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
1615 tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
1616 tcSplitFunTy_maybe _ = Nothing
1617 -- Note the typeKind guard
1618 -- Consider (?x::Int) => Bool
1619 -- We don't want to treat this as a function type!
1620 -- A concrete example is test tc230:
1621 -- f :: () -> (?p :: ()) => () -> ()
1622 --
1623 -- g = f () ()
1624
1625 tcSplitFunTysN :: Arity -- N: Number of desired args
1626 -> TcRhoType
1627 -> Either Arity -- Number of missing arrows
1628 ([TcSigmaType], -- Arg types (always N types)
1629 TcSigmaType) -- The rest of the type
1630 -- ^ Split off exactly the specified number argument types
1631 -- Returns
1632 -- (Left m) if there are 'm' missing arrows in the type
1633 -- (Right (tys,res)) if the type looks like t1 -> ... -> tn -> res
1634 tcSplitFunTysN n ty
1635 | n == 0
1636 = Right ([], ty)
1637 | Just (arg,res) <- tcSplitFunTy_maybe ty
1638 = case tcSplitFunTysN (n-1) res of
1639 Left m -> Left m
1640 Right (args,body) -> Right (arg:args, body)
1641 | otherwise
1642 = Left n
1643
1644 tcSplitFunTy :: Type -> (Type, Type)
1645 tcSplitFunTy ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
1646
1647 tcFunArgTy :: Type -> Type
1648 tcFunArgTy ty = fst (tcSplitFunTy ty)
1649
1650 tcFunResultTy :: Type -> Type
1651 tcFunResultTy ty = snd (tcSplitFunTy ty)
1652
1653 -- | Strips off n *visible* arguments and returns the resulting type
1654 tcFunResultTyN :: HasDebugCallStack => Arity -> Type -> Type
1655 tcFunResultTyN n ty
1656 | Right (_, res_ty) <- tcSplitFunTysN n ty
1657 = res_ty
1658 | otherwise
1659 = pprPanic "tcFunResultTyN" (ppr n <+> ppr ty)
1660
1661 -----------------------
1662 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
1663 tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
1664 tcSplitAppTy_maybe ty = tcRepSplitAppTy_maybe ty
1665
1666 tcSplitAppTy :: Type -> (Type, Type)
1667 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
1668 Just stuff -> stuff
1669 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
1670
1671 tcSplitAppTys :: Type -> (Type, [Type])
1672 tcSplitAppTys ty
1673 = go ty []
1674 where
1675 go ty args = case tcSplitAppTy_maybe ty of
1676 Just (ty', arg) -> go ty' (arg:args)
1677 Nothing -> (ty,args)
1678
1679 -- | Returns the number of arguments in the given type, without
1680 -- looking through synonyms. This is used only for error reporting.
1681 -- We don't look through synonyms because of #11313.
1682 tcRepGetNumAppTys :: Type -> Arity
1683 tcRepGetNumAppTys = length . snd . repSplitAppTys
1684
1685 -----------------------
1686 -- | If the type is a tyvar, possibly under a cast, returns it, along
1687 -- with the coercion. Thus, the co is :: kind tv ~N kind type
1688 tcGetCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN)
1689 tcGetCastedTyVar_maybe ty | Just ty' <- tcView ty = tcGetCastedTyVar_maybe ty'
1690 tcGetCastedTyVar_maybe (CastTy (TyVarTy tv) co) = Just (tv, co)
1691 tcGetCastedTyVar_maybe (TyVarTy tv) = Just (tv, mkNomReflCo (tyVarKind tv))
1692 tcGetCastedTyVar_maybe _ = Nothing
1693
1694 tcGetTyVar_maybe :: Type -> Maybe TyVar
1695 tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
1696 tcGetTyVar_maybe (TyVarTy tv) = Just tv
1697 tcGetTyVar_maybe _ = Nothing
1698
1699 tcGetTyVar :: String -> Type -> TyVar
1700 tcGetTyVar msg ty
1701 = case tcGetTyVar_maybe ty of
1702 Just tv -> tv
1703 Nothing -> pprPanic msg (ppr ty)
1704
1705 tcIsTyVarTy :: Type -> Bool
1706 tcIsTyVarTy ty | Just ty' <- tcView ty = tcIsTyVarTy ty'
1707 tcIsTyVarTy (CastTy ty _) = tcIsTyVarTy ty -- look through casts, as
1708 -- this is only used for
1709 -- e.g., FlexibleContexts
1710 tcIsTyVarTy (TyVarTy _) = True
1711 tcIsTyVarTy _ = False
1712
1713 -----------------------
1714 tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
1715 -- Split the type of a dictionary function
1716 -- We don't use tcSplitSigmaTy, because a DFun may (with NDP)
1717 -- have non-Pred arguments, such as
1718 -- df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
1719 --
1720 -- Also NB splitFunTys, not tcSplitFunTys;
1721 -- the latter specifically stops at PredTy arguments,
1722 -- and we don't want to do that here
1723 tcSplitDFunTy ty
1724 = case tcSplitForAllTys ty of { (tvs, rho) ->
1725 case splitFunTys rho of { (theta, tau) ->
1726 case tcSplitDFunHead tau of { (clas, tys) ->
1727 (tvs, theta, clas, tys) }}}
1728
1729 tcSplitDFunHead :: Type -> (Class, [Type])
1730 tcSplitDFunHead = getClassPredTys
1731
1732 tcSplitMethodTy :: Type -> ([TyVar], PredType, Type)
1733 -- A class method (selector) always has a type like
1734 -- forall as. C as => blah
1735 -- So if the class looks like
1736 -- class C a where
1737 -- op :: forall b. (Eq a, Ix b) => a -> b
1738 -- the class method type looks like
1739 -- op :: forall a. C a => forall b. (Eq a, Ix b) => a -> b
1740 --
1741 -- tcSplitMethodTy just peels off the outer forall and
1742 -- that first predicate
1743 tcSplitMethodTy ty
1744 | (sel_tyvars,sel_rho) <- tcSplitForAllTys ty
1745 , Just (first_pred, local_meth_ty) <- tcSplitPredFunTy_maybe sel_rho
1746 = (sel_tyvars, first_pred, local_meth_ty)
1747 | otherwise
1748 = pprPanic "tcSplitMethodTy" (ppr ty)
1749
1750
1751 {- *********************************************************************
1752 * *
1753 Type equalities
1754 * *
1755 ********************************************************************* -}
1756
1757 tcEqKind :: HasDebugCallStack => TcKind -> TcKind -> Bool
1758 tcEqKind = tcEqType
1759
1760 tcEqType :: HasDebugCallStack => TcType -> TcType -> Bool
1761 -- tcEqType is a proper implements the same Note [Non-trivial definitional
1762 -- equality] (in TyCoRep) as `eqType`, but Type.eqType believes (* ==
1763 -- Constraint), and that is NOT what we want in the type checker!
1764 tcEqType ty1 ty2
1765 = isNothing (tc_eq_type tcView ki1 ki2) &&
1766 isNothing (tc_eq_type tcView ty1 ty2)
1767 where
1768 ki1 = typeKind ty1
1769 ki2 = typeKind ty2
1770
1771 -- | Just like 'tcEqType', but will return True for types of different kinds
1772 -- as long as their non-coercion structure is identical.
1773 tcEqTypeNoKindCheck :: TcType -> TcType -> Bool
1774 tcEqTypeNoKindCheck ty1 ty2
1775 = isNothing $ tc_eq_type tcView ty1 ty2
1776
1777 -- | Like 'tcEqType', but returns information about whether the difference
1778 -- is visible in the case of a mismatch.
1779 -- @Nothing@ : the types are equal
1780 -- @Just True@ : the types differ, and the point of difference is visible
1781 -- @Just False@ : the types differ, and the point of difference is invisible
1782 tcEqTypeVis :: TcType -> TcType -> Maybe Bool
1783 tcEqTypeVis ty1 ty2
1784 = tc_eq_type tcView ty1 ty2 <!> invis (tc_eq_type tcView ki1 ki2)
1785 where
1786 ki1 = typeKind ty1
1787 ki2 = typeKind ty2
1788
1789 -- convert Just True to Just False
1790 invis :: Maybe Bool -> Maybe Bool
1791 invis = fmap (const False)
1792
1793 (<!>) :: Maybe Bool -> Maybe Bool -> Maybe Bool
1794 Nothing <!> x = x
1795 Just True <!> _ = Just True
1796 Just _vis <!> Just True = Just True
1797 Just vis <!> _ = Just vis
1798 infixr 3 <!>
1799
1800 -- | Real worker for 'tcEqType'. No kind check!
1801 tc_eq_type :: (TcType -> Maybe TcType) -- ^ @tcView@, if you want unwrapping
1802 -> Type -> Type -> Maybe Bool
1803 tc_eq_type view_fun orig_ty1 orig_ty2 = go True orig_env orig_ty1 orig_ty2
1804 where
1805 go :: Bool -> RnEnv2 -> Type -> Type -> Maybe Bool
1806 go vis env t1 t2 | Just t1' <- view_fun t1 = go vis env t1' t2
1807 go vis env t1 t2 | Just t2' <- view_fun t2 = go vis env t1 t2'
1808
1809 go vis env (TyVarTy tv1) (TyVarTy tv2)
1810 = check vis $ rnOccL env tv1 == rnOccR env tv2
1811
1812 go vis _ (LitTy lit1) (LitTy lit2)
1813 = check vis $ lit1 == lit2
1814
1815 go vis env (ForAllTy (TvBndr tv1 vis1) ty1)
1816 (ForAllTy (TvBndr tv2 vis2) ty2)
1817 = go (isVisibleArgFlag vis1) env (tyVarKind tv1) (tyVarKind tv2)
1818 <!> go vis (rnBndr2 env tv1 tv2) ty1 ty2
1819 <!> check vis (vis1 == vis2)
1820 -- Make sure we handle all FunTy cases since falling through to the
1821 -- AppTy case means that tcRepSplitAppTy_maybe may see an unzonked
1822 -- kind variable, which causes things to blow up.
1823 go vis env (FunTy arg1 res1) (FunTy arg2 res2)
1824 = go vis env arg1 arg2 <!> go vis env res1 res2
1825 go vis env ty (FunTy arg res)
1826 = eqFunTy vis env arg res ty
1827 go vis env (FunTy arg res) ty
1828 = eqFunTy vis env arg res ty
1829
1830 -- See Note [Equality on AppTys] in Type
1831 go vis env (AppTy s1 t1) ty2
1832 | Just (s2, t2) <- tcRepSplitAppTy_maybe ty2
1833 = go vis env s1 s2 <!> go vis env t1 t2
1834 go vis env ty1 (AppTy s2 t2)
1835 | Just (s1, t1) <- tcRepSplitAppTy_maybe ty1
1836 = go vis env s1 s2 <!> go vis env t1 t2
1837 go vis env (TyConApp tc1 ts1) (TyConApp tc2 ts2)
1838 = check vis (tc1 == tc2) <!> gos (tc_vis vis tc1) env ts1 ts2
1839 go vis env (CastTy t1 _) t2 = go vis env t1 t2
1840 go vis env t1 (CastTy t2 _) = go vis env t1 t2
1841 go _ _ (CoercionTy {}) (CoercionTy {}) = Nothing
1842 go vis _ _ _ = Just vis
1843
1844 gos _ _ [] [] = Nothing
1845 gos (v:vs) env (t1:ts1) (t2:ts2) = go v env t1 t2 <!> gos vs env ts1 ts2
1846 gos (v:_) _ _ _ = Just v
1847 gos _ _ _ _ = panic "tc_eq_type"
1848
1849 tc_vis :: Bool -> TyCon -> [Bool]
1850 tc_vis True tc = viss ++ repeat True
1851 -- the repeat True is necessary because tycons can legitimately
1852 -- be oversaturated
1853 where
1854 bndrs = tyConBinders tc
1855 viss = map isVisibleTyConBinder bndrs
1856 tc_vis False _ = repeat False -- if we're not in a visible context, our args
1857 -- aren't either
1858
1859 check :: Bool -> Bool -> Maybe Bool
1860 check _ True = Nothing
1861 check vis False = Just vis
1862
1863 orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
1864
1865 -- @eqFunTy arg res ty@ is True when @ty@ equals @FunTy arg res@. This is
1866 -- sometimes hard to know directly because @ty@ might have some casts
1867 -- obscuring the FunTy. And 'splitAppTy' is difficult because we can't
1868 -- always extract a RuntimeRep (see Note [xyz]) if the kind of the arg or
1869 -- res is unzonked/unflattened. Thus this function, which handles this
1870 -- corner case.
1871 eqFunTy :: Bool -> RnEnv2 -> Type -> Type -> Type -> Maybe Bool
1872 eqFunTy vis env arg res (FunTy arg' res')
1873 = go vis env arg arg' <!> go vis env res res'
1874 eqFunTy vis env arg res ty@(AppTy{})
1875 | Just (tc, [_, _, arg', res']) <- get_args ty []
1876 , tc == funTyCon
1877 = go vis env arg arg' <!> go vis env res res'
1878 where
1879 get_args :: Type -> [Type] -> Maybe (TyCon, [Type])
1880 get_args (AppTy f x) args = get_args f (x:args)
1881 get_args (CastTy t _) args = get_args t args
1882 get_args (TyConApp tc tys) args = Just (tc, tys ++ args)
1883 get_args _ _ = Nothing
1884 eqFunTy vis _ _ _ _
1885 = Just vis
1886
1887 -- | Like 'pickyEqTypeVis', but returns a Bool for convenience
1888 pickyEqType :: TcType -> TcType -> Bool
1889 -- Check when two types _look_ the same, _including_ synonyms.
1890 -- So (pickyEqType String [Char]) returns False
1891 -- This ignores kinds and coercions, because this is used only for printing.
1892 pickyEqType ty1 ty2
1893 = isNothing $
1894 tc_eq_type (const Nothing) ty1 ty2
1895
1896 {- *********************************************************************
1897 * *
1898 Predicate types
1899 * *
1900 ************************************************************************
1901
1902 Deconstructors and tests on predicate types
1903
1904 Note [Kind polymorphic type classes]
1905 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1906 class C f where... -- C :: forall k. k -> Constraint
1907 g :: forall (f::*). C f => f -> f
1908
1909 Here the (C f) in the signature is really (C * f), and we
1910 don't want to complain that the * isn't a type variable!
1911 -}
1912
1913 isTyVarClassPred :: PredType -> Bool
1914 isTyVarClassPred ty = case getClassPredTys_maybe ty of
1915 Just (_, tys) -> all isTyVarTy tys
1916 _ -> False
1917
1918 -------------------------
1919 checkValidClsArgs :: Bool -> Class -> [KindOrType] -> Bool
1920 -- If the Bool is True (flexible contexts), return True (i.e. ok)
1921 -- Otherwise, check that the type (not kind) args are all headed by a tyvar
1922 -- E.g. (Eq a) accepted, (Eq (f a)) accepted, but (Eq Int) rejected
1923 -- This function is here rather than in TcValidity because it is
1924 -- called from TcSimplify, which itself is imported by TcValidity
1925 checkValidClsArgs flexible_contexts cls kts
1926 | flexible_contexts = True
1927 | otherwise = all hasTyVarHead tys
1928 where
1929 tys = filterOutInvisibleTypes (classTyCon cls) kts
1930
1931 hasTyVarHead :: Type -> Bool
1932 -- Returns true of (a t1 .. tn), where 'a' is a type variable
1933 hasTyVarHead ty -- Haskell 98 allows predicates of form
1934 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1935 | otherwise -- where a is a type variable
1936 = case tcSplitAppTy_maybe ty of
1937 Just (ty, _) -> hasTyVarHead ty
1938 Nothing -> False
1939
1940 evVarPred_maybe :: EvVar -> Maybe PredType
1941 evVarPred_maybe v = if isPredTy ty then Just ty else Nothing
1942 where ty = varType v
1943
1944 evVarPred :: EvVar -> PredType
1945 evVarPred var
1946 | debugIsOn
1947 = case evVarPred_maybe var of
1948 Just pred -> pred
1949 Nothing -> pprPanic "tcEvVarPred" (ppr var <+> ppr (varType var))
1950 | otherwise
1951 = varType var
1952
1953 ------------------
1954 -- | When inferring types, should we quantify over a given predicate?
1955 -- Generally true of classes; generally false of equality constraints.
1956 -- Equality constraints that mention quantified type variables and
1957 -- implicit variables complicate the story. See Notes
1958 -- [Inheriting implicit parameters] and [Quantifying over equality constraints]
1959 pickQuantifiablePreds
1960 :: TyVarSet -- Quantifying over these
1961 -> TcThetaType -- Proposed constraints to quantify
1962 -> TcThetaType -- A subset that we can actually quantify
1963 -- This function decides whether a particular constraint should be
1964 -- quantified over, given the type variables that are being quantified
1965 pickQuantifiablePreds qtvs theta
1966 = let flex_ctxt = True in -- Quantify over non-tyvar constraints, even without
1967 -- -XFlexibleContexts: see Trac #10608, #10351
1968 -- flex_ctxt <- xoptM Opt_FlexibleContexts
1969 filter (pick_me flex_ctxt) theta
1970 where
1971 pick_me flex_ctxt pred
1972 = case classifyPredType pred of
1973
1974 ClassPred cls tys
1975 | Just {} <- isCallStackPred cls tys
1976 -- NEVER infer a CallStack constraint
1977 -- Otherwise, we let the constraints bubble up to be
1978 -- solved from the outer context, or be defaulted when we
1979 -- reach the top-level.
1980 -- see Note [Overview of implicit CallStacks]
1981 -> False
1982
1983 | isIPClass cls -> True -- See note [Inheriting implicit parameters]
1984
1985 | otherwise
1986 -> pick_cls_pred flex_ctxt cls tys
1987
1988 EqPred ReprEq ty1 ty2 -> pick_cls_pred flex_ctxt coercibleClass [ty1, ty2]
1989 -- representational equality is like a class constraint
1990
1991 EqPred NomEq ty1 ty2 -> quant_fun ty1 || quant_fun ty2
1992 IrredPred ty -> tyCoVarsOfType ty `intersectsVarSet` qtvs
1993
1994 pick_cls_pred flex_ctxt cls tys
1995 = tyCoVarsOfTypes tys `intersectsVarSet` qtvs
1996 && (checkValidClsArgs flex_ctxt cls tys)
1997 -- Only quantify over predicates that checkValidType
1998 -- will pass! See Trac #10351.
1999
2000 -- See Note [Quantifying over equality constraints]
2001 quant_fun ty
2002 = case tcSplitTyConApp_maybe ty of
2003 Just (tc, tys) | isTypeFamilyTyCon tc
2004 -> tyCoVarsOfTypes tys `intersectsVarSet` qtvs
2005 _ -> False
2006
2007 pickCapturedPreds
2008 :: TyVarSet -- Quantifying over these
2009 -> TcThetaType -- Proposed constraints to quantify
2010 -> TcThetaType -- A subset that we can actually quantify
2011 -- A simpler version of pickQuantifiablePreds, used to winnow down
2012 -- the inferred constraints of a group of bindings, into those for
2013 -- one particular identifier
2014 pickCapturedPreds qtvs theta
2015 = filter captured theta
2016 where
2017 captured pred = isIPPred pred || (tyCoVarsOfType pred `intersectsVarSet` qtvs)
2018
2019
2020 -- Superclasses
2021
2022 type PredWithSCs a = (PredType, [PredType], a)
2023
2024 mkMinimalBySCs :: forall a. (a -> PredType) -> [a] -> [a]
2025 -- Remove predicates that
2026 --
2027 -- - are the same as another predicate
2028 --
2029 -- - can be deduced from another by superclasses,
2030 --
2031 -- - are a reflexive equality (e.g * ~ *)
2032 -- (see Note [Remove redundant provided dicts] in PatSyn)
2033 --
2034 -- The result is a subset of the input.
2035 -- The 'a' is just paired up with the PredType;
2036 -- typically it might be a dictionary Id
2037 mkMinimalBySCs get_pred xs = go preds_with_scs []
2038 where
2039 preds_with_scs :: [PredWithSCs a]
2040 preds_with_scs = [ (pred, pred : transSuperClasses pred, x)
2041 | x <- xs
2042 , let pred = get_pred x ]
2043
2044 go :: [PredWithSCs a] -- Work list
2045 -> [PredWithSCs a] -- Accumulating result
2046 -> [a]
2047 go [] min_preds
2048 = reverse (map thdOf3 min_preds)
2049 -- The 'reverse' isn't strictly necessary, but it
2050 -- means that the results are returned in the same
2051 -- order as the input, which is generally saner
2052 go (work_item@(p,_,_) : work_list) min_preds
2053 | EqPred _ t1 t2 <- classifyPredType p
2054 , t1 `tcEqType` t2 -- See Note [Discard reflexive equalities]
2055 = go work_list min_preds
2056 | p `in_cloud` work_list || p `in_cloud` min_preds
2057 = go work_list min_preds
2058 | otherwise
2059 = go work_list (work_item : min_preds)
2060
2061 in_cloud :: PredType -> [PredWithSCs a] -> Bool
2062 in_cloud p ps = or [ p `tcEqType` p' | (_, scs, _) <- ps, p' <- scs ]
2063
2064 transSuperClasses :: PredType -> [PredType]
2065 -- (transSuperClasses p) returns (p's superclasses) not including p
2066 -- Stop if you encounter the same class again
2067 -- See Note [Expanding superclasses]
2068 transSuperClasses p
2069 = go emptyNameSet p
2070 where
2071 go :: NameSet -> PredType -> [PredType]
2072 go rec_clss p
2073 | ClassPred cls tys <- classifyPredType p
2074 , let cls_nm = className cls
2075 , not (cls_nm `elemNameSet` rec_clss)
2076 , let rec_clss' | isCTupleClass cls = rec_clss
2077 | otherwise = rec_clss `extendNameSet` cls_nm
2078 = [ p' | sc <- immSuperClasses cls tys
2079 , p' <- sc : go rec_clss' sc ]
2080 | otherwise
2081 = []
2082
2083 immSuperClasses :: Class -> [Type] -> [PredType]
2084 immSuperClasses cls tys
2085 = substTheta (zipTvSubst tyvars tys) sc_theta
2086 where
2087 (tyvars,sc_theta,_,_) = classBigSig cls
2088
2089 isImprovementPred :: PredType -> Bool
2090 -- Either it's an equality, or has some functional dependency
2091 isImprovementPred ty
2092 = case classifyPredType ty of
2093 EqPred NomEq t1 t2 -> not (t1 `tcEqType` t2)
2094 EqPred ReprEq _ _ -> False
2095 ClassPred cls _ -> classHasFds cls
2096 IrredPred {} -> True -- Might have equalities after reduction?
2097
2098 {- Note [Expanding superclasses]
2099 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2100 When we expand superclasses, we use the following algorithm:
2101
2102 expand( so_far, pred ) returns the transitive superclasses of pred,
2103 not including pred itself
2104 1. If pred is not a class constraint, return empty set
2105 Otherwise pred = C ts
2106 2. If C is in so_far, return empty set (breaks loops)
2107 3. Find the immediate superclasses constraints of (C ts)
2108 4. For each such sc_pred, return (sc_pred : expand( so_far+C, D ss )
2109
2110 Notice that
2111
2112 * With normal Haskell-98 classes, the loop-detector will never bite,
2113 so we'll get all the superclasses.
2114
2115 * Since there is only a finite number of distinct classes, expansion
2116 must terminate.
2117
2118 * The loop breaking is a bit conservative. Notably, a tuple class
2119 could contain many times without threatening termination:
2120 (Eq a, (Ord a, Ix a))
2121 And this is try of any class that we can statically guarantee
2122 as non-recursive (in some sense). For now, we just make a special
2123 case for tuples. Something better would be cool.
2124
2125 See also TcTyDecls.checkClassCycles.
2126
2127 Note [Inheriting implicit parameters]
2128 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2129 Consider this:
2130
2131 f x = (x::Int) + ?y
2132
2133 where f is *not* a top-level binding.
2134 From the RHS of f we'll get the constraint (?y::Int).
2135 There are two types we might infer for f:
2136
2137 f :: Int -> Int
2138
2139 (so we get ?y from the context of f's definition), or
2140
2141 f :: (?y::Int) => Int -> Int
2142
2143 At first you might think the first was better, because then
2144 ?y behaves like a free variable of the definition, rather than
2145 having to be passed at each call site. But of course, the WHOLE
2146 IDEA is that ?y should be passed at each call site (that's what
2147 dynamic binding means) so we'd better infer the second.
2148
2149 BOTTOM LINE: when *inferring types* you must quantify over implicit
2150 parameters, *even if* they don't mention the bound type variables.
2151 Reason: because implicit parameters, uniquely, have local instance
2152 declarations. See pickQuantifiablePreds.
2153
2154 Note [Quantifying over equality constraints]
2155 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2156 Should we quantify over an equality constraint (s ~ t)? In general, we don't.
2157 Doing so may simply postpone a type error from the function definition site to
2158 its call site. (At worst, imagine (Int ~ Bool)).
2159
2160 However, consider this
2161 forall a. (F [a] ~ Int) => blah
2162 Should we quantify over the (F [a] ~ Int). Perhaps yes, because at the call
2163 site we will know 'a', and perhaps we have instance F [Bool] = Int.
2164 So we *do* quantify over a type-family equality where the arguments mention
2165 the quantified variables.
2166
2167 ************************************************************************
2168 * *
2169 \subsection{Predicates}
2170 * *
2171 ************************************************************************
2172 -}
2173
2174 isSigmaTy :: TcType -> Bool
2175 -- isSigmaTy returns true of any qualified type. It doesn't
2176 -- *necessarily* have any foralls. E.g
2177 -- f :: (?x::Int) => Int -> Int
2178 isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
2179 isSigmaTy (ForAllTy {}) = True
2180 isSigmaTy (FunTy a _) = isPredTy a
2181 isSigmaTy _ = False
2182
2183 isRhoTy :: TcType -> Bool -- True of TcRhoTypes; see Note [TcRhoType]
2184 isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty'
2185 isRhoTy (ForAllTy {}) = False
2186 isRhoTy (FunTy a r) = not (isPredTy a) && isRhoTy r
2187 isRhoTy _ = True
2188
2189 -- | Like 'isRhoTy', but also says 'True' for 'Infer' types
2190 isRhoExpTy :: ExpType -> Bool
2191 isRhoExpTy (Check ty) = isRhoTy ty
2192 isRhoExpTy (Infer {}) = True
2193
2194 isOverloadedTy :: Type -> Bool
2195 -- Yes for a type of a function that might require evidence-passing
2196 -- Used only by bindLocalMethods
2197 isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
2198 isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty
2199 isOverloadedTy (FunTy a _) = isPredTy a
2200 isOverloadedTy _ = False
2201
2202 isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
2203 isUnitTy, isCharTy, isAnyTy :: Type -> Bool
2204 isFloatTy = is_tc floatTyConKey
2205 isDoubleTy = is_tc doubleTyConKey
2206 isIntegerTy = is_tc integerTyConKey
2207 isIntTy = is_tc intTyConKey
2208 isWordTy = is_tc wordTyConKey
2209 isBoolTy = is_tc boolTyConKey
2210 isUnitTy = is_tc unitTyConKey
2211 isCharTy = is_tc charTyConKey
2212 isAnyTy = is_tc anyTyConKey
2213
2214 -- | Does a type represent a floating-point number?
2215 isFloatingTy :: Type -> Bool
2216 isFloatingTy ty = isFloatTy ty || isDoubleTy ty
2217
2218 -- | Is a type 'String'?
2219 isStringTy :: Type -> Bool
2220 isStringTy ty
2221 = case tcSplitTyConApp_maybe ty of
2222 Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty
2223 _ -> False
2224
2225 -- | Is a type a 'CallStack'?
2226 isCallStackTy :: Type -> Bool
2227 isCallStackTy ty
2228 | Just tc <- tyConAppTyCon_maybe ty
2229 = tc `hasKey` callStackTyConKey
2230 | otherwise
2231 = False
2232
2233 -- | Is a 'PredType' a 'CallStack' implicit parameter?
2234 --
2235 -- If so, return the name of the parameter.
2236 isCallStackPred :: Class -> [Type] -> Maybe FastString
2237 isCallStackPred cls tys
2238 | [ty1, ty2] <- tys
2239 , isIPClass cls
2240 , isCallStackTy ty2
2241 = isStrLitTy ty1
2242 | otherwise
2243 = Nothing
2244
2245 hasIPPred :: PredType -> Bool
2246 hasIPPred pred
2247 = case classifyPredType pred of
2248 ClassPred cls tys
2249 | isIPClass cls -> True
2250 | isCTupleClass cls -> any hasIPPred tys
2251 _other -> False
2252
2253 is_tc :: Unique -> Type -> Bool
2254 -- Newtypes are opaque to this
2255 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
2256 Just (tc, _) -> uniq == getUnique tc
2257 Nothing -> False
2258
2259 -- | Does the given tyvar appear at the head of a chain of applications
2260 -- (a t1 ... tn)
2261 isTyVarHead :: TcTyVar -> TcType -> Bool
2262 isTyVarHead tv (TyVarTy tv') = tv == tv'
2263 isTyVarHead tv (AppTy fun _) = isTyVarHead tv fun
2264 isTyVarHead tv (CastTy ty _) = isTyVarHead tv ty
2265 isTyVarHead _ (TyConApp {}) = False
2266 isTyVarHead _ (LitTy {}) = False
2267 isTyVarHead _ (ForAllTy {}) = False
2268 isTyVarHead _ (FunTy {}) = False
2269 isTyVarHead _ (CoercionTy {}) = False
2270
2271 -- | Is the equality
2272 -- a ~r ...a....
2273 -- definitely insoluble or not?
2274 -- a ~r Maybe a -- Definitely insoluble
2275 -- a ~N ...(F a)... -- Not definitely insoluble
2276 -- -- Perhaps (F a) reduces to Int
2277 -- a ~R ...(N a)... -- Not definitely insoluble
2278 -- -- Perhaps newtype N a = MkN Int
2279 -- See Note [Occurs check error] in
2280 -- TcCanonical for the motivation for this function.
2281 isInsolubleOccursCheck :: EqRel -> TcTyVar -> TcType -> Bool
2282 isInsolubleOccursCheck eq_rel tv ty
2283 = go ty
2284 where
2285 go ty | Just ty' <- tcView ty = go ty'
2286 go (TyVarTy tv') = tv == tv' || go (tyVarKind tv')
2287 go (LitTy {}) = False
2288 go (AppTy t1 t2) = case eq_rel of -- See Note [AppTy and ReprEq]
2289 NomEq -> go t1 || go t2
2290 ReprEq -> go t1
2291 go (FunTy t1 t2) = go t1 || go t2
2292 go (ForAllTy (TvBndr tv' _) inner_ty)
2293 | tv' == tv = False
2294 | otherwise = go (tyVarKind tv') || go inner_ty
2295 go (CastTy ty _) = go ty -- ToDo: what about the coercion
2296 go (CoercionTy _) = False -- ToDo: what about the coercion
2297 go (TyConApp tc tys)
2298 | isGenerativeTyCon tc role = any go tys
2299 | otherwise = any go (drop (tyConArity tc) tys)
2300 -- (a ~ F b a), where F has arity 1,
2301 -- has an insoluble occurs check
2302
2303 role = eqRelRole eq_rel
2304
2305 {- Note [AppTy and ReprEq]
2306 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2307 Consider a ~R# b a
2308 a ~R# a b
2309
2310 The former is /not/ a definite error; we might instantiate 'b' with Id
2311 newtype Id a = MkId a
2312 but the latter /is/ a definite error.
2313
2314 On the other hand, with nominal equality, both are definite errors
2315 -}
2316
2317 isRigidTy :: TcType -> Bool
2318 isRigidTy ty
2319 | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
2320 | Just {} <- tcSplitAppTy_maybe ty = True
2321 | isForAllTy ty = True
2322 | otherwise = False
2323
2324
2325 {-
2326 ************************************************************************
2327 * *
2328 \subsection{Misc}
2329 * *
2330 ************************************************************************
2331
2332 Note [Visible type application]
2333 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2334 GHC implements a generalisation of the algorithm described in the
2335 "Visible Type Application" paper (available from
2336 http://www.cis.upenn.edu/~sweirich/publications.html). A key part
2337 of that algorithm is to distinguish user-specified variables from inferred
2338 variables. For example, the following should typecheck:
2339
2340 f :: forall a b. a -> b -> b
2341 f = const id
2342
2343 g = const id
2344
2345 x = f @Int @Bool 5 False
2346 y = g 5 @Bool False
2347
2348 The idea is that we wish to allow visible type application when we are
2349 instantiating a specified, fixed variable. In practice, specified, fixed
2350 variables are either written in a type signature (or
2351 annotation), OR are imported from another module. (We could do better here,
2352 for example by doing SCC analysis on parts of a module and considering any
2353 type from outside one's SCC to be fully specified, but this is very confusing to
2354 users. The simple rule above is much more straightforward and predictable.)
2355
2356 So, both of f's quantified variables are specified and may be instantiated.
2357 But g has no type signature, so only id's variable is specified (because id
2358 is imported). We write the type of g as forall {a}. a -> forall b. b -> b.
2359 Note that the a is in braces, meaning it cannot be instantiated with
2360 visible type application.
2361
2362 Tracking specified vs. inferred variables is done conveniently by a field
2363 in TyBinder.
2364
2365 -}
2366
2367 deNoteType :: Type -> Type
2368 -- Remove all *outermost* type synonyms and other notes
2369 deNoteType ty | Just ty' <- coreView ty = deNoteType ty'
2370 deNoteType ty = ty
2371
2372 {-
2373 Find the free tycons and classes of a type. This is used in the front
2374 end of the compiler.
2375 -}
2376
2377 {-
2378 ************************************************************************
2379 * *
2380 \subsection[TysWiredIn-ext-type]{External types}
2381 * *
2382 ************************************************************************
2383
2384 The compiler's foreign function interface supports the passing of a
2385 restricted set of types as arguments and results (the restricting factor
2386 being the )
2387 -}
2388
2389 tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type)
2390 -- (tcSplitIOType_maybe t) returns Just (IO,t',co)
2391 -- if co : t ~ IO t'
2392 -- returns Nothing otherwise
2393 tcSplitIOType_maybe ty
2394 = case tcSplitTyConApp_maybe ty of
2395 Just (io_tycon, [io_res_ty])
2396 | io_tycon `hasKey` ioTyConKey ->
2397 Just (io_tycon, io_res_ty)
2398 _ ->
2399 Nothing
2400
2401 isFFITy :: Type -> Bool
2402 -- True for any TyCon that can possibly be an arg or result of an FFI call
2403 isFFITy ty = isValid (checkRepTyCon legalFFITyCon ty)
2404
2405 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Validity
2406 -- Checks for valid argument type for a 'foreign import'
2407 isFFIArgumentTy dflags safety ty
2408 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
2409
2410 isFFIExternalTy :: Type -> Validity
2411 -- Types that are allowed as arguments of a 'foreign export'
2412 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
2413
2414 isFFIImportResultTy :: DynFlags -> Type -> Validity
2415 isFFIImportResultTy dflags ty
2416 = checkRepTyCon (legalFIResultTyCon dflags) ty
2417
2418 isFFIExportResultTy :: Type -> Validity
2419 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
2420
2421 isFFIDynTy :: Type -> Type -> Validity
2422 -- The type in a foreign import dynamic must be Ptr, FunPtr, or a newtype of
2423 -- either, and the wrapped function type must be equal to the given type.
2424 -- We assume that all types have been run through normaliseFfiType, so we don't
2425 -- need to worry about expanding newtypes here.
2426 isFFIDynTy expected ty
2427 -- Note [Foreign import dynamic]
2428 -- In the example below, expected would be 'CInt -> IO ()', while ty would
2429 -- be 'FunPtr (CDouble -> IO ())'.
2430 | Just (tc, [ty']) <- splitTyConApp_maybe ty
2431 , tyConUnique tc `elem` [ptrTyConKey, funPtrTyConKey]
2432 , eqType ty' expected
2433 = IsValid
2434 | otherwise
2435 = NotValid (vcat [ text "Expected: Ptr/FunPtr" <+> pprParendType expected <> comma
2436 , text " Actual:" <+> ppr ty ])
2437
2438 isFFILabelTy :: Type -> Validity
2439 -- The type of a foreign label must be Ptr, FunPtr, or a newtype of either.
2440 isFFILabelTy ty = checkRepTyCon ok ty
2441 where
2442 ok tc | tc `hasKey` funPtrTyConKey || tc `hasKey` ptrTyConKey
2443 = IsValid
2444 | otherwise
2445 = NotValid (text "A foreign-imported address (via &foo) must have type (Ptr a) or (FunPtr a)")
2446
2447 isFFIPrimArgumentTy :: DynFlags -> Type -> Validity
2448 -- Checks for valid argument type for a 'foreign import prim'
2449 -- Currently they must all be simple unlifted types, or the well-known type
2450 -- Any, which can be used to pass the address to a Haskell object on the heap to
2451 -- the foreign function.
2452 isFFIPrimArgumentTy dflags ty
2453 | isAnyTy ty = IsValid
2454 | otherwise = checkRepTyCon (legalFIPrimArgTyCon dflags) ty
2455
2456 isFFIPrimResultTy :: DynFlags -> Type -> Validity
2457 -- Checks for valid result type for a 'foreign import prim' Currently
2458 -- it must be an unlifted type, including unboxed tuples, unboxed
2459 -- sums, or the well-known type Any.
2460 isFFIPrimResultTy dflags ty
2461 | isAnyTy ty = IsValid
2462 | otherwise = checkRepTyCon (legalFIPrimResultTyCon dflags) ty
2463
2464 isFunPtrTy :: Type -> Bool
2465 isFunPtrTy ty
2466 | Just (tc, [_]) <- splitTyConApp_maybe ty
2467 = tc `hasKey` funPtrTyConKey
2468 | otherwise
2469 = False
2470
2471 -- normaliseFfiType gets run before checkRepTyCon, so we don't
2472 -- need to worry about looking through newtypes or type functions
2473 -- here; that's already been taken care of.
2474 checkRepTyCon :: (TyCon -> Validity) -> Type -> Validity
2475 checkRepTyCon check_tc ty
2476 = case splitTyConApp_maybe ty of
2477 Just (tc, tys)
2478 | isNewTyCon tc -> NotValid (hang msg 2 (mk_nt_reason tc tys $$ nt_fix))
2479 | otherwise -> case check_tc tc of
2480 IsValid -> IsValid
2481 NotValid extra -> NotValid (msg $$ extra)
2482 Nothing -> NotValid (quotes (ppr ty) <+> text "is not a data type")
2483 where
2484 msg = quotes (ppr ty) <+> text "cannot be marshalled in a foreign call"
2485 mk_nt_reason tc tys
2486 | null tys = text "because its data constructor is not in scope"
2487 | otherwise = text "because the data constructor for"
2488 <+> quotes (ppr tc) <+> text "is not in scope"
2489 nt_fix = text "Possible fix: import the data constructor to bring it into scope"
2490
2491 {-
2492 Note [Foreign import dynamic]
2493 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2494 A dynamic stub must be of the form 'FunPtr ft -> ft' where ft is any foreign
2495 type. Similarly, a wrapper stub must be of the form 'ft -> IO (FunPtr ft)'.
2496
2497 We use isFFIDynTy to check whether a signature is well-formed. For example,
2498 given a (illegal) declaration like:
2499
2500 foreign import ccall "dynamic"
2501 foo :: FunPtr (CDouble -> IO ()) -> CInt -> IO ()
2502
2503 isFFIDynTy will compare the 'FunPtr' type 'CDouble -> IO ()' with the curried
2504 result type 'CInt -> IO ()', and return False, as they are not equal.
2505
2506
2507 ----------------------------------------------
2508 These chaps do the work; they are not exported
2509 ----------------------------------------------
2510 -}
2511
2512 legalFEArgTyCon :: TyCon -> Validity
2513 legalFEArgTyCon tc
2514 -- It's illegal to make foreign exports that take unboxed
2515 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
2516 = boxedMarshalableTyCon tc
2517
2518 legalFIResultTyCon :: DynFlags -> TyCon -> Validity
2519 legalFIResultTyCon dflags tc
2520 | tc == unitTyCon = IsValid
2521 | otherwise = marshalableTyCon dflags tc
2522
2523 legalFEResultTyCon :: TyCon -> Validity
2524 legalFEResultTyCon tc
2525 | tc == unitTyCon = IsValid
2526 | otherwise = boxedMarshalableTyCon tc
2527
2528 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Validity
2529 -- Checks validity of types going from Haskell -> external world
2530 legalOutgoingTyCon dflags _ tc
2531 = marshalableTyCon dflags tc
2532
2533 legalFFITyCon :: TyCon -> Validity
2534 -- True for any TyCon that can possibly be an arg or result of an FFI call
2535 legalFFITyCon tc
2536 | isUnliftedTyCon tc = IsValid
2537 | tc == unitTyCon = IsValid
2538 | otherwise = boxedMarshalableTyCon tc
2539
2540 marshalableTyCon :: DynFlags -> TyCon -> Validity
2541 marshalableTyCon dflags tc
2542 | isUnliftedTyCon tc
2543 , not (isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc)
2544 , not (null (tyConPrimRep tc)) -- Note [Marshalling void]
2545 = validIfUnliftedFFITypes dflags
2546 | otherwise
2547 = boxedMarshalableTyCon tc
2548
2549 boxedMarshalableTyCon :: TyCon -> Validity
2550 boxedMarshalableTyCon tc
2551 | getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
2552 , int32TyConKey, int64TyConKey
2553 , wordTyConKey, word8TyConKey, word16TyConKey
2554 , word32TyConKey, word64TyConKey
2555 , floatTyConKey, doubleTyConKey
2556 , ptrTyConKey, funPtrTyConKey
2557 , charTyConKey
2558 , stablePtrTyConKey
2559 , boolTyConKey
2560 ]
2561 = IsValid
2562
2563 | otherwise = NotValid empty
2564
2565 legalFIPrimArgTyCon :: DynFlags -> TyCon -> Validity
2566 -- Check args of 'foreign import prim', only allow simple unlifted types.
2567 -- Strictly speaking it is unnecessary to ban unboxed tuples and sums here since
2568 -- currently they're of the wrong kind to use in function args anyway.
2569 legalFIPrimArgTyCon dflags tc
2570 | isUnliftedTyCon tc
2571 , not (isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc)
2572 = validIfUnliftedFFITypes dflags
2573 | otherwise
2574 = NotValid unlifted_only
2575
2576 legalFIPrimResultTyCon :: DynFlags -> TyCon -> Validity
2577 -- Check result type of 'foreign import prim'. Allow simple unlifted
2578 -- types and also unboxed tuple and sum result types.
2579 legalFIPrimResultTyCon dflags tc
2580 | isUnliftedTyCon tc
2581 , isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc
2582 || not (null (tyConPrimRep tc)) -- Note [Marshalling void]
2583 = validIfUnliftedFFITypes dflags
2584
2585 | otherwise
2586 = NotValid unlifted_only
2587
2588 unlifted_only :: MsgDoc
2589 unlifted_only = text "foreign import prim only accepts simple unlifted types"
2590
2591 validIfUnliftedFFITypes :: DynFlags -> Validity
2592 validIfUnliftedFFITypes dflags
2593 | xopt LangExt.UnliftedFFITypes dflags = IsValid
2594 | otherwise = NotValid (text "To marshal unlifted types, use UnliftedFFITypes")
2595
2596 {-
2597 Note [Marshalling void]
2598 ~~~~~~~~~~~~~~~~~~~~~~~
2599 We don't treat State# (whose PrimRep is VoidRep) as marshalable.
2600 In turn that means you can't write
2601 foreign import foo :: Int -> State# RealWorld
2602
2603 Reason: the back end falls over with panic "primRepHint:VoidRep";
2604 and there is no compelling reason to permit it
2605 -}
2606
2607 {-
2608 ************************************************************************
2609 * *
2610 The "Paterson size" of a type
2611 * *
2612 ************************************************************************
2613 -}
2614
2615 {-
2616 Note [Paterson conditions on PredTypes]
2617 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2618 We are considering whether *class* constraints terminate
2619 (see Note [Paterson conditions]). Precisely, the Paterson conditions
2620 would have us check that "the constraint has fewer constructors and variables
2621 (taken together and counting repetitions) than the head.".
2622
2623 However, we can be a bit more refined by looking at which kind of constraint
2624 this actually is. There are two main tricks:
2625
2626 1. It seems like it should be OK not to count the tuple type constructor
2627 for a PredType like (Show a, Eq a) :: Constraint, since we don't
2628 count the "implicit" tuple in the ThetaType itself.
2629
2630 In fact, the Paterson test just checks *each component* of the top level
2631 ThetaType against the size bound, one at a time. By analogy, it should be
2632 OK to return the size of the *largest* tuple component as the size of the
2633 whole tuple.
2634
2635 2. Once we get into an implicit parameter or equality we
2636 can't get back to a class constraint, so it's safe
2637 to say "size 0". See Trac #4200.
2638
2639 NB: we don't want to detect PredTypes in sizeType (and then call
2640 sizePred on them), or we might get an infinite loop if that PredType
2641 is irreducible. See Trac #5581.
2642 -}
2643
2644 type TypeSize = IntWithInf
2645
2646 sizeType :: Type -> TypeSize
2647 -- Size of a type: the number of variables and constructors
2648 -- Ignore kinds altogether
2649 sizeType = go
2650 where
2651 go ty | Just exp_ty <- tcView ty = go exp_ty
2652 go (TyVarTy {}) = 1
2653 go (TyConApp tc tys)
2654 | isTypeFamilyTyCon tc = infinity -- Type-family applications can
2655 -- expand to any arbitrary size
2656 | otherwise = sizeTypes (filterOutInvisibleTypes tc tys) + 1
2657 -- Why filter out invisible args? I suppose any
2658 -- size ordering is sound, but why is this better?
2659 -- I came across this when investigating #14010.
2660 go (LitTy {}) = 1
2661 go (FunTy arg res) = go arg + go res + 1
2662 go (AppTy fun arg) = go fun + go arg
2663 go (ForAllTy (TvBndr tv vis) ty)
2664 | isVisibleArgFlag vis = go (tyVarKind tv) + go ty + 1
2665 | otherwise = go ty + 1
2666 go (CastTy ty _) = go ty
2667 go (CoercionTy {}) = 0
2668
2669 sizeTypes :: [Type] -> TypeSize
2670 sizeTypes tys = sum (map sizeType tys)
2671
2672 -----------------------------------------------------------------------------------
2673 -----------------------------------------------------------------------------------
2674 -----------------------
2675 -- | For every arg a tycon can take, the returned list says True if the argument
2676 -- is taken visibly, and False otherwise. Ends with an infinite tail of Trues to
2677 -- allow for oversaturation.
2678 tcTyConVisibilities :: TyCon -> [Bool]
2679 tcTyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True
2680 where
2681 tc_binder_viss = map isVisibleTyConBinder (tyConBinders tc)
2682 tc_return_kind_viss = map isVisibleBinder (fst $ tcSplitPiTys (tyConResKind tc))
2683
2684 -- | If the tycon is applied to the types, is the next argument visible?
2685 isNextTyConArgVisible :: TyCon -> [Type] -> Bool
2686 isNextTyConArgVisible tc tys
2687 = tcTyConVisibilities tc `getNth` length tys
2688
2689 -- | Should this type be applied to a visible argument?
2690 isNextArgVisible :: TcType -> Bool
2691 isNextArgVisible ty
2692 | Just (bndr, _) <- tcSplitPiTy_maybe ty = isVisibleBinder bndr
2693 | otherwise = True
2694 -- this second case might happen if, say, we have an unzonked TauTv.
2695 -- But TauTvs can't range over types that take invisible arguments