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