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