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