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