Fix solving of implicit parameter constraints
[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, isTyVarExposed, isInsolubleOccursCheck,
83 checkValidClsArgs, hasTyVarHead,
84 isRigidEqPred, 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,
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 {-
827 ************************************************************************
828 * *
829 The "exact" free variables of a type
830 * *
831 ************************************************************************
832
833 Note [Silly type synonym]
834 ~~~~~~~~~~~~~~~~~~~~~~~~~
835 Consider
836 type T a = Int
837 What are the free tyvars of (T x)? Empty, of course!
838 Here's the example that Ralf Laemmel showed me:
839 foo :: (forall a. C u a -> C u a) -> u
840 mappend :: Monoid u => u -> u -> u
841
842 bar :: Monoid u => u
843 bar = foo (\t -> t `mappend` t)
844 We have to generalise at the arg to f, and we don't
845 want to capture the constraint (Monad (C u a)) because
846 it appears to mention a. Pretty silly, but it was useful to him.
847
848 exactTyCoVarsOfType is used by the type checker to figure out exactly
849 which type variables are mentioned in a type. It's also used in the
850 smart-app checking code --- see TcExpr.tcIdApp
851
852 On the other hand, consider a *top-level* definition
853 f = (\x -> x) :: T a -> T a
854 If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
855 if we have an application like (f "x") we get a confusing error message
856 involving Any. So the conclusion is this: when generalising
857 - at top level use tyCoVarsOfType
858 - in nested bindings use exactTyCoVarsOfType
859 See Trac #1813 for example.
860 -}
861
862 exactTyCoVarsOfType :: Type -> TyCoVarSet
863 -- Find the free type variables (of any kind)
864 -- but *expand* type synonyms. See Note [Silly type synonym] above.
865 exactTyCoVarsOfType ty
866 = go ty
867 where
868 go ty | Just ty' <- tcView ty = go ty' -- This is the key line
869 go (TyVarTy tv) = unitVarSet tv `unionVarSet` go (tyVarKind tv)
870 go (TyConApp _ tys) = exactTyCoVarsOfTypes tys
871 go (LitTy {}) = emptyVarSet
872 go (AppTy fun arg) = go fun `unionVarSet` go arg
873 go (FunTy arg res) = go arg `unionVarSet` go res
874 go (ForAllTy bndr ty) = delBinderVar (go ty) bndr `unionVarSet` go (binderKind bndr)
875 go (CastTy ty co) = go ty `unionVarSet` goCo co
876 go (CoercionTy co) = goCo co
877
878 goCo (Refl _ ty) = go ty
879 goCo (TyConAppCo _ _ args)= goCos args
880 goCo (AppCo co arg) = goCo co `unionVarSet` goCo arg
881 goCo (ForAllCo tv k_co co)
882 = goCo co `delVarSet` tv `unionVarSet` goCo k_co
883 goCo (FunCo _ co1 co2) = goCo co1 `unionVarSet` goCo co2
884 goCo (CoVarCo v) = unitVarSet v `unionVarSet` go (varType v)
885 goCo (AxiomInstCo _ _ args) = goCos args
886 goCo (UnivCo p _ t1 t2) = goProv p `unionVarSet` go t1 `unionVarSet` go t2
887 goCo (SymCo co) = goCo co
888 goCo (TransCo co1 co2) = goCo co1 `unionVarSet` goCo co2
889 goCo (NthCo _ co) = goCo co
890 goCo (LRCo _ co) = goCo co
891 goCo (InstCo co arg) = goCo co `unionVarSet` goCo arg
892 goCo (CoherenceCo c1 c2) = goCo c1 `unionVarSet` goCo c2
893 goCo (KindCo co) = goCo co
894 goCo (SubCo co) = goCo co
895 goCo (AxiomRuleCo _ c) = goCos c
896
897 goCos cos = foldr (unionVarSet . goCo) emptyVarSet cos
898
899 goProv UnsafeCoerceProv = emptyVarSet
900 goProv (PhantomProv kco) = goCo kco
901 goProv (ProofIrrelProv kco) = goCo kco
902 goProv (PluginProv _) = emptyVarSet
903 goProv (HoleProv _) = emptyVarSet
904
905 exactTyCoVarsOfTypes :: [Type] -> TyVarSet
906 exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
907
908 anyRewritableTyVar :: Bool -> (TcTyVar -> Bool)
909 -> TcType -> Bool
910 -- (anyRewritableTyVar ignore_cos pred ty) returns True
911 -- if the 'pred' returns True of free TyVar in 'ty'
912 -- Do not look inside casts and coercions if 'ignore_cos' is True
913 -- See Note [anyRewritableTyVar]
914 anyRewritableTyVar ignore_cos pred ty
915 = go emptyVarSet ty
916 where
917 go_tv bound tv | tv `elemVarSet` bound = False
918 | otherwise = pred tv
919
920 go bound (TyVarTy tv) = go_tv bound tv
921 go _ (LitTy {}) = False
922 go bound (TyConApp _ tys) = any (go bound) tys
923 go bound (AppTy fun arg) = go bound fun || go bound arg
924 go bound (FunTy arg res) = go bound arg || go bound res
925 go bound (ForAllTy tv ty) = go (bound `extendVarSet` binderVar tv) ty
926 go bound (CastTy ty co) = go bound ty || go_co bound co
927 go bound (CoercionTy co) = go_co bound co
928
929 go_co bound co
930 | ignore_cos = False
931 | otherwise = anyVarSet (go_tv bound) (tyCoVarsOfCo co)
932 -- We don't have an equivalent of anyRewritableTyVar for coercions
933 -- (at least not yet) so take the free vars and test them
934
935 {- Note [anyRewritableTyVar]
936 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
937 anyRewritableTyVar is used during kick-out from the inert set,
938 to decide if, given a new equality (a ~ ty), we should kick out
939 a constraint C. Rather than gather free variables and see if 'a'
940 is among them, we instead pass in a predicate; this is just efficiency.
941 -}
942
943 {- *********************************************************************
944 * *
945 Bound variables in a type
946 * *
947 ********************************************************************* -}
948
949 -- | Find all variables bound anywhere in a type.
950 -- See also Note [Scope-check inferred kinds] in TcHsType
951 allBoundVariables :: Type -> TyVarSet
952 allBoundVariables ty = fvVarSet $ go ty
953 where
954 go :: Type -> FV
955 go (TyVarTy tv) = go (tyVarKind tv)
956 go (TyConApp _ tys) = mapUnionFV go tys
957 go (AppTy t1 t2) = go t1 `unionFV` go t2
958 go (FunTy t1 t2) = go t1 `unionFV` go t2
959 go (ForAllTy (TvBndr tv _) t2) = FV.unitFV tv `unionFV`
960 go (tyVarKind tv) `unionFV` go t2
961 go (LitTy {}) = emptyFV
962 go (CastTy ty _) = go ty
963 go (CoercionTy {}) = emptyFV
964 -- any types mentioned in a coercion should also be mentioned in
965 -- a type.
966
967 allBoundVariabless :: [Type] -> TyVarSet
968 allBoundVariabless = mapUnionVarSet allBoundVariables
969
970 {- *********************************************************************
971 * *
972 Type and kind variables in a type
973 * *
974 ********************************************************************* -}
975
976 data CandidatesQTvs -- See Note [Dependent type variables]
977 -- See Note [CandidatesQTvs determinism]
978 = DV { dv_kvs :: DTyCoVarSet -- "kind" variables (dependent)
979 , dv_tvs :: DTyVarSet -- "type" variables (non-dependent)
980 -- A variable may appear in both sets
981 -- E.g. T k (x::k) The first occurrence of k makes it
982 -- show up in dv_tvs, the second in dv_kvs
983 -- See Note [Dependent type variables]
984 }
985
986 instance Semi.Semigroup CandidatesQTvs where
987 (DV { dv_kvs = kv1, dv_tvs = tv1 }) <> (DV { dv_kvs = kv2, dv_tvs = tv2 })
988 = DV { dv_kvs = kv1 `unionDVarSet` kv2
989 , dv_tvs = tv1 `unionDVarSet` tv2}
990
991 instance Monoid CandidatesQTvs where
992 mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet }
993 mappend = (Semi.<>)
994
995 instance Outputable CandidatesQTvs where
996 ppr (DV {dv_kvs = kvs, dv_tvs = tvs })
997 = text "DV" <+> braces (sep [ text "dv_kvs =" <+> ppr kvs
998 , text "dv_tvs =" <+> ppr tvs ])
999
1000 {- Note [Dependent type variables]
1001 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1002 In Haskell type inference we quantify over type variables; but we only
1003 quantify over /kind/ variables when -XPolyKinds is on. Without -XPolyKinds
1004 we default the kind variables to *.
1005
1006 So, to support this defaulting, and only for that reason, when
1007 collecting the free vars of a type, prior to quantifying, we must keep
1008 the type and kind variables separate.
1009
1010 But what does that mean in a system where kind variables /are/ type
1011 variables? It's a fairly arbitrary distinction based on how the
1012 variables appear:
1013
1014 - "Kind variables" appear in the kind of some other free variable
1015 PLUS any free coercion variables
1016
1017 These are the ones we default to * if -XPolyKinds is off
1018
1019 - "Type variables" are all free vars that are not kind variables
1020
1021 E.g. In the type T k (a::k)
1022 'k' is a kind variable, because it occurs in the kind of 'a',
1023 even though it also appears at "top level" of the type
1024 'a' is a type variable, because it doesn't
1025
1026 We gather these variables using a CandidatesQTvs record:
1027 DV { dv_kvs: Variables free in the kind of a free type variable
1028 or of a forall-bound type variable
1029 , dv_tvs: Variables sytactically free in the type }
1030
1031 So: dv_kvs are the kind variables of the type
1032 (dv_tvs - dv_kvs) are the type variable of the type
1033
1034 Note that
1035
1036 * A variable can occur in both.
1037 T k (x::k) The first occurrence of k makes it
1038 show up in dv_tvs, the second in dv_kvs
1039
1040 * We include any coercion variables in the "dependent",
1041 "kind-variable" set because we never quantify over them.
1042
1043 * Both sets are un-ordered, of course.
1044
1045 * The "kind variables" might depend on each other; e.g
1046 (k1 :: k2), (k2 :: *)
1047 The "type variables" do not depend on each other; if
1048 one did, it'd be classified as a kind variable!
1049
1050 Note [CandidatesQTvs determinism and order]
1051 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1052 * Determinism: when we quantify over type variables we decide the
1053 order in which they appear in the final type. Because the order of
1054 type variables in the type can end up in the interface file and
1055 affects some optimizations like worker-wrapper, we want this order to
1056 be deterministic.
1057
1058 To achieve that we use deterministic sets of variables that can be
1059 converted to lists in a deterministic order. For more information
1060 about deterministic sets see Note [Deterministic UniqFM] in UniqDFM.
1061
1062 * Order: as well as being deterministic, we use an
1063 accumulating-parameter style for candidateQTyVarsOfType so that we
1064 add variables one at a time, left to right. That means we tend to
1065 produce the variables in left-to-right order. This is just to make
1066 it bit more predicatable for the programmer.
1067 -}
1068
1069 -- | Worker for 'splitDepVarsOfType'. This might output the same var
1070 -- in both sets, if it's used in both a type and a kind.
1071 -- See Note [CandidatesQTvs determinism and order]
1072 -- See Note [Dependent type variables]
1073 candidateQTyVarsOfType :: Type -> CandidatesQTvs
1074 candidateQTyVarsOfType = split_dvs emptyVarSet mempty
1075
1076 split_dvs :: VarSet -> CandidatesQTvs -> Type -> CandidatesQTvs
1077 split_dvs bound dvs ty
1078 = go dvs ty
1079 where
1080 go dv (AppTy t1 t2) = go (go dv t1) t2
1081 go dv (TyConApp _ tys) = foldl go dv tys
1082 go dv (FunTy arg res) = go (go dv arg) res
1083 go dv (LitTy {}) = dv
1084 go dv (CastTy ty co) = go dv ty `mappend` go_co co
1085 go dv (CoercionTy co) = dv `mappend` go_co co
1086
1087 go dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) (TyVarTy tv)
1088 | tv `elemVarSet` bound
1089 = dv
1090 | otherwise
1091 = DV { dv_kvs = kvs `unionDVarSet`
1092 kill_bound (tyCoVarsOfTypeDSet (tyVarKind tv))
1093 , dv_tvs = tvs `extendDVarSet` tv }
1094
1095 go dv (ForAllTy (TvBndr tv _) ty)
1096 = DV { dv_kvs = kvs `unionDVarSet`
1097 kill_bound (tyCoVarsOfTypeDSet (tyVarKind tv))
1098 , dv_tvs = tvs }
1099 where
1100 DV { dv_kvs = kvs, dv_tvs = tvs } = split_dvs (bound `extendVarSet` tv) dv ty
1101
1102 go_co co = DV { dv_kvs = kill_bound (tyCoVarsOfCoDSet co)
1103 , dv_tvs = emptyDVarSet }
1104
1105 kill_bound free
1106 | isEmptyVarSet bound = free
1107 | otherwise = free `dVarSetMinusVarSet` bound
1108
1109 -- | Like 'splitDepVarsOfType', but over a list of types
1110 candidateQTyVarsOfTypes :: [Type] -> CandidatesQTvs
1111 candidateQTyVarsOfTypes = foldl (split_dvs emptyVarSet) mempty
1112
1113 {-
1114 ************************************************************************
1115 * *
1116 Predicates
1117 * *
1118 ************************************************************************
1119 -}
1120
1121 tcIsTcTyVar :: TcTyVar -> Bool
1122 -- See Note [TcTyVars in the typechecker]
1123 tcIsTcTyVar tv = isTyVar tv
1124
1125 isTouchableOrFmv :: TcLevel -> TcTyVar -> Bool
1126 isTouchableOrFmv ctxt_tclvl tv
1127 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1128 case tcTyVarDetails tv of
1129 MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info }
1130 -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
1131 ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
1132 case info of
1133 FlatMetaTv -> True
1134 _ -> tv_tclvl `sameDepthAs` ctxt_tclvl
1135 _ -> False
1136
1137 isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
1138 isTouchableMetaTyVar ctxt_tclvl tv
1139 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1140 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1141 case tcTyVarDetails tv of
1142 MetaTv { mtv_tclvl = tv_tclvl }
1143 -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
1144 ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
1145 tv_tclvl `sameDepthAs` ctxt_tclvl
1146 _ -> False
1147 | otherwise = False
1148
1149 isFloatedTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
1150 isFloatedTouchableMetaTyVar ctxt_tclvl tv
1151 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1152 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1153 case tcTyVarDetails tv of
1154 MetaTv { mtv_tclvl = tv_tclvl } -> tv_tclvl `strictlyDeeperThan` ctxt_tclvl
1155 _ -> False
1156 | otherwise = False
1157
1158 isImmutableTyVar :: TyVar -> Bool
1159 isImmutableTyVar tv = isSkolemTyVar tv
1160
1161 isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
1162 isMetaTyVar, isAmbiguousTyVar,
1163 isFmvTyVar, isFskTyVar, isFlattenTyVar :: TcTyVar -> Bool
1164
1165 isTyConableTyVar tv
1166 -- True of a meta-type variable that can be filled in
1167 -- with a type constructor application; in particular,
1168 -- not a SigTv
1169 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1170 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1171 case tcTyVarDetails tv of
1172 MetaTv { mtv_info = SigTv } -> False
1173 _ -> True
1174 | otherwise = True
1175
1176 isFmvTyVar tv
1177 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1178 case tcTyVarDetails tv of
1179 MetaTv { mtv_info = FlatMetaTv } -> True
1180 _ -> False
1181
1182 isFskTyVar tv
1183 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1184 case tcTyVarDetails tv of
1185 MetaTv { mtv_info = FlatSkolTv } -> True
1186 _ -> False
1187
1188 -- | True of both given and wanted flatten-skolems (fak and usk)
1189 isFlattenTyVar tv
1190 = isFmvTyVar tv || isFskTyVar tv
1191
1192 isSkolemTyVar tv
1193 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1194 case tcTyVarDetails tv of
1195 MetaTv {} -> False
1196 _other -> True
1197
1198 isOverlappableTyVar tv
1199 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1200 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1201 case tcTyVarDetails tv of
1202 SkolemTv _ overlappable -> overlappable
1203 _ -> False
1204 | otherwise = False
1205
1206 isMetaTyVar tv
1207 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1208 = ASSERT2( tcIsTcTyVar tv, ppr tv )
1209 case tcTyVarDetails tv of
1210 MetaTv {} -> True
1211 _ -> False
1212 | otherwise = False
1213
1214 -- isAmbiguousTyVar is used only when reporting type errors
1215 -- It picks out variables that are unbound, namely meta
1216 -- type variables and the RuntimUnk variables created by
1217 -- RtClosureInspect.zonkRTTIType. These are "ambiguous" in
1218 -- the sense that they stand for an as-yet-unknown type
1219 isAmbiguousTyVar tv
1220 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1221 = case tcTyVarDetails tv of
1222 MetaTv {} -> True
1223 RuntimeUnk {} -> True
1224 _ -> False
1225 | otherwise = False
1226
1227 isMetaTyVarTy :: TcType -> Bool
1228 isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
1229 isMetaTyVarTy _ = False
1230
1231 metaTyVarInfo :: TcTyVar -> MetaInfo
1232 metaTyVarInfo tv
1233 = case tcTyVarDetails tv of
1234 MetaTv { mtv_info = info } -> info
1235 _ -> pprPanic "metaTyVarInfo" (ppr tv)
1236
1237 metaTyVarTcLevel :: TcTyVar -> TcLevel
1238 metaTyVarTcLevel tv
1239 = case tcTyVarDetails tv of
1240 MetaTv { mtv_tclvl = tclvl } -> tclvl
1241 _ -> pprPanic "metaTyVarTcLevel" (ppr tv)
1242
1243 metaTyVarTcLevel_maybe :: TcTyVar -> Maybe TcLevel
1244 metaTyVarTcLevel_maybe tv
1245 = case tcTyVarDetails tv of
1246 MetaTv { mtv_tclvl = tclvl } -> Just tclvl
1247 _ -> Nothing
1248
1249 metaTyVarRef :: TyVar -> IORef MetaDetails
1250 metaTyVarRef tv
1251 = case tcTyVarDetails tv of
1252 MetaTv { mtv_ref = ref } -> ref
1253 _ -> pprPanic "metaTyVarRef" (ppr tv)
1254
1255 setMetaTyVarTcLevel :: TcTyVar -> TcLevel -> TcTyVar
1256 setMetaTyVarTcLevel tv tclvl
1257 = case tcTyVarDetails tv of
1258 details@(MetaTv {}) -> setTcTyVarDetails tv (details { mtv_tclvl = tclvl })
1259 _ -> pprPanic "metaTyVarTcLevel" (ppr tv)
1260
1261 isSigTyVar :: Var -> Bool
1262 isSigTyVar tv
1263 = case tcTyVarDetails tv of
1264 MetaTv { mtv_info = SigTv } -> True
1265 _ -> False
1266
1267 isFlexi, isIndirect :: MetaDetails -> Bool
1268 isFlexi Flexi = True
1269 isFlexi _ = False
1270
1271 isIndirect (Indirect _) = True
1272 isIndirect _ = False
1273
1274 isRuntimeUnkSkol :: TyVar -> Bool
1275 -- Called only in TcErrors; see Note [Runtime skolems] there
1276 isRuntimeUnkSkol x
1277 | RuntimeUnk <- tcTyVarDetails x = True
1278 | otherwise = False
1279
1280 {-
1281 ************************************************************************
1282 * *
1283 \subsection{Tau, sigma and rho}
1284 * *
1285 ************************************************************************
1286 -}
1287
1288 mkSigmaTy :: [TyVarBinder] -> [PredType] -> Type -> Type
1289 mkSigmaTy bndrs theta tau = mkForAllTys bndrs (mkPhiTy theta tau)
1290
1291 -- | Make a sigma ty where all type variables are 'Inferred'. That is,
1292 -- they cannot be used with visible type application.
1293 mkInfSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
1294 mkInfSigmaTy tyvars theta ty = mkSigmaTy (mkTyVarBinders Inferred tyvars) theta ty
1295
1296 -- | Make a sigma ty where all type variables are "specified". That is,
1297 -- they can be used with visible type application
1298 mkSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
1299 mkSpecSigmaTy tyvars ty = mkSigmaTy (mkTyVarBinders Specified tyvars) ty
1300
1301 mkPhiTy :: [PredType] -> Type -> Type
1302 mkPhiTy = mkFunTys
1303
1304 ---------------
1305 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
1306 -- construct a dictionary function name
1307 getDFunTyKey ty | Just ty' <- coreView ty = getDFunTyKey ty'
1308 getDFunTyKey (TyVarTy tv) = getOccName tv
1309 getDFunTyKey (TyConApp tc _) = getOccName tc
1310 getDFunTyKey (LitTy x) = getDFunTyLitKey x
1311 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
1312 getDFunTyKey (FunTy _ _) = getOccName funTyCon
1313 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
1314 getDFunTyKey (CastTy ty _) = getDFunTyKey ty
1315 getDFunTyKey t@(CoercionTy _) = pprPanic "getDFunTyKey" (ppr t)
1316
1317 getDFunTyLitKey :: TyLit -> OccName
1318 getDFunTyLitKey (NumTyLit n) = mkOccName Name.varName (show n)
1319 getDFunTyLitKey (StrTyLit n) = mkOccName Name.varName (show n) -- hm
1320
1321 ---------------
1322 mkNakedTyConApp :: TyCon -> [Type] -> Type
1323 -- Builds a TyConApp
1324 -- * without being strict in TyCon,
1325 -- * without satisfying the invariants of TyConApp
1326 -- A subsequent zonking will establish the invariants
1327 -- See Note [Type-checking inside the knot] in TcHsType
1328 mkNakedTyConApp tc tys = TyConApp tc tys
1329
1330 mkNakedAppTys :: Type -> [Type] -> Type
1331 -- See Note [Type-checking inside the knot] in TcHsType
1332 mkNakedAppTys ty1 [] = ty1
1333 mkNakedAppTys (TyConApp tc tys1) tys2 = mkNakedTyConApp tc (tys1 ++ tys2)
1334 mkNakedAppTys ty1 tys2 = foldl AppTy ty1 tys2
1335
1336 mkNakedAppTy :: Type -> Type -> Type
1337 -- See Note [Type-checking inside the knot] in TcHsType
1338 mkNakedAppTy ty1 ty2 = mkNakedAppTys ty1 [ty2]
1339
1340 mkNakedCastTy :: Type -> Coercion -> Type
1341 -- Do simple, fast compaction; especially dealing with Refl
1342 -- for which it's plain stupid to create a cast
1343 -- This simple function killed off a huge number of Refl casts
1344 -- in types, at birth.
1345 -- Note that it's fine to do this even for a "mkNaked" function,
1346 -- because we don't look at TyCons. isReflCo checks if the coercion
1347 -- is structurally Refl; it does not check for shape k ~ k.
1348 mkNakedCastTy ty co | isReflCo co = ty
1349 mkNakedCastTy (CastTy ty co1) co2 = CastTy ty (co1 `mkTransCo` co2)
1350 mkNakedCastTy ty co = CastTy ty co
1351
1352 {-
1353 ************************************************************************
1354 * *
1355 \subsection{Expanding and splitting}
1356 * *
1357 ************************************************************************
1358
1359 These tcSplit functions are like their non-Tc analogues, but
1360 *) they do not look through newtypes
1361
1362 However, they are non-monadic and do not follow through mutable type
1363 variables. It's up to you to make sure this doesn't matter.
1364 -}
1365
1366 -- | Splits a forall type into a list of 'TyBinder's and the inner type.
1367 -- Always succeeds, even if it returns an empty list.
1368 tcSplitPiTys :: Type -> ([TyBinder], Type)
1369 tcSplitPiTys = splitPiTys
1370
1371 -- | Splits a type into a TyBinder and a body, if possible. Panics otherwise
1372 tcSplitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
1373 tcSplitPiTy_maybe = splitPiTy_maybe
1374
1375 tcSplitForAllTy_maybe :: Type -> Maybe (TyVarBinder, Type)
1376 tcSplitForAllTy_maybe ty | Just ty' <- tcView ty = tcSplitForAllTy_maybe ty'
1377 tcSplitForAllTy_maybe (ForAllTy tv ty) = Just (tv, ty)
1378 tcSplitForAllTy_maybe _ = Nothing
1379
1380 -- | Like 'tcSplitPiTys', but splits off only named binders, returning
1381 -- just the tycovars.
1382 tcSplitForAllTys :: Type -> ([TyVar], Type)
1383 tcSplitForAllTys = splitForAllTys
1384
1385 -- | Like 'tcSplitForAllTys', but splits off only named binders.
1386 tcSplitForAllTyVarBndrs :: Type -> ([TyVarBinder], Type)
1387 tcSplitForAllTyVarBndrs = splitForAllTyVarBndrs
1388
1389 -- | Is this a ForAllTy with a named binder?
1390 tcIsForAllTy :: Type -> Bool
1391 tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
1392 tcIsForAllTy (ForAllTy {}) = True
1393 tcIsForAllTy _ = False
1394
1395 tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
1396 -- Split off the first predicate argument from a type
1397 tcSplitPredFunTy_maybe ty
1398 | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
1399 tcSplitPredFunTy_maybe (FunTy arg res)
1400 | isPredTy arg = Just (arg, res)
1401 tcSplitPredFunTy_maybe _
1402 = Nothing
1403
1404 tcSplitPhiTy :: Type -> (ThetaType, Type)
1405 tcSplitPhiTy ty
1406 = split ty []
1407 where
1408 split ty ts
1409 = case tcSplitPredFunTy_maybe ty of
1410 Just (pred, ty) -> split ty (pred:ts)
1411 Nothing -> (reverse ts, ty)
1412
1413 -- | Split a sigma type into its parts.
1414 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
1415 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
1416 (tvs, rho) -> case tcSplitPhiTy rho of
1417 (theta, tau) -> (tvs, theta, tau)
1418
1419 -- | Split a sigma type into its parts, going underneath as many @ForAllTy@s
1420 -- as possible. For example, given this type synonym:
1421 --
1422 -- @
1423 -- type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
1424 -- @
1425 --
1426 -- if you called @tcSplitSigmaTy@ on this type:
1427 --
1428 -- @
1429 -- forall s t a b. Each s t a b => Traversal s t a b
1430 -- @
1431 --
1432 -- then it would return @([s,t,a,b], [Each s t a b], Traversal s t a b)@. But
1433 -- if you instead called @tcSplitNestedSigmaTys@ on the type, it would return
1434 -- @([s,t,a,b,f], [Each s t a b, Applicative f], (a -> f b) -> s -> f t)@.
1435 tcSplitNestedSigmaTys :: Type -> ([TyVar], ThetaType, Type)
1436 -- NB: This is basically a pure version of deeplyInstantiate (from Inst) that
1437 -- doesn't compute an HsWrapper.
1438 tcSplitNestedSigmaTys ty
1439 -- If there's a forall, split it apart and try splitting the rho type
1440 -- underneath it.
1441 | Just (arg_tys, tvs1, theta1, rho1) <- tcDeepSplitSigmaTy_maybe ty
1442 = let (tvs2, theta2, rho2) = tcSplitNestedSigmaTys rho1
1443 in (tvs1 ++ tvs2, theta1 ++ theta2, mkFunTys arg_tys rho2)
1444 -- If there's no forall, we're done.
1445 | otherwise = ([], [], ty)
1446
1447 -----------------------
1448 tcDeepSplitSigmaTy_maybe
1449 :: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType)
1450 -- Looks for a *non-trivial* quantified type, under zero or more function arrows
1451 -- By "non-trivial" we mean either tyvars or constraints are non-empty
1452
1453 tcDeepSplitSigmaTy_maybe ty
1454 | Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty
1455 , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty
1456 = Just (arg_ty:arg_tys, tvs, theta, rho)
1457
1458 | (tvs, theta, rho) <- tcSplitSigmaTy ty
1459 , not (null tvs && null theta)
1460 = Just ([], tvs, theta, rho)
1461
1462 | otherwise = Nothing
1463
1464 -----------------------
1465 tcTyConAppTyCon :: Type -> TyCon
1466 tcTyConAppTyCon ty
1467 = case tcTyConAppTyCon_maybe ty of
1468 Just tc -> tc
1469 Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
1470
1471 -- | Like 'tcRepSplitTyConApp_maybe', but only returns the 'TyCon'.
1472 tcTyConAppTyCon_maybe :: Type -> Maybe TyCon
1473 tcTyConAppTyCon_maybe ty
1474 | Just ty' <- tcView ty = tcTyConAppTyCon_maybe ty'
1475 tcTyConAppTyCon_maybe (TyConApp tc _)
1476 = Just tc
1477 tcTyConAppTyCon_maybe (FunTy _ _)
1478 = Just funTyCon
1479 tcTyConAppTyCon_maybe _
1480 = Nothing
1481
1482 tcTyConAppArgs :: Type -> [Type]
1483 tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
1484 Just (_, args) -> args
1485 Nothing -> pprPanic "tcTyConAppArgs" (pprType ty)
1486
1487 tcSplitTyConApp :: Type -> (TyCon, [Type])
1488 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
1489 Just stuff -> stuff
1490 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
1491
1492 -- | Like 'tcRepSplitTyConApp_maybe', but returns 'Nothing' if,
1493 --
1494 -- 1. the type is structurally not a type constructor application, or
1495 --
1496 -- 2. the type is a function type (e.g. application of 'funTyCon'), but we
1497 -- currently don't even enough information to fully determine its RuntimeRep
1498 -- variables. For instance, @FunTy (a :: k) Int@.
1499 --
1500 -- By contrast 'tcRepSplitTyConApp_maybe' panics in the second case.
1501 --
1502 -- The behavior here is needed during canonicalization; see Note [FunTy and
1503 -- decomposing tycon applications] in TcCanonical for details.
1504 tcRepSplitTyConApp_maybe' :: HasCallStack => Type -> Maybe (TyCon, [Type])
1505 tcRepSplitTyConApp_maybe' (TyConApp tc tys) = Just (tc, tys)
1506 tcRepSplitTyConApp_maybe' (FunTy arg res)
1507 | Just arg_rep <- getRuntimeRep_maybe arg
1508 , Just res_rep <- getRuntimeRep_maybe res
1509 = Just (funTyCon, [arg_rep, res_rep, arg, res])
1510 tcRepSplitTyConApp_maybe' _ = Nothing
1511
1512
1513 -----------------------
1514 tcSplitFunTys :: Type -> ([Type], Type)
1515 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
1516 Nothing -> ([], ty)
1517 Just (arg,res) -> (arg:args, res')
1518 where
1519 (args,res') = tcSplitFunTys res
1520
1521 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
1522 tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
1523 tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
1524 tcSplitFunTy_maybe _ = Nothing
1525 -- Note the typeKind guard
1526 -- Consider (?x::Int) => Bool
1527 -- We don't want to treat this as a function type!
1528 -- A concrete example is test tc230:
1529 -- f :: () -> (?p :: ()) => () -> ()
1530 --
1531 -- g = f () ()
1532
1533 tcSplitFunTysN :: Arity -- N: Number of desired args
1534 -> TcRhoType
1535 -> Either Arity -- Number of missing arrows
1536 ([TcSigmaType], -- Arg types (always N types)
1537 TcSigmaType) -- The rest of the type
1538 -- ^ Split off exactly the specified number argument types
1539 -- Returns
1540 -- (Left m) if there are 'm' missing arrows in the type
1541 -- (Right (tys,res)) if the type looks like t1 -> ... -> tn -> res
1542 tcSplitFunTysN n ty
1543 | n == 0
1544 = Right ([], ty)
1545 | Just (arg,res) <- tcSplitFunTy_maybe ty
1546 = case tcSplitFunTysN (n-1) res of
1547 Left m -> Left m
1548 Right (args,body) -> Right (arg:args, body)
1549 | otherwise
1550 = Left n
1551
1552 tcSplitFunTy :: Type -> (Type, Type)
1553 tcSplitFunTy ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
1554
1555 tcFunArgTy :: Type -> Type
1556 tcFunArgTy ty = fst (tcSplitFunTy ty)
1557
1558 tcFunResultTy :: Type -> Type
1559 tcFunResultTy ty = snd (tcSplitFunTy ty)
1560
1561 -- | Strips off n *visible* arguments and returns the resulting type
1562 tcFunResultTyN :: HasDebugCallStack => Arity -> Type -> Type
1563 tcFunResultTyN n ty
1564 | Right (_, res_ty) <- tcSplitFunTysN n ty
1565 = res_ty
1566 | otherwise
1567 = pprPanic "tcFunResultTyN" (ppr n <+> ppr ty)
1568
1569 -----------------------
1570 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
1571 tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
1572 tcSplitAppTy_maybe ty = tcRepSplitAppTy_maybe ty
1573
1574 tcSplitAppTy :: Type -> (Type, Type)
1575 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
1576 Just stuff -> stuff
1577 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
1578
1579 tcSplitAppTys :: Type -> (Type, [Type])
1580 tcSplitAppTys ty
1581 = go ty []
1582 where
1583 go ty args = case tcSplitAppTy_maybe ty of
1584 Just (ty', arg) -> go ty' (arg:args)
1585 Nothing -> (ty,args)
1586
1587 -- | Returns the number of arguments in the given type, without
1588 -- looking through synonyms. This is used only for error reporting.
1589 -- We don't look through synonyms because of #11313.
1590 tcRepGetNumAppTys :: Type -> Arity
1591 tcRepGetNumAppTys = length . snd . repSplitAppTys
1592
1593 -----------------------
1594 -- | If the type is a tyvar, possibly under a cast, returns it, along
1595 -- with the coercion. Thus, the co is :: kind tv ~N kind type
1596 tcGetCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN)
1597 tcGetCastedTyVar_maybe ty | Just ty' <- tcView ty = tcGetCastedTyVar_maybe ty'
1598 tcGetCastedTyVar_maybe (CastTy (TyVarTy tv) co) = Just (tv, co)
1599 tcGetCastedTyVar_maybe (TyVarTy tv) = Just (tv, mkNomReflCo (tyVarKind tv))
1600 tcGetCastedTyVar_maybe _ = Nothing
1601
1602 tcGetTyVar_maybe :: Type -> Maybe TyVar
1603 tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
1604 tcGetTyVar_maybe (TyVarTy tv) = Just tv
1605 tcGetTyVar_maybe _ = Nothing
1606
1607 tcGetTyVar :: String -> Type -> TyVar
1608 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
1609
1610 tcIsTyVarTy :: Type -> Bool
1611 tcIsTyVarTy ty | Just ty' <- tcView ty = tcIsTyVarTy ty'
1612 tcIsTyVarTy (CastTy ty _) = tcIsTyVarTy ty -- look through casts, as
1613 -- this is only used for
1614 -- e.g., FlexibleContexts
1615 tcIsTyVarTy (TyVarTy _) = True
1616 tcIsTyVarTy _ = False
1617
1618 -----------------------
1619 tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
1620 -- Split the type of a dictionary function
1621 -- We don't use tcSplitSigmaTy, because a DFun may (with NDP)
1622 -- have non-Pred arguments, such as
1623 -- df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
1624 --
1625 -- Also NB splitFunTys, not tcSplitFunTys;
1626 -- the latter specifically stops at PredTy arguments,
1627 -- and we don't want to do that here
1628 tcSplitDFunTy ty
1629 = case tcSplitForAllTys ty of { (tvs, rho) ->
1630 case splitFunTys rho of { (theta, tau) ->
1631 case tcSplitDFunHead tau of { (clas, tys) ->
1632 (tvs, theta, clas, tys) }}}
1633
1634 tcSplitDFunHead :: Type -> (Class, [Type])
1635 tcSplitDFunHead = getClassPredTys
1636
1637 tcSplitMethodTy :: Type -> ([TyVar], PredType, Type)
1638 -- A class method (selector) always has a type like
1639 -- forall as. C as => blah
1640 -- So if the class looks like
1641 -- class C a where
1642 -- op :: forall b. (Eq a, Ix b) => a -> b
1643 -- the class method type looks like
1644 -- op :: forall a. C a => forall b. (Eq a, Ix b) => a -> b
1645 --
1646 -- tcSplitMethodTy just peels off the outer forall and
1647 -- that first predicate
1648 tcSplitMethodTy ty
1649 | (sel_tyvars,sel_rho) <- tcSplitForAllTys ty
1650 , Just (first_pred, local_meth_ty) <- tcSplitPredFunTy_maybe sel_rho
1651 = (sel_tyvars, first_pred, local_meth_ty)
1652 | otherwise
1653 = pprPanic "tcSplitMethodTy" (ppr ty)
1654
1655
1656 {- *********************************************************************
1657 * *
1658 Type equalities
1659 * *
1660 ********************************************************************* -}
1661
1662 tcEqKind :: TcKind -> TcKind -> Bool
1663 tcEqKind = tcEqType
1664
1665 tcEqType :: TcType -> TcType -> Bool
1666 -- tcEqType is a proper implements the same Note [Non-trivial definitional
1667 -- equality] (in TyCoRep) as `eqType`, but Type.eqType believes (* ==
1668 -- Constraint), and that is NOT what we want in the type checker!
1669 tcEqType ty1 ty2
1670 = isNothing (tc_eq_type tcView ki1 ki2) &&
1671 isNothing (tc_eq_type tcView ty1 ty2)
1672 where
1673 ki1 = typeKind ty1
1674 ki2 = typeKind ty2
1675
1676 -- | Just like 'tcEqType', but will return True for types of different kinds
1677 -- as long as their non-coercion structure is identical.
1678 tcEqTypeNoKindCheck :: TcType -> TcType -> Bool
1679 tcEqTypeNoKindCheck ty1 ty2
1680 = isNothing $ tc_eq_type tcView ty1 ty2
1681
1682 -- | Like 'tcEqType', but returns information about whether the difference
1683 -- is visible in the case of a mismatch.
1684 -- @Nothing@ : the types are equal
1685 -- @Just True@ : the types differ, and the point of difference is visible
1686 -- @Just False@ : the types differ, and the point of difference is invisible
1687 tcEqTypeVis :: TcType -> TcType -> Maybe Bool
1688 tcEqTypeVis ty1 ty2
1689 = tc_eq_type tcView ty1 ty2 <!> invis (tc_eq_type tcView ki1 ki2)
1690 where
1691 ki1 = typeKind ty1
1692 ki2 = typeKind ty2
1693
1694 -- convert Just True to Just False
1695 invis :: Maybe Bool -> Maybe Bool
1696 invis = fmap (const False)
1697
1698 (<!>) :: Maybe Bool -> Maybe Bool -> Maybe Bool
1699 Nothing <!> x = x
1700 Just True <!> _ = Just True
1701 Just _vis <!> Just True = Just True
1702 Just vis <!> _ = Just vis
1703 infixr 3 <!>
1704
1705 -- | Real worker for 'tcEqType'. No kind check!
1706 tc_eq_type :: (TcType -> Maybe TcType) -- ^ @tcView@, if you want unwrapping
1707 -> Type -> Type -> Maybe Bool
1708 tc_eq_type view_fun orig_ty1 orig_ty2 = go True orig_env orig_ty1 orig_ty2
1709 where
1710 go :: Bool -> RnEnv2 -> Type -> Type -> Maybe Bool
1711 go vis env t1 t2 | Just t1' <- view_fun t1 = go vis env t1' t2
1712 go vis env t1 t2 | Just t2' <- view_fun t2 = go vis env t1 t2'
1713
1714 go vis env (TyVarTy tv1) (TyVarTy tv2)
1715 = check vis $ rnOccL env tv1 == rnOccR env tv2
1716
1717 go vis _ (LitTy lit1) (LitTy lit2)
1718 = check vis $ lit1 == lit2
1719
1720 go vis env (ForAllTy (TvBndr tv1 vis1) ty1)
1721 (ForAllTy (TvBndr tv2 vis2) ty2)
1722 = go (isVisibleArgFlag vis1) env (tyVarKind tv1) (tyVarKind tv2)
1723 <!> go vis (rnBndr2 env tv1 tv2) ty1 ty2
1724 <!> check vis (vis1 == vis2)
1725 -- Make sure we handle all FunTy cases since falling through to the
1726 -- AppTy case means that tcRepSplitAppTy_maybe may see an unzonked
1727 -- kind variable, which causes things to blow up.
1728 go vis env (FunTy arg1 res1) (FunTy arg2 res2)
1729 = go vis env arg1 arg2 <!> go vis env res1 res2
1730 go vis env ty (FunTy arg res)
1731 = eqFunTy vis env arg res ty
1732 go vis env (FunTy arg res) ty
1733 = eqFunTy vis env arg res ty
1734
1735 -- See Note [Equality on AppTys] in Type
1736 go vis env (AppTy s1 t1) ty2
1737 | Just (s2, t2) <- tcRepSplitAppTy_maybe ty2
1738 = go vis env s1 s2 <!> go vis env t1 t2
1739 go vis env ty1 (AppTy s2 t2)
1740 | Just (s1, t1) <- tcRepSplitAppTy_maybe ty1
1741 = go vis env s1 s2 <!> go vis env t1 t2
1742 go vis env (TyConApp tc1 ts1) (TyConApp tc2 ts2)
1743 = check vis (tc1 == tc2) <!> gos (tc_vis vis tc1) env ts1 ts2
1744 go vis env (CastTy t1 _) t2 = go vis env t1 t2
1745 go vis env t1 (CastTy t2 _) = go vis env t1 t2
1746 go _ _ (CoercionTy {}) (CoercionTy {}) = Nothing
1747 go vis _ _ _ = Just vis
1748
1749 gos _ _ [] [] = Nothing
1750 gos (v:vs) env (t1:ts1) (t2:ts2) = go v env t1 t2 <!> gos vs env ts1 ts2
1751 gos (v:_) _ _ _ = Just v
1752 gos _ _ _ _ = panic "tc_eq_type"
1753
1754 tc_vis :: Bool -> TyCon -> [Bool]
1755 tc_vis True tc = viss ++ repeat True
1756 -- the repeat True is necessary because tycons can legitimately
1757 -- be oversaturated
1758 where
1759 bndrs = tyConBinders tc
1760 viss = map isVisibleTyConBinder bndrs
1761 tc_vis False _ = repeat False -- if we're not in a visible context, our args
1762 -- aren't either
1763
1764 check :: Bool -> Bool -> Maybe Bool
1765 check _ True = Nothing
1766 check vis False = Just vis
1767
1768 orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
1769
1770 -- @eqFunTy arg res ty@ is True when @ty@ equals @FunTy arg res@. This is
1771 -- sometimes hard to know directly because @ty@ might have some casts
1772 -- obscuring the FunTy. And 'splitAppTy' is difficult because we can't
1773 -- always extract a RuntimeRep (see Note [xyz]) if the kind of the arg or
1774 -- res is unzonked/unflattened. Thus this function, which handles this
1775 -- corner case.
1776 eqFunTy :: Bool -> RnEnv2 -> Type -> Type -> Type -> Maybe Bool
1777 eqFunTy vis env arg res (FunTy arg' res')
1778 = go vis env arg arg' <!> go vis env res res'
1779 eqFunTy vis env arg res ty@(AppTy{})
1780 | Just (tc, [_, _, arg', res']) <- get_args ty []
1781 , tc == funTyCon
1782 = go vis env arg arg' <!> go vis env res res'
1783 where
1784 get_args :: Type -> [Type] -> Maybe (TyCon, [Type])
1785 get_args (AppTy f x) args = get_args f (x:args)
1786 get_args (CastTy t _) args = get_args t args
1787 get_args (TyConApp tc tys) args = Just (tc, tys ++ args)
1788 get_args _ _ = Nothing
1789 eqFunTy vis _ _ _ _
1790 = Just vis
1791
1792 -- | Like 'pickyEqTypeVis', but returns a Bool for convenience
1793 pickyEqType :: TcType -> TcType -> Bool
1794 -- Check when two types _look_ the same, _including_ synonyms.
1795 -- So (pickyEqType String [Char]) returns False
1796 -- This ignores kinds and coercions, because this is used only for printing.
1797 pickyEqType ty1 ty2
1798 = isNothing $
1799 tc_eq_type (const Nothing) ty1 ty2
1800
1801 {- *********************************************************************
1802 * *
1803 Predicate types
1804 * *
1805 ************************************************************************
1806
1807 Deconstructors and tests on predicate types
1808
1809 Note [Kind polymorphic type classes]
1810 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1811 class C f where... -- C :: forall k. k -> Constraint
1812 g :: forall (f::*). C f => f -> f
1813
1814 Here the (C f) in the signature is really (C * f), and we
1815 don't want to complain that the * isn't a type variable!
1816 -}
1817
1818 isTyVarClassPred :: PredType -> Bool
1819 isTyVarClassPred ty = case getClassPredTys_maybe ty of
1820 Just (_, tys) -> all isTyVarTy tys
1821 _ -> False
1822
1823 -------------------------
1824 checkValidClsArgs :: Bool -> Class -> [KindOrType] -> Bool
1825 -- If the Bool is True (flexible contexts), return True (i.e. ok)
1826 -- Otherwise, check that the type (not kind) args are all headed by a tyvar
1827 -- E.g. (Eq a) accepted, (Eq (f a)) accepted, but (Eq Int) rejected
1828 -- This function is here rather than in TcValidity because it is
1829 -- called from TcSimplify, which itself is imported by TcValidity
1830 checkValidClsArgs flexible_contexts cls kts
1831 | flexible_contexts = True
1832 | otherwise = all hasTyVarHead tys
1833 where
1834 tys = filterOutInvisibleTypes (classTyCon cls) kts
1835
1836 hasTyVarHead :: Type -> Bool
1837 -- Returns true of (a t1 .. tn), where 'a' is a type variable
1838 hasTyVarHead ty -- Haskell 98 allows predicates of form
1839 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1840 | otherwise -- where a is a type variable
1841 = case tcSplitAppTy_maybe ty of
1842 Just (ty, _) -> hasTyVarHead ty
1843 Nothing -> False
1844
1845 evVarPred_maybe :: EvVar -> Maybe PredType
1846 evVarPred_maybe v = if isPredTy ty then Just ty else Nothing
1847 where ty = varType v
1848
1849 evVarPred :: EvVar -> PredType
1850 evVarPred var
1851 | debugIsOn
1852 = case evVarPred_maybe var of
1853 Just pred -> pred
1854 Nothing -> pprPanic "tcEvVarPred" (ppr var <+> ppr (varType var))
1855 | otherwise
1856 = varType var
1857
1858 ------------------
1859 -- | When inferring types, should we quantify over a given predicate?
1860 -- Generally true of classes; generally false of equality constraints.
1861 -- Equality constraints that mention quantified type variables and
1862 -- implicit variables complicate the story. See Notes
1863 -- [Inheriting implicit parameters] and [Quantifying over equality constraints]
1864 pickQuantifiablePreds
1865 :: TyVarSet -- Quantifying over these
1866 -> TcThetaType -- Proposed constraints to quantify
1867 -> TcThetaType -- A subset that we can actually quantify
1868 -- This function decides whether a particular constraint should be
1869 -- quantified over, given the type variables that are being quantified
1870 pickQuantifiablePreds qtvs theta
1871 = let flex_ctxt = True in -- Quantify over non-tyvar constraints, even without
1872 -- -XFlexibleContexts: see Trac #10608, #10351
1873 -- flex_ctxt <- xoptM Opt_FlexibleContexts
1874 filter (pick_me flex_ctxt) theta
1875 where
1876 pick_me flex_ctxt pred
1877 = case classifyPredType pred of
1878
1879 ClassPred cls tys
1880 | Just {} <- isCallStackPred cls tys
1881 -- NEVER infer a CallStack constraint
1882 -- Otherwise, we let the constraints bubble up to be
1883 -- solved from the outer context, or be defaulted when we
1884 -- reach the top-level.
1885 -- see Note [Overview of implicit CallStacks]
1886 -> False
1887
1888 | isIPClass cls -> True -- See note [Inheriting implicit parameters]
1889
1890 | otherwise
1891 -> pick_cls_pred flex_ctxt cls tys
1892
1893 EqPred ReprEq ty1 ty2 -> pick_cls_pred flex_ctxt coercibleClass [ty1, ty2]
1894 -- representational equality is like a class constraint
1895
1896 EqPred NomEq ty1 ty2 -> quant_fun ty1 || quant_fun ty2
1897 IrredPred ty -> tyCoVarsOfType ty `intersectsVarSet` qtvs
1898
1899 pick_cls_pred flex_ctxt cls tys
1900 = tyCoVarsOfTypes tys `intersectsVarSet` qtvs
1901 && (checkValidClsArgs flex_ctxt cls tys)
1902 -- Only quantify over predicates that checkValidType
1903 -- will pass! See Trac #10351.
1904
1905 -- See Note [Quantifying over equality constraints]
1906 quant_fun ty
1907 = case tcSplitTyConApp_maybe ty of
1908 Just (tc, tys) | isTypeFamilyTyCon tc
1909 -> tyCoVarsOfTypes tys `intersectsVarSet` qtvs
1910 _ -> False
1911
1912 pickCapturedPreds
1913 :: TyVarSet -- Quantifying over these
1914 -> TcThetaType -- Proposed constraints to quantify
1915 -> TcThetaType -- A subset that we can actually quantify
1916 -- A simpler version of pickQuantifiablePreds, used to winnow down
1917 -- the inferred constraints of a group of bindings, into those for
1918 -- one particular identifier
1919 pickCapturedPreds qtvs theta
1920 = filter captured theta
1921 where
1922 captured pred = isIPPred pred || (tyCoVarsOfType pred `intersectsVarSet` qtvs)
1923
1924
1925 -- Superclasses
1926
1927 type PredWithSCs = (PredType, [PredType])
1928
1929 mkMinimalBySCs :: [PredType] -> [PredType]
1930 -- Remove predicates that can be deduced from others by superclasses,
1931 -- including duplicate predicates. The result is a subset of the input.
1932 mkMinimalBySCs ptys = go preds_with_scs []
1933 where
1934 preds_with_scs :: [PredWithSCs]
1935 preds_with_scs = [ (pred, pred : transSuperClasses pred)
1936 | pred <- ptys ]
1937
1938 go :: [PredWithSCs] -- Work list
1939 -> [PredWithSCs] -- Accumulating result
1940 -> [PredType]
1941 go [] min_preds = map fst min_preds
1942 go (work_item@(p,_) : work_list) min_preds
1943 | p `in_cloud` work_list || p `in_cloud` min_preds
1944 = go work_list min_preds
1945 | otherwise
1946 = go work_list (work_item : min_preds)
1947
1948 in_cloud :: PredType -> [PredWithSCs] -> Bool
1949 in_cloud p ps = or [ p `eqType` p' | (_, scs) <- ps, p' <- scs ]
1950
1951 transSuperClasses :: PredType -> [PredType]
1952 -- (transSuperClasses p) returns (p's superclasses) not including p
1953 -- Stop if you encounter the same class again
1954 -- See Note [Expanding superclasses]
1955 transSuperClasses p
1956 = go emptyNameSet p
1957 where
1958 go :: NameSet -> PredType -> [PredType]
1959 go rec_clss p
1960 | ClassPred cls tys <- classifyPredType p
1961 , let cls_nm = className cls
1962 , not (cls_nm `elemNameSet` rec_clss)
1963 , let rec_clss' | isCTupleClass cls = rec_clss
1964 | otherwise = rec_clss `extendNameSet` cls_nm
1965 = [ p' | sc <- immSuperClasses cls tys
1966 , p' <- sc : go rec_clss' sc ]
1967 | otherwise
1968 = []
1969
1970 immSuperClasses :: Class -> [Type] -> [PredType]
1971 immSuperClasses cls tys
1972 = substTheta (zipTvSubst tyvars tys) sc_theta
1973 where
1974 (tyvars,sc_theta,_,_) = classBigSig cls
1975
1976 isImprovementPred :: PredType -> Bool
1977 -- Either it's an equality, or has some functional dependency
1978 isImprovementPred ty
1979 = case classifyPredType ty of
1980 EqPred NomEq t1 t2 -> not (t1 `tcEqType` t2)
1981 EqPred ReprEq _ _ -> False
1982 ClassPred cls _ -> classHasFds cls
1983 IrredPred {} -> True -- Might have equalities after reduction?
1984
1985 {- Note [Expanding superclasses]
1986 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1987 When we expand superclasses, we use the following algorithm:
1988
1989 expand( so_far, pred ) returns the transitive superclasses of pred,
1990 not including pred itself
1991 1. If pred is not a class constraint, return empty set
1992 Otherwise pred = C ts
1993 2. If C is in so_far, return empty set (breaks loops)
1994 3. Find the immediate superclasses constraints of (C ts)
1995 4. For each such sc_pred, return (sc_pred : expand( so_far+C, D ss )
1996
1997 Notice that
1998
1999 * With normal Haskell-98 classes, the loop-detector will never bite,
2000 so we'll get all the superclasses.
2001
2002 * Since there is only a finite number of distinct classes, expansion
2003 must terminate.
2004
2005 * The loop breaking is a bit conservative. Notably, a tuple class
2006 could contain many times without threatening termination:
2007 (Eq a, (Ord a, Ix a))
2008 And this is try of any class that we can statically guarantee
2009 as non-recursive (in some sense). For now, we just make a special
2010 case for tuples. Something better would be cool.
2011
2012 See also TcTyDecls.checkClassCycles.
2013
2014 Note [Inheriting implicit parameters]
2015 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2016 Consider this:
2017
2018 f x = (x::Int) + ?y
2019
2020 where f is *not* a top-level binding.
2021 From the RHS of f we'll get the constraint (?y::Int).
2022 There are two types we might infer for f:
2023
2024 f :: Int -> Int
2025
2026 (so we get ?y from the context of f's definition), or
2027
2028 f :: (?y::Int) => Int -> Int
2029
2030 At first you might think the first was better, because then
2031 ?y behaves like a free variable of the definition, rather than
2032 having to be passed at each call site. But of course, the WHOLE
2033 IDEA is that ?y should be passed at each call site (that's what
2034 dynamic binding means) so we'd better infer the second.
2035
2036 BOTTOM LINE: when *inferring types* you must quantify over implicit
2037 parameters, *even if* they don't mention the bound type variables.
2038 Reason: because implicit parameters, uniquely, have local instance
2039 declarations. See pickQuantifiablePreds.
2040
2041 Note [Quantifying over equality constraints]
2042 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2043 Should we quantify over an equality constraint (s ~ t)? In general, we don't.
2044 Doing so may simply postpone a type error from the function definition site to
2045 its call site. (At worst, imagine (Int ~ Bool)).
2046
2047 However, consider this
2048 forall a. (F [a] ~ Int) => blah
2049 Should we quantify over the (F [a] ~ Int). Perhaps yes, because at the call
2050 site we will know 'a', and perhaps we have instance F [Bool] = Int.
2051 So we *do* quantify over a type-family equality where the arguments mention
2052 the quantified variables.
2053
2054 ************************************************************************
2055 * *
2056 \subsection{Predicates}
2057 * *
2058 ************************************************************************
2059 -}
2060
2061 isSigmaTy :: TcType -> Bool
2062 -- isSigmaTy returns true of any qualified type. It doesn't
2063 -- *necessarily* have any foralls. E.g
2064 -- f :: (?x::Int) => Int -> Int
2065 isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
2066 isSigmaTy (ForAllTy {}) = True
2067 isSigmaTy (FunTy a _) = isPredTy a
2068 isSigmaTy _ = False
2069
2070 isRhoTy :: TcType -> Bool -- True of TcRhoTypes; see Note [TcRhoType]
2071 isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty'
2072 isRhoTy (ForAllTy {}) = False
2073 isRhoTy (FunTy a r) = not (isPredTy a) && isRhoTy r
2074 isRhoTy _ = True
2075
2076 -- | Like 'isRhoTy', but also says 'True' for 'Infer' types
2077 isRhoExpTy :: ExpType -> Bool
2078 isRhoExpTy (Check ty) = isRhoTy ty
2079 isRhoExpTy (Infer {}) = True
2080
2081 isOverloadedTy :: Type -> Bool
2082 -- Yes for a type of a function that might require evidence-passing
2083 -- Used only by bindLocalMethods
2084 isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
2085 isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty
2086 isOverloadedTy (FunTy a _) = isPredTy a
2087 isOverloadedTy _ = False
2088
2089 isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
2090 isUnitTy, isCharTy, isAnyTy :: Type -> Bool
2091 isFloatTy = is_tc floatTyConKey
2092 isDoubleTy = is_tc doubleTyConKey
2093 isIntegerTy = is_tc integerTyConKey
2094 isIntTy = is_tc intTyConKey
2095 isWordTy = is_tc wordTyConKey
2096 isBoolTy = is_tc boolTyConKey
2097 isUnitTy = is_tc unitTyConKey
2098 isCharTy = is_tc charTyConKey
2099 isAnyTy = is_tc anyTyConKey
2100
2101 -- | Does a type represent a floating-point number?
2102 isFloatingTy :: Type -> Bool
2103 isFloatingTy ty = isFloatTy ty || isDoubleTy ty
2104
2105 -- | Is a type 'String'?
2106 isStringTy :: Type -> Bool
2107 isStringTy ty
2108 = case tcSplitTyConApp_maybe ty of
2109 Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty
2110 _ -> False
2111
2112 -- | Is a type a 'CallStack'?
2113 isCallStackTy :: Type -> Bool
2114 isCallStackTy ty
2115 | Just tc <- tyConAppTyCon_maybe ty
2116 = tc `hasKey` callStackTyConKey
2117 | otherwise
2118 = False
2119
2120 -- | Is a 'PredType' a 'CallStack' implicit parameter?
2121 --
2122 -- If so, return the name of the parameter.
2123 isCallStackPred :: Class -> [Type] -> Maybe FastString
2124 isCallStackPred cls tys
2125 | [ty1, ty2] <- tys
2126 , isIPClass cls
2127 , isCallStackTy ty2
2128 = isStrLitTy ty1
2129 | otherwise
2130 = Nothing
2131
2132 hasIPPred :: PredType -> Bool
2133 hasIPPred pred
2134 = case classifyPredType pred of
2135 ClassPred cls tys
2136 | isIPClass cls -> True
2137 | isCTupleClass cls -> any hasIPPred tys
2138 _other -> False
2139
2140 is_tc :: Unique -> Type -> Bool
2141 -- Newtypes are opaque to this
2142 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
2143 Just (tc, _) -> uniq == getUnique tc
2144 Nothing -> False
2145
2146 -- | Does the given tyvar appear in the given type outside of any
2147 -- non-newtypes? Assume we're looking for @a@. Says "yes" for
2148 -- @a@, @N a@, @b a@, @a b@, @b (N a)@. Says "no" for
2149 -- @[a]@, @Maybe a@, @T a@, where @N@ is a newtype and @T@ is a datatype.
2150 isTyVarExposed :: TcTyVar -> TcType -> Bool
2151 isTyVarExposed tv (TyVarTy tv') = tv == tv'
2152 isTyVarExposed tv (TyConApp tc tys)
2153 | isNewTyCon tc = any (isTyVarExposed tv) tys
2154 | otherwise = False
2155 isTyVarExposed _ (LitTy {}) = False
2156 isTyVarExposed tv (AppTy fun arg) = isTyVarExposed tv fun
2157 || isTyVarExposed tv arg
2158 isTyVarExposed _ (ForAllTy {}) = False
2159 isTyVarExposed _ (FunTy {}) = False
2160 isTyVarExposed tv (CastTy ty _) = isTyVarExposed tv ty
2161 isTyVarExposed _ (CoercionTy {}) = False
2162
2163 -- | Is the equality
2164 -- a ~r ...a....
2165 -- definitely insoluble or not?
2166 -- a ~r Maybe a -- Definitely insoluble
2167 -- a ~N ...(F a)... -- Not definitely insoluble
2168 -- -- Perhaps (F a) reduces to Int
2169 -- a ~R ...(N a)... -- Not definitely insoluble
2170 -- -- Perhaps newtype N a = MkN Int
2171 -- See Note [Occurs check error] in
2172 -- TcCanonical for the motivation for this function.
2173 isInsolubleOccursCheck :: EqRel -> TcTyVar -> TcType -> Bool
2174 isInsolubleOccursCheck eq_rel tv ty
2175 = go ty
2176 where
2177 go ty | Just ty' <- tcView ty = go ty'
2178 go (TyVarTy tv') = tv == tv' || go (tyVarKind tv')
2179 go (LitTy {}) = False
2180 go (AppTy t1 t2) = go t1 || go t2
2181 go (FunTy t1 t2) = go t1 || go t2
2182 go (ForAllTy (TvBndr tv' _) inner_ty)
2183 | tv' == tv = False
2184 | otherwise = go (tyVarKind tv') || go inner_ty
2185 go (CastTy ty _) = go ty -- ToDo: what about the coercion
2186 go (CoercionTy _) = False -- ToDo: what about the coercion
2187 go (TyConApp tc tys)
2188 | isGenerativeTyCon tc role = any go tys
2189 | otherwise = any go (drop (tyConArity tc) tys)
2190 -- (a ~ F b a), where F has arity 1,
2191 -- has an insoluble occurs check
2192
2193 role = eqRelRole eq_rel
2194
2195 isRigidTy :: TcType -> Bool
2196 isRigidTy ty
2197 | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
2198 | Just {} <- tcSplitAppTy_maybe ty = True
2199 | isForAllTy ty = True
2200 | otherwise = False
2201
2202 isRigidEqPred :: TcLevel -> PredTree -> Bool
2203 -- ^ True of all Nominal equalities that are solidly insoluble
2204 -- This means all equalities *except*
2205 -- * Meta-tv non-SigTv on LHS
2206 -- * Meta-tv SigTv on LHS, tyvar on right
2207 isRigidEqPred tc_lvl (EqPred NomEq ty1 _)
2208 | Just tv1 <- tcGetTyVar_maybe ty1
2209 = ASSERT2( tcIsTcTyVar tv1, ppr tv1 )
2210 not (isMetaTyVar tv1) || isTouchableMetaTyVar tc_lvl tv1
2211
2212 | otherwise -- LHS is not a tyvar
2213 = True
2214
2215 isRigidEqPred _ _ = False -- Not an equality
2216
2217 {-
2218 ************************************************************************
2219 * *
2220 \subsection{Transformation of Types to TcTypes}
2221 * *
2222 ************************************************************************
2223 -}
2224
2225 toTcType :: Type -> TcType
2226 -- The constraint solver expects EvVars to have TcType, in which the
2227 -- free type variables are TcTyVars. So we convert from Type to TcType here
2228 -- A bit tiresome; but one day I expect the two types to be entirely separate
2229 -- in which case we'll definitely need to do this
2230 toTcType = runIdentity . to_tc_type emptyVarSet
2231
2232 toTcTypeBag :: Bag EvVar -> Bag EvVar -- All TyVars are transformed to TcTyVars
2233 toTcTypeBag evvars = mapBag (\tv -> setTyVarKind tv (toTcType (tyVarKind tv))) evvars
2234
2235 to_tc_mapper :: TyCoMapper VarSet Identity
2236 to_tc_mapper
2237 = TyCoMapper { tcm_smart = False -- more efficient not to use smart ctors
2238 , tcm_tyvar = tyvar
2239 , tcm_covar = covar
2240 , tcm_hole = hole
2241 , tcm_tybinder = tybinder }
2242 where
2243 tyvar :: VarSet -> TyVar -> Identity Type
2244 tyvar ftvs tv
2245 | Just var <- lookupVarSet ftvs tv = return $ TyVarTy var
2246 | isTcTyVar tv = TyVarTy <$> updateTyVarKindM (to_tc_type ftvs) tv
2247 | otherwise
2248 = do { kind' <- to_tc_type ftvs (tyVarKind tv)
2249 ; return $ TyVarTy $ mkTcTyVar (tyVarName tv) kind' vanillaSkolemTv }
2250
2251 covar :: VarSet -> CoVar -> Identity Coercion
2252 covar ftvs cv
2253 | Just var <- lookupVarSet ftvs cv = return $ CoVarCo var
2254 | otherwise = CoVarCo <$> updateVarTypeM (to_tc_type ftvs) cv
2255
2256 hole :: VarSet -> CoercionHole -> Role -> Type -> Type
2257 -> Identity Coercion
2258 hole ftvs h r t1 t2 = mkHoleCo h r <$> to_tc_type ftvs t1
2259 <*> to_tc_type ftvs t2
2260
2261 tybinder :: VarSet -> TyVar -> ArgFlag -> Identity (VarSet, TyVar)
2262 tybinder ftvs tv _vis = do { kind' <- to_tc_type ftvs (tyVarKind tv)
2263 ; let tv' = mkTcTyVar (tyVarName tv) kind'
2264 vanillaSkolemTv
2265 ; return (ftvs `extendVarSet` tv', tv') }
2266
2267 to_tc_type :: VarSet -> Type -> Identity TcType
2268 to_tc_type = mapType to_tc_mapper
2269
2270 {-
2271 ************************************************************************
2272 * *
2273 \subsection{Misc}
2274 * *
2275 ************************************************************************
2276
2277 Note [Visible type application]
2278 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2279 GHC implements a generalisation of the algorithm described in the
2280 "Visible Type Application" paper (available from
2281 http://www.cis.upenn.edu/~sweirich/publications.html). A key part
2282 of that algorithm is to distinguish user-specified variables from inferred
2283 variables. For example, the following should typecheck:
2284
2285 f :: forall a b. a -> b -> b
2286 f = const id
2287
2288 g = const id
2289
2290 x = f @Int @Bool 5 False
2291 y = g 5 @Bool False
2292
2293 The idea is that we wish to allow visible type application when we are
2294 instantiating a specified, fixed variable. In practice, specified, fixed
2295 variables are either written in a type signature (or
2296 annotation), OR are imported from another module. (We could do better here,
2297 for example by doing SCC analysis on parts of a module and considering any
2298 type from outside one's SCC to be fully specified, but this is very confusing to
2299 users. The simple rule above is much more straightforward and predictable.)
2300
2301 So, both of f's quantified variables are specified and may be instantiated.
2302 But g has no type signature, so only id's variable is specified (because id
2303 is imported). We write the type of g as forall {a}. a -> forall b. b -> b.
2304 Note that the a is in braces, meaning it cannot be instantiated with
2305 visible type application.
2306
2307 Tracking specified vs. inferred variables is done conveniently by a field
2308 in TyBinder.
2309
2310 -}
2311
2312 deNoteType :: Type -> Type
2313 -- Remove all *outermost* type synonyms and other notes
2314 deNoteType ty | Just ty' <- coreView ty = deNoteType ty'
2315 deNoteType ty = ty
2316
2317 {-
2318 Find the free tycons and classes of a type. This is used in the front
2319 end of the compiler.
2320 -}
2321
2322 {-
2323 ************************************************************************
2324 * *
2325 \subsection[TysWiredIn-ext-type]{External types}
2326 * *
2327 ************************************************************************
2328
2329 The compiler's foreign function interface supports the passing of a
2330 restricted set of types as arguments and results (the restricting factor
2331 being the )
2332 -}
2333
2334 tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type)
2335 -- (tcSplitIOType_maybe t) returns Just (IO,t',co)
2336 -- if co : t ~ IO t'
2337 -- returns Nothing otherwise
2338 tcSplitIOType_maybe ty
2339 = case tcSplitTyConApp_maybe ty of
2340 Just (io_tycon, [io_res_ty])
2341 | io_tycon `hasKey` ioTyConKey ->
2342 Just (io_tycon, io_res_ty)
2343 _ ->
2344 Nothing
2345
2346 isFFITy :: Type -> Bool
2347 -- True for any TyCon that can possibly be an arg or result of an FFI call
2348 isFFITy ty = isValid (checkRepTyCon legalFFITyCon ty)
2349
2350 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Validity
2351 -- Checks for valid argument type for a 'foreign import'
2352 isFFIArgumentTy dflags safety ty
2353 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
2354
2355 isFFIExternalTy :: Type -> Validity
2356 -- Types that are allowed as arguments of a 'foreign export'
2357 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
2358
2359 isFFIImportResultTy :: DynFlags -> Type -> Validity
2360 isFFIImportResultTy dflags ty
2361 = checkRepTyCon (legalFIResultTyCon dflags) ty
2362
2363 isFFIExportResultTy :: Type -> Validity
2364 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
2365
2366 isFFIDynTy :: Type -> Type -> Validity
2367 -- The type in a foreign import dynamic must be Ptr, FunPtr, or a newtype of
2368 -- either, and the wrapped function type must be equal to the given type.
2369 -- We assume that all types have been run through normaliseFfiType, so we don't
2370 -- need to worry about expanding newtypes here.
2371 isFFIDynTy expected ty
2372 -- Note [Foreign import dynamic]
2373 -- In the example below, expected would be 'CInt -> IO ()', while ty would
2374 -- be 'FunPtr (CDouble -> IO ())'.
2375 | Just (tc, [ty']) <- splitTyConApp_maybe ty
2376 , tyConUnique tc `elem` [ptrTyConKey, funPtrTyConKey]
2377 , eqType ty' expected
2378 = IsValid
2379 | otherwise
2380 = NotValid (vcat [ text "Expected: Ptr/FunPtr" <+> pprParendType expected <> comma
2381 , text " Actual:" <+> ppr ty ])
2382
2383 isFFILabelTy :: Type -> Validity
2384 -- The type of a foreign label must be Ptr, FunPtr, or a newtype of either.
2385 isFFILabelTy ty = checkRepTyCon ok ty
2386 where
2387 ok tc | tc `hasKey` funPtrTyConKey || tc `hasKey` ptrTyConKey
2388 = IsValid
2389 | otherwise
2390 = NotValid (text "A foreign-imported address (via &foo) must have type (Ptr a) or (FunPtr a)")
2391
2392 isFFIPrimArgumentTy :: DynFlags -> Type -> Validity
2393 -- Checks for valid argument type for a 'foreign import prim'
2394 -- Currently they must all be simple unlifted types, or the well-known type
2395 -- Any, which can be used to pass the address to a Haskell object on the heap to
2396 -- the foreign function.
2397 isFFIPrimArgumentTy dflags ty
2398 | isAnyTy ty = IsValid
2399 | otherwise = checkRepTyCon (legalFIPrimArgTyCon dflags) ty
2400
2401 isFFIPrimResultTy :: DynFlags -> Type -> Validity
2402 -- Checks for valid result type for a 'foreign import prim' Currently
2403 -- it must be an unlifted type, including unboxed tuples, unboxed
2404 -- sums, or the well-known type Any.
2405 isFFIPrimResultTy dflags ty
2406 | isAnyTy ty = IsValid
2407 | otherwise = checkRepTyCon (legalFIPrimResultTyCon dflags) ty
2408
2409 isFunPtrTy :: Type -> Bool
2410 isFunPtrTy ty
2411 | Just (tc, [_]) <- splitTyConApp_maybe ty
2412 = tc `hasKey` funPtrTyConKey
2413 | otherwise
2414 = False
2415
2416 -- normaliseFfiType gets run before checkRepTyCon, so we don't
2417 -- need to worry about looking through newtypes or type functions
2418 -- here; that's already been taken care of.
2419 checkRepTyCon :: (TyCon -> Validity) -> Type -> Validity
2420 checkRepTyCon check_tc ty
2421 = case splitTyConApp_maybe ty of
2422 Just (tc, tys)
2423 | isNewTyCon tc -> NotValid (hang msg 2 (mk_nt_reason tc tys $$ nt_fix))
2424 | otherwise -> case check_tc tc of
2425 IsValid -> IsValid
2426 NotValid extra -> NotValid (msg $$ extra)
2427 Nothing -> NotValid (quotes (ppr ty) <+> text "is not a data type")
2428 where
2429 msg = quotes (ppr ty) <+> text "cannot be marshalled in a foreign call"
2430 mk_nt_reason tc tys
2431 | null tys = text "because its data constructor is not in scope"
2432 | otherwise = text "because the data constructor for"
2433 <+> quotes (ppr tc) <+> text "is not in scope"
2434 nt_fix = text "Possible fix: import the data constructor to bring it into scope"
2435
2436 {-
2437 Note [Foreign import dynamic]
2438 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2439 A dynamic stub must be of the form 'FunPtr ft -> ft' where ft is any foreign
2440 type. Similarly, a wrapper stub must be of the form 'ft -> IO (FunPtr ft)'.
2441
2442 We use isFFIDynTy to check whether a signature is well-formed. For example,
2443 given a (illegal) declaration like:
2444
2445 foreign import ccall "dynamic"
2446 foo :: FunPtr (CDouble -> IO ()) -> CInt -> IO ()
2447
2448 isFFIDynTy will compare the 'FunPtr' type 'CDouble -> IO ()' with the curried
2449 result type 'CInt -> IO ()', and return False, as they are not equal.
2450
2451
2452 ----------------------------------------------
2453 These chaps do the work; they are not exported
2454 ----------------------------------------------
2455 -}
2456
2457 legalFEArgTyCon :: TyCon -> Validity
2458 legalFEArgTyCon tc
2459 -- It's illegal to make foreign exports that take unboxed
2460 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
2461 = boxedMarshalableTyCon tc
2462
2463 legalFIResultTyCon :: DynFlags -> TyCon -> Validity
2464 legalFIResultTyCon dflags tc
2465 | tc == unitTyCon = IsValid
2466 | otherwise = marshalableTyCon dflags tc
2467
2468 legalFEResultTyCon :: TyCon -> Validity
2469 legalFEResultTyCon tc
2470 | tc == unitTyCon = IsValid
2471 | otherwise = boxedMarshalableTyCon tc
2472
2473 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Validity
2474 -- Checks validity of types going from Haskell -> external world
2475 legalOutgoingTyCon dflags _ tc
2476 = marshalableTyCon dflags tc
2477
2478 legalFFITyCon :: TyCon -> Validity
2479 -- True for any TyCon that can possibly be an arg or result of an FFI call
2480 legalFFITyCon tc
2481 | isUnliftedTyCon tc = IsValid
2482 | tc == unitTyCon = IsValid
2483 | otherwise = boxedMarshalableTyCon tc
2484
2485 marshalableTyCon :: DynFlags -> TyCon -> Validity
2486 marshalableTyCon dflags tc
2487 | isUnliftedTyCon tc
2488 , not (isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc)
2489 , not (null (tyConPrimRep tc)) -- Note [Marshalling void]
2490 = validIfUnliftedFFITypes dflags
2491 | otherwise
2492 = boxedMarshalableTyCon tc
2493
2494 boxedMarshalableTyCon :: TyCon -> Validity
2495 boxedMarshalableTyCon tc
2496 | getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
2497 , int32TyConKey, int64TyConKey
2498 , wordTyConKey, word8TyConKey, word16TyConKey
2499 , word32TyConKey, word64TyConKey
2500 , floatTyConKey, doubleTyConKey
2501 , ptrTyConKey, funPtrTyConKey
2502 , charTyConKey
2503 , stablePtrTyConKey
2504 , boolTyConKey
2505 ]
2506 = IsValid
2507
2508 | otherwise = NotValid empty
2509
2510 legalFIPrimArgTyCon :: DynFlags -> TyCon -> Validity
2511 -- Check args of 'foreign import prim', only allow simple unlifted types.
2512 -- Strictly speaking it is unnecessary to ban unboxed tuples and sums here since
2513 -- currently they're of the wrong kind to use in function args anyway.
2514 legalFIPrimArgTyCon dflags tc
2515 | isUnliftedTyCon tc
2516 , not (isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc)
2517 = validIfUnliftedFFITypes dflags
2518 | otherwise
2519 = NotValid unlifted_only
2520
2521 legalFIPrimResultTyCon :: DynFlags -> TyCon -> Validity
2522 -- Check result type of 'foreign import prim'. Allow simple unlifted
2523 -- types and also unboxed tuple and sum result types.
2524 legalFIPrimResultTyCon dflags tc
2525 | isUnliftedTyCon tc
2526 , isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc
2527 || not (null (tyConPrimRep tc)) -- Note [Marshalling void]
2528 = validIfUnliftedFFITypes dflags
2529
2530 | otherwise
2531 = NotValid unlifted_only
2532
2533 unlifted_only :: MsgDoc
2534 unlifted_only = text "foreign import prim only accepts simple unlifted types"
2535
2536 validIfUnliftedFFITypes :: DynFlags -> Validity
2537 validIfUnliftedFFITypes dflags
2538 | xopt LangExt.UnliftedFFITypes dflags = IsValid
2539 | otherwise = NotValid (text "To marshal unlifted types, use UnliftedFFITypes")
2540
2541 {-
2542 Note [Marshalling void]
2543 ~~~~~~~~~~~~~~~~~~~~~~~
2544 We don't treat State# (whose PrimRep is VoidRep) as marshalable.
2545 In turn that means you can't write
2546 foreign import foo :: Int -> State# RealWorld
2547
2548 Reason: the back end falls over with panic "primRepHint:VoidRep";
2549 and there is no compelling reason to permit it
2550 -}
2551
2552 {-
2553 ************************************************************************
2554 * *
2555 The "Paterson size" of a type
2556 * *
2557 ************************************************************************
2558 -}
2559
2560 {-
2561 Note [Paterson conditions on PredTypes]
2562 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2563 We are considering whether *class* constraints terminate
2564 (see Note [Paterson conditions]). Precisely, the Paterson conditions
2565 would have us check that "the constraint has fewer constructors and variables
2566 (taken together and counting repetitions) than the head.".
2567
2568 However, we can be a bit more refined by looking at which kind of constraint
2569 this actually is. There are two main tricks:
2570
2571 1. It seems like it should be OK not to count the tuple type constructor
2572 for a PredType like (Show a, Eq a) :: Constraint, since we don't
2573 count the "implicit" tuple in the ThetaType itself.
2574
2575 In fact, the Paterson test just checks *each component* of the top level
2576 ThetaType against the size bound, one at a time. By analogy, it should be
2577 OK to return the size of the *largest* tuple component as the size of the
2578 whole tuple.
2579
2580 2. Once we get into an implicit parameter or equality we
2581 can't get back to a class constraint, so it's safe
2582 to say "size 0". See Trac #4200.
2583
2584 NB: we don't want to detect PredTypes in sizeType (and then call
2585 sizePred on them), or we might get an infinite loop if that PredType
2586 is irreducible. See Trac #5581.
2587 -}
2588
2589 type TypeSize = IntWithInf
2590
2591 sizeType :: Type -> TypeSize
2592 -- Size of a type: the number of variables and constructors
2593 -- Ignore kinds altogether
2594 sizeType = go
2595 where
2596 go ty | Just exp_ty <- tcView ty = go exp_ty
2597 go (TyVarTy {}) = 1
2598 go (TyConApp tc tys)
2599 | isTypeFamilyTyCon tc = infinity -- Type-family applications can
2600 -- expand to any arbitrary size
2601 | otherwise = sizeTypes (filterOutInvisibleTypes tc tys) + 1
2602 -- Why filter out invisible args? I suppose any
2603 -- size ordering is sound, but why is this better?
2604 -- I came across this when investigating #14010.
2605 go (LitTy {}) = 1
2606 go (FunTy arg res) = go arg + go res + 1
2607 go (AppTy fun arg) = go fun + go arg
2608 go (ForAllTy (TvBndr tv vis) ty)
2609 | isVisibleArgFlag vis = go (tyVarKind tv) + go ty + 1
2610 | otherwise = go ty + 1
2611 go (CastTy ty _) = go ty
2612 go (CoercionTy {}) = 0
2613
2614 sizeTypes :: [Type] -> TypeSize
2615 sizeTypes tys = sum (map sizeType tys)
2616
2617 -----------------------------------------------------------------------------------
2618 -----------------------------------------------------------------------------------
2619 -----------------------
2620 -- | For every arg a tycon can take, the returned list says True if the argument
2621 -- is taken visibly, and False otherwise. Ends with an infinite tail of Trues to
2622 -- allow for oversaturation.
2623 tcTyConVisibilities :: TyCon -> [Bool]
2624 tcTyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True
2625 where
2626 tc_binder_viss = map isVisibleTyConBinder (tyConBinders tc)
2627 tc_return_kind_viss = map isVisibleBinder (fst $ tcSplitPiTys (tyConResKind tc))
2628
2629 -- | If the tycon is applied to the types, is the next argument visible?
2630 isNextTyConArgVisible :: TyCon -> [Type] -> Bool
2631 isNextTyConArgVisible tc tys
2632 = tcTyConVisibilities tc `getNth` length tys
2633
2634 -- | Should this type be applied to a visible argument?
2635 isNextArgVisible :: TcType -> Bool
2636 isNextArgVisible ty
2637 | Just (bndr, _) <- tcSplitPiTy_maybe ty = isVisibleBinder bndr
2638 | otherwise = True
2639 -- this second case might happen if, say, we have an unzonked TauTv.
2640 -- But TauTvs can't range over types that take invisible arguments