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