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