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