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