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, newOpenTypeKind,
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,
42 #include "HsVersions.h"
46 import HsSyn ( HsType )
47 import TypeRep ( Type(..), PredType(..), TyNote(..), -- Friend; can see representation
50 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
51 TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
52 tcEqType, tcCmpPred, isClassPred, mkTyConApp, typeCon,
53 tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
54 tcSplitTyConApp_maybe, tcSplitForAllTys,
55 tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy,
56 isUnLiftedType, isIPPred,
58 mkAppTy, mkTyVarTy, mkTyVarTys,
59 tyVarsOfPred, getClassPredTys_maybe,
61 liftedTypeKind, defaultKind, superKind,
62 superBoxity, liftedBoxity, typeKind,
63 tyVarsOfType, tyVarsOfTypes,
66 import PprType ( pprThetaArrow )
67 import Subst ( Subst, mkTopTyVarSubst, substTy )
68 import Class ( Class, classArity, className )
69 import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
70 tyConArity, tyConName )
71 import Var ( TyVar, tyVarKind, tyVarName, isTyVar,
72 mkTyVar, mkMutTyVar, isMutTyVar, mutTyVarRef )
75 import TcRnMonad -- TcType, amongst others
76 import FunDeps ( grow )
77 import PprType ( pprPred, pprTheta, pprClassPred )
78 import Name ( Name, setNameUnique, mkSystemTvNameEncoded )
80 import CmdLineOpts ( dopt, DynFlag(..) )
81 import Util ( nOfThem, isSingleton, equalLength, notNull )
82 import ListSetOps ( removeDups )
87 %************************************************************************
89 \subsection{New type variables}
91 %************************************************************************
94 newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar
95 newMutTyVar name kind details
96 = do { ref <- newMutVar Nothing ;
97 return (mkMutTyVar name kind details ref) }
99 readMutTyVar :: TyVar -> TcM (Maybe Type)
100 readMutTyVar tyvar = readMutVar (mutTyVarRef tyvar)
102 writeMutTyVar :: TyVar -> Maybe Type -> TcM ()
103 writeMutTyVar tyvar val = writeMutVar (mutTyVarRef tyvar) val
105 newTyVar :: Kind -> TcM TcTyVar
107 = newUnique `thenM` \ uniq ->
108 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
110 newSigTyVar :: Kind -> TcM TcTyVar
112 = newUnique `thenM` \ uniq ->
113 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("s")) kind SigTv
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 newBoxityVar :: TcM TcKind -- Really TcBoxity
133 = newUnique `thenM` \ uniq ->
134 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx"))
135 superBoxity VanillaTv `thenM` \ kv ->
138 newOpenTypeKind :: TcM TcKind
139 newOpenTypeKind = newBoxityVar `thenM` \ bx_var ->
140 returnM (mkTyConApp typeCon [bx_var])
144 %************************************************************************
146 \subsection{Type instantiation}
148 %************************************************************************
150 Instantiating a bunch of type variables
153 tcInstTyVars :: TyVarDetails -> [TyVar]
154 -> TcM ([TcTyVar], [TcType], Subst)
156 tcInstTyVars tv_details tyvars
157 = mappM (tcInstTyVar tv_details) tyvars `thenM` \ tc_tyvars ->
159 tys = mkTyVarTys tc_tyvars
161 returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
162 -- Since the tyvars are freshly made,
163 -- they cannot possibly be captured by
164 -- any existing for-alls. Hence mkTopTyVarSubst
166 tcInstTyVar tv_details tyvar
167 = newUnique `thenM` \ uniq ->
169 name = setNameUnique (tyVarName tyvar) uniq
170 -- Note that we don't change the print-name
171 -- This won't confuse the type checker but there's a chance
172 -- that two different tyvars will print the same way
173 -- in an error message. -dppr-debug will show up the difference
174 -- Better watch out for this. If worst comes to worst, just
177 newMutTyVar name (tyVarKind tyvar) tv_details
179 tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
180 -- tcInstType instantiates the outer-level for-alls of a TcType with
181 -- fresh (mutable) type variables, splits off the dictionary part,
182 -- and returns the pieces.
183 tcInstType tv_details ty
184 = case tcSplitForAllTys ty of
185 ([], rho) -> -- There may be overloading despite no type variables;
186 -- (?x :: Int) => Int -> Int
188 (theta, tau) = tcSplitPhiTy rho
190 returnM ([], theta, tau)
192 (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenM` \ (tyvars', _, tenv) ->
194 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
196 returnM (tyvars', theta, tau)
200 %************************************************************************
202 \subsection{Putting and getting mutable type variables}
204 %************************************************************************
207 putTcTyVar :: TcTyVar -> TcType -> TcM TcType
208 getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
215 | not (isMutTyVar tyvar)
216 = pprTrace "putTcTyVar" (ppr tyvar) $
220 = ASSERT( isMutTyVar tyvar )
221 writeMutTyVar tyvar (Just ty) `thenM_`
225 Getting is more interesting. The easy thing to do is just to read, thus:
228 getTcTyVar tyvar = readMutTyVar tyvar
231 But it's more fun to short out indirections on the way: If this
232 version returns a TyVar, then that TyVar is unbound. If it returns
233 any other type, then there might be bound TyVars embedded inside it.
235 We return Nothing iff the original box was unbound.
239 | not (isMutTyVar tyvar)
240 = pprTrace "getTcTyVar" (ppr tyvar) $
241 returnM (Just (mkTyVarTy tyvar))
244 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
245 readMutTyVar tyvar `thenM` \ maybe_ty ->
247 Just ty -> short_out ty `thenM` \ ty' ->
248 writeMutTyVar tyvar (Just ty') `thenM_`
251 Nothing -> returnM Nothing
253 short_out :: TcType -> TcM TcType
254 short_out ty@(TyVarTy tyvar)
255 | not (isMutTyVar tyvar)
259 = readMutTyVar tyvar `thenM` \ maybe_ty ->
261 Just ty' -> short_out ty' `thenM` \ ty' ->
262 writeMutTyVar tyvar (Just ty') `thenM_`
267 short_out other_ty = returnM other_ty
271 %************************************************************************
273 \subsection{Zonking -- the exernal interfaces}
275 %************************************************************************
277 ----------------- Type variables
280 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
281 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
283 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
284 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
285 returnM (tyVarsOfTypes tys)
287 zonkTcTyVar :: TcTyVar -> TcM TcType
288 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
291 ----------------- Types
294 zonkTcType :: TcType -> TcM TcType
295 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
297 zonkTcTypes :: [TcType] -> TcM [TcType]
298 zonkTcTypes tys = mappM zonkTcType tys
300 zonkTcClassConstraints cts = mappM zonk cts
301 where zonk (clas, tys)
302 = zonkTcTypes tys `thenM` \ new_tys ->
303 returnM (clas, new_tys)
305 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
306 zonkTcThetaType theta = mappM zonkTcPredType theta
308 zonkTcPredType :: TcPredType -> TcM TcPredType
309 zonkTcPredType (ClassP c ts)
310 = zonkTcTypes ts `thenM` \ new_ts ->
311 returnM (ClassP c new_ts)
312 zonkTcPredType (IParam n t)
313 = zonkTcType t `thenM` \ new_t ->
314 returnM (IParam n new_t)
317 ------------------- These ...ToType, ...ToKind versions
318 are used at the end of type checking
321 zonkTcKindToKind :: TcKind -> TcM Kind
322 zonkTcKindToKind tc_kind
323 = zonkType zonk_unbound_kind_var tc_kind
325 -- When zonking a kind, we want to
326 -- zonk a *kind* variable to (Type *)
327 -- zonk a *boxity* variable to *
328 zonk_unbound_kind_var kv
329 | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
330 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
331 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
333 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
334 -- of a type variable, at the *end* of type checking. It changes
335 -- the *mutable* type variable into an *immutable* one.
337 -- It does this by making an immutable version of tv and binds tv to it.
338 -- Now any bound occurences of the original type variable will get
339 -- zonked to the immutable version.
341 zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
342 zonkTcTyVarToTyVar tv
344 -- Make an immutable version, defaulting
345 -- the kind to lifted if necessary
346 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
347 immut_tv_ty = mkTyVarTy immut_tv
349 zap tv = putTcTyVar tv immut_tv_ty
350 -- Bind the mutable version to the immutable one
352 -- If the type variable is mutable, then bind it to immut_tv_ty
353 -- so that all other occurrences of the tyvar will get zapped too
354 zonkTyVar zap tv `thenM` \ ty2 ->
356 -- This warning shows up if the allegedly-unbound tyvar is
357 -- already bound to something. It can actually happen, and
358 -- in a harmless way (see [Silly Type Synonyms] below) so
359 -- it's only a warning
360 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
365 [Silly Type Synonyms]
368 type C u a = u -- Note 'a' unused
370 foo :: (forall a. C u a -> C u a) -> u
374 bar = foo (\t -> t + t)
376 * From the (\t -> t+t) we get type {Num d} => d -> d
379 * Now unify with type of foo's arg, and we get:
380 {Num (C d a)} => C d a -> C d a
383 * Now abstract over the 'a', but float out the Num (C d a) constraint
384 because it does not 'really' mention a. (see Type.tyVarsOfType)
385 The arg to foo becomes
388 * So we get a dict binding for Num (C d a), which is zonked to give
391 * Then the /\a abstraction has a zonked 'a' in it.
393 All very silly. I think its harmless to ignore the problem.
396 %************************************************************************
398 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
400 %* For internal use only! *
402 %************************************************************************
405 -- zonkType is used for Kinds as well
407 -- For unbound, mutable tyvars, zonkType uses the function given to it
408 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
409 -- type variable and zonks the kind too
411 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
412 -- see zonkTcType, and zonkTcTypeToType
415 zonkType unbound_var_fn ty
418 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
419 returnM (TyConApp tycon tys')
421 go (NewTcApp tycon tys) = mappM go tys `thenM` \ tys' ->
422 returnM (NewTcApp tycon tys')
424 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
425 go ty2 `thenM` \ ty2' ->
426 returnM (NoteTy (SynNote ty1') ty2')
428 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
430 go (PredTy p) = go_pred p `thenM` \ p' ->
433 go (FunTy arg res) = go arg `thenM` \ arg' ->
434 go res `thenM` \ res' ->
435 returnM (FunTy arg' res')
437 go (AppTy fun arg) = go fun `thenM` \ fun' ->
438 go arg `thenM` \ arg' ->
439 returnM (mkAppTy fun' arg')
440 -- NB the mkAppTy; we might have instantiated a
441 -- type variable to a type constructor, so we need
442 -- to pull the TyConApp to the top.
444 -- The two interesting cases!
445 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
447 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenM` \ tyvar' ->
448 go ty `thenM` \ ty' ->
449 returnM (ForAllTy tyvar' ty')
451 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
452 returnM (ClassP c tys')
453 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
454 returnM (IParam n ty')
456 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
457 -> TcTyVar -> TcM TcType
458 zonkTyVar unbound_var_fn tyvar
459 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
460 -- zonking a forall type, when the bound type variable
461 -- needn't be mutable
462 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
463 returnM (TyVarTy tyvar)
466 = getTcTyVar tyvar `thenM` \ maybe_ty ->
468 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
469 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
474 %************************************************************************
476 \subsection{Checking a user type}
478 %************************************************************************
480 When dealing with a user-written type, we first translate it from an HsType
481 to a Type, performing kind checking, and then check various things that should
482 be true about it. We don't want to perform these checks at the same time
483 as the initial translation because (a) they are unnecessary for interface-file
484 types and (b) when checking a mutually recursive group of type and class decls,
485 we can't "look" at the tycons/classes yet. Also, the checks are are rather
486 diverse, and used to really mess up the other code.
488 One thing we check for is 'rank'.
490 Rank 0: monotypes (no foralls)
491 Rank 1: foralls at the front only, Rank 0 inside
492 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
494 basic ::= tyvar | T basic ... basic
496 r2 ::= forall tvs. cxt => r2a
497 r2a ::= r1 -> r2a | basic
498 r1 ::= forall tvs. cxt => r0
499 r0 ::= r0 -> r0 | basic
501 Another thing is to check that type synonyms are saturated.
502 This might not necessarily show up in kind checking.
504 data T k = MkT (k Int)
510 = FunSigCtxt Name -- Function type signature
511 | ExprSigCtxt -- Expression type signature
512 | ConArgCtxt Name -- Data constructor argument
513 | TySynCtxt Name -- RHS of a type synonym decl
514 | GenPatCtxt -- Pattern in generic decl
515 -- f{| a+b |} (Inl x) = ...
516 | PatSigCtxt -- Type sig in pattern
518 | ResSigCtxt -- Result type sig
520 | ForSigCtxt Name -- Foreign inport or export signature
521 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
522 | DefaultDeclCtxt -- Types in a default declaration
524 -- Notes re TySynCtxt
525 -- We allow type synonyms that aren't types; e.g. type List = []
527 -- If the RHS mentions tyvars that aren't in scope, we'll
528 -- quantify over them:
529 -- e.g. type T = a->a
530 -- will become type T = forall a. a->a
532 -- With gla-exts that's right, but for H98 we should complain.
535 pprHsSigCtxt :: UserTypeCtxt -> HsType Name -> SDoc
536 pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt hs_ty ctxt
538 pprUserTypeCtxt ty (FunSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
539 pprUserTypeCtxt ty ExprSigCtxt = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
540 pprUserTypeCtxt ty (ConArgCtxt c) = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
541 pprUserTypeCtxt ty (TySynCtxt c) = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
542 nest 2 (ptext SLIT(", namely") <+> ppr ty)]
543 pprUserTypeCtxt ty GenPatCtxt = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
544 pprUserTypeCtxt ty PatSigCtxt = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
545 pprUserTypeCtxt ty ResSigCtxt = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
546 pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
547 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
548 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
550 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
554 checkValidType :: UserTypeCtxt -> Type -> TcM ()
555 -- Checks that the type is valid for the given context
556 checkValidType ctxt ty
557 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
558 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
560 rank | gla_exts = Arbitrary
562 = case ctxt of -- Haskell 98
565 DefaultDeclCtxt-> Rank 0
567 TySynCtxt _ -> Rank 0
568 ExprSigCtxt -> Rank 1
569 FunSigCtxt _ -> Rank 1
570 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
571 -- constructor, hence rank 1
572 ForSigCtxt _ -> Rank 1
573 RuleSigCtxt _ -> Rank 1
575 actual_kind = typeKind ty
577 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
579 kind_ok = case ctxt of
580 TySynCtxt _ -> True -- Any kind will do
581 GenPatCtxt -> actual_kind_is_lifted
582 ForSigCtxt _ -> actual_kind_is_lifted
583 other -> isTypeKind actual_kind
585 ubx_tup | not gla_exts = UT_NotOk
586 | otherwise = case ctxt of
589 -- Unboxed tuples ok in function results,
590 -- but for type synonyms we allow them even at
593 -- Check that the thing has kind Type, and is lifted if necessary
594 checkTc kind_ok (kindErr actual_kind) `thenM_`
596 -- Check the internal validity of the type itself
597 check_poly_type rank ubx_tup ty `thenM_`
599 traceTc (text "checkValidType done" <+> ppr ty)
604 data Rank = Rank Int | Arbitrary
606 decRank :: Rank -> Rank
607 decRank Arbitrary = Arbitrary
608 decRank (Rank n) = Rank (n-1)
610 ----------------------------------------
611 data UbxTupFlag = UT_Ok | UT_NotOk
612 -- The "Ok" version means "ok if -fglasgow-exts is on"
614 ----------------------------------------
615 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
616 check_poly_type (Rank 0) ubx_tup ty
617 = check_tau_type (Rank 0) ubx_tup ty
619 check_poly_type rank ubx_tup ty
621 (tvs, theta, tau) = tcSplitSigmaTy ty
623 check_valid_theta SigmaCtxt theta `thenM_`
624 check_tau_type (decRank rank) ubx_tup tau `thenM_`
625 checkFreeness tvs theta `thenM_`
626 checkAmbiguity tvs theta (tyVarsOfType tau)
628 ----------------------------------------
629 check_arg_type :: Type -> TcM ()
630 -- The sort of type that can instantiate a type variable,
631 -- or be the argument of a type constructor.
632 -- Not an unboxed tuple, not a forall.
633 -- Other unboxed types are very occasionally allowed as type
634 -- arguments depending on the kind of the type constructor
636 -- For example, we want to reject things like:
638 -- instance Ord a => Ord (forall s. T s a)
640 -- g :: T s (forall b.b)
642 -- NB: unboxed tuples can have polymorphic or unboxed args.
643 -- This happens in the workers for functions returning
644 -- product types with polymorphic components.
645 -- But not in user code.
646 -- Anyway, they are dealt with by a special case in check_tau_type
649 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
650 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
652 ----------------------------------------
653 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
654 -- Rank is allowed rank for function args
655 -- No foralls otherwise
657 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
658 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
659 check_source_ty dflags TypeCtxt sty
660 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
661 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
662 = check_poly_type rank UT_NotOk arg_ty `thenM_`
663 check_tau_type rank UT_Ok res_ty
665 check_tau_type rank ubx_tup (AppTy ty1 ty2)
666 = check_arg_type ty1 `thenM_` check_arg_type ty2
668 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
669 -- Synonym notes are built only when the synonym is
670 -- saturated (see Type.mkSynTy)
671 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
673 -- If -fglasgow-exts then don't check the 'note' part.
674 -- This allows us to instantiate a synonym defn with a
675 -- for-all type, or with a partially-applied type synonym.
676 -- e.g. type T a b = a
679 -- Here, T is partially applied, so it's illegal in H98.
680 -- But if you expand S first, then T we get just
685 -- For H98, do check the un-expanded part
686 check_tau_type rank ubx_tup syn
689 check_tau_type rank ubx_tup ty
691 check_tau_type rank ubx_tup (NoteTy other_note ty)
692 = check_tau_type rank ubx_tup ty
694 check_tau_type rank ubx_tup (NewTcApp tc tys)
695 = mappM_ check_arg_type tys
697 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
699 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
700 -- synonym application, leaving it to checkValidType (i.e. right here)
702 checkTc syn_arity_ok arity_msg `thenM_`
703 mappM_ check_arg_type tys
705 | isUnboxedTupleTyCon tc
706 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
707 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
708 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
709 -- Args are allowed to be unlifted, or
710 -- more unboxed tuples, so can't use check_arg_ty
713 = mappM_ check_arg_type tys
716 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
718 syn_arity_ok = tc_arity <= n_args
719 -- It's OK to have an *over-applied* type synonym
720 -- data Tree a b = ...
721 -- type Foo a = Tree [a]
722 -- f :: Foo a b -> ...
724 tc_arity = tyConArity tc
726 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
727 ubx_tup_msg = ubxArgTyErr ty
729 ----------------------------------------
730 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr ty
731 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
732 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
733 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
738 %************************************************************************
740 \subsection{Checking a theta or source type}
742 %************************************************************************
745 -- Enumerate the contexts in which a "source type", <S>, can occur
749 -- or (N a) where N is a newtype
752 = ClassSCCtxt Name -- Superclasses of clas
753 -- class <S> => C a where ...
754 | SigmaCtxt -- Theta part of a normal for-all type
755 -- f :: <S> => a -> a
756 | DataTyCtxt Name -- Theta part of a data decl
757 -- data <S> => T a = MkT a
758 | TypeCtxt -- Source type in an ordinary type
760 | InstThetaCtxt -- Context of an instance decl
761 -- instance <S> => C [a] where ...
762 | InstHeadCtxt -- Head of an instance decl
763 -- instance ... => Eq a where ...
765 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
766 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
767 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
768 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
769 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
770 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
774 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
775 checkValidTheta ctxt theta
776 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
778 -------------------------
779 check_valid_theta ctxt []
781 check_valid_theta ctxt theta
782 = getDOpts `thenM` \ dflags ->
783 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
784 -- Actually, in instance decls and type signatures,
785 -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
786 -- so this error can only fire for the context of a class or
788 mappM_ (check_source_ty dflags ctxt) theta
790 (_,dups) = removeDups tcCmpPred theta
792 -------------------------
793 check_source_ty dflags ctxt pred@(ClassP cls tys)
794 = -- Class predicates are valid in all contexts
795 checkTc (arity == n_tys) arity_err `thenM_`
797 -- Check the form of the argument types
798 mappM_ check_arg_type tys `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.
824 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
826 -------------------------
827 check_class_pred_tys dflags ctxt tys
829 InstHeadCtxt -> True -- We check for instance-head
830 -- formation in checkValidInstHead
831 InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
832 other -> gla_exts || all tyvar_head tys
834 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
835 gla_exts = dopt Opt_GlasgowExts dflags
837 -------------------------
838 tyvar_head ty -- Haskell 98 allows predicates of form
839 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
840 | otherwise -- where a is a type variable
841 = case tcSplitAppTy_maybe ty of
842 Just (ty, _) -> tyvar_head ty
849 is ambiguous if P contains generic variables
850 (i.e. one of the Vs) that are not mentioned in tau
852 However, we need to take account of functional dependencies
853 when we speak of 'mentioned in tau'. Example:
854 class C a b | a -> b where ...
856 forall x y. (C x y) => x
857 is not ambiguous because x is mentioned and x determines y
859 NB; the ambiguity check is only used for *user* types, not for types
860 coming from inteface files. The latter can legitimately have
861 ambiguous types. Example
863 class S a where s :: a -> (Int,Int)
864 instance S Char where s _ = (1,1)
865 f:: S a => [a] -> Int -> (Int,Int)
866 f (_::[a]) x = (a*x,b)
867 where (a,b) = s (undefined::a)
869 Here the worker for f gets the type
870 fw :: forall a. S a => Int -> (# Int, Int #)
872 If the list of tv_names is empty, we have a monotype, and then we
873 don't need to check for ambiguity either, because the test can't fail
877 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
878 checkAmbiguity forall_tyvars theta tau_tyvars
879 = mappM_ complain (filter is_ambig theta)
881 complain pred = addErrTc (ambigErr pred)
882 extended_tau_vars = grow theta tau_tyvars
884 -- Only a *class* predicate can give rise to ambiguity
885 -- An *implicit parameter* cannot. For example:
886 -- foo :: (?x :: [a]) => Int
888 -- is fine. The call site will suppply a particular 'x'
889 is_ambig pred = isClassPred pred &&
890 any ambig_var (varSetElems (tyVarsOfPred pred))
892 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
893 not (ct_var `elemVarSet` extended_tau_vars)
896 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
897 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
898 ptext SLIT("must be reachable from the type after the '=>'"))]
901 In addition, GHC insists that at least one type variable
902 in each constraint is in V. So we disallow a type like
903 forall a. Eq b => b -> b
904 even in a scope where b is in scope.
907 checkFreeness forall_tyvars theta
908 = mappM_ complain (filter is_free theta)
910 is_free pred = not (isIPPred pred)
911 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
912 bound_var ct_var = ct_var `elem` forall_tyvars
913 complain pred = addErrTc (freeErr pred)
916 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
917 ptext SLIT("are already in scope"),
918 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
923 checkThetaCtxt ctxt theta
924 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
925 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
927 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
928 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
929 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
931 arityErr kind name n m
932 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
933 n_arguments <> comma, text "but has been given", int m]
935 n_arguments | n == 0 = ptext SLIT("no arguments")
936 | n == 1 = ptext SLIT("1 argument")
937 | True = hsep [int n, ptext SLIT("arguments")]
941 %************************************************************************
943 \subsection{Checking for a decent instance head type}
945 %************************************************************************
947 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
948 it must normally look like: @instance Foo (Tycon a b c ...) ...@
950 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
951 flag is on, or (2)~the instance is imported (they must have been
952 compiled elsewhere). In these cases, we let them go through anyway.
954 We can also have instances for functions: @instance Foo (a -> b) ...@.
957 checkValidInstHead :: Type -> TcM (Class, [TcType])
959 checkValidInstHead ty -- Should be a source type
960 = case tcSplitPredTy_maybe ty of {
961 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
964 case getClassPredTys_maybe pred of {
965 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
968 getDOpts `thenM` \ dflags ->
969 mappM_ check_arg_type tys `thenM_`
970 check_inst_head dflags clas tys `thenM_`
974 check_inst_head dflags clas tys
975 -- If GlasgowExts then check at least one isn't a type variable
976 | dopt Opt_GlasgowExts dflags
977 = check_tyvars dflags clas tys
979 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
981 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
982 not (isSynTyCon tycon), -- ...but not a synonym
983 all tcIsTyVarTy arg_tys, -- Applied to type variables
984 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
985 -- This last condition checks that all the type variables are distinct
989 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
994 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
995 text "where T is not a synonym, and a,b,c are distinct type variables")
997 check_tyvars dflags clas tys
998 -- Check that at least one isn't a type variable
999 -- unless -fallow-undecideable-instances
1000 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1001 | not (all tcIsTyVarTy tys) = returnM ()
1002 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1004 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1007 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1011 instTypeErr pp_ty msg
1012 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,