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