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