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