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, newOpenTypeKind,
18 putTcTyVar, getTcTyVar,
19 newMutTyVar, readMutTyVar, writeMutTyVar,
21 --------------------------------
23 tcInstTyVar, tcInstTyVars, tcInstType,
25 --------------------------------
26 -- Checking type validity
27 Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
28 SourceTyCtxt(..), checkValidTheta,
29 checkValidTyCon, checkValidClass,
30 checkValidInstHead, instTypeErr, checkAmbiguity,
33 --------------------------------
36 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
37 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
38 zonkTcPredType, zonkTcTyVarToTyVar, zonkKindEnv,
42 #include "HsVersions.h"
46 import TypeRep ( Type(..), SourceType(..), TyNote(..), -- Friend; can see representation
47 Kind, ThetaType, typeCon
49 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
50 TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
51 tcEqType, tcCmpPred, isClassPred,
52 tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
53 tcSplitTyConApp_maybe, tcSplitForAllTys,
54 tcIsTyVarTy, tcSplitSigmaTy, mkTyConApp,
55 isUnLiftedType, isIPPred, isTyVarTy,
57 mkAppTy, mkTyVarTy, mkTyVarTys,
58 tyVarsOfPred, getClassPredTys_maybe,
60 liftedTypeKind, openTypeKind, defaultKind, superKind,
61 superBoxity, liftedBoxity, typeKind,
62 tyVarsOfType, tyVarsOfTypes,
64 isFFIArgumentTy, isFFIImportResultTy
66 import Subst ( Subst, mkTopTyVarSubst, substTy )
67 import Class ( Class, DefMeth(..), classArity, className, classBigSig )
68 import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
69 tyConArity, tyConName, tyConTheta,
70 getSynTyConDefn, tyConDataCons )
71 import DataCon ( DataCon, dataConWrapId, dataConName, dataConSig, dataConFieldLabels )
72 import FieldLabel ( fieldLabelName, fieldLabelType )
73 import Var ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar,
74 mkTyVar, mkMutTyVar, isMutTyVar, mutTyVarRef )
77 import Generics ( validGenericMethodType )
78 import TcRnMonad -- TcType, amongst others
79 import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
80 import ForeignCall ( Safety(..) )
81 import FunDeps ( grow )
82 import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
83 import Name ( Name, setNameUnique, mkSystemTvNameEncoded )
85 import CmdLineOpts ( dopt, DynFlag(..) )
86 import Util ( nOfThem, isSingleton, equalLength, notNull, lengthExceeds )
87 import ListSetOps ( equivClasses, removeDups )
92 %************************************************************************
94 \subsection{New type variables}
96 %************************************************************************
99 newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar
100 newMutTyVar name kind details
101 = do { ref <- newMutVar Nothing ;
102 return (mkMutTyVar name kind details ref) }
104 readMutTyVar :: TyVar -> TcM (Maybe Type)
105 readMutTyVar tyvar = readMutVar (mutTyVarRef tyvar)
107 writeMutTyVar :: TyVar -> Maybe Type -> TcM ()
108 writeMutTyVar tyvar val = writeMutVar (mutTyVarRef tyvar) val
110 newTyVar :: Kind -> TcM TcTyVar
112 = newUnique `thenM` \ uniq ->
113 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
115 newTyVarTy :: Kind -> TcM TcType
117 = newTyVar kind `thenM` \ tc_tyvar ->
118 returnM (TyVarTy tc_tyvar)
120 newTyVarTys :: Int -> Kind -> TcM [TcType]
121 newTyVarTys n kind = mappM newTyVarTy (nOfThem n kind)
123 newKindVar :: TcM TcKind
125 = newUnique `thenM` \ uniq ->
126 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv `thenM` \ kv ->
129 newKindVars :: Int -> TcM [TcKind]
130 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
132 newOpenTypeKind :: TcM TcKind -- Returns the kind (Type bx), where bx is fresh
134 = newUnique `thenM` \ uniq ->
135 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) superBoxity VanillaTv `thenM` \ kv ->
136 returnM (mkTyConApp typeCon [TyVarTy kv])
140 %************************************************************************
142 \subsection{Type instantiation}
144 %************************************************************************
146 Instantiating a bunch of type variables
149 tcInstTyVars :: TyVarDetails -> [TyVar]
150 -> TcM ([TcTyVar], [TcType], Subst)
152 tcInstTyVars tv_details tyvars
153 = mappM (tcInstTyVar tv_details) tyvars `thenM` \ tc_tyvars ->
155 tys = mkTyVarTys tc_tyvars
157 returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
158 -- Since the tyvars are freshly made,
159 -- they cannot possibly be captured by
160 -- any existing for-alls. Hence mkTopTyVarSubst
162 tcInstTyVar tv_details tyvar
163 = newUnique `thenM` \ uniq ->
165 name = setNameUnique (tyVarName tyvar) uniq
166 -- Note that we don't change the print-name
167 -- This won't confuse the type checker but there's a chance
168 -- that two different tyvars will print the same way
169 -- in an error message. -dppr-debug will show up the difference
170 -- Better watch out for this. If worst comes to worst, just
173 newMutTyVar name (tyVarKind tyvar) tv_details
175 tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
176 -- tcInstType instantiates the outer-level for-alls of a TcType with
177 -- fresh (mutable) type variables, splits off the dictionary part,
178 -- and returns the pieces.
179 tcInstType tv_details ty
180 = case tcSplitForAllTys ty of
181 ([], rho) -> -- There may be overloading despite no type variables;
182 -- (?x :: Int) => Int -> Int
184 (theta, tau) = tcSplitPhiTy rho
186 returnM ([], theta, tau)
188 (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenM` \ (tyvars', _, tenv) ->
190 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
192 returnM (tyvars', theta, tau)
196 %************************************************************************
198 \subsection{Putting and getting mutable type variables}
200 %************************************************************************
203 putTcTyVar :: TcTyVar -> TcType -> TcM TcType
204 getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
211 | not (isMutTyVar tyvar)
212 = pprTrace "putTcTyVar" (ppr tyvar) $
216 = ASSERT( isMutTyVar tyvar )
217 writeMutTyVar tyvar (Just ty) `thenM_`
221 Getting is more interesting. The easy thing to do is just to read, thus:
224 getTcTyVar tyvar = readMutTyVar tyvar
227 But it's more fun to short out indirections on the way: If this
228 version returns a TyVar, then that TyVar is unbound. If it returns
229 any other type, then there might be bound TyVars embedded inside it.
231 We return Nothing iff the original box was unbound.
235 | not (isMutTyVar tyvar)
236 = pprTrace "getTcTyVar" (ppr tyvar) $
237 returnM (Just (mkTyVarTy tyvar))
240 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
241 readMutTyVar tyvar `thenM` \ maybe_ty ->
243 Just ty -> short_out ty `thenM` \ ty' ->
244 writeMutTyVar tyvar (Just ty') `thenM_`
247 Nothing -> returnM Nothing
249 short_out :: TcType -> TcM TcType
250 short_out ty@(TyVarTy tyvar)
251 | not (isMutTyVar tyvar)
255 = readMutTyVar tyvar `thenM` \ maybe_ty ->
257 Just ty' -> short_out ty' `thenM` \ ty' ->
258 writeMutTyVar tyvar (Just ty') `thenM_`
263 short_out other_ty = returnM other_ty
267 %************************************************************************
269 \subsection{Zonking -- the exernal interfaces}
271 %************************************************************************
273 ----------------- Type variables
276 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
277 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
279 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
280 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
281 returnM (tyVarsOfTypes tys)
283 zonkTcTyVar :: TcTyVar -> TcM TcType
284 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
287 ----------------- Types
290 zonkTcType :: TcType -> TcM TcType
291 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
293 zonkTcTypes :: [TcType] -> TcM [TcType]
294 zonkTcTypes tys = mappM zonkTcType tys
296 zonkTcClassConstraints cts = mappM zonk cts
297 where zonk (clas, tys)
298 = zonkTcTypes tys `thenM` \ new_tys ->
299 returnM (clas, new_tys)
301 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
302 zonkTcThetaType theta = mappM zonkTcPredType theta
304 zonkTcPredType :: TcPredType -> TcM TcPredType
305 zonkTcPredType (ClassP c ts)
306 = zonkTcTypes ts `thenM` \ new_ts ->
307 returnM (ClassP c new_ts)
308 zonkTcPredType (IParam n t)
309 = zonkTcType t `thenM` \ new_t ->
310 returnM (IParam n new_t)
313 ------------------- These ...ToType, ...ToKind versions
314 are used at the end of type checking
317 zonkKindEnv :: [(Name, TcKind)] -> TcM [(Name, Kind)]
319 = mappM zonk_it pairs
321 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenM` \ kind ->
324 -- When zonking a kind, we want to
325 -- zonk a *kind* variable to (Type *)
326 -- zonk a *boxity* variable to *
327 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
328 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
329 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
331 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
332 -- of a type variable, at the *end* of type checking. It changes
333 -- the *mutable* type variable into an *immutable* one.
335 -- It does this by making an immutable version of tv and binds tv to it.
336 -- Now any bound occurences of the original type variable will get
337 -- zonked to the immutable version.
339 zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
340 zonkTcTyVarToTyVar tv
342 -- Make an immutable version, defaulting
343 -- the kind to lifted if necessary
344 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
345 immut_tv_ty = mkTyVarTy immut_tv
347 zap tv = putTcTyVar tv immut_tv_ty
348 -- Bind the mutable version to the immutable one
350 -- If the type variable is mutable, then bind it to immut_tv_ty
351 -- so that all other occurrences of the tyvar will get zapped too
352 zonkTyVar zap tv `thenM` \ ty2 ->
354 -- This warning shows up if the allegedly-unbound tyvar is
355 -- already bound to something. It can actually happen, and
356 -- in a harmless way (see [Silly Type Synonyms] below) so
357 -- it's only a warning
358 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
363 [Silly Type Synonyms]
366 type C u a = u -- Note 'a' unused
368 foo :: (forall a. C u a -> C u a) -> u
372 bar = foo (\t -> t + t)
374 * From the (\t -> t+t) we get type {Num d} => d -> d
377 * Now unify with type of foo's arg, and we get:
378 {Num (C d a)} => C d a -> C d a
381 * Now abstract over the 'a', but float out the Num (C d a) constraint
382 because it does not 'really' mention a. (see Type.tyVarsOfType)
383 The arg to foo becomes
386 * So we get a dict binding for Num (C d a), which is zonked to give
389 * Then the /\a abstraction has a zonked 'a' in it.
391 All very silly. I think its harmless to ignore the problem.
394 %************************************************************************
396 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
398 %* For internal use only! *
400 %************************************************************************
403 -- zonkType is used for Kinds as well
405 -- For unbound, mutable tyvars, zonkType uses the function given to it
406 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
407 -- type variable and zonks the kind too
409 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
410 -- see zonkTcType, and zonkTcTypeToType
413 zonkType unbound_var_fn ty
416 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
417 returnM (TyConApp tycon tys')
419 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
420 go ty2 `thenM` \ ty2' ->
421 returnM (NoteTy (SynNote ty1') ty2')
423 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
425 go (SourceTy p) = go_pred p `thenM` \ p' ->
426 returnM (SourceTy p')
428 go (FunTy arg res) = go arg `thenM` \ arg' ->
429 go res `thenM` \ res' ->
430 returnM (FunTy arg' res')
432 go (AppTy fun arg) = go fun `thenM` \ fun' ->
433 go arg `thenM` \ arg' ->
434 returnM (mkAppTy fun' arg')
435 -- NB the mkAppTy; we might have instantiated a
436 -- type variable to a type constructor, so we need
437 -- to pull the TyConApp to the top.
439 -- The two interesting cases!
440 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
442 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenM` \ tyvar' ->
443 go ty `thenM` \ ty' ->
444 returnM (ForAllTy tyvar' ty')
446 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
447 returnM (ClassP c tys')
448 go_pred (NType tc tys) = mappM go tys `thenM` \ tys' ->
449 returnM (NType tc tys')
450 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
451 returnM (IParam n ty')
453 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
454 -> TcTyVar -> TcM TcType
455 zonkTyVar unbound_var_fn tyvar
456 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
457 -- zonking a forall type, when the bound type variable
458 -- needn't be mutable
459 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
460 returnM (TyVarTy tyvar)
463 = getTcTyVar tyvar `thenM` \ maybe_ty ->
465 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
466 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
471 %************************************************************************
473 \subsection{Checking a user type}
475 %************************************************************************
477 When dealing with a user-written type, we first translate it from an HsType
478 to a Type, performing kind checking, and then check various things that should
479 be true about it. We don't want to perform these checks at the same time
480 as the initial translation because (a) they are unnecessary for interface-file
481 types and (b) when checking a mutually recursive group of type and class decls,
482 we can't "look" at the tycons/classes yet. Also, the checks are are rather
483 diverse, and used to really mess up the other code.
485 One thing we check for is 'rank'.
487 Rank 0: monotypes (no foralls)
488 Rank 1: foralls at the front only, Rank 0 inside
489 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
491 basic ::= tyvar | T basic ... basic
493 r2 ::= forall tvs. cxt => r2a
494 r2a ::= r1 -> r2a | basic
495 r1 ::= forall tvs. cxt => r0
496 r0 ::= r0 -> r0 | basic
498 Another thing is to check that type synonyms are saturated.
499 This might not necessarily show up in kind checking.
501 data T k = MkT (k Int)
507 = FunSigCtxt Name -- Function type signature
508 | ExprSigCtxt -- Expression type signature
509 | ConArgCtxt Name -- Data constructor argument
510 | TySynCtxt Name -- RHS of a type synonym decl
511 | GenPatCtxt -- Pattern in generic decl
512 -- f{| a+b |} (Inl x) = ...
513 | PatSigCtxt -- Type sig in pattern
515 | ResSigCtxt -- Result type sig
517 | ForSigCtxt Name -- Foreign inport or export signature
518 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
520 -- Notes re TySynCtxt
521 -- We allow type synonyms that aren't types; e.g. type List = []
523 -- If the RHS mentions tyvars that aren't in scope, we'll
524 -- quantify over them:
525 -- e.g. type T = a->a
526 -- will become type T = forall a. a->a
528 -- With gla-exts that's right, but for H98 we should complain.
531 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
532 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
533 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
534 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
535 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
536 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
537 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
538 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
539 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
543 checkValidType :: UserTypeCtxt -> Type -> TcM ()
544 -- Checks that the type is valid for the given context
545 checkValidType ctxt ty
546 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
548 rank | gla_exts = Arbitrary
550 = case ctxt of -- Haskell 98
554 TySynCtxt _ -> Rank 0
555 ExprSigCtxt -> Rank 1
556 FunSigCtxt _ -> Rank 1
557 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
558 -- constructor, hence rank 1
559 ForSigCtxt _ -> Rank 1
560 RuleSigCtxt _ -> Rank 1
562 actual_kind = typeKind ty
564 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
566 kind_ok = case ctxt of
567 TySynCtxt _ -> True -- Any kind will do
568 GenPatCtxt -> actual_kind_is_lifted
569 ForSigCtxt _ -> actual_kind_is_lifted
570 other -> isTypeKind actual_kind
572 ubx_tup | not gla_exts = UT_NotOk
573 | otherwise = case ctxt of
576 -- Unboxed tuples ok in function results,
577 -- but for type synonyms we allow them even at
580 addErrCtxt (checkTypeCtxt ctxt ty) $
582 -- Check that the thing has kind Type, and is lifted if necessary
583 checkTc kind_ok (kindErr actual_kind) `thenM_`
585 -- Check the internal validity of the type itself
586 check_poly_type rank ubx_tup ty
589 checkTypeCtxt ctxt ty
590 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
591 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
593 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
594 -- something strange like {Eq k} -> k -> k, because there is no
595 -- ForAll at the top of the type. Since this is going to the user
596 -- we want it to look like a proper Haskell type even then; hence the hack
598 -- This shows up in the complaint about
600 -- op :: Eq a => a -> a
601 ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
604 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
609 data Rank = Rank Int | Arbitrary
611 decRank :: Rank -> Rank
612 decRank Arbitrary = Arbitrary
613 decRank (Rank n) = Rank (n-1)
615 ----------------------------------------
616 data UbxTupFlag = UT_Ok | UT_NotOk
617 -- The "Ok" version means "ok if -fglasgow-exts is on"
619 ----------------------------------------
620 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
621 check_poly_type (Rank 0) ubx_tup ty
622 = check_tau_type (Rank 0) ubx_tup ty
624 check_poly_type rank ubx_tup ty
626 (tvs, theta, tau) = tcSplitSigmaTy ty
628 check_valid_theta SigmaCtxt theta `thenM_`
629 check_tau_type (decRank rank) ubx_tup tau `thenM_`
630 checkFreeness tvs theta `thenM_`
631 checkAmbiguity tvs theta (tyVarsOfType tau)
633 ----------------------------------------
634 check_arg_type :: Type -> TcM ()
635 -- The sort of type that can instantiate a type variable,
636 -- or be the argument of a type constructor.
637 -- Not an unboxed tuple, not a forall.
638 -- Other unboxed types are very occasionally allowed as type
639 -- arguments depending on the kind of the type constructor
641 -- For example, we want to reject things like:
643 -- instance Ord a => Ord (forall s. T s a)
645 -- g :: T s (forall b.b)
647 -- NB: unboxed tuples can have polymorphic or unboxed args.
648 -- This happens in the workers for functions returning
649 -- product types with polymorphic components.
650 -- But not in user code.
651 -- Anyway, they are dealt with by a special case in check_tau_type
654 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
655 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
657 ----------------------------------------
658 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
659 -- Rank is allowed rank for function args
660 -- No foralls otherwise
662 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
663 check_tau_type rank ubx_tup (SourceTy sty) = getDOpts `thenM` \ dflags ->
664 check_source_ty dflags TypeCtxt sty
665 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
666 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
667 = check_poly_type rank UT_NotOk arg_ty `thenM_`
668 check_tau_type rank UT_Ok res_ty
670 check_tau_type rank ubx_tup (AppTy ty1 ty2)
671 = check_arg_type ty1 `thenM_` check_arg_type ty2
673 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
674 -- Synonym notes are built only when the synonym is
675 -- saturated (see Type.mkSynTy)
676 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
678 -- If -fglasgow-exts then don't check the 'note' part.
679 -- This allows us to instantiate a synonym defn with a
680 -- for-all type, or with a partially-applied type synonym.
681 -- e.g. type T a b = a
684 -- Here, T is partially applied, so it's illegal in H98.
685 -- But if you expand S first, then T we get just
690 -- For H98, do check the un-expanded part
691 check_tau_type rank ubx_tup syn
694 check_tau_type rank ubx_tup ty
696 check_tau_type rank ubx_tup (NoteTy other_note ty)
697 = check_tau_type rank ubx_tup ty
699 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
701 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
702 -- synonym application, leaving it to checkValidType (i.e. right here)
704 checkTc syn_arity_ok arity_msg `thenM_`
705 mappM_ check_arg_type tys
707 | isUnboxedTupleTyCon tc
708 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
709 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
710 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
711 -- Args are allowed to be unlifted, or
712 -- more unboxed tuples, so can't use check_arg_ty
715 = mappM_ check_arg_type tys
718 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
720 syn_arity_ok = tc_arity <= n_args
721 -- It's OK to have an *over-applied* type synonym
722 -- data Tree a b = ...
723 -- type Foo a = Tree [a]
724 -- f :: Foo a b -> ...
726 tc_arity = tyConArity tc
728 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
729 ubx_tup_msg = ubxArgTyErr ty
731 ----------------------------------------
732 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
733 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
734 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
735 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
740 %************************************************************************
742 \subsection{Checking a theta or source type}
744 %************************************************************************
747 -- Enumerate the contexts in which a "source type", <S>, can occur
751 -- or (N a) where N is a newtype
754 = ClassSCCtxt Name -- Superclasses of clas
755 -- class <S> => C a where ...
756 | SigmaCtxt -- Theta part of a normal for-all type
757 -- f :: <S> => a -> a
758 | DataTyCtxt Name -- Theta part of a data decl
759 -- data <S> => T a = MkT a
760 | TypeCtxt -- Source type in an ordinary type
762 | InstThetaCtxt -- Context of an instance decl
763 -- instance <S> => C [a] where ...
764 | InstHeadCtxt -- Head of an instance decl
765 -- instance ... => Eq a where ...
767 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
768 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
769 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
770 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
771 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
772 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
776 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
777 checkValidTheta ctxt theta
778 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
780 -------------------------
781 check_valid_theta ctxt []
783 check_valid_theta ctxt theta
784 = getDOpts `thenM` \ dflags ->
785 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
786 -- Actually, in instance decls and type signatures,
787 -- duplicate constraints are eliminated by TcMonoType.hoistForAllTys,
788 -- so this error can only fire for the context of a class or
790 mappM_ (check_source_ty dflags ctxt) theta
792 (_,dups) = removeDups tcCmpPred theta
794 -------------------------
795 check_source_ty dflags ctxt pred@(ClassP cls tys)
796 = -- Class predicates are valid in all contexts
797 mappM_ check_arg_type tys `thenM_`
798 checkTc (arity == n_tys) arity_err `thenM_`
799 checkTc (check_class_pred_tys dflags ctxt tys)
800 (predTyVarErr pred $$ how_to_allow)
803 class_name = className cls
804 arity = classArity cls
806 arity_err = arityErr "Class" class_name arity n_tys
808 how_to_allow = case ctxt of
809 InstHeadCtxt -> empty -- Should not happen
810 InstThetaCtxt -> parens undecidableMsg
811 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
813 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
814 -- Implicit parameters only allows in type
815 -- signatures; not in instance decls, superclasses etc
816 -- The reason for not allowing implicit params in instances is a bit subtle
817 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
818 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
819 -- discharge all the potential usas of the ?x in e. For example, a
820 -- constraint Foo [Int] might come out of e,and applying the
821 -- instance decl would show up two uses of ?x.
823 check_source_ty dflags TypeCtxt (NType tc tys) = mappM_ check_arg_type tys
826 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
828 -------------------------
829 check_class_pred_tys dflags ctxt tys
831 InstHeadCtxt -> True -- We check for instance-head
832 -- formation in checkValidInstHead
833 InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
834 other -> gla_exts || all tyvar_head tys
836 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
837 gla_exts = dopt Opt_GlasgowExts dflags
839 -------------------------
840 tyvar_head ty -- Haskell 98 allows predicates of form
841 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
842 | otherwise -- where a is a type variable
843 = case tcSplitAppTy_maybe ty of
844 Just (ty, _) -> tyvar_head ty
851 is ambiguous if P contains generic variables
852 (i.e. one of the Vs) that are not mentioned in tau
854 However, we need to take account of functional dependencies
855 when we speak of 'mentioned in tau'. Example:
856 class C a b | a -> b where ...
858 forall x y. (C x y) => x
859 is not ambiguous because x is mentioned and x determines y
861 NB; the ambiguity check is only used for *user* types, not for types
862 coming from inteface files. The latter can legitimately have
863 ambiguous types. Example
865 class S a where s :: a -> (Int,Int)
866 instance S Char where s _ = (1,1)
867 f:: S a => [a] -> Int -> (Int,Int)
868 f (_::[a]) x = (a*x,b)
869 where (a,b) = s (undefined::a)
871 Here the worker for f gets the type
872 fw :: forall a. S a => Int -> (# Int, Int #)
874 If the list of tv_names is empty, we have a monotype, and then we
875 don't need to check for ambiguity either, because the test can't fail
879 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
880 checkAmbiguity forall_tyvars theta tau_tyvars
881 = mappM_ complain (filter is_ambig theta)
883 complain pred = addErrTc (ambigErr pred)
884 extended_tau_vars = grow theta tau_tyvars
886 -- Only a *class* predicate can give rise to ambiguity
887 -- An *implicit parameter* cannot. For example:
888 -- foo :: (?x :: [a]) => Int
890 -- is fine. The call site will suppply a particular 'x'
891 is_ambig pred = isClassPred pred &&
892 any ambig_var (varSetElems (tyVarsOfPred pred))
894 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
895 not (ct_var `elemVarSet` extended_tau_vars)
898 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
899 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
900 ptext SLIT("must be reachable from the type after the '=>'"))]
903 In addition, GHC insists that at least one type variable
904 in each constraint is in V. So we disallow a type like
905 forall a. Eq b => b -> b
906 even in a scope where b is in scope.
909 checkFreeness forall_tyvars theta
910 = mappM_ complain (filter is_free theta)
912 is_free pred = not (isIPPred pred)
913 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
914 bound_var ct_var = ct_var `elem` forall_tyvars
915 complain pred = addErrTc (freeErr pred)
918 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
919 ptext SLIT("are already in scope"),
920 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
925 checkThetaCtxt ctxt theta
926 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
927 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
929 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
930 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
931 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
933 arityErr kind name n m
934 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
935 n_arguments <> comma, text "but has been given", int m]
937 n_arguments | n == 0 = ptext SLIT("no arguments")
938 | n == 1 = ptext SLIT("1 argument")
939 | True = hsep [int n, ptext SLIT("arguments")]
943 %************************************************************************
945 \subsection{Validity check for TyCons}
947 %************************************************************************
949 checkValidTyCon is called once the mutually-recursive knot has been
950 tied, so we can look at things freely.
953 checkValidTyCon :: TyCon -> TcM ()
955 | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
957 = -- Check the context on the data decl
958 checkValidTheta (DataTyCtxt name) (tyConTheta tc) `thenM_`
960 -- Check arg types of data constructors
961 mappM_ checkValidDataCon data_cons `thenM_`
963 -- Check that fields with the same name share a type
964 mappM_ check_fields groups
968 (_, syn_rhs) = getSynTyConDefn tc
969 data_cons = tyConDataCons tc
971 fields = [field | con <- data_cons, field <- dataConFieldLabels con]
972 groups = equivClasses cmp_name fields
973 cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
975 check_fields fields@(first_field_label : other_fields)
976 -- These fields all have the same name, but are from
977 -- different constructors in the data type
978 = -- Check that all the fields in the group have the same type
979 -- NB: this check assumes that all the constructors of a given
980 -- data type use the same type variables
981 checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
983 field_ty = fieldLabelType first_field_label
984 field_name = fieldLabelName first_field_label
985 other_tys = map fieldLabelType other_fields
987 checkValidDataCon :: DataCon -> TcM ()
988 checkValidDataCon con
989 = checkValidType ctxt (idType (dataConWrapId con)) `thenM_`
990 -- This checks the argument types and
991 -- ambiguity of the existential context (if any)
992 addErrCtxt (existentialCtxt con)
993 (checkFreeness ex_tvs ex_theta)
995 ctxt = ConArgCtxt (dataConName con)
996 (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
999 fieldTypeMisMatch field_name
1000 = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
1002 existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
1003 <+> quotes (ppr con)
1007 checkValidClass is called once the mutually-recursive knot has been
1008 tied, so we can look at things freely.
1011 checkValidClass :: Class -> TcM ()
1013 = -- CHECK ARITY 1 FOR HASKELL 1.4
1014 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
1016 -- Check that the class is unary, unless GlaExs
1017 checkTc (notNull tyvars) (nullaryClassErr cls) `thenM_`
1018 checkTc (gla_exts || unary) (classArityErr cls) `thenM_`
1020 -- Check the super-classes
1021 checkValidTheta (ClassSCCtxt (className cls)) theta `thenM_`
1023 -- Check the class operations
1024 mappM_ check_op op_stuff `thenM_`
1026 -- Check that if the class has generic methods, then the
1027 -- class has only one parameter. We can't do generic
1028 -- multi-parameter type classes!
1029 checkTc (unary || no_generics) (genericMultiParamErr cls)
1032 (tyvars, theta, _, op_stuff) = classBigSig cls
1033 unary = isSingleton tyvars
1034 no_generics = null [() | (_, GenDefMeth) <- op_stuff]
1036 check_op (sel_id, dm)
1037 = checkValidTheta SigmaCtxt (tail theta) `thenM_`
1038 -- The 'tail' removes the initial (C a) from the
1039 -- class itself, leaving just the method type
1041 checkValidType (FunSigCtxt op_name) tau `thenM_`
1043 -- Check that for a generic method, the type of
1044 -- the method is sufficiently simple
1045 checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
1046 (badGenericMethodType op_name op_ty)
1048 op_name = idName sel_id
1049 op_ty = idType sel_id
1050 (_,theta,tau) = tcSplitSigmaTy op_ty
1053 = ptext SLIT("No parameters for class") <+> quotes (ppr cls)
1056 = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
1057 parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
1059 genericMultiParamErr clas
1060 = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
1061 ptext SLIT("cannot have generic methods")
1063 badGenericMethodType op op_ty
1064 = hang (ptext SLIT("Generic method type is too complex"))
1065 4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
1066 ptext SLIT("You can only use type variables, arrows, and tuples")])
1070 %************************************************************************
1072 \subsection{Checking for a decent instance head type}
1074 %************************************************************************
1076 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1077 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1079 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1080 flag is on, or (2)~the instance is imported (they must have been
1081 compiled elsewhere). In these cases, we let them go through anyway.
1083 We can also have instances for functions: @instance Foo (a -> b) ...@.
1086 checkValidInstHead :: Type -> TcM (Class, [TcType])
1088 checkValidInstHead ty -- Should be a source type
1089 = case tcSplitPredTy_maybe ty of {
1090 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1093 case getClassPredTys_maybe pred of {
1094 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1097 getDOpts `thenM` \ dflags ->
1098 mappM_ check_arg_type tys `thenM_`
1099 check_inst_head dflags clas tys `thenM_`
1103 check_inst_head dflags clas tys
1105 -- A user declaration of a CCallable/CReturnable instance
1106 -- must be for a "boxed primitive" type.
1107 (clas `hasKey` cCallableClassKey
1108 && not (ccallable_type first_ty))
1109 || (clas `hasKey` cReturnableClassKey
1110 && not (creturnable_type first_ty))
1111 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1113 -- If GlasgowExts then check at least one isn't a type variable
1114 | dopt Opt_GlasgowExts dflags
1115 = check_tyvars dflags clas tys
1117 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1119 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1120 not (isSynTyCon tycon), -- ...but not a synonym
1121 all tcIsTyVarTy arg_tys, -- Applied to type variables
1122 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1123 -- This last condition checks that all the type variables are distinct
1127 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1130 (first_ty : _) = tys
1132 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
1133 creturnable_type ty = isFFIImportResultTy dflags ty
1135 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1136 text "where T is not a synonym, and a,b,c are distinct type variables")
1138 check_tyvars dflags clas tys
1139 -- Check that at least one isn't a type variable
1140 -- unless -fallow-undecideable-instances
1141 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1142 | not (all tcIsTyVarTy tys) = returnM ()
1143 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1145 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1148 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1152 instTypeErr pp_ty msg
1153 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1156 nonBoxedPrimCCallErr clas inst_ty
1157 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1158 4 (pprClassPred clas [inst_ty])