60ab685418bc31dd199f6bc7aa049da341ce167e
[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 #-}
19
20 module TcType (
21 --------------------------------
22 -- Types
23 TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
24 TcTyVar, TcTyVarSet, TcDTyVarSet, TcKind, TcCoVar,
25
26 -- TcLevel
27 TcLevel(..), topTcLevel, pushTcLevel,
28 strictlyDeeperThan, sameDepthAs, fmvTcLevel,
29
30 --------------------------------
31 -- MetaDetails
32 UserTypeCtxt(..), pprUserTypeCtxt, pprSigCtxt, isSigMaybe,
33 TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
34 MetaDetails(Flexi, Indirect), MetaInfo(..),
35 isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy,
36 isSigTyVar, isOverlappableTyVar, isTyConableTyVar,
37 isFskTyVar, isFmvTyVar, isFlattenTyVar, isReturnTyVar,
38 isAmbiguousTyVar, metaTvRef, metaTyVarInfo,
39 isFlexi, isIndirect, isRuntimeUnkSkol,
40 isTypeVar, isKindVar,
41 metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
42 isTouchableMetaTyVar, isTouchableOrFmv,
43 isFloatedTouchableMetaTyVar,
44 canUnifyWithPolyType,
45
46 --------------------------------
47 -- Builders
48 mkPhiTy, mkSigmaTy, mkTcEqPred, mkTcReprEqPred, mkTcEqPredRole,
49
50 --------------------------------
51 -- Splitters
52 -- These are important because they do not look through newtypes
53 tcView,
54 tcSplitForAllTys, tcSplitPhiTy, tcSplitPredFunTy_maybe,
55 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
56 tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
57 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, repSplitAppTy_maybe,
58 tcInstHeadTyNotSynonym, tcInstHeadTyAppAllTyVars,
59 tcGetTyVar_maybe, tcGetTyVar, nextRole,
60 tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe,
61
62 ---------------------------------
63 -- Predicates.
64 -- Again, newtypes are opaque
65 eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX,
66 tcEqType, tcEqKind,
67 isSigmaTy, isRhoTy, isOverloadedTy,
68 isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
69 isIntegerTy, isBoolTy, isUnitTy, isCharTy,
70 isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
71 isPredTy, isTyVarClassPred, isTyVarExposed, isTyVarUnderDatatype,
72 checkValidClsArgs, hasTyVarHead,
73 isRigidEqPred, isRigidTy,
74
75 ---------------------------------
76 -- Misc type manipulators
77 deNoteType, occurCheckExpand, OccCheckResult(..),
78 orphNamesOfType, orphNamesOfDFunHead, orphNamesOfCo,
79 orphNamesOfTypes, orphNamesOfCoCon,
80 getDFunTyKey,
81 evVarPred_maybe, evVarPred,
82
83 ---------------------------------
84 -- Predicate types
85 mkMinimalBySCs, transSuperClasses, transSuperClassesPred,
86 immSuperClasses,
87 isImprovementPred,
88
89 -- * Finding type instances
90 tcTyFamInsts,
91
92 -- * Finding "exact" (non-dead) type variables
93 exactTyVarsOfType, exactTyVarsOfTypes,
94
95 ---------------------------------
96 -- Foreign import and export
97 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
98 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
99 isFFIExportResultTy, -- :: Type -> Bool
100 isFFIExternalTy, -- :: Type -> Bool
101 isFFIDynTy, -- :: Type -> Type -> Bool
102 isFFIPrimArgumentTy, -- :: DynFlags -> Type -> Bool
103 isFFIPrimResultTy, -- :: DynFlags -> Type -> Bool
104 isFFILabelTy, -- :: Type -> Bool
105 isFFITy, -- :: Type -> Bool
106 isFunPtrTy, -- :: Type -> Bool
107 tcSplitIOType_maybe, -- :: Type -> Maybe Type
108
109 --------------------------------
110 -- Rexported from Kind
111 Kind, typeKind,
112 unliftedTypeKind, liftedTypeKind,
113 openTypeKind, constraintKind, mkArrowKind, mkArrowKinds,
114 isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind,
115 tcIsSubKind, splitKindFunTys, defaultKind,
116
117 --------------------------------
118 -- Rexported from Type
119 Type, PredType, ThetaType,
120 mkForAllTy, mkForAllTys,
121 mkFunTy, mkFunTys, zipFunTys,
122 mkTyConApp, mkAppTy, mkAppTys, applyTy, applyTys,
123 mkTyVarTy, mkTyVarTys, mkTyConTy,
124
125 isClassPred, isEqPred, isIPPred,
126 mkClassPred,
127 isDictLikeTy,
128 tcSplitDFunTy, tcSplitDFunHead,
129 mkEqPred,
130
131 -- Type substitutions
132 TvSubst(..), -- Representation visible to a few friends
133 TvSubstEnv, emptyTvSubst,
134 mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst,
135 mkTopTvSubst, notElemTvSubst, unionTvSubst,
136 getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
137 Type.lookupTyVar, Type.extendTvSubst, Type.substTyVarBndr,
138 extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
139 Type.substTy, substTys, substTyWith, substTheta, substTyVar, substTyVars,
140
141 isUnLiftedType, -- Source types are always lifted
142 isUnboxedTupleType, -- Ditto
143 isPrimitiveType,
144
145 tyVarsOfType, tyVarsOfTypes, closeOverKinds,
146 tyVarsOfTypeList, tyVarsOfTypesList,
147 tyVarsOfTypeAcc, tyVarsOfTypesAcc,
148 tyVarsOfTypeDSet, tyVarsOfTypesDSet, closeOverKindsDSet,
149 tcTyVarsOfType, tcTyVarsOfTypes,
150
151 --------------------------------
152 -- Transforming Types to TcTypes
153 toTcType, -- :: Type -> TcType
154 toTcTyVar, -- :: TyVar -> TcTyVar
155 toTcTypeBag, -- :: Bag EvVar -> Bag EvVar
156
157 pprKind, pprParendKind, pprSigmaType,
158 pprType, pprParendType, pprTypeApp, pprTyThingCategory,
159 pprTheta, pprThetaArrowTy, pprClassPred,
160
161 TypeSize, sizeType, sizeTypes
162
163 ) where
164
165 #include "HsVersions.h"
166
167 -- friends:
168 import Kind
169 import TypeRep
170 import Class
171 import Var
172 import ForeignCall
173 import VarSet
174 import Coercion
175 import Type
176 import TyCon
177 import CoAxiom
178
179 -- others:
180 import DynFlags
181 import Name -- hiding (varName)
182 -- We use this to make dictionaries for type literals.
183 -- Perhaps there's a better way to do this?
184 import NameSet
185 import VarEnv
186 import PrelNames
187 import TysWiredIn
188 import BasicTypes
189 import Util
190 import Bag
191 import Maybes
192 import ListSetOps
193 import Outputable
194 import FastString
195 import ErrUtils( Validity(..), MsgDoc, isValid )
196
197 import Data.IORef
198 import Control.Monad (liftM, ap)
199 #if __GLASGOW_HASKELL__ < 709
200 import Control.Applicative (Applicative(..))
201 #endif
202
203 {-
204 ************************************************************************
205 * *
206 \subsection{Types}
207 * *
208 ************************************************************************
209
210 The type checker divides the generic Type world into the
211 following more structured beasts:
212
213 sigma ::= forall tyvars. phi
214 -- A sigma type is a qualified type
215 --
216 -- Note that even if 'tyvars' is empty, theta
217 -- may not be: e.g. (?x::Int) => Int
218
219 -- Note that 'sigma' is in prenex form:
220 -- all the foralls are at the front.
221 -- A 'phi' type has no foralls to the right of
222 -- an arrow
223
224 phi :: theta => rho
225
226 rho ::= sigma -> rho
227 | tau
228
229 -- A 'tau' type has no quantification anywhere
230 -- Note that the args of a type constructor must be taus
231 tau ::= tyvar
232 | tycon tau_1 .. tau_n
233 | tau_1 tau_2
234 | tau_1 -> tau_2
235
236 -- In all cases, a (saturated) type synonym application is legal,
237 -- provided it expands to the required form.
238 -}
239
240 type TcTyVar = TyVar -- Used only during type inference
241 type TcCoVar = CoVar -- Used only during type inference; mutable
242 type TcType = Type -- A TcType can have mutable type variables
243 -- Invariant on ForAllTy in TcTypes:
244 -- forall a. T
245 -- a cannot occur inside a MutTyVar in T; that is,
246 -- T is "flattened" before quantifying over a
247
248 -- These types do not have boxy type variables in them
249 type TcPredType = PredType
250 type TcThetaType = ThetaType
251 type TcSigmaType = TcType
252 type TcRhoType = TcType -- Note [TcRhoType]
253 type TcTauType = TcType
254 type TcKind = Kind
255 type TcTyVarSet = TyVarSet
256 type TcDTyVarSet = DTyVarSet
257
258 {-
259 Note [TcRhoType]
260 ~~~~~~~~~~~~~~~~
261 A TcRhoType has no foralls or contexts at the top, or to the right of an arrow
262 YES (forall a. a->a) -> Int
263 NO forall a. a -> Int
264 NO Eq a => a -> a
265 NO Int -> forall a. a -> Int
266
267
268 ************************************************************************
269 * *
270 \subsection{TyVarDetails}
271 * *
272 ************************************************************************
273
274 TyVarDetails gives extra info about type variables, used during type
275 checking. It's attached to mutable type variables only.
276 It's knot-tied back to Var.hs. There is no reason in principle
277 why Var.hs shouldn't actually have the definition, but it "belongs" here.
278
279 Note [Signature skolems]
280 ~~~~~~~~~~~~~~~~~~~~~~~~
281 Consider this
282
283 f :: forall a. [a] -> Int
284 f (x::b : xs) = 3
285
286 Here 'b' is a lexically scoped type variable, but it turns out to be
287 the same as the skolem 'a'. So we have a special kind of skolem
288 constant, SigTv, which can unify with other SigTvs. They are used
289 *only* for pattern type signatures.
290
291 Similarly consider
292 data T (a:k1) = MkT (S a)
293 data S (b:k2) = MkS (T b)
294 When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
295 because they end up unifying; we want those SigTvs again.
296
297 Note [ReturnTv]
298 ~~~~~~~~~~~~~~~
299 We sometimes want to convert a checking algorithm into an inference
300 algorithm. An easy way to do this is to "check" that a term has a
301 metavariable as a type. But, we must be careful to allow that metavariable
302 to unify with *anything*. (Well, anything that doesn't fail an occurs-check.)
303 This is what ReturnTv means.
304
305 For example, if we have
306
307 (undefined :: (forall a. TF1 a ~ TF2 a => a)) x
308
309 we'll call (tcInfer . tcExpr) on the function expression. tcInfer will
310 create a ReturnTv to represent the expression's type. We really need this
311 ReturnTv to become set to (forall a. TF1 a ~ TF2 a => a) despite the fact
312 that this type mentions type families and is a polytype.
313
314 However, we must also be careful to make sure that the ReturnTvs really
315 always do get unified with something -- we don't want these floating
316 around in the solver. So, we check after running the checker to make
317 sure the ReturnTv is filled. If it's not, we set it to a TauTv.
318
319 We can't ASSERT that no ReturnTvs hit the solver, because they
320 can if there's, say, a kind error that stops checkTauTvUpdate from
321 working. This happens in test case typecheck/should_fail/T5570, for
322 example.
323
324 See also the commentary on #9404.
325 -}
326
327 -- A TyVarDetails is inside a TyVar
328 data TcTyVarDetails
329 = SkolemTv -- A skolem
330 Bool -- True <=> this skolem type variable can be overlapped
331 -- when looking up instances
332 -- See Note [Binding when looking up instances] in InstEnv
333
334 | FlatSkol -- A flatten-skolem. It stands for the TcType, and zonking
335 TcType -- will replace it by that type.
336 -- See Note [The flattening story] in TcFlatten
337
338 | RuntimeUnk -- Stands for an as-yet-unknown type in the GHCi
339 -- interactive context
340
341 | MetaTv { mtv_info :: MetaInfo
342 , mtv_ref :: IORef MetaDetails
343 , mtv_tclvl :: TcLevel } -- See Note [TcLevel and untouchable type variables]
344
345 vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
346 -- See Note [Binding when looking up instances] in InstEnv
347 vanillaSkolemTv = SkolemTv False -- Might be instantiated
348 superSkolemTv = SkolemTv True -- Treat this as a completely distinct type
349
350 -----------------------------
351 data MetaDetails
352 = Flexi -- Flexi type variables unify to become Indirects
353 | Indirect TcType
354
355 instance Outputable MetaDetails where
356 ppr Flexi = ptext (sLit "Flexi")
357 ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty
358
359 data MetaInfo
360 = TauTv -- This MetaTv is an ordinary unification variable
361 -- A TauTv is always filled in with a tau-type, which
362 -- never contains any ForAlls.
363
364 | ReturnTv -- Can unify with *anything*. Used to convert a
365 -- type "checking" algorithm into a type inference algorithm.
366 -- See Note [ReturnTv]
367
368 | SigTv -- A variant of TauTv, except that it should not be
369 -- unified with a type, only with a type variable
370 -- SigTvs are only distinguished to improve error messages
371 -- see Note [Signature skolems]
372 -- The MetaDetails, if filled in, will
373 -- always be another SigTv or a SkolemTv
374
375 | FlatMetaTv -- A flatten meta-tyvar
376 -- It is a meta-tyvar, but it is always untouchable, with level 0
377 -- See Note [The flattening story] in TcFlatten
378
379 -------------------------------------
380 -- UserTypeCtxt describes the origin of the polymorphic type
381 -- in the places where we need to an expression has that type
382
383 data UserTypeCtxt
384 = FunSigCtxt -- Function type signature, when checking the type
385 -- Also used for types in SPECIALISE pragmas
386 Name -- Name of the function
387 Bool -- True <=> report redundant constraints
388 -- This is usually True, but False for
389 -- * Record selectors (not important here)
390 -- * Class and instance methods. Here
391 -- the code may legitimately be more
392 -- polymorphic than the signature
393 -- generated from the class
394 -- declaration
395
396 | InfSigCtxt Name -- Inferred type for function
397 | ExprSigCtxt -- Expression type signature
398
399 | ConArgCtxt Name -- Data constructor argument
400 | TySynCtxt Name -- RHS of a type synonym decl
401 | PatSynCtxt Name -- Type sig for a pattern synonym
402 -- eg pattern C :: Int -> T
403 | PatSigCtxt -- Type sig in pattern
404 -- eg f (x::t) = ...
405 -- or (x::t, y) = e
406 | RuleSigCtxt Name -- LHS of a RULE forall
407 -- RULE "foo" forall (x :: a -> a). f (Just x) = ...
408 | ResSigCtxt -- Result type sig
409 -- f x :: t = ....
410 | ForSigCtxt Name -- Foreign import or export signature
411 | DefaultDeclCtxt -- Types in a default declaration
412 | InstDeclCtxt -- An instance declaration
413 | SpecInstCtxt -- SPECIALISE instance pragma
414 | ThBrackCtxt -- Template Haskell type brackets [t| ... |]
415 | GenSigCtxt -- Higher-rank or impredicative situations
416 -- e.g. (f e) where f has a higher-rank type
417 -- We might want to elaborate this
418 | GhciCtxt -- GHCi command :kind <type>
419
420 | ClassSCCtxt Name -- Superclasses of a class
421 | SigmaCtxt -- Theta part of a normal for-all type
422 -- f :: <S> => a -> a
423 | DataTyCtxt Name -- Theta part of a data decl
424 -- data <S> => T a = MkT a
425
426 {-
427 -- Notes re TySynCtxt
428 -- We allow type synonyms that aren't types; e.g. type List = []
429 --
430 -- If the RHS mentions tyvars that aren't in scope, we'll
431 -- quantify over them:
432 -- e.g. type T = a->a
433 -- will become type T = forall a. a->a
434 --
435 -- With gla-exts that's right, but for H98 we should complain.
436 -}
437
438
439 {- *********************************************************************
440 * *
441 Untoucable type variables
442 * *
443 ********************************************************************* -}
444
445 newtype TcLevel = TcLevel Int deriving( Eq, Ord )
446 -- See Note [TcLevel and untouchable type variables] for what this Int is
447 -- See also Note [TcLevel assignment]
448
449 {-
450 Note [TcLevel and untouchable type variables]
451 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
452 * Each unification variable (MetaTv)
453 and each Implication
454 has a level number (of type TcLevel)
455
456 * INVARIANTS. In a tree of Implications,
457
458 (ImplicInv) The level number of an Implication is
459 STRICTLY GREATER THAN that of its parent
460
461 (MetaTvInv) The level number of a unification variable is
462 LESS THAN OR EQUAL TO that of its parent
463 implication
464
465 * A unification variable is *touchable* if its level number
466 is EQUAL TO that of its immediate parent implication.
467
468 * INVARIANT
469 (GivenInv) The free variables of the ic_given of an
470 implication are all untouchable; ie their level
471 numbers are LESS THAN the ic_tclvl of the implication
472
473 Note [Skolem escape prevention]
474 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
475 We only unify touchable unification variables. Because of
476 (MetaTvInv), there can be no occurrences of the variable further out,
477 so the unification can't cause the skolems to escape. Example:
478 data T = forall a. MkT a (a->Int)
479 f x (MkT v f) = length [v,x]
480 We decide (x::alpha), and generate an implication like
481 [1]forall a. (a ~ alpha[0])
482 But we must not unify alpha:=a, because the skolem would escape.
483
484 For the cases where we DO want to unify, we rely on floating the
485 equality. Example (with same T)
486 g x (MkT v f) = x && True
487 We decide (x::alpha), and generate an implication like
488 [1]forall a. (Bool ~ alpha[0])
489 We do NOT unify directly, bur rather float out (if the constraint
490 does not mention 'a') to get
491 (Bool ~ alpha[0]) /\ [1]forall a.()
492 and NOW we can unify alpha.
493
494 The same idea of only unifying touchables solves another problem.
495 Suppose we had
496 (F Int ~ uf[0]) /\ [1](forall a. C a => F Int ~ beta[1])
497 In this example, beta is touchable inside the implication. The
498 first solveSimpleWanteds step leaves 'uf' un-unified. Then we move inside
499 the implication where a new constraint
500 uf ~ beta
501 emerges. If we (wrongly) spontaneously solved it to get uf := beta,
502 the whole implication disappears but when we pop out again we are left with
503 (F Int ~ uf) which will be unified by our final zonking stage and
504 uf will get unified *once more* to (F Int).
505
506 Note [TcLevel assignment]
507 ~~~~~~~~~~~~~~~~~~~~~~~~~
508 We arrange the TcLevels like this
509
510 1 Top level
511 2 Flatten-meta-vars of level 3
512 3 First-level implication constraints
513 4 Flatten-meta-vars of level 5
514 5 Second-level implication constraints
515 ...etc...
516
517 The even-numbered levels are for the flatten-meta-variables assigned
518 at the next level in. Eg for a second-level implication conststraint
519 (level 5), the flatten meta-vars are level 4, which makes them untouchable.
520 The flatten meta-vars could equally well all have level 0, or just NotALevel
521 since they do not live across implications.
522 -}
523
524 fmvTcLevel :: TcLevel -> TcLevel
525 -- See Note [TcLevel assignment]
526 fmvTcLevel (TcLevel n) = TcLevel (n-1)
527
528 topTcLevel :: TcLevel
529 -- See Note [TcLevel assignment]
530 topTcLevel = TcLevel 1 -- 1 = outermost level
531
532 pushTcLevel :: TcLevel -> TcLevel
533 -- See Note [TcLevel assignment]
534 pushTcLevel (TcLevel us) = TcLevel (us + 2)
535
536 strictlyDeeperThan :: TcLevel -> TcLevel -> Bool
537 strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
538 = tv_tclvl > ctxt_tclvl
539
540 sameDepthAs :: TcLevel -> TcLevel -> Bool
541 sameDepthAs (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
542 = ctxt_tclvl == tv_tclvl -- NB: invariant ctxt_tclvl >= tv_tclvl
543 -- So <= would be equivalent
544
545 checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool
546 -- Checks (MetaTvInv) from Note [TcLevel and untouchable type variables]
547 checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
548 = ctxt_tclvl >= tv_tclvl
549
550 instance Outputable TcLevel where
551 ppr (TcLevel us) = ppr us
552
553 {-
554 ************************************************************************
555 * *
556 Pretty-printing
557 * *
558 ************************************************************************
559 -}
560
561 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
562 -- For debugging
563 pprTcTyVarDetails (SkolemTv True) = ptext (sLit "ssk")
564 pprTcTyVarDetails (SkolemTv False) = ptext (sLit "sk")
565 pprTcTyVarDetails (RuntimeUnk {}) = ptext (sLit "rt")
566 pprTcTyVarDetails (FlatSkol {}) = ptext (sLit "fsk")
567 pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
568 = pp_info <> colon <> ppr tclvl
569 where
570 pp_info = case info of
571 ReturnTv -> ptext (sLit "ret")
572 TauTv -> ptext (sLit "tau")
573 SigTv -> ptext (sLit "sig")
574 FlatMetaTv -> ptext (sLit "fuv")
575
576 pprUserTypeCtxt :: UserTypeCtxt -> SDoc
577 pprUserTypeCtxt (FunSigCtxt n _) = ptext (sLit "the type signature for") <+> quotes (ppr n)
578 pprUserTypeCtxt (InfSigCtxt n) = ptext (sLit "the inferred type for") <+> quotes (ppr n)
579 pprUserTypeCtxt (RuleSigCtxt n) = ptext (sLit "a RULE for") <+> quotes (ppr n)
580 pprUserTypeCtxt ExprSigCtxt = ptext (sLit "an expression type signature")
581 pprUserTypeCtxt (ConArgCtxt c) = ptext (sLit "the type of the constructor") <+> quotes (ppr c)
582 pprUserTypeCtxt (TySynCtxt c) = ptext (sLit "the RHS of the type synonym") <+> quotes (ppr c)
583 pprUserTypeCtxt (PatSynCtxt c) = ptext (sLit "the type signature for pattern synonym") <+> quotes (ppr c)
584 pprUserTypeCtxt ThBrackCtxt = ptext (sLit "a Template Haskell quotation [t|...|]")
585 pprUserTypeCtxt PatSigCtxt = ptext (sLit "a pattern type signature")
586 pprUserTypeCtxt ResSigCtxt = ptext (sLit "a result type signature")
587 pprUserTypeCtxt (ForSigCtxt n) = ptext (sLit "the foreign declaration for") <+> quotes (ppr n)
588 pprUserTypeCtxt DefaultDeclCtxt = ptext (sLit "a type in a `default' declaration")
589 pprUserTypeCtxt InstDeclCtxt = ptext (sLit "an instance declaration")
590 pprUserTypeCtxt SpecInstCtxt = ptext (sLit "a SPECIALISE instance pragma")
591 pprUserTypeCtxt GenSigCtxt = ptext (sLit "a type expected by the context")
592 pprUserTypeCtxt GhciCtxt = ptext (sLit "a type in a GHCi command")
593 pprUserTypeCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
594 pprUserTypeCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type")
595 pprUserTypeCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
596
597 pprSigCtxt :: UserTypeCtxt -> SDoc -> SDoc -> SDoc
598 -- (pprSigCtxt ctxt <extra> <type>)
599 -- prints In <extra> the type signature for 'f':
600 -- f :: <type>
601 -- The <extra> is either empty or "the ambiguity check for"
602 pprSigCtxt ctxt extra pp_ty
603 | Just n <- isSigMaybe ctxt
604 = vcat [ ptext (sLit "In") <+> extra <+> ptext (sLit "the type signature:")
605 , nest 2 (pprPrefixOcc n <+> dcolon <+> pp_ty) ]
606
607 | otherwise
608 = hang (ptext (sLit "In") <+> extra <+> pprUserTypeCtxt ctxt <> colon)
609 2 pp_ty
610
611 where
612
613 isSigMaybe :: UserTypeCtxt -> Maybe Name
614 isSigMaybe (FunSigCtxt n _) = Just n
615 isSigMaybe (ConArgCtxt n) = Just n
616 isSigMaybe (ForSigCtxt n) = Just n
617 isSigMaybe (PatSynCtxt n) = Just n
618 isSigMaybe _ = Nothing
619
620 {-
621 ************************************************************************
622 * *
623 Finding type family instances
624 * *
625 ************************************************************************
626 -}
627
628 -- | Finds outermost type-family applications occuring in a type,
629 -- after expanding synonyms.
630 tcTyFamInsts :: Type -> [(TyCon, [Type])]
631 tcTyFamInsts ty
632 | Just exp_ty <- tcView ty = tcTyFamInsts exp_ty
633 tcTyFamInsts (TyVarTy _) = []
634 tcTyFamInsts (TyConApp tc tys)
635 | isTypeFamilyTyCon tc = [(tc, tys)]
636 | otherwise = concat (map tcTyFamInsts tys)
637 tcTyFamInsts (LitTy {}) = []
638 tcTyFamInsts (FunTy ty1 ty2) = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
639 tcTyFamInsts (AppTy ty1 ty2) = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
640 tcTyFamInsts (ForAllTy _ ty) = tcTyFamInsts ty
641
642 {-
643 ************************************************************************
644 * *
645 The "exact" free variables of a type
646 * *
647 ************************************************************************
648
649 Note [Silly type synonym]
650 ~~~~~~~~~~~~~~~~~~~~~~~~~
651 Consider
652 type T a = Int
653 What are the free tyvars of (T x)? Empty, of course!
654 Here's the example that Ralf Laemmel showed me:
655 foo :: (forall a. C u a -> C u a) -> u
656 mappend :: Monoid u => u -> u -> u
657
658 bar :: Monoid u => u
659 bar = foo (\t -> t `mappend` t)
660 We have to generalise at the arg to f, and we don't
661 want to capture the constraint (Monad (C u a)) because
662 it appears to mention a. Pretty silly, but it was useful to him.
663
664 exactTyVarsOfType is used by the type checker to figure out exactly
665 which type variables are mentioned in a type. It's also used in the
666 smart-app checking code --- see TcExpr.tcIdApp
667
668 On the other hand, consider a *top-level* definition
669 f = (\x -> x) :: T a -> T a
670 If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
671 if we have an application like (f "x") we get a confusing error message
672 involving Any. So the conclusion is this: when generalising
673 - at top level use tyVarsOfType
674 - in nested bindings use exactTyVarsOfType
675 See Trac #1813 for example.
676 -}
677
678 exactTyVarsOfType :: Type -> TyVarSet
679 -- Find the free type variables (of any kind)
680 -- but *expand* type synonyms. See Note [Silly type synonym] above.
681 exactTyVarsOfType ty
682 = go ty
683 where
684 go ty | Just ty' <- tcView ty = go ty' -- This is the key line
685 go (TyVarTy tv) = unitVarSet tv
686 go (TyConApp _ tys) = exactTyVarsOfTypes tys
687 go (LitTy {}) = emptyVarSet
688 go (FunTy arg res) = go arg `unionVarSet` go res
689 go (AppTy fun arg) = go fun `unionVarSet` go arg
690 go (ForAllTy tyvar ty) = delVarSet (go ty) tyvar
691
692 exactTyVarsOfTypes :: [Type] -> TyVarSet
693 exactTyVarsOfTypes = mapUnionVarSet exactTyVarsOfType
694
695 {-
696 ************************************************************************
697 * *
698 Predicates
699 * *
700 ************************************************************************
701 -}
702
703 isTouchableOrFmv :: TcLevel -> TcTyVar -> Bool
704 isTouchableOrFmv ctxt_tclvl tv
705 = ASSERT2( isTcTyVar tv, ppr tv )
706 case tcTyVarDetails tv of
707 MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info }
708 -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
709 ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
710 case info of
711 FlatMetaTv -> True
712 _ -> tv_tclvl `sameDepthAs` ctxt_tclvl
713 _ -> False
714
715 isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
716 isTouchableMetaTyVar ctxt_tclvl tv
717 = ASSERT2( isTcTyVar tv, ppr tv )
718 case tcTyVarDetails tv of
719 MetaTv { mtv_tclvl = tv_tclvl }
720 -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
721 ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
722 tv_tclvl `sameDepthAs` ctxt_tclvl
723 _ -> False
724
725 isFloatedTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
726 isFloatedTouchableMetaTyVar ctxt_tclvl tv
727 = ASSERT2( isTcTyVar tv, ppr tv )
728 case tcTyVarDetails tv of
729 MetaTv { mtv_tclvl = tv_tclvl } -> tv_tclvl `strictlyDeeperThan` ctxt_tclvl
730 _ -> False
731
732 isImmutableTyVar :: TyVar -> Bool
733 isImmutableTyVar tv
734 | isTcTyVar tv = isSkolemTyVar tv
735 | otherwise = True
736
737 isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
738 isMetaTyVar, isAmbiguousTyVar,
739 isFmvTyVar, isFskTyVar, isFlattenTyVar, isReturnTyVar :: TcTyVar -> Bool
740
741 isTyConableTyVar tv
742 -- True of a meta-type variable that can be filled in
743 -- with a type constructor application; in particular,
744 -- not a SigTv
745 = ASSERT( isTcTyVar tv)
746 case tcTyVarDetails tv of
747 MetaTv { mtv_info = SigTv } -> False
748 _ -> True
749
750 isFmvTyVar tv
751 = ASSERT2( isTcTyVar tv, ppr tv )
752 case tcTyVarDetails tv of
753 MetaTv { mtv_info = FlatMetaTv } -> True
754 _ -> False
755
756 -- | True of both given and wanted flatten-skolems (fak and usk)
757 isFlattenTyVar tv
758 = ASSERT2( isTcTyVar tv, ppr tv )
759 case tcTyVarDetails tv of
760 FlatSkol {} -> True
761 MetaTv { mtv_info = FlatMetaTv } -> True
762 _ -> False
763
764 -- | True of FlatSkol skolems only
765 isFskTyVar tv
766 = ASSERT2( isTcTyVar tv, ppr tv )
767 case tcTyVarDetails tv of
768 FlatSkol {} -> True
769 _ -> False
770
771 isSkolemTyVar tv
772 = ASSERT2( isTcTyVar tv, ppr tv )
773 case tcTyVarDetails tv of
774 MetaTv {} -> False
775 _other -> True
776
777 isOverlappableTyVar tv
778 = ASSERT( isTcTyVar tv )
779 case tcTyVarDetails tv of
780 SkolemTv overlappable -> overlappable
781 _ -> False
782
783 isMetaTyVar tv
784 = ASSERT2( isTcTyVar tv, ppr tv )
785 case tcTyVarDetails tv of
786 MetaTv {} -> True
787 _ -> False
788
789 isReturnTyVar tv
790 = ASSERT2( isTcTyVar tv, ppr tv )
791 case tcTyVarDetails tv of
792 MetaTv { mtv_info = ReturnTv } -> True
793 _ -> False
794
795 -- isAmbiguousTyVar is used only when reporting type errors
796 -- It picks out variables that are unbound, namely meta
797 -- type variables and the RuntimUnk variables created by
798 -- RtClosureInspect.zonkRTTIType. These are "ambiguous" in
799 -- the sense that they stand for an as-yet-unknown type
800 isAmbiguousTyVar tv
801 = ASSERT2( isTcTyVar tv, ppr tv )
802 case tcTyVarDetails tv of
803 MetaTv {} -> True
804 RuntimeUnk {} -> True
805 _ -> False
806
807 isMetaTyVarTy :: TcType -> Bool
808 isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
809 isMetaTyVarTy _ = False
810
811 metaTyVarInfo :: TcTyVar -> MetaInfo
812 metaTyVarInfo tv
813 = ASSERT( isTcTyVar tv )
814 case tcTyVarDetails tv of
815 MetaTv { mtv_info = info } -> info
816 _ -> pprPanic "metaTyVarInfo" (ppr tv)
817
818 metaTyVarTcLevel :: TcTyVar -> TcLevel
819 metaTyVarTcLevel tv
820 = ASSERT( isTcTyVar tv )
821 case tcTyVarDetails tv of
822 MetaTv { mtv_tclvl = tclvl } -> tclvl
823 _ -> pprPanic "metaTyVarTcLevel" (ppr tv)
824
825 metaTyVarTcLevel_maybe :: TcTyVar -> Maybe TcLevel
826 metaTyVarTcLevel_maybe tv
827 = ASSERT( isTcTyVar tv )
828 case tcTyVarDetails tv of
829 MetaTv { mtv_tclvl = tclvl } -> Just tclvl
830 _ -> Nothing
831
832 setMetaTyVarTcLevel :: TcTyVar -> TcLevel -> TcTyVar
833 setMetaTyVarTcLevel tv tclvl
834 = ASSERT( isTcTyVar tv )
835 case tcTyVarDetails tv of
836 details@(MetaTv {}) -> setTcTyVarDetails tv (details { mtv_tclvl = tclvl })
837 _ -> pprPanic "metaTyVarTcLevel" (ppr tv)
838
839 isSigTyVar :: Var -> Bool
840 isSigTyVar tv
841 = ASSERT( isTcTyVar tv )
842 case tcTyVarDetails tv of
843 MetaTv { mtv_info = SigTv } -> True
844 _ -> False
845
846 metaTvRef :: TyVar -> IORef MetaDetails
847 metaTvRef tv
848 = ASSERT2( isTcTyVar tv, ppr tv )
849 case tcTyVarDetails tv of
850 MetaTv { mtv_ref = ref } -> ref
851 _ -> pprPanic "metaTvRef" (ppr tv)
852
853 isFlexi, isIndirect :: MetaDetails -> Bool
854 isFlexi Flexi = True
855 isFlexi _ = False
856
857 isIndirect (Indirect _) = True
858 isIndirect _ = False
859
860 isRuntimeUnkSkol :: TyVar -> Bool
861 -- Called only in TcErrors; see Note [Runtime skolems] there
862 isRuntimeUnkSkol x
863 | isTcTyVar x, RuntimeUnk <- tcTyVarDetails x = True
864 | otherwise = False
865
866 {-
867 ************************************************************************
868 * *
869 \subsection{Tau, sigma and rho}
870 * *
871 ************************************************************************
872 -}
873
874 mkSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
875 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
876
877 mkPhiTy :: [PredType] -> Type -> Type
878 mkPhiTy theta ty = foldr mkFunTy ty theta
879
880 mkTcEqPred :: TcType -> TcType -> Type
881 -- During type checking we build equalities between
882 -- type variables with OpenKind or ArgKind. Ultimately
883 -- they will all settle, but we want the equality predicate
884 -- itself to have kind '*'. I think.
885 --
886 -- But for now we call mkTyConApp, not mkEqPred, because the invariants
887 -- of the latter might not be satisfied during type checking.
888 -- Notably when we form an equalty (a : OpenKind) ~ (Int : *)
889 --
890 -- But this is horribly delicate: what about type variables
891 -- that turn out to be bound to Int#?
892 mkTcEqPred ty1 ty2
893 = mkTyConApp eqTyCon [k, ty1, ty2]
894 where
895 k = typeKind ty1
896
897 -- | Make a representational equality predicate
898 mkTcReprEqPred :: TcType -> TcType -> Type
899 mkTcReprEqPred ty1 ty2
900 = mkTyConApp coercibleTyCon [k, ty1, ty2]
901 where
902 k = typeKind ty1
903
904 -- | Make an equality predicate at a given role. The role must not be Phantom.
905 mkTcEqPredRole :: Role -> TcType -> TcType -> Type
906 mkTcEqPredRole Nominal = mkTcEqPred
907 mkTcEqPredRole Representational = mkTcReprEqPred
908 mkTcEqPredRole Phantom = panic "mkTcEqPredRole Phantom"
909
910 -- @isTauTy@ tests for nested for-alls.
911
912 isTauTy :: Type -> Bool
913 isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
914 isTauTy (TyVarTy _) = True
915 isTauTy (LitTy {}) = True
916 isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
917 isTauTy (AppTy a b) = isTauTy a && isTauTy b
918 isTauTy (FunTy a b) = isTauTy a && isTauTy b
919 isTauTy (ForAllTy {}) = False
920
921 isTauTyCon :: TyCon -> Bool
922 -- Returns False for type synonyms whose expansion is a polytype
923 isTauTyCon tc
924 | Just (_, rhs) <- synTyConDefn_maybe tc = isTauTy rhs
925 | otherwise = True
926
927 ---------------
928 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
929 -- construct a dictionary function name
930 getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
931 getDFunTyKey (TyVarTy tv) = getOccName tv
932 getDFunTyKey (TyConApp tc _) = getOccName tc
933 getDFunTyKey (LitTy x) = getDFunTyLitKey x
934 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
935 getDFunTyKey (FunTy _ _) = getOccName funTyCon
936 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
937
938 getDFunTyLitKey :: TyLit -> OccName
939 getDFunTyLitKey (NumTyLit n) = mkOccName Name.varName (show n)
940 getDFunTyLitKey (StrTyLit n) = mkOccName Name.varName (show n) -- hm
941
942 {-
943 ************************************************************************
944 * *
945 \subsection{Expanding and splitting}
946 * *
947 ************************************************************************
948
949 These tcSplit functions are like their non-Tc analogues, but
950 *) they do not look through newtypes
951
952 However, they are non-monadic and do not follow through mutable type
953 variables. It's up to you to make sure this doesn't matter.
954 -}
955
956 tcSplitForAllTys :: Type -> ([TyVar], Type)
957 tcSplitForAllTys ty = split ty ty []
958 where
959 split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
960 split _ (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
961 split orig_ty _ tvs = (reverse tvs, orig_ty)
962
963 tcIsForAllTy :: Type -> Bool
964 tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
965 tcIsForAllTy (ForAllTy {}) = True
966 tcIsForAllTy _ = False
967
968 tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
969 -- Split off the first predicate argument from a type
970 tcSplitPredFunTy_maybe ty
971 | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
972 tcSplitPredFunTy_maybe (FunTy arg res)
973 | isPredTy arg = Just (arg, res)
974 tcSplitPredFunTy_maybe _
975 = Nothing
976
977 tcSplitPhiTy :: Type -> (ThetaType, Type)
978 tcSplitPhiTy ty
979 = split ty []
980 where
981 split ty ts
982 = case tcSplitPredFunTy_maybe ty of
983 Just (pred, ty) -> split ty (pred:ts)
984 Nothing -> (reverse ts, ty)
985
986 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
987 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
988 (tvs, rho) -> case tcSplitPhiTy rho of
989 (theta, tau) -> (tvs, theta, tau)
990
991 -----------------------
992 tcDeepSplitSigmaTy_maybe
993 :: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType)
994 -- Looks for a *non-trivial* quantified type, under zero or more function arrows
995 -- By "non-trivial" we mean either tyvars or constraints are non-empty
996
997 tcDeepSplitSigmaTy_maybe ty
998 | Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty
999 , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty
1000 = Just (arg_ty:arg_tys, tvs, theta, rho)
1001
1002 | (tvs, theta, rho) <- tcSplitSigmaTy ty
1003 , not (null tvs && null theta)
1004 = Just ([], tvs, theta, rho)
1005
1006 | otherwise = Nothing
1007
1008 -----------------------
1009 tcTyConAppTyCon :: Type -> TyCon
1010 tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
1011 Just (tc, _) -> tc
1012 Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
1013
1014 tcTyConAppArgs :: Type -> [Type]
1015 tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
1016 Just (_, args) -> args
1017 Nothing -> pprPanic "tcTyConAppArgs" (pprType ty)
1018
1019 tcSplitTyConApp :: Type -> (TyCon, [Type])
1020 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
1021 Just stuff -> stuff
1022 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
1023
1024 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
1025 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
1026 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
1027 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
1028 -- Newtypes are opaque, so they may be split
1029 -- However, predicates are not treated
1030 -- as tycon applications by the type checker
1031 tcSplitTyConApp_maybe _ = Nothing
1032
1033 -----------------------
1034 tcSplitFunTys :: Type -> ([Type], Type)
1035 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
1036 Nothing -> ([], ty)
1037 Just (arg,res) -> (arg:args, res')
1038 where
1039 (args,res') = tcSplitFunTys res
1040
1041 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
1042 tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
1043 tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
1044 tcSplitFunTy_maybe _ = Nothing
1045 -- Note the typeKind guard
1046 -- Consider (?x::Int) => Bool
1047 -- We don't want to treat this as a function type!
1048 -- A concrete example is test tc230:
1049 -- f :: () -> (?p :: ()) => () -> ()
1050 --
1051 -- g = f () ()
1052
1053 tcSplitFunTysN
1054 :: TcRhoType
1055 -> Arity -- N: Number of desired args
1056 -> ([TcSigmaType], -- Arg types (N or fewer)
1057 TcSigmaType) -- The rest of the type
1058
1059 tcSplitFunTysN ty n_args
1060 | n_args == 0
1061 = ([], ty)
1062 | Just (arg,res) <- tcSplitFunTy_maybe ty
1063 = case tcSplitFunTysN res (n_args - 1) of
1064 (args, res) -> (arg:args, res)
1065 | otherwise
1066 = ([], ty)
1067
1068 tcSplitFunTy :: Type -> (Type, Type)
1069 tcSplitFunTy ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
1070
1071 tcFunArgTy :: Type -> Type
1072 tcFunArgTy ty = fst (tcSplitFunTy ty)
1073
1074 tcFunResultTy :: Type -> Type
1075 tcFunResultTy ty = snd (tcSplitFunTy ty)
1076
1077 -----------------------
1078 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
1079 tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
1080 tcSplitAppTy_maybe ty = repSplitAppTy_maybe ty
1081
1082 tcSplitAppTy :: Type -> (Type, Type)
1083 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
1084 Just stuff -> stuff
1085 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
1086
1087 tcSplitAppTys :: Type -> (Type, [Type])
1088 tcSplitAppTys ty
1089 = go ty []
1090 where
1091 go ty args = case tcSplitAppTy_maybe ty of
1092 Just (ty', arg) -> go ty' (arg:args)
1093 Nothing -> (ty,args)
1094
1095 -----------------------
1096 tcGetTyVar_maybe :: Type -> Maybe TyVar
1097 tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
1098 tcGetTyVar_maybe (TyVarTy tv) = Just tv
1099 tcGetTyVar_maybe _ = Nothing
1100
1101 tcGetTyVar :: String -> Type -> TyVar
1102 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
1103
1104 tcIsTyVarTy :: Type -> Bool
1105 tcIsTyVarTy ty = isJust (tcGetTyVar_maybe ty)
1106
1107 -----------------------
1108 tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
1109 -- Split the type of a dictionary function
1110 -- We don't use tcSplitSigmaTy, because a DFun may (with NDP)
1111 -- have non-Pred arguments, such as
1112 -- df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
1113 --
1114 -- Also NB splitFunTys, not tcSplitFunTys;
1115 -- the latter specifically stops at PredTy arguments,
1116 -- and we don't want to do that here
1117 tcSplitDFunTy ty
1118 = case tcSplitForAllTys ty of { (tvs, rho) ->
1119 case splitFunTys rho of { (theta, tau) ->
1120 case tcSplitDFunHead tau of { (clas, tys) ->
1121 (tvs, theta, clas, tys) }}}
1122
1123 tcSplitDFunHead :: Type -> (Class, [Type])
1124 tcSplitDFunHead = getClassPredTys
1125
1126 tcInstHeadTyNotSynonym :: Type -> Bool
1127 -- Used in Haskell-98 mode, for the argument types of an instance head
1128 -- These must not be type synonyms, but everywhere else type synonyms
1129 -- are transparent, so we need a special function here
1130 tcInstHeadTyNotSynonym ty
1131 = case ty of
1132 TyConApp tc _ -> not (isTypeSynonymTyCon tc)
1133 _ -> True
1134
1135 tcInstHeadTyAppAllTyVars :: Type -> Bool
1136 -- Used in Haskell-98 mode, for the argument types of an instance head
1137 -- These must be a constructor applied to type variable arguments.
1138 -- But we allow kind instantiations.
1139 tcInstHeadTyAppAllTyVars ty
1140 | Just ty' <- tcView ty -- Look through synonyms
1141 = tcInstHeadTyAppAllTyVars ty'
1142 | otherwise
1143 = case ty of
1144 TyConApp _ tys -> ok (filter (not . isKind) tys) -- avoid kinds
1145 FunTy arg res -> ok [arg, res]
1146 _ -> False
1147 where
1148 -- Check that all the types are type variables,
1149 -- and that each is distinct
1150 ok tys = equalLength tvs tys && hasNoDups tvs
1151 where
1152 tvs = mapMaybe get_tv tys
1153
1154 get_tv (TyVarTy tv) = Just tv -- through synonyms
1155 get_tv _ = Nothing
1156
1157 tcEqKind :: TcKind -> TcKind -> Bool
1158 tcEqKind = tcEqType
1159
1160 tcEqType :: TcType -> TcType -> Bool
1161 -- tcEqType is a proper, sensible type-equality function, that does
1162 -- just what you'd expect The function Type.eqType (currently) has a
1163 -- grotesque hack that makes OpenKind = *, and that is NOT what we
1164 -- want in the type checker! Otherwise, for example, TcCanonical.reOrient
1165 -- thinks the LHS and RHS have the same kinds, when they don't, and
1166 -- fails to re-orient. That in turn caused Trac #8553.
1167
1168 tcEqType ty1 ty2
1169 = go init_env ty1 ty2
1170 where
1171 init_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
1172 go env t1 t2 | Just t1' <- tcView t1 = go env t1' t2
1173 | Just t2' <- tcView t2 = go env t1 t2'
1174 go env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2
1175 go _ (LitTy lit1) (LitTy lit2) = lit1 == lit2
1176 go env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = go env (tyVarKind tv1) (tyVarKind tv2)
1177 && go (rnBndr2 env tv1 tv2) t1 t2
1178 go env (AppTy s1 t1) (AppTy s2 t2) = go env s1 s2 && go env t1 t2
1179 go env (FunTy s1 t1) (FunTy s2 t2) = go env s1 s2 && go env t1 t2
1180 go env (TyConApp tc1 ts1) (TyConApp tc2 ts2) = (tc1 == tc2) && gos env ts1 ts2
1181 go _ _ _ = False
1182
1183 gos _ [] [] = True
1184 gos env (t1:ts1) (t2:ts2) = go env t1 t2 && gos env ts1 ts2
1185 gos _ _ _ = False
1186
1187 {-
1188 Note [Occurs check expansion]
1189 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1190 (occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
1191 of occurrences of tv outside type function arguments, if that is
1192 possible; otherwise, it returns Nothing.
1193
1194 For example, suppose we have
1195 type F a b = [a]
1196 Then
1197 occurCheckExpand b (F Int b) = Just [Int]
1198 but
1199 occurCheckExpand a (F a Int) = Nothing
1200
1201 We don't promise to do the absolute minimum amount of expanding
1202 necessary, but we try not to do expansions we don't need to. We
1203 prefer doing inner expansions first. For example,
1204 type F a b = (a, Int, a, [a])
1205 type G b = Char
1206 We have
1207 occurCheckExpand b (F (G b)) = F Char
1208 even though we could also expand F to get rid of b.
1209
1210 See also Note [occurCheckExpand] in TcCanonical
1211 -}
1212
1213 data OccCheckResult a
1214 = OC_OK a
1215 | OC_Forall
1216 | OC_NonTyVar
1217 | OC_Occurs
1218
1219 instance Functor OccCheckResult where
1220 fmap = liftM
1221
1222 instance Applicative OccCheckResult where
1223 pure = OC_OK
1224 (<*>) = ap
1225
1226 instance Monad OccCheckResult where
1227 return = pure
1228 OC_OK x >>= k = k x
1229 OC_Forall >>= _ = OC_Forall
1230 OC_NonTyVar >>= _ = OC_NonTyVar
1231 OC_Occurs >>= _ = OC_Occurs
1232
1233 occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
1234 -- See Note [Occurs check expansion]
1235 -- Check whether
1236 -- a) the given variable occurs in the given type.
1237 -- b) there is a forall in the type (unless we have -XImpredicativeTypes
1238 -- or it's a ReturnTv
1239 -- c) if it's a SigTv, ty should be a tyvar
1240 --
1241 -- We may have needed to do some type synonym unfolding in order to
1242 -- get rid of the variable (or forall), so we also return the unfolded
1243 -- version of the type, which is guaranteed to be syntactically free
1244 -- of the given type variable. If the type is already syntactically
1245 -- free of the variable, then the same type is returned.
1246
1247 occurCheckExpand dflags tv ty
1248 | MetaTv { mtv_info = SigTv } <- details
1249 = go_sig_tv ty
1250 | fast_check ty = return ty
1251 | otherwise = go ty
1252 where
1253 details = ASSERT2( isTcTyVar tv, ppr tv ) tcTyVarDetails tv
1254
1255 impredicative = canUnifyWithPolyType dflags details (tyVarKind tv)
1256
1257 -- Check 'ty' is a tyvar, or can be expanded into one
1258 go_sig_tv ty@(TyVarTy {}) = OC_OK ty
1259 go_sig_tv ty | Just ty' <- tcView ty = go_sig_tv ty'
1260 go_sig_tv _ = OC_NonTyVar
1261
1262 -- True => fine
1263 fast_check (LitTy {}) = True
1264 fast_check (TyVarTy tv') = tv /= tv'
1265 fast_check (TyConApp tc tys) = all fast_check tys && (isTauTyCon tc || impredicative)
1266 fast_check (FunTy arg res) = fast_check arg && fast_check res
1267 fast_check (AppTy fun arg) = fast_check fun && fast_check arg
1268 fast_check (ForAllTy tv' ty) = impredicative
1269 && fast_check (tyVarKind tv')
1270 && (tv == tv' || fast_check ty)
1271
1272 go t@(TyVarTy tv') | tv == tv' = OC_Occurs
1273 | otherwise = return t
1274 go ty@(LitTy {}) = return ty
1275 go (AppTy ty1 ty2) = do { ty1' <- go ty1
1276 ; ty2' <- go ty2
1277 ; return (mkAppTy ty1' ty2') }
1278 go (FunTy ty1 ty2) = do { ty1' <- go ty1
1279 ; ty2' <- go ty2
1280 ; return (mkFunTy ty1' ty2') }
1281 go ty@(ForAllTy tv' body_ty)
1282 | not impredicative = OC_Forall
1283 | not (fast_check (tyVarKind tv')) = OC_Occurs
1284 -- Can't expand away the kinds unless we create
1285 -- fresh variables which we don't want to do at this point.
1286 -- In principle fast_check might fail because of a for-all
1287 -- but we don't yet have poly-kinded tyvars so I'm not
1288 -- going to worry about that now
1289 | tv == tv' = return ty
1290 | otherwise = do { body' <- go body_ty
1291 ; return (ForAllTy tv' body') }
1292
1293 -- For a type constructor application, first try expanding away the
1294 -- offending variable from the arguments. If that doesn't work, next
1295 -- see if the type constructor is a type synonym, and if so, expand
1296 -- it and try again.
1297 go ty@(TyConApp tc tys)
1298 = case do { tys <- mapM go tys; return (mkTyConApp tc tys) } of
1299 OC_OK ty
1300 | impredicative || isTauTyCon tc
1301 -> return ty -- First try to eliminate the tyvar from the args
1302 | otherwise
1303 -> OC_Forall -- A type synonym with a forall on the RHS
1304 bad | Just ty' <- tcView ty -> go ty'
1305 | otherwise -> bad
1306 -- Failing that, try to expand a synonym
1307
1308 canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> TcKind -> Bool
1309 canUnifyWithPolyType dflags details kind
1310 = case details of
1311 MetaTv { mtv_info = ReturnTv } -> True -- See Note [ReturnTv]
1312 MetaTv { mtv_info = SigTv } -> False
1313 MetaTv { mtv_info = TauTv } -> xopt Opt_ImpredicativeTypes dflags
1314 || isOpenTypeKind kind
1315 -- Note [OpenTypeKind accepts foralls]
1316 _other -> True
1317 -- We can have non-meta tyvars in given constraints
1318
1319 {-
1320 Note [OpenTypeKind accepts foralls]
1321 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1322 Here is a common paradigm:
1323 foo :: (forall a. a -> a) -> Int
1324 foo = error "urk"
1325 To make this work we need to instantiate 'error' with a polytype.
1326 A similar case is
1327 bar :: Bool -> (forall a. a->a) -> Int
1328 bar True = \x. (x 3)
1329 bar False = error "urk"
1330 Here we need to instantiate 'error' with a polytype.
1331
1332 But 'error' has an OpenTypeKind type variable, precisely so that
1333 we can instantiate it with Int#. So we also allow such type variables
1334 to be instantiated with foralls. It's a bit of a hack, but seems
1335 straightforward.
1336
1337 ************************************************************************
1338 * *
1339 \subsection{Predicate types}
1340 * *
1341 ************************************************************************
1342
1343 Deconstructors and tests on predicate types
1344
1345 Note [Kind polymorphic type classes]
1346 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1347 class C f where... -- C :: forall k. k -> Constraint
1348 g :: forall (f::*). C f => f -> f
1349
1350 Here the (C f) in the signature is really (C * f), and we
1351 don't want to complain that the * isn't a type variable!
1352 -}
1353
1354 isTyVarClassPred :: PredType -> Bool
1355 isTyVarClassPred ty = case getClassPredTys_maybe ty of
1356 Just (_, tys) -> all isTyVarTy tys
1357 _ -> False
1358
1359 -------------------------
1360 checkValidClsArgs :: Bool -> [KindOrType] -> Bool
1361 -- If the Bool is True (flexible contexts), return True (i.e. ok)
1362 -- Otherwise, check that the type (not kind) args are all headed by a tyvar
1363 -- E.g. (Eq a) accepted, (Eq (f a)) accepted, but (Eq Int) rejected
1364 -- This function is here rather than in TcValidity because it is
1365 -- called from TcSimplify, which itself is imported by TcValidity
1366 checkValidClsArgs flexible_contexts kts
1367 | flexible_contexts = True
1368 | otherwise = all hasTyVarHead tys
1369 where
1370 (_, tys) = span isKind kts -- see Note [Kind polymorphic type classes]
1371
1372 hasTyVarHead :: Type -> Bool
1373 -- Returns true of (a t1 .. tn), where 'a' is a type variable
1374 hasTyVarHead ty -- Haskell 98 allows predicates of form
1375 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1376 | otherwise -- where a is a type variable
1377 = case tcSplitAppTy_maybe ty of
1378 Just (ty, _) -> hasTyVarHead ty
1379 Nothing -> False
1380
1381 evVarPred_maybe :: EvVar -> Maybe PredType
1382 evVarPred_maybe v = if isPredTy ty then Just ty else Nothing
1383 where ty = varType v
1384
1385 evVarPred :: EvVar -> PredType
1386 evVarPred var
1387 | debugIsOn
1388 = case evVarPred_maybe var of
1389 Just pred -> pred
1390 Nothing -> pprPanic "tcEvVarPred" (ppr var <+> ppr (varType var))
1391 | otherwise
1392 = varType var
1393
1394 -- Superclasses
1395
1396 mkMinimalBySCs :: [PredType] -> [PredType]
1397 -- Remove predicates that can be deduced from others by superclasses
1398 mkMinimalBySCs ptys = [ ploc | ploc <- ptys
1399 , ploc `not_in_preds` rec_scs ]
1400 where
1401 rec_scs = concatMap trans_super_classes ptys
1402 not_in_preds p ps = not (any (eqPred p) ps)
1403
1404 trans_super_classes pred -- Superclasses of pred, excluding pred itself
1405 = case classifyPredType pred of
1406 ClassPred cls tys -> transSuperClasses cls tys
1407 _ -> []
1408
1409 transSuperClasses :: Class -> [Type] -> [PredType]
1410 transSuperClasses cls tys -- Superclasses of (cls tys),
1411 -- excluding (cls tys) itself
1412 = concatMap transSuperClassesPred (immSuperClasses cls tys)
1413
1414 transSuperClassesPred :: PredType -> [PredType]
1415 -- (transSuperClassesPred p) returns (p : p's superclasses)
1416 transSuperClassesPred p
1417 = case classifyPredType p of
1418 ClassPred cls tys -> p : transSuperClasses cls tys
1419 _ -> [p]
1420
1421 immSuperClasses :: Class -> [Type] -> [PredType]
1422 immSuperClasses cls tys
1423 = substTheta (zipTopTvSubst tyvars tys) sc_theta
1424 where
1425 (tyvars,sc_theta,_,_) = classBigSig cls
1426
1427 isImprovementPred :: PredType -> Bool
1428 -- Either it's an equality, or has some functional dependency
1429 isImprovementPred ty
1430 = case classifyPredType ty of
1431 EqPred NomEq t1 t2 -> not (t1 `tcEqType` t2)
1432 EqPred ReprEq _ _ -> False
1433 ClassPred cls _ -> classHasFds cls
1434 IrredPred {} -> True -- Might have equalities after reduction?
1435
1436 {-
1437 ************************************************************************
1438 * *
1439 \subsection{Predicates}
1440 * *
1441 ************************************************************************
1442 -}
1443
1444 isSigmaTy :: TcType -> Bool
1445 -- isSigmaTy returns true of any qualified type. It doesn't
1446 -- *necessarily* have any foralls. E.g
1447 -- f :: (?x::Int) => Int -> Int
1448 isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
1449 isSigmaTy (ForAllTy _ _) = True
1450 isSigmaTy (FunTy a _) = isPredTy a
1451 isSigmaTy _ = False
1452
1453 isRhoTy :: TcType -> Bool -- True of TcRhoTypes; see Note [TcRhoType]
1454 isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty'
1455 isRhoTy (ForAllTy {}) = False
1456 isRhoTy (FunTy a r) = not (isPredTy a) && isRhoTy r
1457 isRhoTy _ = True
1458
1459 isOverloadedTy :: Type -> Bool
1460 -- Yes for a type of a function that might require evidence-passing
1461 -- Used only by bindLocalMethods
1462 isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
1463 isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty
1464 isOverloadedTy (FunTy a _) = isPredTy a
1465 isOverloadedTy _ = False
1466
1467 isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
1468 isUnitTy, isCharTy, isAnyTy :: Type -> Bool
1469 isFloatTy = is_tc floatTyConKey
1470 isDoubleTy = is_tc doubleTyConKey
1471 isIntegerTy = is_tc integerTyConKey
1472 isIntTy = is_tc intTyConKey
1473 isWordTy = is_tc wordTyConKey
1474 isBoolTy = is_tc boolTyConKey
1475 isUnitTy = is_tc unitTyConKey
1476 isCharTy = is_tc charTyConKey
1477 isAnyTy = is_tc anyTyConKey
1478
1479 -- | Does a type represent a floating-point number?
1480 isFloatingTy :: Type -> Bool
1481 isFloatingTy ty = isFloatTy ty || isDoubleTy ty
1482
1483 -- | Is a type 'String'?
1484 isStringTy :: Type -> Bool
1485 isStringTy ty
1486 = case tcSplitTyConApp_maybe ty of
1487 Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty
1488 _ -> False
1489
1490 is_tc :: Unique -> Type -> Bool
1491 -- Newtypes are opaque to this
1492 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
1493 Just (tc, _) -> uniq == getUnique tc
1494 Nothing -> False
1495
1496 -- | Does the given tyvar appear in the given type outside of any
1497 -- non-newtypes? Assume we're looking for @a@. Says "yes" for
1498 -- @a@, @N a@, @b a@, @a b@, @b (N a)@. Says "no" for
1499 -- @[a]@, @Maybe a@, @T a@, where @N@ is a newtype and @T@ is a datatype.
1500 isTyVarExposed :: TcTyVar -> TcType -> Bool
1501 isTyVarExposed tv (TyVarTy tv') = tv == tv'
1502 isTyVarExposed tv (TyConApp tc tys)
1503 | isNewTyCon tc = any (isTyVarExposed tv) tys
1504 | otherwise = False
1505 isTyVarExposed _ (LitTy {}) = False
1506 isTyVarExposed _ (FunTy {}) = False
1507 isTyVarExposed tv (AppTy fun arg) = isTyVarExposed tv fun
1508 || isTyVarExposed tv arg
1509 isTyVarExposed _ (ForAllTy {}) = False
1510
1511 -- | Does the given tyvar appear under a type generative w.r.t.
1512 -- representational equality? See Note [Occurs check error] in
1513 -- TcCanonical for the motivation for this function.
1514 isTyVarUnderDatatype :: TcTyVar -> TcType -> Bool
1515 isTyVarUnderDatatype tv = go False
1516 where
1517 go under_dt ty | Just ty' <- tcView ty = go under_dt ty'
1518 go under_dt (TyVarTy tv') = under_dt && (tv == tv')
1519 go under_dt (TyConApp tc tys) = let under_dt' = under_dt ||
1520 isGenerativeTyCon tc
1521 Representational
1522 in any (go under_dt') tys
1523 go _ (LitTy {}) = False
1524 go _ (FunTy arg res) = go True arg || go True res
1525 go under_dt (AppTy fun arg) = go under_dt fun || go under_dt arg
1526 go under_dt (ForAllTy tv' inner_ty)
1527 | tv' == tv = False
1528 | otherwise = go under_dt inner_ty
1529
1530 isRigidTy :: TcType -> Bool
1531 isRigidTy ty
1532 | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
1533 | Just {} <- tcSplitAppTy_maybe ty = True
1534 | isForAllTy ty = True
1535 | otherwise = False
1536
1537 isRigidEqPred :: TcLevel -> PredTree -> Bool
1538 -- ^ True of all Nominal equalities that are solidly insoluble
1539 -- This means all equalities *except*
1540 -- * Meta-tv non-SigTv on LHS
1541 -- * Meta-tv SigTv on LHS, tyvar on right
1542 isRigidEqPred tc_lvl (EqPred NomEq ty1 _)
1543 | Just tv1 <- tcGetTyVar_maybe ty1
1544 = ASSERT2( isTcTyVar tv1, ppr tv1 )
1545 not (isMetaTyVar tv1) || isTouchableMetaTyVar tc_lvl tv1
1546
1547 | otherwise -- LHS is not a tyvar
1548 = True
1549
1550 isRigidEqPred _ _ = False -- Not an equality
1551
1552 {-
1553 ************************************************************************
1554 * *
1555 \subsection{Transformation of Types to TcTypes}
1556 * *
1557 ************************************************************************
1558 -}
1559
1560 toTcType :: Type -> TcType
1561 toTcType ty = to_tc_type emptyVarSet ty
1562 where
1563 to_tc_type :: VarSet -> Type -> TcType
1564 -- The constraint solver expects EvVars to have TcType, in which the
1565 -- free type variables are TcTyVars. So we convert from Type to TcType here
1566 -- A bit tiresome; but one day I expect the two types to be entirely separate
1567 -- in which case we'll definitely need to do this
1568 to_tc_type forall_tvs (TyVarTy tv)
1569 | Just var <- lookupVarSet forall_tvs tv = TyVarTy var
1570 | otherwise = TyVarTy (toTcTyVar tv)
1571 to_tc_type ftvs (FunTy t1 t2) = FunTy (to_tc_type ftvs t1) (to_tc_type ftvs t2)
1572 to_tc_type ftvs (AppTy t1 t2) = AppTy (to_tc_type ftvs t1) (to_tc_type ftvs t2)
1573 to_tc_type ftvs (TyConApp tc tys) = TyConApp tc (map (to_tc_type ftvs) tys)
1574 to_tc_type ftvs (ForAllTy tv ty) = let tv' = toTcTyVar tv
1575 in ForAllTy tv' (to_tc_type (ftvs `extendVarSet` tv') ty)
1576 to_tc_type _ftvs (LitTy l) = LitTy l
1577
1578 toTcTyVar :: TyVar -> TcTyVar
1579 toTcTyVar tv
1580 | isTcTyVar tv = setVarType tv (toTcType (tyVarKind tv))
1581 | isId tv = pprPanic "toTcTyVar: Id:" (ppr tv)
1582 | otherwise = mkTcTyVar (tyVarName tv) (toTcType (tyVarKind tv)) vanillaSkolemTv
1583
1584 toTcTypeBag :: Bag EvVar -> Bag EvVar -- All TyVars are transformed to TcTyVars
1585 toTcTypeBag evvars = mapBag (\tv -> setTyVarKind tv (toTcType (tyVarKind tv))) evvars
1586
1587 {-
1588 ************************************************************************
1589 * *
1590 \subsection{Misc}
1591 * *
1592 ************************************************************************
1593 -}
1594
1595 deNoteType :: Type -> Type
1596 -- Remove all *outermost* type synonyms and other notes
1597 deNoteType ty | Just ty' <- tcView ty = deNoteType ty'
1598 deNoteType ty = ty
1599
1600 tcTyVarsOfType :: Type -> TcTyVarSet
1601 -- Just the *TcTyVars* free in the type
1602 -- (Types.tyVarsOfTypes finds all free TyVars)
1603 tcTyVarsOfType (TyVarTy tv) = if isTcTyVar tv then unitVarSet tv
1604 else emptyVarSet
1605 tcTyVarsOfType (TyConApp _ tys) = tcTyVarsOfTypes tys
1606 tcTyVarsOfType (LitTy {}) = emptyVarSet
1607 tcTyVarsOfType (FunTy arg res) = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
1608 tcTyVarsOfType (AppTy fun arg) = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
1609 tcTyVarsOfType (ForAllTy tyvar ty) = tcTyVarsOfType ty `delVarSet` tyvar
1610 -- We do sometimes quantify over skolem TcTyVars
1611
1612 tcTyVarsOfTypes :: [Type] -> TyVarSet
1613 tcTyVarsOfTypes = mapUnionVarSet tcTyVarsOfType
1614
1615 {-
1616 Find the free tycons and classes of a type. This is used in the front
1617 end of the compiler.
1618 -}
1619
1620 orphNamesOfTyCon :: TyCon -> NameSet
1621 orphNamesOfTyCon tycon = unitNameSet (getName tycon) `unionNameSet` case tyConClass_maybe tycon of
1622 Nothing -> emptyNameSet
1623 Just cls -> unitNameSet (getName cls)
1624
1625 orphNamesOfType :: Type -> NameSet
1626 orphNamesOfType ty | Just ty' <- tcView ty = orphNamesOfType ty'
1627 -- Look through type synonyms (Trac #4912)
1628 orphNamesOfType (TyVarTy _) = emptyNameSet
1629 orphNamesOfType (LitTy {}) = emptyNameSet
1630 orphNamesOfType (TyConApp tycon tys) = orphNamesOfTyCon tycon
1631 `unionNameSet` orphNamesOfTypes tys
1632 orphNamesOfType (FunTy arg res) = orphNamesOfTyCon funTyCon -- NB! See Trac #8535
1633 `unionNameSet` orphNamesOfType arg
1634 `unionNameSet` orphNamesOfType res
1635 orphNamesOfType (AppTy fun arg) = orphNamesOfType fun `unionNameSet` orphNamesOfType arg
1636 orphNamesOfType (ForAllTy _ ty) = orphNamesOfType ty
1637
1638 orphNamesOfThings :: (a -> NameSet) -> [a] -> NameSet
1639 orphNamesOfThings f = foldr (unionNameSet . f) emptyNameSet
1640
1641 orphNamesOfTypes :: [Type] -> NameSet
1642 orphNamesOfTypes = orphNamesOfThings orphNamesOfType
1643
1644 orphNamesOfDFunHead :: Type -> NameSet
1645 -- Find the free type constructors and classes
1646 -- of the head of the dfun instance type
1647 -- The 'dfun_head_type' is because of
1648 -- instance Foo a => Baz T where ...
1649 -- The decl is an orphan if Baz and T are both not locally defined,
1650 -- even if Foo *is* locally defined
1651 orphNamesOfDFunHead dfun_ty
1652 = case tcSplitSigmaTy dfun_ty of
1653 (_, _, head_ty) -> orphNamesOfType head_ty
1654
1655 orphNamesOfCo :: Coercion -> NameSet
1656 orphNamesOfCo (Refl _ ty) = orphNamesOfType ty
1657 orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos
1658 orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
1659 orphNamesOfCo (ForAllCo _ co) = orphNamesOfCo co
1660 orphNamesOfCo (CoVarCo _) = emptyNameSet
1661 orphNamesOfCo (AxiomInstCo con _ cos) = orphNamesOfCoCon con `unionNameSet` orphNamesOfCos cos
1662 orphNamesOfCo (UnivCo _ _ ty1 ty2) = orphNamesOfType ty1 `unionNameSet` orphNamesOfType ty2
1663 orphNamesOfCo (SymCo co) = orphNamesOfCo co
1664 orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
1665 orphNamesOfCo (NthCo _ co) = orphNamesOfCo co
1666 orphNamesOfCo (LRCo _ co) = orphNamesOfCo co
1667 orphNamesOfCo (InstCo co ty) = orphNamesOfCo co `unionNameSet` orphNamesOfType ty
1668 orphNamesOfCo (SubCo co) = orphNamesOfCo co
1669 orphNamesOfCo (AxiomRuleCo _ ts cs) = orphNamesOfTypes ts `unionNameSet`
1670 orphNamesOfCos cs
1671
1672 orphNamesOfCos :: [Coercion] -> NameSet
1673 orphNamesOfCos = orphNamesOfThings orphNamesOfCo
1674
1675 orphNamesOfCoCon :: CoAxiom br -> NameSet
1676 orphNamesOfCoCon (CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
1677 = orphNamesOfTyCon tc `unionNameSet` orphNamesOfCoAxBranches branches
1678
1679 orphNamesOfCoAxBranches :: Branches br -> NameSet
1680 orphNamesOfCoAxBranches
1681 = foldr (unionNameSet . orphNamesOfCoAxBranch) emptyNameSet . fromBranches
1682
1683 orphNamesOfCoAxBranch :: CoAxBranch -> NameSet
1684 orphNamesOfCoAxBranch (CoAxBranch { cab_lhs = lhs, cab_rhs = rhs })
1685 = orphNamesOfTypes lhs `unionNameSet` orphNamesOfType rhs
1686
1687 {-
1688 ************************************************************************
1689 * *
1690 \subsection[TysWiredIn-ext-type]{External types}
1691 * *
1692 ************************************************************************
1693
1694 The compiler's foreign function interface supports the passing of a
1695 restricted set of types as arguments and results (the restricting factor
1696 being the )
1697 -}
1698
1699 tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type)
1700 -- (tcSplitIOType_maybe t) returns Just (IO,t',co)
1701 -- if co : t ~ IO t'
1702 -- returns Nothing otherwise
1703 tcSplitIOType_maybe ty
1704 = case tcSplitTyConApp_maybe ty of
1705 Just (io_tycon, [io_res_ty])
1706 | io_tycon `hasKey` ioTyConKey ->
1707 Just (io_tycon, io_res_ty)
1708 _ ->
1709 Nothing
1710
1711 isFFITy :: Type -> Bool
1712 -- True for any TyCon that can possibly be an arg or result of an FFI call
1713 isFFITy ty = isValid (checkRepTyCon legalFFITyCon ty)
1714
1715 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Validity
1716 -- Checks for valid argument type for a 'foreign import'
1717 isFFIArgumentTy dflags safety ty
1718 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
1719
1720 isFFIExternalTy :: Type -> Validity
1721 -- Types that are allowed as arguments of a 'foreign export'
1722 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
1723
1724 isFFIImportResultTy :: DynFlags -> Type -> Validity
1725 isFFIImportResultTy dflags ty
1726 = checkRepTyCon (legalFIResultTyCon dflags) ty
1727
1728 isFFIExportResultTy :: Type -> Validity
1729 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
1730
1731 isFFIDynTy :: Type -> Type -> Validity
1732 -- The type in a foreign import dynamic must be Ptr, FunPtr, or a newtype of
1733 -- either, and the wrapped function type must be equal to the given type.
1734 -- We assume that all types have been run through normaliseFfiType, so we don't
1735 -- need to worry about expanding newtypes here.
1736 isFFIDynTy expected ty
1737 -- Note [Foreign import dynamic]
1738 -- In the example below, expected would be 'CInt -> IO ()', while ty would
1739 -- be 'FunPtr (CDouble -> IO ())'.
1740 | Just (tc, [ty']) <- splitTyConApp_maybe ty
1741 , tyConUnique tc `elem` [ptrTyConKey, funPtrTyConKey]
1742 , eqType ty' expected
1743 = IsValid
1744 | otherwise
1745 = NotValid (vcat [ ptext (sLit "Expected: Ptr/FunPtr") <+> pprParendType expected <> comma
1746 , ptext (sLit " Actual:") <+> ppr ty ])
1747
1748 isFFILabelTy :: Type -> Validity
1749 -- The type of a foreign label must be Ptr, FunPtr, or a newtype of either.
1750 isFFILabelTy ty = checkRepTyCon ok ty
1751 where
1752 ok tc | tc `hasKey` funPtrTyConKey || tc `hasKey` ptrTyConKey
1753 = IsValid
1754 | otherwise
1755 = NotValid (ptext (sLit "A foreign-imported address (via &foo) must have type (Ptr a) or (FunPtr a)"))
1756
1757 isFFIPrimArgumentTy :: DynFlags -> Type -> Validity
1758 -- Checks for valid argument type for a 'foreign import prim'
1759 -- Currently they must all be simple unlifted types, or the well-known type
1760 -- Any, which can be used to pass the address to a Haskell object on the heap to
1761 -- the foreign function.
1762 isFFIPrimArgumentTy dflags ty
1763 | isAnyTy ty = IsValid
1764 | otherwise = checkRepTyCon (legalFIPrimArgTyCon dflags) ty
1765
1766 isFFIPrimResultTy :: DynFlags -> Type -> Validity
1767 -- Checks for valid result type for a 'foreign import prim'
1768 -- Currently it must be an unlifted type, including unboxed tuples,
1769 -- or the well-known type Any.
1770 isFFIPrimResultTy dflags ty
1771 | isAnyTy ty = IsValid
1772 | otherwise = checkRepTyCon (legalFIPrimResultTyCon dflags) ty
1773
1774 isFunPtrTy :: Type -> Bool
1775 isFunPtrTy ty
1776 | Just (tc, [_]) <- splitTyConApp_maybe ty
1777 = tc `hasKey` funPtrTyConKey
1778 | otherwise
1779 = False
1780
1781 -- normaliseFfiType gets run before checkRepTyCon, so we don't
1782 -- need to worry about looking through newtypes or type functions
1783 -- here; that's already been taken care of.
1784 checkRepTyCon :: (TyCon -> Validity) -> Type -> Validity
1785 checkRepTyCon check_tc ty
1786 = case splitTyConApp_maybe ty of
1787 Just (tc, tys)
1788 | isNewTyCon tc -> NotValid (hang msg 2 (mk_nt_reason tc tys $$ nt_fix))
1789 | otherwise -> case check_tc tc of
1790 IsValid -> IsValid
1791 NotValid extra -> NotValid (msg $$ extra)
1792 Nothing -> NotValid (quotes (ppr ty) <+> ptext (sLit "is not a data type"))
1793 where
1794 msg = quotes (ppr ty) <+> ptext (sLit "cannot be marshalled in a foreign call")
1795 mk_nt_reason tc tys
1796 | null tys = ptext (sLit "because its data constructor is not in scope")
1797 | otherwise = ptext (sLit "because the data constructor for")
1798 <+> quotes (ppr tc) <+> ptext (sLit "is not in scope")
1799 nt_fix = ptext (sLit "Possible fix: import the data constructor to bring it into scope")
1800
1801 {-
1802 Note [Foreign import dynamic]
1803 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1804 A dynamic stub must be of the form 'FunPtr ft -> ft' where ft is any foreign
1805 type. Similarly, a wrapper stub must be of the form 'ft -> IO (FunPtr ft)'.
1806
1807 We use isFFIDynTy to check whether a signature is well-formed. For example,
1808 given a (illegal) declaration like:
1809
1810 foreign import ccall "dynamic"
1811 foo :: FunPtr (CDouble -> IO ()) -> CInt -> IO ()
1812
1813 isFFIDynTy will compare the 'FunPtr' type 'CDouble -> IO ()' with the curried
1814 result type 'CInt -> IO ()', and return False, as they are not equal.
1815
1816
1817 ----------------------------------------------
1818 These chaps do the work; they are not exported
1819 ----------------------------------------------
1820 -}
1821
1822 legalFEArgTyCon :: TyCon -> Validity
1823 legalFEArgTyCon tc
1824 -- It's illegal to make foreign exports that take unboxed
1825 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
1826 = boxedMarshalableTyCon tc
1827
1828 legalFIResultTyCon :: DynFlags -> TyCon -> Validity
1829 legalFIResultTyCon dflags tc
1830 | tc == unitTyCon = IsValid
1831 | otherwise = marshalableTyCon dflags tc
1832
1833 legalFEResultTyCon :: TyCon -> Validity
1834 legalFEResultTyCon tc
1835 | tc == unitTyCon = IsValid
1836 | otherwise = boxedMarshalableTyCon tc
1837
1838 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Validity
1839 -- Checks validity of types going from Haskell -> external world
1840 legalOutgoingTyCon dflags _ tc
1841 = marshalableTyCon dflags tc
1842
1843 legalFFITyCon :: TyCon -> Validity
1844 -- True for any TyCon that can possibly be an arg or result of an FFI call
1845 legalFFITyCon tc
1846 | isUnLiftedTyCon tc = IsValid
1847 | tc == unitTyCon = IsValid
1848 | otherwise = boxedMarshalableTyCon tc
1849
1850 marshalableTyCon :: DynFlags -> TyCon -> Validity
1851 marshalableTyCon dflags tc
1852 | isUnLiftedTyCon tc
1853 , not (isUnboxedTupleTyCon tc)
1854 , case tyConPrimRep tc of -- Note [Marshalling VoidRep]
1855 VoidRep -> False
1856 _ -> True
1857 = validIfUnliftedFFITypes dflags
1858 | otherwise
1859 = boxedMarshalableTyCon tc
1860
1861 boxedMarshalableTyCon :: TyCon -> Validity
1862 boxedMarshalableTyCon tc
1863 | getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
1864 , int32TyConKey, int64TyConKey
1865 , wordTyConKey, word8TyConKey, word16TyConKey
1866 , word32TyConKey, word64TyConKey
1867 , floatTyConKey, doubleTyConKey
1868 , ptrTyConKey, funPtrTyConKey
1869 , charTyConKey
1870 , stablePtrTyConKey
1871 , boolTyConKey
1872 ]
1873 = IsValid
1874
1875 | otherwise = NotValid empty
1876
1877 legalFIPrimArgTyCon :: DynFlags -> TyCon -> Validity
1878 -- Check args of 'foreign import prim', only allow simple unlifted types.
1879 -- Strictly speaking it is unnecessary to ban unboxed tuples here since
1880 -- currently they're of the wrong kind to use in function args anyway.
1881 legalFIPrimArgTyCon dflags tc
1882 | isUnLiftedTyCon tc
1883 , not (isUnboxedTupleTyCon tc)
1884 = validIfUnliftedFFITypes dflags
1885 | otherwise
1886 = NotValid unlifted_only
1887
1888 legalFIPrimResultTyCon :: DynFlags -> TyCon -> Validity
1889 -- Check result type of 'foreign import prim'. Allow simple unlifted
1890 -- types and also unboxed tuple result types '... -> (# , , #)'
1891 legalFIPrimResultTyCon dflags tc
1892 | isUnLiftedTyCon tc
1893 , (isUnboxedTupleTyCon tc
1894 || case tyConPrimRep tc of -- Note [Marshalling VoidRep]
1895 VoidRep -> False
1896 _ -> True)
1897 = validIfUnliftedFFITypes dflags
1898
1899 | otherwise
1900 = NotValid unlifted_only
1901
1902 unlifted_only :: MsgDoc
1903 unlifted_only = ptext (sLit "foreign import prim only accepts simple unlifted types")
1904
1905 validIfUnliftedFFITypes :: DynFlags -> Validity
1906 validIfUnliftedFFITypes dflags
1907 | xopt Opt_UnliftedFFITypes dflags = IsValid
1908 | otherwise = NotValid (ptext (sLit "To marshal unlifted types, use UnliftedFFITypes"))
1909
1910 {-
1911 Note [Marshalling VoidRep]
1912 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1913 We don't treat State# (whose PrimRep is VoidRep) as marshalable.
1914 In turn that means you can't write
1915 foreign import foo :: Int -> State# RealWorld
1916
1917 Reason: the back end falls over with panic "primRepHint:VoidRep";
1918 and there is no compelling reason to permit it
1919 -}
1920
1921 {-
1922 ************************************************************************
1923 * *
1924 The "Paterson size" of a type
1925 * *
1926 ************************************************************************
1927 -}
1928
1929 {-
1930 Note [Paterson conditions on PredTypes]
1931 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1932 We are considering whether *class* constraints terminate
1933 (see Note [Paterson conditions]). Precisely, the Paterson conditions
1934 would have us check that "the constraint has fewer constructors and variables
1935 (taken together and counting repetitions) than the head.".
1936
1937 However, we can be a bit more refined by looking at which kind of constraint
1938 this actually is. There are two main tricks:
1939
1940 1. It seems like it should be OK not to count the tuple type constructor
1941 for a PredType like (Show a, Eq a) :: Constraint, since we don't
1942 count the "implicit" tuple in the ThetaType itself.
1943
1944 In fact, the Paterson test just checks *each component* of the top level
1945 ThetaType against the size bound, one at a time. By analogy, it should be
1946 OK to return the size of the *largest* tuple component as the size of the
1947 whole tuple.
1948
1949 2. Once we get into an implicit parameter or equality we
1950 can't get back to a class constraint, so it's safe
1951 to say "size 0". See Trac #4200.
1952
1953 NB: we don't want to detect PredTypes in sizeType (and then call
1954 sizePred on them), or we might get an infinite loop if that PredType
1955 is irreducible. See Trac #5581.
1956 -}
1957
1958 type TypeSize = IntWithInf
1959
1960 sizeType, size_type :: Type -> TypeSize
1961 -- Size of a type: the number of variables and constructors
1962 -- Ignore kinds altogether
1963 sizeType ty | isKind ty = 0
1964 | otherwise = size_type ty
1965
1966 size_type ty | Just exp_ty <- tcView ty = size_type exp_ty
1967 size_type (TyVarTy {}) = 1
1968 size_type (TyConApp tc tys)
1969 | isTypeFamilyTyCon tc = infinity -- Type-family applications can
1970 -- expand to any arbitrary size
1971 | otherwise = sizeTypes tys + 1
1972 size_type (LitTy {}) = 1
1973 size_type (FunTy arg res) = size_type arg + size_type res + 1
1974 size_type (AppTy fun arg) = size_type fun + size_type arg
1975 size_type (ForAllTy _ ty) = size_type ty
1976
1977 sizeTypes :: [Type] -> TypeSize
1978 sizeTypes tys = sum (map sizeType tys)