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