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