2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Monadic type operations}
6 This module contains monadic operations over types that contain mutable type variables
10 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
12 --------------------------------
13 -- Creating new mutable type variables
15 newTyVarTy, -- Kind -> TcM TcType
16 newTyVarTys, -- Int -> Kind -> TcM [TcType]
17 newKindVar, newKindVars, newBoxityVar,
18 putTcTyVar, getTcTyVar,
19 newMutTyVar, readMutTyVar, writeMutTyVar,
21 newHoleTyVarTy, readHoleResult, zapToType,
23 --------------------------------
25 tcInstTyVar, tcInstTyVars, tcInstType,
27 --------------------------------
28 -- Checking type validity
29 Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
30 SourceTyCtxt(..), checkValidTheta,
31 checkValidTyCon, checkValidClass,
32 checkValidInstHead, instTypeErr, checkAmbiguity,
35 --------------------------------
38 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
39 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
40 zonkTcPredType, zonkTcTyVarToTyVar, zonkKindEnv,
44 #include "HsVersions.h"
48 import TypeRep ( Type(..), SourceType(..), TyNote(..), -- Friend; can see representation
51 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
52 TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
54 tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
55 tcSplitTyConApp_maybe, tcSplitForAllTys,
56 tcIsTyVarTy, tcSplitSigmaTy,
57 isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy,
59 mkAppTy, mkTyVarTy, mkTyVarTys,
60 tyVarsOfPred, getClassPredTys_maybe,
62 liftedTypeKind, openTypeKind, defaultKind, superKind,
63 superBoxity, liftedBoxity, typeKind,
64 tyVarsOfType, tyVarsOfTypes,
66 isFFIArgumentTy, isFFIImportResultTy
68 import qualified Type ( splitFunTys )
69 import Subst ( Subst, mkTopTyVarSubst, substTy )
70 import Class ( Class, DefMeth(..), classArity, className, classBigSig )
71 import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
72 tyConArity, tyConName, tyConKind, tyConTheta,
73 getSynTyConDefn, tyConDataCons )
74 import DataCon ( DataCon, dataConWrapId, dataConName, dataConSig, dataConFieldLabels )
75 import FieldLabel ( fieldLabelName, fieldLabelType )
76 import Var ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar,
77 mkTyVar, mkMutTyVar, isMutTyVar, mutTyVarRef )
80 import Generics ( validGenericMethodType )
81 import TcRnMonad -- TcType, amongst others
82 import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
83 import ForeignCall ( Safety(..) )
84 import FunDeps ( grow )
85 import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
86 import Name ( Name, NamedThing(..), setNameUnique,
87 mkSystemTvNameEncoded,
90 import BasicTypes ( Boxity(Boxed) )
91 import CmdLineOpts ( dopt, DynFlag(..) )
92 import SrcLoc ( noSrcLoc )
93 import Util ( nOfThem, isSingleton, equalLength, notNull )
94 import ListSetOps ( equivClasses, removeDups )
99 %************************************************************************
101 \subsection{New type variables}
103 %************************************************************************
106 newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar
107 newMutTyVar name kind details
108 = do { ref <- newMutVar Nothing ;
109 return (mkMutTyVar name kind details ref) }
111 readMutTyVar :: TyVar -> TcM (Maybe Type)
112 readMutTyVar tyvar = readMutVar (mutTyVarRef tyvar)
114 writeMutTyVar :: TyVar -> Maybe Type -> TcM ()
115 writeMutTyVar tyvar val = writeMutVar (mutTyVarRef tyvar) val
117 newTyVar :: Kind -> TcM TcTyVar
119 = newUnique `thenM` \ uniq ->
120 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
122 newTyVarTy :: Kind -> TcM TcType
124 = newTyVar kind `thenM` \ tc_tyvar ->
125 returnM (TyVarTy tc_tyvar)
127 newTyVarTys :: Int -> Kind -> TcM [TcType]
128 newTyVarTys n kind = mappM newTyVarTy (nOfThem n kind)
130 newKindVar :: TcM TcKind
132 = newUnique `thenM` \ uniq ->
133 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv `thenM` \ kv ->
136 newKindVars :: Int -> TcM [TcKind]
137 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
139 newBoxityVar :: TcM TcKind
141 = newUnique `thenM` \ uniq ->
142 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) superBoxity VanillaTv `thenM` \ kv ->
147 %************************************************************************
149 \subsection{'hole' type variables}
151 %************************************************************************
154 newHoleTyVarTy :: TcM TcType
155 = newUnique `thenM` \ uniq ->
156 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("h")) openTypeKind HoleTv `thenM` \ tv ->
159 readHoleResult :: TcType -> TcM TcType
160 -- Read the answer out of a hole, constructed by newHoleTyVarTy
161 readHoleResult (TyVarTy tv)
162 = ASSERT( isHoleTyVar tv )
163 getTcTyVar tv `thenM` \ maybe_res ->
165 Just ty -> returnM ty
166 Nothing -> pprPanic "readHoleResult: empty" (ppr tv)
167 readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
169 zapToType :: TcType -> TcM TcType
170 zapToType (TyVarTy tv)
172 = getTcTyVar tv `thenM` \ maybe_res ->
174 Nothing -> newTyVarTy openTypeKind `thenM` \ ty ->
175 putTcTyVar tv ty `thenM_`
177 Just ty -> returnM ty -- No need to loop; we never
178 -- have chains of holes
180 zapToType other_ty = returnM other_ty
183 %************************************************************************
185 \subsection{Type instantiation}
187 %************************************************************************
189 Instantiating a bunch of type variables
192 tcInstTyVars :: TyVarDetails -> [TyVar]
193 -> TcM ([TcTyVar], [TcType], Subst)
195 tcInstTyVars tv_details tyvars
196 = mappM (tcInstTyVar tv_details) tyvars `thenM` \ tc_tyvars ->
198 tys = mkTyVarTys tc_tyvars
200 returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
201 -- Since the tyvars are freshly made,
202 -- they cannot possibly be captured by
203 -- any existing for-alls. Hence mkTopTyVarSubst
205 tcInstTyVar tv_details tyvar
206 = newUnique `thenM` \ uniq ->
208 name = setNameUnique (tyVarName tyvar) uniq
209 -- Note that we don't change the print-name
210 -- This won't confuse the type checker but there's a chance
211 -- that two different tyvars will print the same way
212 -- in an error message. -dppr-debug will show up the difference
213 -- Better watch out for this. If worst comes to worst, just
216 newMutTyVar name (tyVarKind tyvar) tv_details
218 tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
219 -- tcInstType instantiates the outer-level for-alls of a TcType with
220 -- fresh (mutable) type variables, splits off the dictionary part,
221 -- and returns the pieces.
222 tcInstType tv_details ty
223 = case tcSplitForAllTys ty of
224 ([], rho) -> -- There may be overloading despite no type variables;
225 -- (?x :: Int) => Int -> Int
227 (theta, tau) = tcSplitPhiTy rho
229 returnM ([], theta, tau)
231 (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenM` \ (tyvars', _, tenv) ->
233 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
235 returnM (tyvars', theta, tau)
239 %************************************************************************
241 \subsection{Putting and getting mutable type variables}
243 %************************************************************************
246 putTcTyVar :: TcTyVar -> TcType -> TcM TcType
247 getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
254 | not (isMutTyVar tyvar)
255 = pprTrace "putTcTyVar" (ppr tyvar) $
259 = ASSERT( isMutTyVar tyvar )
260 writeMutTyVar tyvar (Just ty) `thenM_`
264 Getting is more interesting. The easy thing to do is just to read, thus:
267 getTcTyVar tyvar = readMutTyVar tyvar
270 But it's more fun to short out indirections on the way: If this
271 version returns a TyVar, then that TyVar is unbound. If it returns
272 any other type, then there might be bound TyVars embedded inside it.
274 We return Nothing iff the original box was unbound.
278 | not (isMutTyVar tyvar)
279 = pprTrace "getTcTyVar" (ppr tyvar) $
280 returnM (Just (mkTyVarTy tyvar))
283 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
284 readMutTyVar tyvar `thenM` \ maybe_ty ->
286 Just ty -> short_out ty `thenM` \ ty' ->
287 writeMutTyVar tyvar (Just ty') `thenM_`
290 Nothing -> returnM Nothing
292 short_out :: TcType -> TcM TcType
293 short_out ty@(TyVarTy tyvar)
294 | not (isMutTyVar tyvar)
298 = readMutTyVar tyvar `thenM` \ maybe_ty ->
300 Just ty' -> short_out ty' `thenM` \ ty' ->
301 writeMutTyVar tyvar (Just ty') `thenM_`
306 short_out other_ty = returnM other_ty
310 %************************************************************************
312 \subsection{Zonking -- the exernal interfaces}
314 %************************************************************************
316 ----------------- Type variables
319 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
320 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
322 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
323 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
324 returnM (tyVarsOfTypes tys)
326 zonkTcTyVar :: TcTyVar -> TcM TcType
327 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
330 ----------------- Types
333 zonkTcType :: TcType -> TcM TcType
334 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
336 zonkTcTypes :: [TcType] -> TcM [TcType]
337 zonkTcTypes tys = mappM zonkTcType tys
339 zonkTcClassConstraints cts = mappM zonk cts
340 where zonk (clas, tys)
341 = zonkTcTypes tys `thenM` \ new_tys ->
342 returnM (clas, new_tys)
344 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
345 zonkTcThetaType theta = mappM zonkTcPredType theta
347 zonkTcPredType :: TcPredType -> TcM TcPredType
348 zonkTcPredType (ClassP c ts)
349 = zonkTcTypes ts `thenM` \ new_ts ->
350 returnM (ClassP c new_ts)
351 zonkTcPredType (IParam n t)
352 = zonkTcType t `thenM` \ new_t ->
353 returnM (IParam n new_t)
356 ------------------- These ...ToType, ...ToKind versions
357 are used at the end of type checking
360 zonkKindEnv :: [(Name, TcKind)] -> TcM [(Name, Kind)]
362 = mappM zonk_it pairs
364 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenM` \ kind ->
367 -- When zonking a kind, we want to
368 -- zonk a *kind* variable to (Type *)
369 -- zonk a *boxity* variable to *
370 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
371 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
372 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
374 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
375 -- of a type variable, at the *end* of type checking. It changes
376 -- the *mutable* type variable into an *immutable* one.
378 -- It does this by making an immutable version of tv and binds tv to it.
379 -- Now any bound occurences of the original type variable will get
380 -- zonked to the immutable version.
382 zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
383 zonkTcTyVarToTyVar tv
385 -- Make an immutable version, defaulting
386 -- the kind to lifted if necessary
387 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
388 immut_tv_ty = mkTyVarTy immut_tv
390 zap tv = putTcTyVar tv immut_tv_ty
391 -- Bind the mutable version to the immutable one
393 -- If the type variable is mutable, then bind it to immut_tv_ty
394 -- so that all other occurrences of the tyvar will get zapped too
395 zonkTyVar zap tv `thenM` \ ty2 ->
397 -- This warning shows up if the allegedly-unbound tyvar is
398 -- already bound to something. It can actually happen, and
399 -- in a harmless way (see [Silly Type Synonyms] below) so
400 -- it's only a warning
401 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
406 [Silly Type Synonyms]
409 type C u a = u -- Note 'a' unused
411 foo :: (forall a. C u a -> C u a) -> u
415 bar = foo (\t -> t + t)
417 * From the (\t -> t+t) we get type {Num d} => d -> d
420 * Now unify with type of foo's arg, and we get:
421 {Num (C d a)} => C d a -> C d a
424 * Now abstract over the 'a', but float out the Num (C d a) constraint
425 because it does not 'really' mention a. (see Type.tyVarsOfType)
426 The arg to foo becomes
429 * So we get a dict binding for Num (C d a), which is zonked to give
432 * Then the /\a abstraction has a zonked 'a' in it.
434 All very silly. I think its harmless to ignore the problem.
437 %************************************************************************
439 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
441 %* For internal use only! *
443 %************************************************************************
446 -- zonkType is used for Kinds as well
448 -- For unbound, mutable tyvars, zonkType uses the function given to it
449 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
450 -- type variable and zonks the kind too
452 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
453 -- see zonkTcType, and zonkTcTypeToType
456 zonkType unbound_var_fn ty
459 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
460 returnM (TyConApp tycon tys')
462 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
463 go ty2 `thenM` \ ty2' ->
464 returnM (NoteTy (SynNote ty1') ty2')
466 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
468 go (SourceTy p) = go_pred p `thenM` \ p' ->
469 returnM (SourceTy p')
471 go (FunTy arg res) = go arg `thenM` \ arg' ->
472 go res `thenM` \ res' ->
473 returnM (FunTy arg' res')
475 go (AppTy fun arg) = go fun `thenM` \ fun' ->
476 go arg `thenM` \ arg' ->
477 returnM (mkAppTy fun' arg')
478 -- NB the mkAppTy; we might have instantiated a
479 -- type variable to a type constructor, so we need
480 -- to pull the TyConApp to the top.
482 -- The two interesting cases!
483 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
485 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenM` \ tyvar' ->
486 go ty `thenM` \ ty' ->
487 returnM (ForAllTy tyvar' ty')
489 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
490 returnM (ClassP c tys')
491 go_pred (NType tc tys) = mappM go tys `thenM` \ tys' ->
492 returnM (NType tc tys')
493 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
494 returnM (IParam n ty')
496 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
497 -> TcTyVar -> TcM TcType
498 zonkTyVar unbound_var_fn tyvar
499 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
500 -- zonking a forall type, when the bound type variable
501 -- needn't be mutable
502 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
503 returnM (TyVarTy tyvar)
506 = getTcTyVar tyvar `thenM` \ maybe_ty ->
508 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
509 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
514 %************************************************************************
516 \subsection{Checking a user type}
518 %************************************************************************
520 When dealing with a user-written type, we first translate it from an HsType
521 to a Type, performing kind checking, and then check various things that should
522 be true about it. We don't want to perform these checks at the same time
523 as the initial translation because (a) they are unnecessary for interface-file
524 types and (b) when checking a mutually recursive group of type and class decls,
525 we can't "look" at the tycons/classes yet. Also, the checks are are rather
526 diverse, and used to really mess up the other code.
528 One thing we check for is 'rank'.
530 Rank 0: monotypes (no foralls)
531 Rank 1: foralls at the front only, Rank 0 inside
532 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
534 basic ::= tyvar | T basic ... basic
536 r2 ::= forall tvs. cxt => r2a
537 r2a ::= r1 -> r2a | basic
538 r1 ::= forall tvs. cxt => r0
539 r0 ::= r0 -> r0 | basic
541 Another thing is to check that type synonyms are saturated.
542 This might not necessarily show up in kind checking.
544 data T k = MkT (k Int)
550 = FunSigCtxt Name -- Function type signature
551 | ExprSigCtxt -- Expression type signature
552 | ConArgCtxt Name -- Data constructor argument
553 | TySynCtxt Name -- RHS of a type synonym decl
554 | GenPatCtxt -- Pattern in generic decl
555 -- f{| a+b |} (Inl x) = ...
556 | PatSigCtxt -- Type sig in pattern
558 | ResSigCtxt -- Result type sig
560 | ForSigCtxt Name -- Foreign inport or export signature
561 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
563 -- Notes re TySynCtxt
564 -- We allow type synonyms that aren't types; e.g. type List = []
566 -- If the RHS mentions tyvars that aren't in scope, we'll
567 -- quantify over them:
568 -- e.g. type T = a->a
569 -- will become type T = forall a. a->a
571 -- With gla-exts that's right, but for H98 we should complain.
574 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
575 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
576 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
577 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
578 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
579 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
580 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
581 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
582 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
586 checkValidType :: UserTypeCtxt -> Type -> TcM ()
587 -- Checks that the type is valid for the given context
588 checkValidType ctxt ty
589 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
591 rank | gla_exts = Arbitrary
593 = case ctxt of -- Haskell 98
597 TySynCtxt _ -> Rank 0
598 ExprSigCtxt -> Rank 1
599 FunSigCtxt _ -> Rank 1
600 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
601 -- constructor, hence rank 1
602 ForSigCtxt _ -> Rank 1
603 RuleSigCtxt _ -> Rank 1
605 actual_kind = typeKind ty
607 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
609 kind_ok = case ctxt of
610 TySynCtxt _ -> True -- Any kind will do
611 GenPatCtxt -> actual_kind_is_lifted
612 ForSigCtxt _ -> actual_kind_is_lifted
613 other -> isTypeKind actual_kind
615 ubx_tup | not gla_exts = UT_NotOk
616 | otherwise = case ctxt of
619 -- Unboxed tuples ok in function results,
620 -- but for type synonyms we allow them even at
623 addErrCtxt (checkTypeCtxt ctxt ty) $
625 -- Check that the thing has kind Type, and is lifted if necessary
626 checkTc kind_ok (kindErr actual_kind) `thenM_`
628 -- Check the internal validity of the type itself
629 check_poly_type rank ubx_tup ty
632 checkTypeCtxt ctxt ty
633 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
634 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
636 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
637 -- something strange like {Eq k} -> k -> k, because there is no
638 -- ForAll at the top of the type. Since this is going to the user
639 -- we want it to look like a proper Haskell type even then; hence the hack
641 -- This shows up in the complaint about
643 -- op :: Eq a => a -> a
644 ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
647 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
652 data Rank = Rank Int | Arbitrary
654 decRank :: Rank -> Rank
655 decRank Arbitrary = Arbitrary
656 decRank (Rank n) = Rank (n-1)
658 ----------------------------------------
659 data UbxTupFlag = UT_Ok | UT_NotOk
660 -- The "Ok" version means "ok if -fglasgow-exts is on"
662 ----------------------------------------
663 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
664 check_poly_type (Rank 0) ubx_tup ty
665 = check_tau_type (Rank 0) ubx_tup ty
667 check_poly_type rank ubx_tup ty
669 (tvs, theta, tau) = tcSplitSigmaTy ty
671 check_valid_theta SigmaCtxt theta `thenM_`
672 check_tau_type (decRank rank) ubx_tup tau `thenM_`
673 checkFreeness tvs theta `thenM_`
674 checkAmbiguity tvs theta (tyVarsOfType tau)
676 ----------------------------------------
677 check_arg_type :: Type -> TcM ()
678 -- The sort of type that can instantiate a type variable,
679 -- or be the argument of a type constructor.
680 -- Not an unboxed tuple, not a forall.
681 -- Other unboxed types are very occasionally allowed as type
682 -- arguments depending on the kind of the type constructor
684 -- For example, we want to reject things like:
686 -- instance Ord a => Ord (forall s. T s a)
688 -- g :: T s (forall b.b)
690 -- NB: unboxed tuples can have polymorphic or unboxed args.
691 -- This happens in the workers for functions returning
692 -- product types with polymorphic components.
693 -- But not in user code.
694 -- Anyway, they are dealt with by a special case in check_tau_type
697 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
698 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
700 ----------------------------------------
701 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
702 -- Rank is allowed rank for function args
703 -- No foralls otherwise
705 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
706 check_tau_type rank ubx_tup (SourceTy sty) = getDOpts `thenM` \ dflags ->
707 check_source_ty dflags TypeCtxt sty
708 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
709 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
710 = check_poly_type rank UT_NotOk arg_ty `thenM_`
711 check_tau_type rank UT_Ok res_ty
713 check_tau_type rank ubx_tup (AppTy ty1 ty2)
714 = check_arg_type ty1 `thenM_` check_arg_type ty2
716 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
717 -- Synonym notes are built only when the synonym is
718 -- saturated (see Type.mkSynTy)
719 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
721 -- If -fglasgow-exts then don't check the 'note' part.
722 -- This allows us to instantiate a synonym defn with a
723 -- for-all type, or with a partially-applied type synonym.
724 -- e.g. type T a b = a
727 -- Here, T is partially applied, so it's illegal in H98.
728 -- But if you expand S first, then T we get just
733 -- For H98, do check the un-expanded part
734 check_tau_type rank ubx_tup syn
737 check_tau_type rank ubx_tup ty
739 check_tau_type rank ubx_tup (NoteTy other_note ty)
740 = check_tau_type rank ubx_tup ty
742 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
744 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
745 -- synonym application, leaving it to checkValidType (i.e. right here)
747 checkTc syn_arity_ok arity_msg `thenM_`
748 mappM_ check_arg_type tys
750 | isUnboxedTupleTyCon tc
751 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
752 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
753 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
754 -- Args are allowed to be unlifted, or
755 -- more unboxed tuples, so can't use check_arg_ty
758 = mappM_ check_arg_type tys
761 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
763 syn_arity_ok = tc_arity <= n_args
764 -- It's OK to have an *over-applied* type synonym
765 -- data Tree a b = ...
766 -- type Foo a = Tree [a]
767 -- f :: Foo a b -> ...
769 tc_arity = tyConArity tc
771 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
772 ubx_tup_msg = ubxArgTyErr ty
774 ----------------------------------------
775 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
776 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
777 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
778 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
783 %************************************************************************
785 \subsection{Checking a theta or source type}
787 %************************************************************************
791 = ClassSCCtxt Name -- Superclasses of clas
792 | SigmaCtxt -- Context of a normal for-all type
793 | DataTyCtxt Name -- Context of a data decl
794 | TypeCtxt -- Source type in an ordinary type
795 | InstThetaCtxt -- Context of an instance decl
796 | InstHeadCtxt -- Head of an instance decl
798 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
799 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
800 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
801 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
802 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
803 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
807 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
808 checkValidTheta ctxt theta
809 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
811 -------------------------
812 check_valid_theta ctxt []
814 check_valid_theta ctxt theta
815 = getDOpts `thenM` \ dflags ->
816 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
817 -- Actually, in instance decls and type signatures,
818 -- duplicate constraints are eliminated by TcMonoType.hoistForAllTys,
819 -- so this error can only fire for the context of a class or
821 mappM_ (check_source_ty dflags ctxt) theta
823 (_,dups) = removeDups tcCmpPred theta
825 -------------------------
826 check_source_ty dflags ctxt pred@(ClassP cls tys)
827 = -- Class predicates are valid in all contexts
828 mappM_ check_arg_type tys `thenM_`
829 checkTc (arity == n_tys) arity_err `thenM_`
830 checkTc (check_class_pred_tys dflags ctxt tys)
831 (predTyVarErr pred $$ how_to_allow)
834 class_name = className cls
835 arity = classArity cls
837 arity_err = arityErr "Class" class_name arity n_tys
839 how_to_allow = case ctxt of
840 InstHeadCtxt -> empty -- Should not happen
841 InstThetaCtxt -> parens undecidableMsg
842 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
844 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
845 -- Implicit parameters only allows in type
846 -- signatures; not in instance decls, superclasses etc
847 -- The reason for not allowing implicit params in instances is a bit subtle
848 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
849 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
850 -- discharge all the potential usas of the ?x in e. For example, a
851 -- constraint Foo [Int] might come out of e,and applying the
852 -- instance decl would show up two uses of ?x.
854 check_source_ty dflags TypeCtxt (NType tc tys) = mappM_ check_arg_type tys
857 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
859 -------------------------
860 check_class_pred_tys dflags ctxt tys
862 InstHeadCtxt -> True -- We check for instance-head
863 -- formation in checkValidInstHead
864 InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
865 other -> gla_exts || all tyvar_head tys
867 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
868 gla_exts = dopt Opt_GlasgowExts dflags
870 -------------------------
871 tyvar_head ty -- Haskell 98 allows predicates of form
872 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
873 | otherwise -- where a is a type variable
874 = case tcSplitAppTy_maybe ty of
875 Just (ty, _) -> tyvar_head ty
882 is ambiguous if P contains generic variables
883 (i.e. one of the Vs) that are not mentioned in tau
885 However, we need to take account of functional dependencies
886 when we speak of 'mentioned in tau'. Example:
887 class C a b | a -> b where ...
889 forall x y. (C x y) => x
890 is not ambiguous because x is mentioned and x determines y
892 NB; the ambiguity check is only used for *user* types, not for types
893 coming from inteface files. The latter can legitimately have
894 ambiguous types. Example
896 class S a where s :: a -> (Int,Int)
897 instance S Char where s _ = (1,1)
898 f:: S a => [a] -> Int -> (Int,Int)
899 f (_::[a]) x = (a*x,b)
900 where (a,b) = s (undefined::a)
902 Here the worker for f gets the type
903 fw :: forall a. S a => Int -> (# Int, Int #)
905 If the list of tv_names is empty, we have a monotype, and then we
906 don't need to check for ambiguity either, because the test can't fail
910 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
911 checkAmbiguity forall_tyvars theta tau_tyvars
912 = mappM_ complain (filter is_ambig theta)
914 complain pred = addErrTc (ambigErr pred)
915 extended_tau_vars = grow theta tau_tyvars
916 is_ambig pred = any ambig_var (varSetElems (tyVarsOfPred pred))
918 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
919 not (ct_var `elemVarSet` extended_tau_vars)
921 is_free ct_var = not (ct_var `elem` forall_tyvars)
924 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
925 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
926 ptext SLIT("must be reachable from the type after the '=>'"))]
929 In addition, GHC insists that at least one type variable
930 in each constraint is in V. So we disallow a type like
931 forall a. Eq b => b -> b
932 even in a scope where b is in scope.
935 checkFreeness forall_tyvars theta
936 = mappM_ complain (filter is_free theta)
938 is_free pred = not (isIPPred pred)
939 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
940 bound_var ct_var = ct_var `elem` forall_tyvars
941 complain pred = addErrTc (freeErr pred)
944 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
945 ptext SLIT("are already in scope"),
946 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
951 checkThetaCtxt ctxt theta
952 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
953 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
955 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
956 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
957 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
959 arityErr kind name n m
960 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
961 n_arguments <> comma, text "but has been given", int m]
963 n_arguments | n == 0 = ptext SLIT("no arguments")
964 | n == 1 = ptext SLIT("1 argument")
965 | True = hsep [int n, ptext SLIT("arguments")]
969 %************************************************************************
971 \subsection{Validity check for TyCons}
973 %************************************************************************
975 checkValidTyCon is called once the mutually-recursive knot has been
976 tied, so we can look at things freely.
979 checkValidTyCon :: TyCon -> TcM ()
981 | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
983 = -- Check the context on the data decl
984 checkValidTheta (DataTyCtxt name) (tyConTheta tc) `thenM_`
986 -- Check arg types of data constructors
987 mappM_ checkValidDataCon data_cons `thenM_`
989 -- Check that fields with the same name share a type
990 mappM_ check_fields groups
994 (_, syn_rhs) = getSynTyConDefn tc
995 data_cons = tyConDataCons tc
997 fields = [field | con <- data_cons, field <- dataConFieldLabels con]
998 groups = equivClasses cmp_name fields
999 cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
1001 check_fields fields@(first_field_label : other_fields)
1002 -- These fields all have the same name, but are from
1003 -- different constructors in the data type
1004 = -- Check that all the fields in the group have the same type
1005 -- NB: this check assumes that all the constructors of a given
1006 -- data type use the same type variables
1007 checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
1009 field_ty = fieldLabelType first_field_label
1010 field_name = fieldLabelName first_field_label
1011 other_tys = map fieldLabelType other_fields
1013 checkValidDataCon :: DataCon -> TcM ()
1014 checkValidDataCon con
1015 = checkValidType ctxt (idType (dataConWrapId con)) `thenM_`
1016 -- This checks the argument types and
1017 -- ambiguity of the existential context (if any)
1018 addErrCtxt (existentialCtxt con)
1019 (checkFreeness ex_tvs ex_theta)
1021 ctxt = ConArgCtxt (dataConName con)
1022 (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
1025 fieldTypeMisMatch field_name
1026 = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
1028 existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
1029 <+> quotes (ppr con)
1033 checkValidClass is called once the mutually-recursive knot has been
1034 tied, so we can look at things freely.
1037 checkValidClass :: Class -> TcM ()
1039 = -- CHECK ARITY 1 FOR HASKELL 1.4
1040 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
1042 -- Check that the class is unary, unless GlaExs
1043 checkTc (notNull tyvars) (nullaryClassErr cls) `thenM_`
1044 checkTc (gla_exts || unary) (classArityErr cls) `thenM_`
1046 -- Check the super-classes
1047 checkValidTheta (ClassSCCtxt (className cls)) theta `thenM_`
1049 -- Check the class operations
1050 mappM_ check_op op_stuff `thenM_`
1052 -- Check that if the class has generic methods, then the
1053 -- class has only one parameter. We can't do generic
1054 -- multi-parameter type classes!
1055 checkTc (unary || no_generics) (genericMultiParamErr cls)
1058 (tyvars, theta, _, op_stuff) = classBigSig cls
1059 unary = isSingleton tyvars
1060 no_generics = null [() | (_, GenDefMeth) <- op_stuff]
1062 check_op (sel_id, dm)
1063 = checkValidTheta SigmaCtxt (tail theta) `thenM_`
1064 -- The 'tail' removes the initial (C a) from the
1065 -- class itself, leaving just the method type
1067 checkValidType (FunSigCtxt op_name) tau `thenM_`
1069 -- Check that for a generic method, the type of
1070 -- the method is sufficiently simple
1071 checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
1072 (badGenericMethodType op_name op_ty)
1074 op_name = idName sel_id
1075 op_ty = idType sel_id
1076 (_,theta,tau) = tcSplitSigmaTy op_ty
1079 = ptext SLIT("No parameters for class") <+> quotes (ppr cls)
1082 = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
1083 parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
1085 genericMultiParamErr clas
1086 = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
1087 ptext SLIT("cannot have generic methods")
1089 badGenericMethodType op op_ty
1090 = hang (ptext SLIT("Generic method type is too complex"))
1091 4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
1092 ptext SLIT("You can only use type variables, arrows, and tuples")])
1096 %************************************************************************
1098 \subsection{Checking for a decent instance head type}
1100 %************************************************************************
1102 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1103 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1105 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1106 flag is on, or (2)~the instance is imported (they must have been
1107 compiled elsewhere). In these cases, we let them go through anyway.
1109 We can also have instances for functions: @instance Foo (a -> b) ...@.
1112 checkValidInstHead :: Type -> TcM (Class, [TcType])
1114 checkValidInstHead ty -- Should be a source type
1115 = case tcSplitPredTy_maybe ty of {
1116 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1119 case getClassPredTys_maybe pred of {
1120 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1123 getDOpts `thenM` \ dflags ->
1124 mappM_ check_arg_type tys `thenM_`
1125 check_inst_head dflags clas tys `thenM_`
1129 check_inst_head dflags clas tys
1131 -- A user declaration of a CCallable/CReturnable instance
1132 -- must be for a "boxed primitive" type.
1133 (clas `hasKey` cCallableClassKey
1134 && not (ccallable_type first_ty))
1135 || (clas `hasKey` cReturnableClassKey
1136 && not (creturnable_type first_ty))
1137 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1139 -- If GlasgowExts then check at least one isn't a type variable
1140 | dopt Opt_GlasgowExts dflags
1141 = check_tyvars dflags clas tys
1143 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1145 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1146 not (isSynTyCon tycon), -- ...but not a synonym
1147 all tcIsTyVarTy arg_tys, -- Applied to type variables
1148 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1149 -- This last condition checks that all the type variables are distinct
1153 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1156 (first_ty : _) = tys
1158 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
1159 creturnable_type ty = isFFIImportResultTy dflags ty
1161 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1162 text "where T is not a synonym, and a,b,c are distinct type variables")
1164 check_tyvars dflags clas tys
1165 -- Check that at least one isn't a type variable
1166 -- unless -fallow-undecideable-instances
1167 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1168 | not (all tcIsTyVarTy tys) = returnM ()
1169 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1171 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1174 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1178 instTypeErr pp_ty msg
1179 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1182 nonBoxedPrimCCallErr clas inst_ty
1183 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1184 4 (pprClassPred clas [inst_ty])