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