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