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
14 newTyVar, newSigTyVar,
15 newTyVarTy, -- Kind -> TcM TcType
16 newTyVarTys, -- Int -> Kind -> TcM [TcType]
17 newKindVar, newKindVars,
18 putTcTyVar, getTcTyVar,
19 newMutTyVar, readMutTyVar, writeMutTyVar,
21 --------------------------------
23 tcInstTyVar, tcInstTyVars, tcInstType,
25 --------------------------------
26 -- Checking type validity
27 Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
28 SourceTyCtxt(..), checkValidTheta, checkFreeness,
29 checkValidInstHead, instTypeErr, checkAmbiguity,
32 --------------------------------
35 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
36 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
37 zonkTcPredType, zonkTcTyVarToTyVar,
38 zonkTcKindToKind, zonkTcKind,
40 readKindVar, writeKindVar
44 #include "HsVersions.h"
48 import HsSyn ( LHsType )
49 import TypeRep ( Type(..), PredType(..), TyNote(..), -- Friend; can see representation
52 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
53 TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
54 tcEqType, tcCmpPred, isClassPred,
55 tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
56 tcSplitTyConApp_maybe, tcSplitForAllTys,
57 tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy,
58 isUnLiftedType, isIPPred,
60 mkAppTy, mkTyVarTy, mkTyVarTys,
61 tyVarsOfPred, getClassPredTys_maybe,
62 tyVarsOfType, tyVarsOfTypes,
63 pprPred, pprTheta, pprClassPred )
64 import Kind ( Kind(..), KindVar(..), mkKindVar,
65 isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
68 import Subst ( Subst, mkTopTyVarSubst, substTy )
69 import Class ( Class, classArity, className )
70 import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
71 tyConArity, tyConName )
72 import Var ( TyVar, tyVarKind, tyVarName, isTyVar,
73 mkTyVar, mkTcTyVar, tcTyVarRef, isTcTyVar )
76 import TcRnMonad -- TcType, amongst others
77 import FunDeps ( grow )
78 import Name ( Name, setNameUnique, mkSysTvName )
80 import CmdLineOpts ( dopt, DynFlag(..) )
81 import Util ( nOfThem, isSingleton, equalLength, notNull )
82 import ListSetOps ( removeDups )
83 import SrcLoc ( unLoc )
88 %************************************************************************
90 \subsection{New type variables}
92 %************************************************************************
95 newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar
96 newMutTyVar name kind details
97 = do { ref <- newMutVar Nothing ;
98 return (mkTcTyVar name kind details ref) }
100 readMutTyVar :: TyVar -> TcM (Maybe Type)
101 readMutTyVar tyvar = readMutVar (tcTyVarRef tyvar)
103 writeMutTyVar :: TyVar -> Maybe Type -> TcM ()
104 writeMutTyVar tyvar val = writeMutVar (tcTyVarRef tyvar) val
106 newTyVar :: Kind -> TcM TcTyVar
108 = newUnique `thenM` \ uniq ->
109 newMutTyVar (mkSysTvName uniq FSLIT("t")) kind VanillaTv
111 newSigTyVar :: Kind -> TcM TcTyVar
113 = newUnique `thenM` \ uniq ->
114 newMutTyVar (mkSysTvName uniq FSLIT("s")) kind SigTv
116 newTyVarTy :: Kind -> TcM TcType
118 = newTyVar kind `thenM` \ tc_tyvar ->
119 returnM (TyVarTy tc_tyvar)
121 newTyVarTys :: Int -> Kind -> TcM [TcType]
122 newTyVarTys n kind = mappM newTyVarTy (nOfThem n kind)
124 newKindVar :: TcM TcKind
125 newKindVar = do { uniq <- newUnique
126 ; ref <- newMutVar Nothing
127 ; return (KindVar (mkKindVar uniq ref)) }
129 newKindVars :: Int -> TcM [TcKind]
130 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
134 %************************************************************************
136 \subsection{Type instantiation}
138 %************************************************************************
140 Instantiating a bunch of type variables
143 tcInstTyVars :: TyVarDetails -> [TyVar]
144 -> TcM ([TcTyVar], [TcType], Subst)
146 tcInstTyVars tv_details tyvars
147 = mappM (tcInstTyVar tv_details) tyvars `thenM` \ tc_tyvars ->
149 tys = mkTyVarTys tc_tyvars
151 returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
152 -- Since the tyvars are freshly made,
153 -- they cannot possibly be captured by
154 -- any existing for-alls. Hence mkTopTyVarSubst
156 tcInstTyVar tv_details tyvar
157 = newUnique `thenM` \ uniq ->
159 name = setNameUnique (tyVarName tyvar) uniq
160 -- Note that we don't change the print-name
161 -- This won't confuse the type checker but there's a chance
162 -- that two different tyvars will print the same way
163 -- in an error message. -dppr-debug will show up the difference
164 -- Better watch out for this. If worst comes to worst, just
167 newMutTyVar name (tyVarKind tyvar) tv_details
169 tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
170 -- tcInstType instantiates the outer-level for-alls of a TcType with
171 -- fresh (mutable) type variables, splits off the dictionary part,
172 -- and returns the pieces.
173 tcInstType tv_details ty
174 = case tcSplitForAllTys ty of
175 ([], rho) -> -- There may be overloading despite no type variables;
176 -- (?x :: Int) => Int -> Int
178 (theta, tau) = tcSplitPhiTy rho
180 returnM ([], theta, tau)
182 (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenM` \ (tyvars', _, tenv) ->
184 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
186 returnM (tyvars', theta, tau)
190 %************************************************************************
192 \subsection{Putting and getting mutable type variables}
194 %************************************************************************
197 putTcTyVar :: TcTyVar -> TcType -> TcM TcType
198 getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
205 | not (isTcTyVar tyvar)
206 = pprTrace "putTcTyVar" (ppr tyvar) $
210 = ASSERT( isTcTyVar tyvar )
211 writeMutTyVar tyvar (Just ty) `thenM_`
215 Getting is more interesting. The easy thing to do is just to read, thus:
218 getTcTyVar tyvar = readMutTyVar tyvar
221 But it's more fun to short out indirections on the way: If this
222 version returns a TyVar, then that TyVar is unbound. If it returns
223 any other type, then there might be bound TyVars embedded inside it.
225 We return Nothing iff the original box was unbound.
229 | not (isTcTyVar tyvar)
230 = pprTrace "getTcTyVar" (ppr tyvar) $
231 returnM (Just (mkTyVarTy tyvar))
234 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
235 readMutTyVar tyvar `thenM` \ maybe_ty ->
237 Just ty -> short_out ty `thenM` \ ty' ->
238 writeMutTyVar tyvar (Just ty') `thenM_`
241 Nothing -> returnM Nothing
243 short_out :: TcType -> TcM TcType
244 short_out ty@(TyVarTy tyvar)
245 | not (isTcTyVar tyvar)
249 = readMutTyVar tyvar `thenM` \ maybe_ty ->
251 Just ty' -> short_out ty' `thenM` \ ty' ->
252 writeMutTyVar tyvar (Just ty') `thenM_`
257 short_out other_ty = returnM other_ty
261 %************************************************************************
263 \subsection{Zonking -- the exernal interfaces}
265 %************************************************************************
267 ----------------- Type variables
270 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
271 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
273 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
274 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
275 returnM (tyVarsOfTypes tys)
277 zonkTcTyVar :: TcTyVar -> TcM TcType
278 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
281 ----------------- Types
284 zonkTcType :: TcType -> TcM TcType
285 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
287 zonkTcTypes :: [TcType] -> TcM [TcType]
288 zonkTcTypes tys = mappM zonkTcType tys
290 zonkTcClassConstraints cts = mappM zonk cts
291 where zonk (clas, tys)
292 = zonkTcTypes tys `thenM` \ new_tys ->
293 returnM (clas, new_tys)
295 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
296 zonkTcThetaType theta = mappM zonkTcPredType theta
298 zonkTcPredType :: TcPredType -> TcM TcPredType
299 zonkTcPredType (ClassP c ts)
300 = zonkTcTypes ts `thenM` \ new_ts ->
301 returnM (ClassP c new_ts)
302 zonkTcPredType (IParam n t)
303 = zonkTcType t `thenM` \ new_t ->
304 returnM (IParam n new_t)
307 ------------------- These ...ToType, ...ToKind versions
308 are used at the end of type checking
311 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
312 -- of a type variable, at the *end* of type checking. It changes
313 -- the *mutable* type variable into an *immutable* one.
315 -- It does this by making an immutable version of tv and binds tv to it.
316 -- Now any bound occurences of the original type variable will get
317 -- zonked to the immutable version.
319 zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
320 zonkTcTyVarToTyVar tv
322 -- Make an immutable version, defaulting
323 -- the kind to lifted if necessary
324 immut_tv = mkTyVar (tyVarName tv) (tyVarKind tv)
325 -- was: defaultKind (tyVarKind tv), but I don't
326 immut_tv_ty = mkTyVarTy immut_tv
328 zap tv = putTcTyVar tv immut_tv_ty
329 -- Bind the mutable version to the immutable one
331 -- If the type variable is mutable, then bind it to immut_tv_ty
332 -- so that all other occurrences of the tyvar will get zapped too
333 zonkTyVar zap tv `thenM` \ ty2 ->
335 -- This warning shows up if the allegedly-unbound tyvar is
336 -- already bound to something. It can actually happen, and
337 -- in a harmless way (see [Silly Type Synonyms] below) so
338 -- it's only a warning
339 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
344 [Silly Type Synonyms]
347 type C u a = u -- Note 'a' unused
349 foo :: (forall a. C u a -> C u a) -> u
353 bar = foo (\t -> t + t)
355 * From the (\t -> t+t) we get type {Num d} => d -> d
358 * Now unify with type of foo's arg, and we get:
359 {Num (C d a)} => C d a -> C d a
362 * Now abstract over the 'a', but float out the Num (C d a) constraint
363 because it does not 'really' mention a. (see Type.tyVarsOfType)
364 The arg to foo becomes
367 * So we get a dict binding for Num (C d a), which is zonked to give
370 * Then the /\a abstraction has a zonked 'a' in it.
372 All very silly. I think its harmless to ignore the problem.
375 %************************************************************************
377 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
379 %* For internal use only! *
381 %************************************************************************
384 -- For unbound, mutable tyvars, zonkType uses the function given to it
385 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
386 -- type variable and zonks the kind too
388 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
389 -- see zonkTcType, and zonkTcTypeToType
392 zonkType unbound_var_fn ty
395 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
396 returnM (TyConApp tycon tys')
398 go (NewTcApp tycon tys) = mappM go tys `thenM` \ tys' ->
399 returnM (NewTcApp tycon tys')
401 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
402 go ty2 `thenM` \ ty2' ->
403 returnM (NoteTy (SynNote ty1') ty2')
405 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
407 go (PredTy p) = go_pred p `thenM` \ p' ->
410 go (FunTy arg res) = go arg `thenM` \ arg' ->
411 go res `thenM` \ res' ->
412 returnM (FunTy arg' res')
414 go (AppTy fun arg) = go fun `thenM` \ fun' ->
415 go arg `thenM` \ arg' ->
416 returnM (mkAppTy fun' arg')
417 -- NB the mkAppTy; we might have instantiated a
418 -- type variable to a type constructor, so we need
419 -- to pull the TyConApp to the top.
421 -- The two interesting cases!
422 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
424 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenM` \ tyvar' ->
425 go ty `thenM` \ ty' ->
426 returnM (ForAllTy tyvar' ty')
428 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
429 returnM (ClassP c tys')
430 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
431 returnM (IParam n ty')
433 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
434 -> TcTyVar -> TcM TcType
435 zonkTyVar unbound_var_fn tyvar
436 | not (isTcTyVar tyvar) -- Not a mutable tyvar. This can happen when
437 -- zonking a forall type, when the bound type variable
438 -- needn't be mutable
439 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
440 returnM (TyVarTy tyvar)
443 = getTcTyVar tyvar `thenM` \ maybe_ty ->
445 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
446 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
451 %************************************************************************
455 %************************************************************************
458 readKindVar :: KindVar -> TcM (Maybe TcKind)
459 writeKindVar :: KindVar -> TcKind -> TcM ()
460 readKindVar (KVar _ ref) = readMutVar ref
461 writeKindVar (KVar _ ref) val = writeMutVar ref (Just val)
464 zonkTcKind :: TcKind -> TcM TcKind
465 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
466 ; k2' <- zonkTcKind k2
467 ; returnM (FunKind k1' k2') }
468 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
471 Just k -> zonkTcKind k }
472 zonkTcKind other_kind = returnM other_kind
475 zonkTcKindToKind :: TcKind -> TcM Kind
476 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
477 ; k2' <- zonkTcKindToKind k2
478 ; returnM (FunKind k1' k2') }
480 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
482 Nothing -> return liftedTypeKind
483 Just k -> zonkTcKindToKind k }
485 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
486 zonkTcKindToKind other_kind = returnM other_kind
489 %************************************************************************
491 \subsection{Checking a user type}
493 %************************************************************************
495 When dealing with a user-written type, we first translate it from an HsType
496 to a Type, performing kind checking, and then check various things that should
497 be true about it. We don't want to perform these checks at the same time
498 as the initial translation because (a) they are unnecessary for interface-file
499 types and (b) when checking a mutually recursive group of type and class decls,
500 we can't "look" at the tycons/classes yet. Also, the checks are are rather
501 diverse, and used to really mess up the other code.
503 One thing we check for is 'rank'.
505 Rank 0: monotypes (no foralls)
506 Rank 1: foralls at the front only, Rank 0 inside
507 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
509 basic ::= tyvar | T basic ... basic
511 r2 ::= forall tvs. cxt => r2a
512 r2a ::= r1 -> r2a | basic
513 r1 ::= forall tvs. cxt => r0
514 r0 ::= r0 -> r0 | basic
516 Another thing is to check that type synonyms are saturated.
517 This might not necessarily show up in kind checking.
519 data T k = MkT (k Int)
525 = FunSigCtxt Name -- Function type signature
526 | ExprSigCtxt -- Expression type signature
527 | ConArgCtxt Name -- Data constructor argument
528 | TySynCtxt Name -- RHS of a type synonym decl
529 | GenPatCtxt -- Pattern in generic decl
530 -- f{| a+b |} (Inl x) = ...
531 | PatSigCtxt -- Type sig in pattern
533 | ResSigCtxt -- Result type sig
535 | ForSigCtxt Name -- Foreign inport or export signature
536 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
537 | DefaultDeclCtxt -- Types in a default declaration
539 -- Notes re TySynCtxt
540 -- We allow type synonyms that aren't types; e.g. type List = []
542 -- If the RHS mentions tyvars that aren't in scope, we'll
543 -- quantify over them:
544 -- e.g. type T = a->a
545 -- will become type T = forall a. a->a
547 -- With gla-exts that's right, but for H98 we should complain.
550 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
551 pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt
553 pprUserTypeCtxt ty (FunSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
554 pprUserTypeCtxt ty ExprSigCtxt = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
555 pprUserTypeCtxt ty (ConArgCtxt c) = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
556 pprUserTypeCtxt ty (TySynCtxt c) = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
557 nest 2 (ptext SLIT(", namely") <+> ppr ty)]
558 pprUserTypeCtxt ty GenPatCtxt = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
559 pprUserTypeCtxt ty PatSigCtxt = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
560 pprUserTypeCtxt ty ResSigCtxt = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
561 pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
562 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
563 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
565 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
569 checkValidType :: UserTypeCtxt -> Type -> TcM ()
570 -- Checks that the type is valid for the given context
571 checkValidType ctxt ty
572 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
573 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
575 rank | gla_exts = Arbitrary
577 = case ctxt of -- Haskell 98
580 DefaultDeclCtxt-> Rank 0
582 TySynCtxt _ -> Rank 0
583 ExprSigCtxt -> Rank 1
584 FunSigCtxt _ -> Rank 1
585 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
586 -- constructor, hence rank 1
587 ForSigCtxt _ -> Rank 1
588 RuleSigCtxt _ -> Rank 1
590 actual_kind = typeKind ty
592 kind_ok = case ctxt of
593 TySynCtxt _ -> True -- Any kind will do
594 ResSigCtxt -> isOpenTypeKind actual_kind
595 ExprSigCtxt -> isOpenTypeKind actual_kind
596 GenPatCtxt -> isLiftedTypeKind actual_kind
597 ForSigCtxt _ -> isLiftedTypeKind actual_kind
598 other -> isArgTypeKind actual_kind
600 ubx_tup | not gla_exts = UT_NotOk
601 | otherwise = case ctxt of
605 -- Unboxed tuples ok in function results,
606 -- but for type synonyms we allow them even at
609 -- Check that the thing has kind Type, and is lifted if necessary
610 checkTc kind_ok (kindErr actual_kind) `thenM_`
612 -- Check the internal validity of the type itself
613 check_poly_type rank ubx_tup ty `thenM_`
615 traceTc (text "checkValidType done" <+> ppr ty)
620 data Rank = Rank Int | Arbitrary
622 decRank :: Rank -> Rank
623 decRank Arbitrary = Arbitrary
624 decRank (Rank n) = Rank (n-1)
626 ----------------------------------------
627 data UbxTupFlag = UT_Ok | UT_NotOk
628 -- The "Ok" version means "ok if -fglasgow-exts is on"
630 ----------------------------------------
631 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
632 check_poly_type (Rank 0) ubx_tup ty
633 = check_tau_type (Rank 0) ubx_tup ty
635 check_poly_type rank ubx_tup ty
637 (tvs, theta, tau) = tcSplitSigmaTy ty
639 check_valid_theta SigmaCtxt theta `thenM_`
640 check_tau_type (decRank rank) ubx_tup tau `thenM_`
641 checkFreeness tvs theta `thenM_`
642 checkAmbiguity tvs theta (tyVarsOfType tau)
644 ----------------------------------------
645 check_arg_type :: Type -> TcM ()
646 -- The sort of type that can instantiate a type variable,
647 -- or be the argument of a type constructor.
648 -- Not an unboxed tuple, not a forall.
649 -- Other unboxed types are very occasionally allowed as type
650 -- arguments depending on the kind of the type constructor
652 -- For example, we want to reject things like:
654 -- instance Ord a => Ord (forall s. T s a)
656 -- g :: T s (forall b.b)
658 -- NB: unboxed tuples can have polymorphic or unboxed args.
659 -- This happens in the workers for functions returning
660 -- product types with polymorphic components.
661 -- But not in user code.
662 -- Anyway, they are dealt with by a special case in check_tau_type
665 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
666 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
668 ----------------------------------------
669 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
670 -- Rank is allowed rank for function args
671 -- No foralls otherwise
673 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
674 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
675 check_source_ty dflags TypeCtxt sty
676 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
677 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
678 = check_poly_type rank UT_NotOk arg_ty `thenM_`
679 check_tau_type rank UT_Ok res_ty
681 check_tau_type rank ubx_tup (AppTy ty1 ty2)
682 = check_arg_type ty1 `thenM_` check_arg_type ty2
684 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
685 -- Synonym notes are built only when the synonym is
686 -- saturated (see Type.mkSynTy)
687 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
689 -- If -fglasgow-exts then don't check the 'note' part.
690 -- This allows us to instantiate a synonym defn with a
691 -- for-all type, or with a partially-applied type synonym.
692 -- e.g. type T a b = a
695 -- Here, T is partially applied, so it's illegal in H98.
696 -- But if you expand S first, then T we get just
701 -- For H98, do check the un-expanded part
702 check_tau_type rank ubx_tup syn
705 check_tau_type rank ubx_tup ty
707 check_tau_type rank ubx_tup (NoteTy other_note ty)
708 = check_tau_type rank ubx_tup ty
710 check_tau_type rank ubx_tup (NewTcApp tc tys)
711 = mappM_ check_arg_type tys
713 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
715 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
716 -- synonym application, leaving it to checkValidType (i.e. right here)
718 checkTc syn_arity_ok arity_msg `thenM_`
719 mappM_ check_arg_type tys
721 | isUnboxedTupleTyCon tc
722 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
723 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
724 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
725 -- Args are allowed to be unlifted, or
726 -- more unboxed tuples, so can't use check_arg_ty
729 = mappM_ check_arg_type tys
732 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
734 syn_arity_ok = tc_arity <= n_args
735 -- It's OK to have an *over-applied* type synonym
736 -- data Tree a b = ...
737 -- type Foo a = Tree [a]
738 -- f :: Foo a b -> ...
740 tc_arity = tyConArity tc
742 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
743 ubx_tup_msg = ubxArgTyErr ty
745 ----------------------------------------
746 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr ty
747 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
748 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
749 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
754 %************************************************************************
756 \subsection{Checking a theta or source type}
758 %************************************************************************
761 -- Enumerate the contexts in which a "source type", <S>, can occur
765 -- or (N a) where N is a newtype
768 = ClassSCCtxt Name -- Superclasses of clas
769 -- class <S> => C a where ...
770 | SigmaCtxt -- Theta part of a normal for-all type
771 -- f :: <S> => a -> a
772 | DataTyCtxt Name -- Theta part of a data decl
773 -- data <S> => T a = MkT a
774 | TypeCtxt -- Source type in an ordinary type
776 | InstThetaCtxt -- Context of an instance decl
777 -- instance <S> => C [a] where ...
778 | InstHeadCtxt -- Head of an instance decl
779 -- instance ... => Eq a where ...
781 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
782 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
783 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
784 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
785 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
786 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
790 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
791 checkValidTheta ctxt theta
792 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
794 -------------------------
795 check_valid_theta ctxt []
797 check_valid_theta ctxt theta
798 = getDOpts `thenM` \ dflags ->
799 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
800 -- Actually, in instance decls and type signatures,
801 -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
802 -- so this error can only fire for the context of a class or
804 mappM_ (check_source_ty dflags ctxt) theta
806 (_,dups) = removeDups tcCmpPred theta
808 -------------------------
809 check_source_ty dflags ctxt pred@(ClassP cls tys)
810 = -- Class predicates are valid in all contexts
811 checkTc (arity == n_tys) arity_err `thenM_`
813 -- Check the form of the argument types
814 mappM_ check_arg_type tys `thenM_`
815 checkTc (check_class_pred_tys dflags ctxt tys)
816 (predTyVarErr pred $$ how_to_allow)
819 class_name = className cls
820 arity = classArity cls
822 arity_err = arityErr "Class" class_name arity n_tys
824 how_to_allow = case ctxt of
825 InstHeadCtxt -> empty -- Should not happen
826 InstThetaCtxt -> parens undecidableMsg
827 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
829 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
830 -- Implicit parameters only allows in type
831 -- signatures; not in instance decls, superclasses etc
832 -- The reason for not allowing implicit params in instances is a bit subtle
833 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
834 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
835 -- discharge all the potential usas of the ?x in e. For example, a
836 -- constraint Foo [Int] might come out of e,and applying the
837 -- instance decl would show up two uses of ?x.
840 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
842 -------------------------
843 check_class_pred_tys dflags ctxt tys
845 InstHeadCtxt -> True -- We check for instance-head
846 -- formation in checkValidInstHead
847 InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
848 other -> gla_exts || all tyvar_head tys
850 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
851 gla_exts = dopt Opt_GlasgowExts dflags
853 -------------------------
854 tyvar_head ty -- Haskell 98 allows predicates of form
855 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
856 | otherwise -- where a is a type variable
857 = case tcSplitAppTy_maybe ty of
858 Just (ty, _) -> tyvar_head ty
865 is ambiguous if P contains generic variables
866 (i.e. one of the Vs) that are not mentioned in tau
868 However, we need to take account of functional dependencies
869 when we speak of 'mentioned in tau'. Example:
870 class C a b | a -> b where ...
872 forall x y. (C x y) => x
873 is not ambiguous because x is mentioned and x determines y
875 NB; the ambiguity check is only used for *user* types, not for types
876 coming from inteface files. The latter can legitimately have
877 ambiguous types. Example
879 class S a where s :: a -> (Int,Int)
880 instance S Char where s _ = (1,1)
881 f:: S a => [a] -> Int -> (Int,Int)
882 f (_::[a]) x = (a*x,b)
883 where (a,b) = s (undefined::a)
885 Here the worker for f gets the type
886 fw :: forall a. S a => Int -> (# Int, Int #)
888 If the list of tv_names is empty, we have a monotype, and then we
889 don't need to check for ambiguity either, because the test can't fail
893 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
894 checkAmbiguity forall_tyvars theta tau_tyvars
895 = mappM_ complain (filter is_ambig theta)
897 complain pred = addErrTc (ambigErr pred)
898 extended_tau_vars = grow theta tau_tyvars
900 -- Only a *class* predicate can give rise to ambiguity
901 -- An *implicit parameter* cannot. For example:
902 -- foo :: (?x :: [a]) => Int
904 -- is fine. The call site will suppply a particular 'x'
905 is_ambig pred = isClassPred pred &&
906 any ambig_var (varSetElems (tyVarsOfPred pred))
908 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
909 not (ct_var `elemVarSet` extended_tau_vars)
912 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
913 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
914 ptext SLIT("must be reachable from the type after the '=>'"))]
917 In addition, GHC insists that at least one type variable
918 in each constraint is in V. So we disallow a type like
919 forall a. Eq b => b -> b
920 even in a scope where b is in scope.
923 checkFreeness forall_tyvars theta
924 = mappM_ complain (filter is_free theta)
926 is_free pred = not (isIPPred pred)
927 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
928 bound_var ct_var = ct_var `elem` forall_tyvars
929 complain pred = addErrTc (freeErr pred)
932 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
933 ptext SLIT("are already in scope"),
934 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
939 checkThetaCtxt ctxt theta
940 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
941 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
943 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
944 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
945 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
947 arityErr kind name n m
948 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
949 n_arguments <> comma, text "but has been given", int m]
951 n_arguments | n == 0 = ptext SLIT("no arguments")
952 | n == 1 = ptext SLIT("1 argument")
953 | True = hsep [int n, ptext SLIT("arguments")]
957 %************************************************************************
959 \subsection{Checking for a decent instance head type}
961 %************************************************************************
963 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
964 it must normally look like: @instance Foo (Tycon a b c ...) ...@
966 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
967 flag is on, or (2)~the instance is imported (they must have been
968 compiled elsewhere). In these cases, we let them go through anyway.
970 We can also have instances for functions: @instance Foo (a -> b) ...@.
973 checkValidInstHead :: Type -> TcM (Class, [TcType])
975 checkValidInstHead ty -- Should be a source type
976 = case tcSplitPredTy_maybe ty of {
977 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
980 case getClassPredTys_maybe pred of {
981 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
984 getDOpts `thenM` \ dflags ->
985 mappM_ check_arg_type tys `thenM_`
986 check_inst_head dflags clas tys `thenM_`
990 check_inst_head dflags clas tys
991 -- If GlasgowExts then check at least one isn't a type variable
992 | dopt Opt_GlasgowExts dflags
993 = check_tyvars dflags clas tys
995 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
997 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
998 not (isSynTyCon tycon), -- ...but not a synonym
999 all tcIsTyVarTy arg_tys, -- Applied to type variables
1000 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1001 -- This last condition checks that all the type variables are distinct
1005 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1008 (first_ty : _) = tys
1010 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1011 text "where T is not a synonym, and a,b,c are distinct type variables")
1013 check_tyvars dflags clas tys
1014 -- Check that at least one isn't a type variable
1015 -- unless -fallow-undecideable-instances
1016 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1017 | not (all tcIsTyVarTy tys) = returnM ()
1018 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1020 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1023 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1027 instTypeErr pp_ty msg
1028 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,