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