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