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