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