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