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