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