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 Subst ( Subst, mkTopTyVarSubst, substTy )
69 import Class ( Class, DefMeth(..), classArity, className, classBigSig )
70 import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
71 tyConArity, tyConName, tyConTheta,
72 getSynTyConDefn, tyConDataCons )
73 import DataCon ( DataCon, dataConWrapId, dataConName, dataConSig, dataConFieldLabels )
74 import FieldLabel ( fieldLabelName, fieldLabelType )
75 import Var ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar,
76 mkTyVar, mkMutTyVar, isMutTyVar, mutTyVarRef )
79 import Generics ( validGenericMethodType )
80 import TcRnMonad -- TcType, amongst others
81 import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
82 import ForeignCall ( Safety(..) )
83 import FunDeps ( grow )
84 import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
85 import Name ( Name, setNameUnique, mkSystemTvNameEncoded )
87 import CmdLineOpts ( dopt, DynFlag(..) )
88 import Util ( nOfThem, isSingleton, equalLength, notNull )
89 import ListSetOps ( equivClasses, removeDups )
94 %************************************************************************
96 \subsection{New type variables}
98 %************************************************************************
101 newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar
102 newMutTyVar name kind details
103 = do { ref <- newMutVar Nothing ;
104 return (mkMutTyVar name kind details ref) }
106 readMutTyVar :: TyVar -> TcM (Maybe Type)
107 readMutTyVar tyvar = readMutVar (mutTyVarRef tyvar)
109 writeMutTyVar :: TyVar -> Maybe Type -> TcM ()
110 writeMutTyVar tyvar val = writeMutVar (mutTyVarRef tyvar) val
112 newTyVar :: Kind -> TcM TcTyVar
114 = newUnique `thenM` \ uniq ->
115 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
117 newTyVarTy :: Kind -> TcM TcType
119 = newTyVar kind `thenM` \ tc_tyvar ->
120 returnM (TyVarTy tc_tyvar)
122 newTyVarTys :: Int -> Kind -> TcM [TcType]
123 newTyVarTys n kind = mappM newTyVarTy (nOfThem n kind)
125 newKindVar :: TcM TcKind
127 = newUnique `thenM` \ uniq ->
128 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv `thenM` \ kv ->
131 newKindVars :: Int -> TcM [TcKind]
132 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
134 newBoxityVar :: TcM TcKind
136 = newUnique `thenM` \ uniq ->
137 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) superBoxity VanillaTv `thenM` \ kv ->
142 %************************************************************************
144 \subsection{'hole' type variables}
146 %************************************************************************
149 newHoleTyVarTy :: TcM TcType
150 = newUnique `thenM` \ uniq ->
151 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("h")) openTypeKind HoleTv `thenM` \ tv ->
154 readHoleResult :: TcType -> TcM TcType
155 -- Read the answer out of a hole, constructed by newHoleTyVarTy
156 readHoleResult (TyVarTy tv)
157 = ASSERT( isHoleTyVar tv )
158 getTcTyVar tv `thenM` \ maybe_res ->
160 Just ty -> returnM ty
161 Nothing -> pprPanic "readHoleResult: empty" (ppr tv)
162 readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
164 zapToType :: TcType -> TcM TcType
165 zapToType (TyVarTy tv)
167 = getTcTyVar tv `thenM` \ maybe_res ->
169 Nothing -> newTyVarTy openTypeKind `thenM` \ ty ->
170 putTcTyVar tv ty `thenM_`
172 Just ty -> returnM ty -- No need to loop; we never
173 -- have chains of holes
175 zapToType other_ty = returnM other_ty
178 %************************************************************************
180 \subsection{Type instantiation}
182 %************************************************************************
184 Instantiating a bunch of type variables
187 tcInstTyVars :: TyVarDetails -> [TyVar]
188 -> TcM ([TcTyVar], [TcType], Subst)
190 tcInstTyVars tv_details tyvars
191 = mappM (tcInstTyVar tv_details) tyvars `thenM` \ tc_tyvars ->
193 tys = mkTyVarTys tc_tyvars
195 returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
196 -- Since the tyvars are freshly made,
197 -- they cannot possibly be captured by
198 -- any existing for-alls. Hence mkTopTyVarSubst
200 tcInstTyVar tv_details tyvar
201 = newUnique `thenM` \ uniq ->
203 name = setNameUnique (tyVarName tyvar) uniq
204 -- Note that we don't change the print-name
205 -- This won't confuse the type checker but there's a chance
206 -- that two different tyvars will print the same way
207 -- in an error message. -dppr-debug will show up the difference
208 -- Better watch out for this. If worst comes to worst, just
211 newMutTyVar name (tyVarKind tyvar) tv_details
213 tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
214 -- tcInstType instantiates the outer-level for-alls of a TcType with
215 -- fresh (mutable) type variables, splits off the dictionary part,
216 -- and returns the pieces.
217 tcInstType tv_details ty
218 = case tcSplitForAllTys ty of
219 ([], rho) -> -- There may be overloading despite no type variables;
220 -- (?x :: Int) => Int -> Int
222 (theta, tau) = tcSplitPhiTy rho
224 returnM ([], theta, tau)
226 (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenM` \ (tyvars', _, tenv) ->
228 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
230 returnM (tyvars', theta, tau)
234 %************************************************************************
236 \subsection{Putting and getting mutable type variables}
238 %************************************************************************
241 putTcTyVar :: TcTyVar -> TcType -> TcM TcType
242 getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
249 | not (isMutTyVar tyvar)
250 = pprTrace "putTcTyVar" (ppr tyvar) $
254 = ASSERT( isMutTyVar tyvar )
255 writeMutTyVar tyvar (Just ty) `thenM_`
259 Getting is more interesting. The easy thing to do is just to read, thus:
262 getTcTyVar tyvar = readMutTyVar tyvar
265 But it's more fun to short out indirections on the way: If this
266 version returns a TyVar, then that TyVar is unbound. If it returns
267 any other type, then there might be bound TyVars embedded inside it.
269 We return Nothing iff the original box was unbound.
273 | not (isMutTyVar tyvar)
274 = pprTrace "getTcTyVar" (ppr tyvar) $
275 returnM (Just (mkTyVarTy tyvar))
278 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
279 readMutTyVar tyvar `thenM` \ maybe_ty ->
281 Just ty -> short_out ty `thenM` \ ty' ->
282 writeMutTyVar tyvar (Just ty') `thenM_`
285 Nothing -> returnM Nothing
287 short_out :: TcType -> TcM TcType
288 short_out ty@(TyVarTy tyvar)
289 | not (isMutTyVar tyvar)
293 = readMutTyVar tyvar `thenM` \ maybe_ty ->
295 Just ty' -> short_out ty' `thenM` \ ty' ->
296 writeMutTyVar tyvar (Just ty') `thenM_`
301 short_out other_ty = returnM other_ty
305 %************************************************************************
307 \subsection{Zonking -- the exernal interfaces}
309 %************************************************************************
311 ----------------- Type variables
314 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
315 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
317 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
318 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
319 returnM (tyVarsOfTypes tys)
321 zonkTcTyVar :: TcTyVar -> TcM TcType
322 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
325 ----------------- Types
328 zonkTcType :: TcType -> TcM TcType
329 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
331 zonkTcTypes :: [TcType] -> TcM [TcType]
332 zonkTcTypes tys = mappM zonkTcType tys
334 zonkTcClassConstraints cts = mappM zonk cts
335 where zonk (clas, tys)
336 = zonkTcTypes tys `thenM` \ new_tys ->
337 returnM (clas, new_tys)
339 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
340 zonkTcThetaType theta = mappM zonkTcPredType theta
342 zonkTcPredType :: TcPredType -> TcM TcPredType
343 zonkTcPredType (ClassP c ts)
344 = zonkTcTypes ts `thenM` \ new_ts ->
345 returnM (ClassP c new_ts)
346 zonkTcPredType (IParam n t)
347 = zonkTcType t `thenM` \ new_t ->
348 returnM (IParam n new_t)
351 ------------------- These ...ToType, ...ToKind versions
352 are used at the end of type checking
355 zonkKindEnv :: [(Name, TcKind)] -> TcM [(Name, Kind)]
357 = mappM zonk_it pairs
359 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenM` \ kind ->
362 -- When zonking a kind, we want to
363 -- zonk a *kind* variable to (Type *)
364 -- zonk a *boxity* variable to *
365 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
366 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
367 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
369 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
370 -- of a type variable, at the *end* of type checking. It changes
371 -- the *mutable* type variable into an *immutable* one.
373 -- It does this by making an immutable version of tv and binds tv to it.
374 -- Now any bound occurences of the original type variable will get
375 -- zonked to the immutable version.
377 zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
378 zonkTcTyVarToTyVar tv
380 -- Make an immutable version, defaulting
381 -- the kind to lifted if necessary
382 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
383 immut_tv_ty = mkTyVarTy immut_tv
385 zap tv = putTcTyVar tv immut_tv_ty
386 -- Bind the mutable version to the immutable one
388 -- If the type variable is mutable, then bind it to immut_tv_ty
389 -- so that all other occurrences of the tyvar will get zapped too
390 zonkTyVar zap tv `thenM` \ ty2 ->
392 -- This warning shows up if the allegedly-unbound tyvar is
393 -- already bound to something. It can actually happen, and
394 -- in a harmless way (see [Silly Type Synonyms] below) so
395 -- it's only a warning
396 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
401 [Silly Type Synonyms]
404 type C u a = u -- Note 'a' unused
406 foo :: (forall a. C u a -> C u a) -> u
410 bar = foo (\t -> t + t)
412 * From the (\t -> t+t) we get type {Num d} => d -> d
415 * Now unify with type of foo's arg, and we get:
416 {Num (C d a)} => C d a -> C d a
419 * Now abstract over the 'a', but float out the Num (C d a) constraint
420 because it does not 'really' mention a. (see Type.tyVarsOfType)
421 The arg to foo becomes
424 * So we get a dict binding for Num (C d a), which is zonked to give
427 * Then the /\a abstraction has a zonked 'a' in it.
429 All very silly. I think its harmless to ignore the problem.
432 %************************************************************************
434 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
436 %* For internal use only! *
438 %************************************************************************
441 -- zonkType is used for Kinds as well
443 -- For unbound, mutable tyvars, zonkType uses the function given to it
444 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
445 -- type variable and zonks the kind too
447 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
448 -- see zonkTcType, and zonkTcTypeToType
451 zonkType unbound_var_fn ty
454 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
455 returnM (TyConApp tycon tys')
457 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
458 go ty2 `thenM` \ ty2' ->
459 returnM (NoteTy (SynNote ty1') ty2')
461 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
463 go (SourceTy p) = go_pred p `thenM` \ p' ->
464 returnM (SourceTy p')
466 go (FunTy arg res) = go arg `thenM` \ arg' ->
467 go res `thenM` \ res' ->
468 returnM (FunTy arg' res')
470 go (AppTy fun arg) = go fun `thenM` \ fun' ->
471 go arg `thenM` \ arg' ->
472 returnM (mkAppTy fun' arg')
473 -- NB the mkAppTy; we might have instantiated a
474 -- type variable to a type constructor, so we need
475 -- to pull the TyConApp to the top.
477 -- The two interesting cases!
478 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
480 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenM` \ tyvar' ->
481 go ty `thenM` \ ty' ->
482 returnM (ForAllTy tyvar' ty')
484 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
485 returnM (ClassP c tys')
486 go_pred (NType tc tys) = mappM go tys `thenM` \ tys' ->
487 returnM (NType tc tys')
488 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
489 returnM (IParam n ty')
491 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
492 -> TcTyVar -> TcM TcType
493 zonkTyVar unbound_var_fn tyvar
494 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
495 -- zonking a forall type, when the bound type variable
496 -- needn't be mutable
497 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
498 returnM (TyVarTy tyvar)
501 = getTcTyVar tyvar `thenM` \ maybe_ty ->
503 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
504 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
509 %************************************************************************
511 \subsection{Checking a user type}
513 %************************************************************************
515 When dealing with a user-written type, we first translate it from an HsType
516 to a Type, performing kind checking, and then check various things that should
517 be true about it. We don't want to perform these checks at the same time
518 as the initial translation because (a) they are unnecessary for interface-file
519 types and (b) when checking a mutually recursive group of type and class decls,
520 we can't "look" at the tycons/classes yet. Also, the checks are are rather
521 diverse, and used to really mess up the other code.
523 One thing we check for is 'rank'.
525 Rank 0: monotypes (no foralls)
526 Rank 1: foralls at the front only, Rank 0 inside
527 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
529 basic ::= tyvar | T basic ... basic
531 r2 ::= forall tvs. cxt => r2a
532 r2a ::= r1 -> r2a | basic
533 r1 ::= forall tvs. cxt => r0
534 r0 ::= r0 -> r0 | basic
536 Another thing is to check that type synonyms are saturated.
537 This might not necessarily show up in kind checking.
539 data T k = MkT (k Int)
545 = FunSigCtxt Name -- Function type signature
546 | ExprSigCtxt -- Expression type signature
547 | ConArgCtxt Name -- Data constructor argument
548 | TySynCtxt Name -- RHS of a type synonym decl
549 | GenPatCtxt -- Pattern in generic decl
550 -- f{| a+b |} (Inl x) = ...
551 | PatSigCtxt -- Type sig in pattern
553 | ResSigCtxt -- Result type sig
555 | ForSigCtxt Name -- Foreign inport or export signature
556 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
558 -- Notes re TySynCtxt
559 -- We allow type synonyms that aren't types; e.g. type List = []
561 -- If the RHS mentions tyvars that aren't in scope, we'll
562 -- quantify over them:
563 -- e.g. type T = a->a
564 -- will become type T = forall a. a->a
566 -- With gla-exts that's right, but for H98 we should complain.
569 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
570 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
571 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
572 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
573 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
574 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
575 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
576 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
577 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
581 checkValidType :: UserTypeCtxt -> Type -> TcM ()
582 -- Checks that the type is valid for the given context
583 checkValidType ctxt ty
584 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
586 rank | gla_exts = Arbitrary
588 = case ctxt of -- Haskell 98
592 TySynCtxt _ -> Rank 0
593 ExprSigCtxt -> Rank 1
594 FunSigCtxt _ -> Rank 1
595 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
596 -- constructor, hence rank 1
597 ForSigCtxt _ -> Rank 1
598 RuleSigCtxt _ -> Rank 1
600 actual_kind = typeKind ty
602 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
604 kind_ok = case ctxt of
605 TySynCtxt _ -> True -- Any kind will do
606 GenPatCtxt -> actual_kind_is_lifted
607 ForSigCtxt _ -> actual_kind_is_lifted
608 other -> isTypeKind actual_kind
610 ubx_tup | not gla_exts = UT_NotOk
611 | otherwise = case ctxt of
614 -- Unboxed tuples ok in function results,
615 -- but for type synonyms we allow them even at
618 addErrCtxt (checkTypeCtxt ctxt ty) $
620 -- Check that the thing has kind Type, and is lifted if necessary
621 checkTc kind_ok (kindErr actual_kind) `thenM_`
623 -- Check the internal validity of the type itself
624 check_poly_type rank ubx_tup ty
627 checkTypeCtxt ctxt ty
628 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
629 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
631 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
632 -- something strange like {Eq k} -> k -> k, because there is no
633 -- ForAll at the top of the type. Since this is going to the user
634 -- we want it to look like a proper Haskell type even then; hence the hack
636 -- This shows up in the complaint about
638 -- op :: Eq a => a -> a
639 ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
642 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
647 data Rank = Rank Int | Arbitrary
649 decRank :: Rank -> Rank
650 decRank Arbitrary = Arbitrary
651 decRank (Rank n) = Rank (n-1)
653 ----------------------------------------
654 data UbxTupFlag = UT_Ok | UT_NotOk
655 -- The "Ok" version means "ok if -fglasgow-exts is on"
657 ----------------------------------------
658 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
659 check_poly_type (Rank 0) ubx_tup ty
660 = check_tau_type (Rank 0) ubx_tup ty
662 check_poly_type rank ubx_tup ty
664 (tvs, theta, tau) = tcSplitSigmaTy ty
666 check_valid_theta SigmaCtxt theta `thenM_`
667 check_tau_type (decRank rank) ubx_tup tau `thenM_`
668 checkFreeness tvs theta `thenM_`
669 checkAmbiguity tvs theta (tyVarsOfType tau)
671 ----------------------------------------
672 check_arg_type :: Type -> TcM ()
673 -- The sort of type that can instantiate a type variable,
674 -- or be the argument of a type constructor.
675 -- Not an unboxed tuple, not a forall.
676 -- Other unboxed types are very occasionally allowed as type
677 -- arguments depending on the kind of the type constructor
679 -- For example, we want to reject things like:
681 -- instance Ord a => Ord (forall s. T s a)
683 -- g :: T s (forall b.b)
685 -- NB: unboxed tuples can have polymorphic or unboxed args.
686 -- This happens in the workers for functions returning
687 -- product types with polymorphic components.
688 -- But not in user code.
689 -- Anyway, they are dealt with by a special case in check_tau_type
692 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
693 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
695 ----------------------------------------
696 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
697 -- Rank is allowed rank for function args
698 -- No foralls otherwise
700 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
701 check_tau_type rank ubx_tup (SourceTy sty) = getDOpts `thenM` \ dflags ->
702 check_source_ty dflags TypeCtxt sty
703 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
704 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
705 = check_poly_type rank UT_NotOk arg_ty `thenM_`
706 check_tau_type rank UT_Ok res_ty
708 check_tau_type rank ubx_tup (AppTy ty1 ty2)
709 = check_arg_type ty1 `thenM_` check_arg_type ty2
711 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
712 -- Synonym notes are built only when the synonym is
713 -- saturated (see Type.mkSynTy)
714 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
716 -- If -fglasgow-exts then don't check the 'note' part.
717 -- This allows us to instantiate a synonym defn with a
718 -- for-all type, or with a partially-applied type synonym.
719 -- e.g. type T a b = a
722 -- Here, T is partially applied, so it's illegal in H98.
723 -- But if you expand S first, then T we get just
728 -- For H98, do check the un-expanded part
729 check_tau_type rank ubx_tup syn
732 check_tau_type rank ubx_tup ty
734 check_tau_type rank ubx_tup (NoteTy other_note ty)
735 = check_tau_type rank ubx_tup ty
737 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
739 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
740 -- synonym application, leaving it to checkValidType (i.e. right here)
742 checkTc syn_arity_ok arity_msg `thenM_`
743 mappM_ check_arg_type tys
745 | isUnboxedTupleTyCon tc
746 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
747 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
748 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
749 -- Args are allowed to be unlifted, or
750 -- more unboxed tuples, so can't use check_arg_ty
753 = mappM_ check_arg_type tys
756 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
758 syn_arity_ok = tc_arity <= n_args
759 -- It's OK to have an *over-applied* type synonym
760 -- data Tree a b = ...
761 -- type Foo a = Tree [a]
762 -- f :: Foo a b -> ...
764 tc_arity = tyConArity tc
766 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
767 ubx_tup_msg = ubxArgTyErr ty
769 ----------------------------------------
770 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
771 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
772 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
773 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
778 %************************************************************************
780 \subsection{Checking a theta or source type}
782 %************************************************************************
786 = ClassSCCtxt Name -- Superclasses of clas
787 | SigmaCtxt -- Context of a normal for-all type
788 | DataTyCtxt Name -- Context of a data decl
789 | TypeCtxt -- Source type in an ordinary type
790 | InstThetaCtxt -- Context of an instance decl
791 | InstHeadCtxt -- Head of an instance decl
793 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
794 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
795 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
796 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
797 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
798 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
802 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
803 checkValidTheta ctxt theta
804 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
806 -------------------------
807 check_valid_theta ctxt []
809 check_valid_theta ctxt theta
810 = getDOpts `thenM` \ dflags ->
811 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
812 -- Actually, in instance decls and type signatures,
813 -- duplicate constraints are eliminated by TcMonoType.hoistForAllTys,
814 -- so this error can only fire for the context of a class or
816 mappM_ (check_source_ty dflags ctxt) theta
818 (_,dups) = removeDups tcCmpPred theta
820 -------------------------
821 check_source_ty dflags ctxt pred@(ClassP cls tys)
822 = -- Class predicates are valid in all contexts
823 mappM_ check_arg_type tys `thenM_`
824 checkTc (arity == n_tys) arity_err `thenM_`
825 checkTc (check_class_pred_tys dflags ctxt tys)
826 (predTyVarErr pred $$ how_to_allow)
829 class_name = className cls
830 arity = classArity cls
832 arity_err = arityErr "Class" class_name arity n_tys
834 how_to_allow = case ctxt of
835 InstHeadCtxt -> empty -- Should not happen
836 InstThetaCtxt -> parens undecidableMsg
837 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
839 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
840 -- Implicit parameters only allows in type
841 -- signatures; not in instance decls, superclasses etc
842 -- The reason for not allowing implicit params in instances is a bit subtle
843 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
844 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
845 -- discharge all the potential usas of the ?x in e. For example, a
846 -- constraint Foo [Int] might come out of e,and applying the
847 -- instance decl would show up two uses of ?x.
849 check_source_ty dflags TypeCtxt (NType tc tys) = mappM_ check_arg_type tys
852 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
854 -------------------------
855 check_class_pred_tys dflags ctxt tys
857 InstHeadCtxt -> True -- We check for instance-head
858 -- formation in checkValidInstHead
859 InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
860 other -> gla_exts || all tyvar_head tys
862 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
863 gla_exts = dopt Opt_GlasgowExts dflags
865 -------------------------
866 tyvar_head ty -- Haskell 98 allows predicates of form
867 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
868 | otherwise -- where a is a type variable
869 = case tcSplitAppTy_maybe ty of
870 Just (ty, _) -> tyvar_head ty
877 is ambiguous if P contains generic variables
878 (i.e. one of the Vs) that are not mentioned in tau
880 However, we need to take account of functional dependencies
881 when we speak of 'mentioned in tau'. Example:
882 class C a b | a -> b where ...
884 forall x y. (C x y) => x
885 is not ambiguous because x is mentioned and x determines y
887 NB; the ambiguity check is only used for *user* types, not for types
888 coming from inteface files. The latter can legitimately have
889 ambiguous types. Example
891 class S a where s :: a -> (Int,Int)
892 instance S Char where s _ = (1,1)
893 f:: S a => [a] -> Int -> (Int,Int)
894 f (_::[a]) x = (a*x,b)
895 where (a,b) = s (undefined::a)
897 Here the worker for f gets the type
898 fw :: forall a. S a => Int -> (# Int, Int #)
900 If the list of tv_names is empty, we have a monotype, and then we
901 don't need to check for ambiguity either, because the test can't fail
905 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
906 checkAmbiguity forall_tyvars theta tau_tyvars
907 = mappM_ complain (filter is_ambig theta)
909 complain pred = addErrTc (ambigErr pred)
910 extended_tau_vars = grow theta tau_tyvars
911 is_ambig pred = any ambig_var (varSetElems (tyVarsOfPred pred))
913 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
914 not (ct_var `elemVarSet` extended_tau_vars)
916 is_free ct_var = not (ct_var `elem` forall_tyvars)
919 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
920 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
921 ptext SLIT("must be reachable from the type after the '=>'"))]
924 In addition, GHC insists that at least one type variable
925 in each constraint is in V. So we disallow a type like
926 forall a. Eq b => b -> b
927 even in a scope where b is in scope.
930 checkFreeness forall_tyvars theta
931 = mappM_ complain (filter is_free theta)
933 is_free pred = not (isIPPred pred)
934 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
935 bound_var ct_var = ct_var `elem` forall_tyvars
936 complain pred = addErrTc (freeErr pred)
939 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
940 ptext SLIT("are already in scope"),
941 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
946 checkThetaCtxt ctxt theta
947 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
948 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
950 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
951 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
952 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
954 arityErr kind name n m
955 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
956 n_arguments <> comma, text "but has been given", int m]
958 n_arguments | n == 0 = ptext SLIT("no arguments")
959 | n == 1 = ptext SLIT("1 argument")
960 | True = hsep [int n, ptext SLIT("arguments")]
964 %************************************************************************
966 \subsection{Validity check for TyCons}
968 %************************************************************************
970 checkValidTyCon is called once the mutually-recursive knot has been
971 tied, so we can look at things freely.
974 checkValidTyCon :: TyCon -> TcM ()
976 | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
978 = -- Check the context on the data decl
979 checkValidTheta (DataTyCtxt name) (tyConTheta tc) `thenM_`
981 -- Check arg types of data constructors
982 mappM_ checkValidDataCon data_cons `thenM_`
984 -- Check that fields with the same name share a type
985 mappM_ check_fields groups
989 (_, syn_rhs) = getSynTyConDefn tc
990 data_cons = tyConDataCons tc
992 fields = [field | con <- data_cons, field <- dataConFieldLabels con]
993 groups = equivClasses cmp_name fields
994 cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
996 check_fields fields@(first_field_label : other_fields)
997 -- These fields all have the same name, but are from
998 -- different constructors in the data type
999 = -- Check that all the fields in the group have the same type
1000 -- NB: this check assumes that all the constructors of a given
1001 -- data type use the same type variables
1002 checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
1004 field_ty = fieldLabelType first_field_label
1005 field_name = fieldLabelName first_field_label
1006 other_tys = map fieldLabelType other_fields
1008 checkValidDataCon :: DataCon -> TcM ()
1009 checkValidDataCon con
1010 = checkValidType ctxt (idType (dataConWrapId con)) `thenM_`
1011 -- This checks the argument types and
1012 -- ambiguity of the existential context (if any)
1013 addErrCtxt (existentialCtxt con)
1014 (checkFreeness ex_tvs ex_theta)
1016 ctxt = ConArgCtxt (dataConName con)
1017 (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
1020 fieldTypeMisMatch field_name
1021 = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
1023 existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
1024 <+> quotes (ppr con)
1028 checkValidClass is called once the mutually-recursive knot has been
1029 tied, so we can look at things freely.
1032 checkValidClass :: Class -> TcM ()
1034 = -- CHECK ARITY 1 FOR HASKELL 1.4
1035 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
1037 -- Check that the class is unary, unless GlaExs
1038 checkTc (notNull tyvars) (nullaryClassErr cls) `thenM_`
1039 checkTc (gla_exts || unary) (classArityErr cls) `thenM_`
1041 -- Check the super-classes
1042 checkValidTheta (ClassSCCtxt (className cls)) theta `thenM_`
1044 -- Check the class operations
1045 mappM_ check_op op_stuff `thenM_`
1047 -- Check that if the class has generic methods, then the
1048 -- class has only one parameter. We can't do generic
1049 -- multi-parameter type classes!
1050 checkTc (unary || no_generics) (genericMultiParamErr cls)
1053 (tyvars, theta, _, op_stuff) = classBigSig cls
1054 unary = isSingleton tyvars
1055 no_generics = null [() | (_, GenDefMeth) <- op_stuff]
1057 check_op (sel_id, dm)
1058 = checkValidTheta SigmaCtxt (tail theta) `thenM_`
1059 -- The 'tail' removes the initial (C a) from the
1060 -- class itself, leaving just the method type
1062 checkValidType (FunSigCtxt op_name) tau `thenM_`
1064 -- Check that for a generic method, the type of
1065 -- the method is sufficiently simple
1066 checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
1067 (badGenericMethodType op_name op_ty)
1069 op_name = idName sel_id
1070 op_ty = idType sel_id
1071 (_,theta,tau) = tcSplitSigmaTy op_ty
1074 = ptext SLIT("No parameters for class") <+> quotes (ppr cls)
1077 = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
1078 parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
1080 genericMultiParamErr clas
1081 = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
1082 ptext SLIT("cannot have generic methods")
1084 badGenericMethodType op op_ty
1085 = hang (ptext SLIT("Generic method type is too complex"))
1086 4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
1087 ptext SLIT("You can only use type variables, arrows, and tuples")])
1091 %************************************************************************
1093 \subsection{Checking for a decent instance head type}
1095 %************************************************************************
1097 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1098 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1100 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1101 flag is on, or (2)~the instance is imported (they must have been
1102 compiled elsewhere). In these cases, we let them go through anyway.
1104 We can also have instances for functions: @instance Foo (a -> b) ...@.
1107 checkValidInstHead :: Type -> TcM (Class, [TcType])
1109 checkValidInstHead ty -- Should be a source type
1110 = case tcSplitPredTy_maybe ty of {
1111 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1114 case getClassPredTys_maybe pred of {
1115 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1118 getDOpts `thenM` \ dflags ->
1119 mappM_ check_arg_type tys `thenM_`
1120 check_inst_head dflags clas tys `thenM_`
1124 check_inst_head dflags clas tys
1126 -- A user declaration of a CCallable/CReturnable instance
1127 -- must be for a "boxed primitive" type.
1128 (clas `hasKey` cCallableClassKey
1129 && not (ccallable_type first_ty))
1130 || (clas `hasKey` cReturnableClassKey
1131 && not (creturnable_type first_ty))
1132 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1134 -- If GlasgowExts then check at least one isn't a type variable
1135 | dopt Opt_GlasgowExts dflags
1136 = check_tyvars dflags clas tys
1138 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1140 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1141 not (isSynTyCon tycon), -- ...but not a synonym
1142 all tcIsTyVarTy arg_tys, -- Applied to type variables
1143 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1144 -- This last condition checks that all the type variables are distinct
1148 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1151 (first_ty : _) = tys
1153 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
1154 creturnable_type ty = isFFIImportResultTy dflags ty
1156 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1157 text "where T is not a synonym, and a,b,c are distinct type variables")
1159 check_tyvars dflags clas tys
1160 -- Check that at least one isn't a type variable
1161 -- unless -fallow-undecideable-instances
1162 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1163 | not (all tcIsTyVarTy tys) = returnM ()
1164 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1166 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1169 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1173 instTypeErr pp_ty msg
1174 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1177 nonBoxedPrimCCallErr clas inst_ty
1178 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1179 4 (pprClassPred clas [inst_ty])