compiler: de-lhs typecheck/
[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,
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,
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,
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 "tau")
526 TauTv False -> ptext (sLit "twc")
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 -- @isTauTy@ tests for nested for-alls. It should not be called on a boxy type.
838
839 isTauTy :: Type -> Bool
840 isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
841 isTauTy (TyVarTy _) = True
842 isTauTy (LitTy {}) = True
843 isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
844 isTauTy (AppTy a b) = isTauTy a && isTauTy b
845 isTauTy (FunTy a b) = isTauTy a && isTauTy b
846 isTauTy (ForAllTy {}) = False
847
848 isTauTyCon :: TyCon -> Bool
849 -- Returns False for type synonyms whose expansion is a polytype
850 isTauTyCon tc
851 | Just (_, rhs) <- synTyConDefn_maybe tc = isTauTy rhs
852 | otherwise = True
853
854 ---------------
855 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
856 -- construct a dictionary function name
857 getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
858 getDFunTyKey (TyVarTy tv) = getOccName tv
859 getDFunTyKey (TyConApp tc _) = getOccName tc
860 getDFunTyKey (LitTy x) = getDFunTyLitKey x
861 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
862 getDFunTyKey (FunTy _ _) = getOccName funTyCon
863 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
864
865 getDFunTyLitKey :: TyLit -> OccName
866 getDFunTyLitKey (NumTyLit n) = mkOccName Name.varName (show n)
867 getDFunTyLitKey (StrTyLit n) = mkOccName Name.varName (show n) -- hm
868
869 {-
870 ************************************************************************
871 * *
872 \subsection{Expanding and splitting}
873 * *
874 ************************************************************************
875
876 These tcSplit functions are like their non-Tc analogues, but
877 *) they do not look through newtypes
878
879 However, they are non-monadic and do not follow through mutable type
880 variables. It's up to you to make sure this doesn't matter.
881 -}
882
883 tcSplitForAllTys :: Type -> ([TyVar], Type)
884 tcSplitForAllTys ty = split ty ty []
885 where
886 split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
887 split _ (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
888 split orig_ty _ tvs = (reverse tvs, orig_ty)
889
890 tcIsForAllTy :: Type -> Bool
891 tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
892 tcIsForAllTy (ForAllTy {}) = True
893 tcIsForAllTy _ = False
894
895 tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
896 -- Split off the first predicate argument from a type
897 tcSplitPredFunTy_maybe ty
898 | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
899 tcSplitPredFunTy_maybe (FunTy arg res)
900 | isPredTy arg = Just (arg, res)
901 tcSplitPredFunTy_maybe _
902 = Nothing
903
904 tcSplitPhiTy :: Type -> (ThetaType, Type)
905 tcSplitPhiTy ty
906 = split ty []
907 where
908 split ty ts
909 = case tcSplitPredFunTy_maybe ty of
910 Just (pred, ty) -> split ty (pred:ts)
911 Nothing -> (reverse ts, ty)
912
913 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
914 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
915 (tvs, rho) -> case tcSplitPhiTy rho of
916 (theta, tau) -> (tvs, theta, tau)
917
918 -----------------------
919 tcDeepSplitSigmaTy_maybe
920 :: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType)
921 -- Looks for a *non-trivial* quantified type, under zero or more function arrows
922 -- By "non-trivial" we mean either tyvars or constraints are non-empty
923
924 tcDeepSplitSigmaTy_maybe ty
925 | Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty
926 , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty
927 = Just (arg_ty:arg_tys, tvs, theta, rho)
928
929 | (tvs, theta, rho) <- tcSplitSigmaTy ty
930 , not (null tvs && null theta)
931 = Just ([], tvs, theta, rho)
932
933 | otherwise = Nothing
934
935 -----------------------
936 tcTyConAppTyCon :: Type -> TyCon
937 tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
938 Just (tc, _) -> tc
939 Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
940
941 tcTyConAppArgs :: Type -> [Type]
942 tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
943 Just (_, args) -> args
944 Nothing -> pprPanic "tcTyConAppArgs" (pprType ty)
945
946 tcSplitTyConApp :: Type -> (TyCon, [Type])
947 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
948 Just stuff -> stuff
949 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
950
951 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
952 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
953 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
954 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
955 -- Newtypes are opaque, so they may be split
956 -- However, predicates are not treated
957 -- as tycon applications by the type checker
958 tcSplitTyConApp_maybe _ = Nothing
959
960 -----------------------
961 tcSplitFunTys :: Type -> ([Type], Type)
962 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
963 Nothing -> ([], ty)
964 Just (arg,res) -> (arg:args, res')
965 where
966 (args,res') = tcSplitFunTys res
967
968 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
969 tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
970 tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
971 tcSplitFunTy_maybe _ = Nothing
972 -- Note the typeKind guard
973 -- Consider (?x::Int) => Bool
974 -- We don't want to treat this as a function type!
975 -- A concrete example is test tc230:
976 -- f :: () -> (?p :: ()) => () -> ()
977 --
978 -- g = f () ()
979
980 tcSplitFunTysN
981 :: TcRhoType
982 -> Arity -- N: Number of desired args
983 -> ([TcSigmaType], -- Arg types (N or fewer)
984 TcSigmaType) -- The rest of the type
985
986 tcSplitFunTysN ty n_args
987 | n_args == 0
988 = ([], ty)
989 | Just (arg,res) <- tcSplitFunTy_maybe ty
990 = case tcSplitFunTysN res (n_args - 1) of
991 (args, res) -> (arg:args, res)
992 | otherwise
993 = ([], ty)
994
995 tcSplitFunTy :: Type -> (Type, Type)
996 tcSplitFunTy ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
997
998 tcFunArgTy :: Type -> Type
999 tcFunArgTy ty = fst (tcSplitFunTy ty)
1000
1001 tcFunResultTy :: Type -> Type
1002 tcFunResultTy ty = snd (tcSplitFunTy ty)
1003
1004 -----------------------
1005 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
1006 tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
1007 tcSplitAppTy_maybe ty = repSplitAppTy_maybe ty
1008
1009 tcSplitAppTy :: Type -> (Type, Type)
1010 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
1011 Just stuff -> stuff
1012 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
1013
1014 tcSplitAppTys :: Type -> (Type, [Type])
1015 tcSplitAppTys ty
1016 = go ty []
1017 where
1018 go ty args = case tcSplitAppTy_maybe ty of
1019 Just (ty', arg) -> go ty' (arg:args)
1020 Nothing -> (ty,args)
1021
1022 -----------------------
1023 tcGetTyVar_maybe :: Type -> Maybe TyVar
1024 tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
1025 tcGetTyVar_maybe (TyVarTy tv) = Just tv
1026 tcGetTyVar_maybe _ = Nothing
1027
1028 tcGetTyVar :: String -> Type -> TyVar
1029 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
1030
1031 tcIsTyVarTy :: Type -> Bool
1032 tcIsTyVarTy ty = isJust (tcGetTyVar_maybe ty)
1033
1034 -----------------------
1035 tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
1036 -- Split the type of a dictionary function
1037 -- We don't use tcSplitSigmaTy, because a DFun may (with NDP)
1038 -- have non-Pred arguments, such as
1039 -- df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
1040 --
1041 -- Also NB splitFunTys, not tcSplitFunTys;
1042 -- the latter specifically stops at PredTy arguments,
1043 -- and we don't want to do that here
1044 tcSplitDFunTy ty
1045 = case tcSplitForAllTys ty of { (tvs, rho) ->
1046 case splitFunTys rho of { (theta, tau) ->
1047 case tcSplitDFunHead tau of { (clas, tys) ->
1048 (tvs, theta, clas, tys) }}}
1049
1050 tcSplitDFunHead :: Type -> (Class, [Type])
1051 tcSplitDFunHead = getClassPredTys
1052
1053 tcInstHeadTyNotSynonym :: Type -> Bool
1054 -- Used in Haskell-98 mode, for the argument types of an instance head
1055 -- These must not be type synonyms, but everywhere else type synonyms
1056 -- are transparent, so we need a special function here
1057 tcInstHeadTyNotSynonym ty
1058 = case ty of
1059 TyConApp tc _ -> not (isTypeSynonymTyCon tc)
1060 _ -> True
1061
1062 tcInstHeadTyAppAllTyVars :: Type -> Bool
1063 -- Used in Haskell-98 mode, for the argument types of an instance head
1064 -- These must be a constructor applied to type variable arguments.
1065 -- But we allow kind instantiations.
1066 tcInstHeadTyAppAllTyVars ty
1067 | Just ty' <- tcView ty -- Look through synonyms
1068 = tcInstHeadTyAppAllTyVars ty'
1069 | otherwise
1070 = case ty of
1071 TyConApp _ tys -> ok (filter (not . isKind) tys) -- avoid kinds
1072 FunTy arg res -> ok [arg, res]
1073 _ -> False
1074 where
1075 -- Check that all the types are type variables,
1076 -- and that each is distinct
1077 ok tys = equalLength tvs tys && hasNoDups tvs
1078 where
1079 tvs = mapMaybe get_tv tys
1080
1081 get_tv (TyVarTy tv) = Just tv -- through synonyms
1082 get_tv _ = Nothing
1083
1084 tcEqKind :: TcKind -> TcKind -> Bool
1085 tcEqKind = tcEqType
1086
1087 tcEqType :: TcType -> TcType -> Bool
1088 -- tcEqType is a proper, sensible type-equality function, that does
1089 -- just what you'd expect The function Type.eqType (currently) has a
1090 -- grotesque hack that makes OpenKind = *, and that is NOT what we
1091 -- want in the type checker! Otherwise, for example, TcCanonical.reOrient
1092 -- thinks the LHS and RHS have the same kinds, when they don't, and
1093 -- fails to re-orient. That in turn caused Trac #8553.
1094
1095 tcEqType ty1 ty2
1096 = go init_env ty1 ty2
1097 where
1098 init_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
1099 go env t1 t2 | Just t1' <- tcView t1 = go env t1' t2
1100 | Just t2' <- tcView t2 = go env t1 t2'
1101 go env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2
1102 go _ (LitTy lit1) (LitTy lit2) = lit1 == lit2
1103 go env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = go env (tyVarKind tv1) (tyVarKind tv2)
1104 && go (rnBndr2 env tv1 tv2) t1 t2
1105 go env (AppTy s1 t1) (AppTy s2 t2) = go env s1 s2 && go env t1 t2
1106 go env (FunTy s1 t1) (FunTy s2 t2) = go env s1 s2 && go env t1 t2
1107 go env (TyConApp tc1 ts1) (TyConApp tc2 ts2) = (tc1 == tc2) && gos env ts1 ts2
1108 go _ _ _ = False
1109
1110 gos _ [] [] = True
1111 gos env (t1:ts1) (t2:ts2) = go env t1 t2 && gos env ts1 ts2
1112 gos _ _ _ = False
1113
1114 pickyEqType :: TcType -> TcType -> Bool
1115 -- Check when two types _look_ the same, _including_ synonyms.
1116 -- So (pickyEqType String [Char]) returns False
1117 pickyEqType ty1 ty2
1118 = go init_env ty1 ty2
1119 where
1120 init_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
1121 go env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2
1122 go _ (LitTy lit1) (LitTy lit2) = lit1 == lit2
1123 go env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = go env (tyVarKind tv1) (tyVarKind tv2)
1124 && go (rnBndr2 env tv1 tv2) t1 t2
1125 go env (AppTy s1 t1) (AppTy s2 t2) = go env s1 s2 && go env t1 t2
1126 go env (FunTy s1 t1) (FunTy s2 t2) = go env s1 s2 && go env t1 t2
1127 go env (TyConApp tc1 ts1) (TyConApp tc2 ts2) = (tc1 == tc2) && gos env ts1 ts2
1128 go _ _ _ = False
1129
1130 gos _ [] [] = True
1131 gos env (t1:ts1) (t2:ts2) = go env t1 t2 && gos env ts1 ts2
1132 gos _ _ _ = False
1133
1134 {-
1135 Note [Occurs check expansion]
1136 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1137 (occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
1138 of occurrences of tv outside type function arguments, if that is
1139 possible; otherwise, it returns Nothing.
1140
1141 For example, suppose we have
1142 type F a b = [a]
1143 Then
1144 occurCheckExpand b (F Int b) = Just [Int]
1145 but
1146 occurCheckExpand a (F a Int) = Nothing
1147
1148 We don't promise to do the absolute minimum amount of expanding
1149 necessary, but we try not to do expansions we don't need to. We
1150 prefer doing inner expansions first. For example,
1151 type F a b = (a, Int, a, [a])
1152 type G b = Char
1153 We have
1154 occurCheckExpand b (F (G b)) = F Char
1155 even though we could also expand F to get rid of b.
1156
1157 See also Note [occurCheckExpand] in TcCanonical
1158 -}
1159
1160 data OccCheckResult a
1161 = OC_OK a
1162 | OC_Forall
1163 | OC_NonTyVar
1164 | OC_Occurs
1165
1166 instance Functor OccCheckResult where
1167 fmap = liftM
1168
1169 instance Applicative OccCheckResult where
1170 pure = return
1171 (<*>) = ap
1172
1173 instance Monad OccCheckResult where
1174 return x = OC_OK x
1175 OC_OK x >>= k = k x
1176 OC_Forall >>= _ = OC_Forall
1177 OC_NonTyVar >>= _ = OC_NonTyVar
1178 OC_Occurs >>= _ = OC_Occurs
1179
1180 occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
1181 -- See Note [Occurs check expansion]
1182 -- Check whether
1183 -- a) the given variable occurs in the given type.
1184 -- b) there is a forall in the type (unless we have -XImpredicativeTypes
1185 -- or it's a ReturnTv
1186 -- c) if it's a SigTv, ty should be a tyvar
1187 --
1188 -- We may have needed to do some type synonym unfolding in order to
1189 -- get rid of the variable (or forall), so we also return the unfolded
1190 -- version of the type, which is guaranteed to be syntactically free
1191 -- of the given type variable. If the type is already syntactically
1192 -- free of the variable, then the same type is returned.
1193
1194 occurCheckExpand dflags tv ty
1195 | MetaTv { mtv_info = SigTv } <- details
1196 = go_sig_tv ty
1197 | fast_check ty = return ty
1198 | otherwise = go ty
1199 where
1200 details = ASSERT2( isTcTyVar tv, ppr tv ) tcTyVarDetails tv
1201
1202 impredicative = canUnifyWithPolyType dflags details (tyVarKind tv)
1203
1204 -- Check 'ty' is a tyvar, or can be expanded into one
1205 go_sig_tv ty@(TyVarTy {}) = OC_OK ty
1206 go_sig_tv ty | Just ty' <- tcView ty = go_sig_tv ty'
1207 go_sig_tv _ = OC_NonTyVar
1208
1209 -- True => fine
1210 fast_check (LitTy {}) = True
1211 fast_check (TyVarTy tv') = tv /= tv'
1212 fast_check (TyConApp _ tys) = all fast_check tys
1213 fast_check (FunTy arg res) = fast_check arg && fast_check res
1214 fast_check (AppTy fun arg) = fast_check fun && fast_check arg
1215 fast_check (ForAllTy tv' ty) = impredicative
1216 && fast_check (tyVarKind tv')
1217 && (tv == tv' || fast_check ty)
1218
1219 go t@(TyVarTy tv') | tv == tv' = OC_Occurs
1220 | otherwise = return t
1221 go ty@(LitTy {}) = return ty
1222 go (AppTy ty1 ty2) = do { ty1' <- go ty1
1223 ; ty2' <- go ty2
1224 ; return (mkAppTy ty1' ty2') }
1225 go (FunTy ty1 ty2) = do { ty1' <- go ty1
1226 ; ty2' <- go ty2
1227 ; return (mkFunTy ty1' ty2') }
1228 go ty@(ForAllTy tv' body_ty)
1229 | not impredicative = OC_Forall
1230 | not (fast_check (tyVarKind tv')) = OC_Occurs
1231 -- Can't expand away the kinds unless we create
1232 -- fresh variables which we don't want to do at this point.
1233 -- In principle fast_check might fail because of a for-all
1234 -- but we don't yet have poly-kinded tyvars so I'm not
1235 -- going to worry about that now
1236 | tv == tv' = return ty
1237 | otherwise = do { body' <- go body_ty
1238 ; return (ForAllTy tv' body') }
1239
1240 -- For a type constructor application, first try expanding away the
1241 -- offending variable from the arguments. If that doesn't work, next
1242 -- see if the type constructor is a type synonym, and if so, expand
1243 -- it and try again.
1244 go ty@(TyConApp tc tys)
1245 = case do { tys <- mapM go tys; return (mkTyConApp tc tys) } of
1246 OC_OK ty -> return ty -- First try to eliminate the tyvar from the args
1247 bad | Just ty' <- tcView ty -> go ty'
1248 | otherwise -> bad
1249 -- Failing that, try to expand a synonym
1250
1251 canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> TcKind -> Bool
1252 canUnifyWithPolyType dflags details kind
1253 = case details of
1254 MetaTv { mtv_info = ReturnTv } -> True -- See Note [ReturnTv]
1255 MetaTv { mtv_info = SigTv } -> False
1256 MetaTv { mtv_info = TauTv _ } -> xopt Opt_ImpredicativeTypes dflags
1257 || isOpenTypeKind kind
1258 -- Note [OpenTypeKind accepts foralls]
1259 _other -> True
1260 -- We can have non-meta tyvars in given constraints
1261
1262 {-
1263 Note [OpenTypeKind accepts foralls]
1264 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1265 Here is a common paradigm:
1266 foo :: (forall a. a -> a) -> Int
1267 foo = error "urk"
1268 To make this work we need to instantiate 'error' with a polytype.
1269 A similar case is
1270 bar :: Bool -> (forall a. a->a) -> Int
1271 bar True = \x. (x 3)
1272 bar False = error "urk"
1273 Here we need to instantiate 'error' with a polytype.
1274
1275 But 'error' has an OpenTypeKind type variable, precisely so that
1276 we can instantiate it with Int#. So we also allow such type variables
1277 to be instantiate with foralls. It's a bit of a hack, but seems
1278 straightforward.
1279
1280 ************************************************************************
1281 * *
1282 \subsection{Predicate types}
1283 * *
1284 ************************************************************************
1285
1286 Deconstructors and tests on predicate types
1287 -}
1288
1289 isTyVarClassPred :: PredType -> Bool
1290 isTyVarClassPred ty = case getClassPredTys_maybe ty of
1291 Just (_, tys) -> all isTyVarTy tys
1292 _ -> False
1293
1294 evVarPred_maybe :: EvVar -> Maybe PredType
1295 evVarPred_maybe v = if isPredTy ty then Just ty else Nothing
1296 where ty = varType v
1297
1298 evVarPred :: EvVar -> PredType
1299 evVarPred var
1300 | debugIsOn
1301 = case evVarPred_maybe var of
1302 Just pred -> pred
1303 Nothing -> pprPanic "tcEvVarPred" (ppr var <+> ppr (varType var))
1304 | otherwise
1305 = varType var
1306
1307 -- Superclasses
1308
1309 mkMinimalBySCs :: [PredType] -> [PredType]
1310 -- Remove predicates that can be deduced from others by superclasses
1311 mkMinimalBySCs ptys = [ ploc | ploc <- ptys
1312 , ploc `not_in_preds` rec_scs ]
1313 where
1314 rec_scs = concatMap trans_super_classes ptys
1315 not_in_preds p ps = not (any (eqPred p) ps)
1316
1317 trans_super_classes pred -- Superclasses of pred, excluding pred itself
1318 = case classifyPredType pred of
1319 ClassPred cls tys -> transSuperClasses cls tys
1320 TuplePred ts -> concatMap trans_super_classes ts
1321 _ -> []
1322
1323 transSuperClasses :: Class -> [Type] -> [PredType]
1324 transSuperClasses cls tys -- Superclasses of (cls tys),
1325 -- excluding (cls tys) itself
1326 = concatMap trans_sc (immSuperClasses cls tys)
1327 where
1328 trans_sc :: PredType -> [PredType]
1329 -- (trans_sc p) returns (p : p's superclasses)
1330 trans_sc p = case classifyPredType p of
1331 ClassPred cls tys -> p : transSuperClasses cls tys
1332 TuplePred ps -> concatMap trans_sc ps
1333 _ -> [p]
1334
1335 immSuperClasses :: Class -> [Type] -> [PredType]
1336 immSuperClasses cls tys
1337 = substTheta (zipTopTvSubst tyvars tys) sc_theta
1338 where
1339 (tyvars,sc_theta,_,_) = classBigSig cls
1340
1341 {-
1342 ************************************************************************
1343 * *
1344 \subsection{Predicates}
1345 * *
1346 ************************************************************************
1347 -}
1348
1349 isSigmaTy :: TcType -> Bool
1350 -- isSigmaTy returns true of any qualified type. It doesn't
1351 -- *necessarily* have any foralls. E.g
1352 -- f :: (?x::Int) => Int -> Int
1353 isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
1354 isSigmaTy (ForAllTy _ _) = True
1355 isSigmaTy (FunTy a _) = isPredTy a
1356 isSigmaTy _ = False
1357
1358 isRhoTy :: TcType -> Bool -- True of TcRhoTypes; see Note [TcRhoType]
1359 isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty'
1360 isRhoTy (ForAllTy {}) = False
1361 isRhoTy (FunTy a r) = not (isPredTy a) && isRhoTy r
1362 isRhoTy _ = True
1363
1364 isOverloadedTy :: Type -> Bool
1365 -- Yes for a type of a function that might require evidence-passing
1366 -- Used only by bindLocalMethods
1367 isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
1368 isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty
1369 isOverloadedTy (FunTy a _) = isPredTy a
1370 isOverloadedTy _ = False
1371
1372 isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
1373 isUnitTy, isCharTy, isAnyTy :: Type -> Bool
1374 isFloatTy = is_tc floatTyConKey
1375 isDoubleTy = is_tc doubleTyConKey
1376 isIntegerTy = is_tc integerTyConKey
1377 isIntTy = is_tc intTyConKey
1378 isWordTy = is_tc wordTyConKey
1379 isBoolTy = is_tc boolTyConKey
1380 isUnitTy = is_tc unitTyConKey
1381 isCharTy = is_tc charTyConKey
1382 isAnyTy = is_tc anyTyConKey
1383
1384 isStringTy :: Type -> Bool
1385 isStringTy ty
1386 = case tcSplitTyConApp_maybe ty of
1387 Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty
1388 _ -> False
1389
1390 is_tc :: Unique -> Type -> Bool
1391 -- Newtypes are opaque to this
1392 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
1393 Just (tc, _) -> uniq == getUnique tc
1394 Nothing -> False
1395
1396 {-
1397 ************************************************************************
1398 * *
1399 \subsection{Misc}
1400 * *
1401 ************************************************************************
1402 -}
1403
1404 deNoteType :: Type -> Type
1405 -- Remove all *outermost* type synonyms and other notes
1406 deNoteType ty | Just ty' <- tcView ty = deNoteType ty'
1407 deNoteType ty = ty
1408
1409 tcTyVarsOfType :: Type -> TcTyVarSet
1410 -- Just the *TcTyVars* free in the type
1411 -- (Types.tyVarsOfTypes finds all free TyVars)
1412 tcTyVarsOfType (TyVarTy tv) = if isTcTyVar tv then unitVarSet tv
1413 else emptyVarSet
1414 tcTyVarsOfType (TyConApp _ tys) = tcTyVarsOfTypes tys
1415 tcTyVarsOfType (LitTy {}) = emptyVarSet
1416 tcTyVarsOfType (FunTy arg res) = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
1417 tcTyVarsOfType (AppTy fun arg) = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
1418 tcTyVarsOfType (ForAllTy tyvar ty) = tcTyVarsOfType ty `delVarSet` tyvar
1419 -- We do sometimes quantify over skolem TcTyVars
1420
1421 tcTyVarsOfTypes :: [Type] -> TyVarSet
1422 tcTyVarsOfTypes = mapUnionVarSet tcTyVarsOfType
1423
1424 {-
1425 Find the free tycons and classes of a type. This is used in the front
1426 end of the compiler.
1427 -}
1428
1429 orphNamesOfTyCon :: TyCon -> NameSet
1430 orphNamesOfTyCon tycon = unitNameSet (getName tycon) `unionNameSet` case tyConClass_maybe tycon of
1431 Nothing -> emptyNameSet
1432 Just cls -> unitNameSet (getName cls)
1433
1434 orphNamesOfType :: Type -> NameSet
1435 orphNamesOfType ty | Just ty' <- tcView ty = orphNamesOfType ty'
1436 -- Look through type synonyms (Trac #4912)
1437 orphNamesOfType (TyVarTy _) = emptyNameSet
1438 orphNamesOfType (LitTy {}) = emptyNameSet
1439 orphNamesOfType (TyConApp tycon tys) = orphNamesOfTyCon tycon
1440 `unionNameSet` orphNamesOfTypes tys
1441 orphNamesOfType (FunTy arg res) = orphNamesOfTyCon funTyCon -- NB! See Trac #8535
1442 `unionNameSet` orphNamesOfType arg
1443 `unionNameSet` orphNamesOfType res
1444 orphNamesOfType (AppTy fun arg) = orphNamesOfType fun `unionNameSet` orphNamesOfType arg
1445 orphNamesOfType (ForAllTy _ ty) = orphNamesOfType ty
1446
1447 orphNamesOfThings :: (a -> NameSet) -> [a] -> NameSet
1448 orphNamesOfThings f = foldr (unionNameSet . f) emptyNameSet
1449
1450 orphNamesOfTypes :: [Type] -> NameSet
1451 orphNamesOfTypes = orphNamesOfThings orphNamesOfType
1452
1453 orphNamesOfDFunHead :: Type -> NameSet
1454 -- Find the free type constructors and classes
1455 -- of the head of the dfun instance type
1456 -- The 'dfun_head_type' is because of
1457 -- instance Foo a => Baz T where ...
1458 -- The decl is an orphan if Baz and T are both not locally defined,
1459 -- even if Foo *is* locally defined
1460 orphNamesOfDFunHead dfun_ty
1461 = case tcSplitSigmaTy dfun_ty of
1462 (_, _, head_ty) -> orphNamesOfType head_ty
1463
1464 orphNamesOfCo :: Coercion -> NameSet
1465 orphNamesOfCo (Refl _ ty) = orphNamesOfType ty
1466 orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos
1467 orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
1468 orphNamesOfCo (ForAllCo _ co) = orphNamesOfCo co
1469 orphNamesOfCo (CoVarCo _) = emptyNameSet
1470 orphNamesOfCo (AxiomInstCo con _ cos) = orphNamesOfCoCon con `unionNameSet` orphNamesOfCos cos
1471 orphNamesOfCo (UnivCo _ ty1 ty2) = orphNamesOfType ty1 `unionNameSet` orphNamesOfType ty2
1472 orphNamesOfCo (SymCo co) = orphNamesOfCo co
1473 orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
1474 orphNamesOfCo (NthCo _ co) = orphNamesOfCo co
1475 orphNamesOfCo (LRCo _ co) = orphNamesOfCo co
1476 orphNamesOfCo (InstCo co ty) = orphNamesOfCo co `unionNameSet` orphNamesOfType ty
1477 orphNamesOfCo (SubCo co) = orphNamesOfCo co
1478 orphNamesOfCo (AxiomRuleCo _ ts cs) = orphNamesOfTypes ts `unionNameSet`
1479 orphNamesOfCos cs
1480
1481 orphNamesOfCos :: [Coercion] -> NameSet
1482 orphNamesOfCos = orphNamesOfThings orphNamesOfCo
1483
1484 orphNamesOfCoCon :: CoAxiom br -> NameSet
1485 orphNamesOfCoCon (CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
1486 = orphNamesOfTyCon tc `unionNameSet` orphNamesOfCoAxBranches branches
1487
1488 orphNamesOfCoAxBranches :: BranchList CoAxBranch br -> NameSet
1489 orphNamesOfCoAxBranches = brListFoldr (unionNameSet . orphNamesOfCoAxBranch) emptyNameSet
1490
1491 orphNamesOfCoAxBranch :: CoAxBranch -> NameSet
1492 orphNamesOfCoAxBranch (CoAxBranch { cab_lhs = lhs, cab_rhs = rhs })
1493 = orphNamesOfTypes lhs `unionNameSet` orphNamesOfType rhs
1494
1495 {-
1496 ************************************************************************
1497 * *
1498 \subsection[TysWiredIn-ext-type]{External types}
1499 * *
1500 ************************************************************************
1501
1502 The compiler's foreign function interface supports the passing of a
1503 restricted set of types as arguments and results (the restricting factor
1504 being the )
1505 -}
1506
1507 tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type)
1508 -- (tcSplitIOType_maybe t) returns Just (IO,t',co)
1509 -- if co : t ~ IO t'
1510 -- returns Nothing otherwise
1511 tcSplitIOType_maybe ty
1512 = case tcSplitTyConApp_maybe ty of
1513 Just (io_tycon, [io_res_ty])
1514 | io_tycon `hasKey` ioTyConKey ->
1515 Just (io_tycon, io_res_ty)
1516 _ ->
1517 Nothing
1518
1519 isFFITy :: Type -> Bool
1520 -- True for any TyCon that can possibly be an arg or result of an FFI call
1521 isFFITy ty = isValid (checkRepTyCon legalFFITyCon ty empty)
1522
1523 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Validity
1524 -- Checks for valid argument type for a 'foreign import'
1525 isFFIArgumentTy dflags safety ty
1526 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty empty
1527
1528 isFFIExternalTy :: Type -> Validity
1529 -- Types that are allowed as arguments of a 'foreign export'
1530 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty empty
1531
1532 isFFIImportResultTy :: DynFlags -> Type -> Validity
1533 isFFIImportResultTy dflags ty
1534 = checkRepTyCon (legalFIResultTyCon dflags) ty empty
1535
1536 isFFIExportResultTy :: Type -> Validity
1537 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty empty
1538
1539 isFFIDynTy :: Type -> Type -> Validity
1540 -- The type in a foreign import dynamic must be Ptr, FunPtr, or a newtype of
1541 -- either, and the wrapped function type must be equal to the given type.
1542 -- We assume that all types have been run through normaliseFfiType, so we don't
1543 -- need to worry about expanding newtypes here.
1544 isFFIDynTy expected ty
1545 -- Note [Foreign import dynamic]
1546 -- In the example below, expected would be 'CInt -> IO ()', while ty would
1547 -- be 'FunPtr (CDouble -> IO ())'.
1548 | Just (tc, [ty']) <- splitTyConApp_maybe ty
1549 , tyConUnique tc `elem` [ptrTyConKey, funPtrTyConKey]
1550 , eqType ty' expected
1551 = IsValid
1552 | otherwise
1553 = NotValid (vcat [ ptext (sLit "Expected: Ptr/FunPtr") <+> pprParendType expected <> comma
1554 , ptext (sLit " Actual:") <+> ppr ty ])
1555
1556 isFFILabelTy :: Type -> Validity
1557 -- The type of a foreign label must be Ptr, FunPtr, or a newtype of either.
1558 isFFILabelTy ty = checkRepTyCon ok ty extra
1559 where
1560 ok tc = tc `hasKey` funPtrTyConKey || tc `hasKey` ptrTyConKey
1561 extra = ptext (sLit "A foreign-imported address (via &foo) must have type (Ptr a) or (FunPtr a)")
1562
1563 isFFIPrimArgumentTy :: DynFlags -> Type -> Validity
1564 -- Checks for valid argument type for a 'foreign import prim'
1565 -- Currently they must all be simple unlifted types, or the well-known type
1566 -- Any, which can be used to pass the address to a Haskell object on the heap to
1567 -- the foreign function.
1568 isFFIPrimArgumentTy dflags ty
1569 | isAnyTy ty = IsValid
1570 | otherwise = checkRepTyCon (legalFIPrimArgTyCon dflags) ty empty
1571
1572 isFFIPrimResultTy :: DynFlags -> Type -> Validity
1573 -- Checks for valid result type for a 'foreign import prim'
1574 -- Currently it must be an unlifted type, including unboxed tuples.
1575 isFFIPrimResultTy dflags ty
1576 = checkRepTyCon (legalFIPrimResultTyCon dflags) ty empty
1577
1578 isFunPtrTy :: Type -> Bool
1579 isFunPtrTy ty = isValid (checkRepTyCon (`hasKey` funPtrTyConKey) ty empty)
1580
1581 -- normaliseFfiType gets run before checkRepTyCon, so we don't
1582 -- need to worry about looking through newtypes or type functions
1583 -- here; that's already been taken care of.
1584 checkRepTyCon :: (TyCon -> Bool) -> Type -> SDoc -> Validity
1585 checkRepTyCon check_tc ty extra
1586 = case splitTyConApp_maybe ty of
1587 Just (tc, tys)
1588 | isNewTyCon tc -> NotValid (hang msg 2 (mk_nt_reason tc tys $$ nt_fix))
1589 | check_tc tc -> IsValid
1590 | otherwise -> NotValid (msg $$ extra)
1591 Nothing -> NotValid (quotes (ppr ty) <+> ptext (sLit "is not a data type") $$ extra)
1592 where
1593 msg = quotes (ppr ty) <+> ptext (sLit "cannot be marshalled in a foreign call")
1594 mk_nt_reason tc tys
1595 | null tys = ptext (sLit "because its data construtor is not in scope")
1596 | otherwise = ptext (sLit "because the data construtor for")
1597 <+> quotes (ppr tc) <+> ptext (sLit "is not in scope")
1598 nt_fix = ptext (sLit "Possible fix: import the data constructor to bring it into scope")
1599
1600 {-
1601 Note [Foreign import dynamic]
1602 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1603 A dynamic stub must be of the form 'FunPtr ft -> ft' where ft is any foreign
1604 type. Similarly, a wrapper stub must be of the form 'ft -> IO (FunPtr ft)'.
1605
1606 We use isFFIDynTy to check whether a signature is well-formed. For example,
1607 given a (illegal) declaration like:
1608
1609 foreign import ccall "dynamic"
1610 foo :: FunPtr (CDouble -> IO ()) -> CInt -> IO ()
1611
1612 isFFIDynTy will compare the 'FunPtr' type 'CDouble -> IO ()' with the curried
1613 result type 'CInt -> IO ()', and return False, as they are not equal.
1614
1615
1616 ----------------------------------------------
1617 These chaps do the work; they are not exported
1618 ----------------------------------------------
1619 -}
1620
1621 legalFEArgTyCon :: TyCon -> Bool
1622 legalFEArgTyCon tc
1623 -- It's illegal to make foreign exports that take unboxed
1624 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
1625 = boxedMarshalableTyCon tc
1626
1627 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
1628 legalFIResultTyCon dflags tc
1629 | tc == unitTyCon = True
1630 | otherwise = marshalableTyCon dflags tc
1631
1632 legalFEResultTyCon :: TyCon -> Bool
1633 legalFEResultTyCon tc
1634 | tc == unitTyCon = True
1635 | otherwise = boxedMarshalableTyCon tc
1636
1637 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
1638 -- Checks validity of types going from Haskell -> external world
1639 legalOutgoingTyCon dflags _ tc
1640 = marshalableTyCon dflags tc
1641
1642 legalFFITyCon :: TyCon -> Bool
1643 -- True for any TyCon that can possibly be an arg or result of an FFI call
1644 legalFFITyCon tc
1645 | isUnLiftedTyCon tc = True
1646 | tc == unitTyCon = True
1647 | otherwise = boxedMarshalableTyCon tc
1648
1649 marshalableTyCon :: DynFlags -> TyCon -> Bool
1650 marshalableTyCon dflags tc
1651 | (xopt Opt_UnliftedFFITypes dflags
1652 && isUnLiftedTyCon tc
1653 && not (isUnboxedTupleTyCon tc)
1654 && case tyConPrimRep tc of -- Note [Marshalling VoidRep]
1655 VoidRep -> False
1656 _ -> True)
1657 = True
1658 | otherwise
1659 = boxedMarshalableTyCon tc
1660
1661 boxedMarshalableTyCon :: TyCon -> Bool
1662 boxedMarshalableTyCon tc
1663 | getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
1664 , int32TyConKey, int64TyConKey
1665 , wordTyConKey, word8TyConKey, word16TyConKey
1666 , word32TyConKey, word64TyConKey
1667 , floatTyConKey, doubleTyConKey
1668 , ptrTyConKey, funPtrTyConKey
1669 , charTyConKey
1670 , stablePtrTyConKey
1671 , boolTyConKey
1672 ]
1673 = True
1674
1675 | otherwise = False
1676
1677 legalFIPrimArgTyCon :: DynFlags -> TyCon -> Bool
1678 -- Check args of 'foreign import prim', only allow simple unlifted types.
1679 -- Strictly speaking it is unnecessary to ban unboxed tuples here since
1680 -- currently they're of the wrong kind to use in function args anyway.
1681 legalFIPrimArgTyCon dflags tc
1682 | xopt Opt_UnliftedFFITypes dflags
1683 && isUnLiftedTyCon tc
1684 && not (isUnboxedTupleTyCon tc)
1685 = True
1686 | otherwise
1687 = False
1688
1689 legalFIPrimResultTyCon :: DynFlags -> TyCon -> Bool
1690 -- Check result type of 'foreign import prim'. Allow simple unlifted
1691 -- types and also unboxed tuple result types '... -> (# , , #)'
1692 legalFIPrimResultTyCon dflags tc
1693 | xopt Opt_UnliftedFFITypes dflags
1694 && isUnLiftedTyCon tc
1695 && (isUnboxedTupleTyCon tc
1696 || case tyConPrimRep tc of -- Note [Marshalling VoidRep]
1697 VoidRep -> False
1698 _ -> True)
1699 = True
1700 | otherwise
1701 = False
1702
1703 {-
1704 Note [Marshalling VoidRep]
1705 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1706 We don't treat State# (whose PrimRep is VoidRep) as marshalable.
1707 In turn that means you can't write
1708 foreign import foo :: Int -> State# RealWorld
1709
1710 Reason: the back end falls over with panic "primRepHint:VoidRep";
1711 and there is no compelling reason to permit it
1712 -}