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