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, newBoxityVar,
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, checkFreeness,
29 checkValidInstHead, instTypeErr, checkAmbiguity,
32 --------------------------------
35 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
36 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
37 zonkTcPredType, zonkTcTyVarToTyVar,
42 #include "HsVersions.h"
46 import TypeRep ( Type(..), PredType(..), TyNote(..), -- Friend; can see representation
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, tcIsTyVarTy,
55 isUnLiftedType, isIPPred,
57 mkAppTy, mkTyVarTy, mkTyVarTys,
58 tyVarsOfPred, getClassPredTys_maybe,
60 liftedTypeKind, defaultKind, superKind,
61 superBoxity, liftedBoxity, typeKind,
62 tyVarsOfType, tyVarsOfTypes,
65 import Subst ( Subst, mkTopTyVarSubst, substTy )
66 import Class ( Class, classArity, className )
67 import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
68 tyConArity, tyConName )
69 import Var ( TyVar, tyVarKind, tyVarName, isTyVar,
70 mkTyVar, mkMutTyVar, isMutTyVar, mutTyVarRef )
73 import TcRnMonad -- TcType, amongst others
74 import FunDeps ( grow )
75 import PprType ( pprPred, pprTheta, pprClassPred )
76 import Name ( Name, setNameUnique, mkSystemTvNameEncoded )
78 import CmdLineOpts ( dopt, DynFlag(..) )
79 import Util ( nOfThem, isSingleton, equalLength, notNull )
80 import ListSetOps ( removeDups )
85 %************************************************************************
87 \subsection{New type variables}
89 %************************************************************************
92 newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar
93 newMutTyVar name kind details
94 = do { ref <- newMutVar Nothing ;
95 return (mkMutTyVar name kind details ref) }
97 readMutTyVar :: TyVar -> TcM (Maybe Type)
98 readMutTyVar tyvar = readMutVar (mutTyVarRef tyvar)
100 writeMutTyVar :: TyVar -> Maybe Type -> TcM ()
101 writeMutTyVar tyvar val = writeMutVar (mutTyVarRef tyvar) val
103 newTyVar :: Kind -> TcM TcTyVar
105 = newUnique `thenM` \ uniq ->
106 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
108 newSigTyVar :: Kind -> TcM TcTyVar
110 = newUnique `thenM` \ uniq ->
111 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("s")) kind SigTv
113 newTyVarTy :: Kind -> TcM TcType
115 = newTyVar kind `thenM` \ tc_tyvar ->
116 returnM (TyVarTy tc_tyvar)
118 newTyVarTys :: Int -> Kind -> TcM [TcType]
119 newTyVarTys n kind = mappM newTyVarTy (nOfThem n kind)
121 newKindVar :: TcM TcKind
123 = newUnique `thenM` \ uniq ->
124 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv `thenM` \ kv ->
127 newKindVars :: Int -> TcM [TcKind]
128 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
130 newBoxityVar :: TcM TcKind -- Really TcBoxity
131 = newUnique `thenM` \ uniq ->
132 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx"))
133 superBoxity VanillaTv `thenM` \ kv ->
138 %************************************************************************
140 \subsection{Type instantiation}
142 %************************************************************************
144 Instantiating a bunch of type variables
147 tcInstTyVars :: TyVarDetails -> [TyVar]
148 -> TcM ([TcTyVar], [TcType], Subst)
150 tcInstTyVars tv_details tyvars
151 = mappM (tcInstTyVar tv_details) tyvars `thenM` \ tc_tyvars ->
153 tys = mkTyVarTys tc_tyvars
155 returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
156 -- Since the tyvars are freshly made,
157 -- they cannot possibly be captured by
158 -- any existing for-alls. Hence mkTopTyVarSubst
160 tcInstTyVar tv_details tyvar
161 = newUnique `thenM` \ uniq ->
163 name = setNameUnique (tyVarName tyvar) uniq
164 -- Note that we don't change the print-name
165 -- This won't confuse the type checker but there's a chance
166 -- that two different tyvars will print the same way
167 -- in an error message. -dppr-debug will show up the difference
168 -- Better watch out for this. If worst comes to worst, just
171 newMutTyVar name (tyVarKind tyvar) tv_details
173 tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
174 -- tcInstType instantiates the outer-level for-alls of a TcType with
175 -- fresh (mutable) type variables, splits off the dictionary part,
176 -- and returns the pieces.
177 tcInstType tv_details ty
178 = case tcSplitForAllTys ty of
179 ([], rho) -> -- There may be overloading despite no type variables;
180 -- (?x :: Int) => Int -> Int
182 (theta, tau) = tcSplitPhiTy rho
184 returnM ([], theta, tau)
186 (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenM` \ (tyvars', _, tenv) ->
188 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
190 returnM (tyvars', theta, tau)
194 %************************************************************************
196 \subsection{Putting and getting mutable type variables}
198 %************************************************************************
201 putTcTyVar :: TcTyVar -> TcType -> TcM TcType
202 getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
209 | not (isMutTyVar tyvar)
210 = pprTrace "putTcTyVar" (ppr tyvar) $
214 = ASSERT( isMutTyVar tyvar )
215 writeMutTyVar tyvar (Just ty) `thenM_`
219 Getting is more interesting. The easy thing to do is just to read, thus:
222 getTcTyVar tyvar = readMutTyVar tyvar
225 But it's more fun to short out indirections on the way: If this
226 version returns a TyVar, then that TyVar is unbound. If it returns
227 any other type, then there might be bound TyVars embedded inside it.
229 We return Nothing iff the original box was unbound.
233 | not (isMutTyVar tyvar)
234 = pprTrace "getTcTyVar" (ppr tyvar) $
235 returnM (Just (mkTyVarTy tyvar))
238 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
239 readMutTyVar tyvar `thenM` \ maybe_ty ->
241 Just ty -> short_out ty `thenM` \ ty' ->
242 writeMutTyVar tyvar (Just ty') `thenM_`
245 Nothing -> returnM Nothing
247 short_out :: TcType -> TcM TcType
248 short_out ty@(TyVarTy tyvar)
249 | not (isMutTyVar tyvar)
253 = readMutTyVar tyvar `thenM` \ maybe_ty ->
255 Just ty' -> short_out ty' `thenM` \ ty' ->
256 writeMutTyVar tyvar (Just ty') `thenM_`
261 short_out other_ty = returnM other_ty
265 %************************************************************************
267 \subsection{Zonking -- the exernal interfaces}
269 %************************************************************************
271 ----------------- Type variables
274 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
275 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
277 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
278 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
279 returnM (tyVarsOfTypes tys)
281 zonkTcTyVar :: TcTyVar -> TcM TcType
282 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
285 ----------------- Types
288 zonkTcType :: TcType -> TcM TcType
289 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
291 zonkTcTypes :: [TcType] -> TcM [TcType]
292 zonkTcTypes tys = mappM zonkTcType tys
294 zonkTcClassConstraints cts = mappM zonk cts
295 where zonk (clas, tys)
296 = zonkTcTypes tys `thenM` \ new_tys ->
297 returnM (clas, new_tys)
299 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
300 zonkTcThetaType theta = mappM zonkTcPredType theta
302 zonkTcPredType :: TcPredType -> TcM TcPredType
303 zonkTcPredType (ClassP c ts)
304 = zonkTcTypes ts `thenM` \ new_ts ->
305 returnM (ClassP c new_ts)
306 zonkTcPredType (IParam n t)
307 = zonkTcType t `thenM` \ new_t ->
308 returnM (IParam n new_t)
311 ------------------- These ...ToType, ...ToKind versions
312 are used at the end of type checking
315 zonkTcKindToKind :: TcKind -> TcM Kind
316 zonkTcKindToKind tc_kind
317 = zonkType zonk_unbound_kind_var tc_kind
319 -- When zonking a kind, we want to
320 -- zonk a *kind* variable to (Type *)
321 -- zonk a *boxity* variable to *
322 zonk_unbound_kind_var kv
323 | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
324 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
325 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
327 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
328 -- of a type variable, at the *end* of type checking. It changes
329 -- the *mutable* type variable into an *immutable* one.
331 -- It does this by making an immutable version of tv and binds tv to it.
332 -- Now any bound occurences of the original type variable will get
333 -- zonked to the immutable version.
335 zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
336 zonkTcTyVarToTyVar tv
338 -- Make an immutable version, defaulting
339 -- the kind to lifted if necessary
340 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
341 immut_tv_ty = mkTyVarTy immut_tv
343 zap tv = putTcTyVar tv immut_tv_ty
344 -- Bind the mutable version to the immutable one
346 -- If the type variable is mutable, then bind it to immut_tv_ty
347 -- so that all other occurrences of the tyvar will get zapped too
348 zonkTyVar zap tv `thenM` \ ty2 ->
350 -- This warning shows up if the allegedly-unbound tyvar is
351 -- already bound to something. It can actually happen, and
352 -- in a harmless way (see [Silly Type Synonyms] below) so
353 -- it's only a warning
354 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
359 [Silly Type Synonyms]
362 type C u a = u -- Note 'a' unused
364 foo :: (forall a. C u a -> C u a) -> u
368 bar = foo (\t -> t + t)
370 * From the (\t -> t+t) we get type {Num d} => d -> d
373 * Now unify with type of foo's arg, and we get:
374 {Num (C d a)} => C d a -> C d a
377 * Now abstract over the 'a', but float out the Num (C d a) constraint
378 because it does not 'really' mention a. (see Type.tyVarsOfType)
379 The arg to foo becomes
382 * So we get a dict binding for Num (C d a), which is zonked to give
385 * Then the /\a abstraction has a zonked 'a' in it.
387 All very silly. I think its harmless to ignore the problem.
390 %************************************************************************
392 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
394 %* For internal use only! *
396 %************************************************************************
399 -- zonkType is used for Kinds as well
401 -- For unbound, mutable tyvars, zonkType uses the function given to it
402 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
403 -- type variable and zonks the kind too
405 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
406 -- see zonkTcType, and zonkTcTypeToType
409 zonkType unbound_var_fn ty
412 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
413 returnM (TyConApp tycon tys')
415 go (NewTcApp tycon tys) = mappM go tys `thenM` \ tys' ->
416 returnM (NewTcApp tycon tys')
418 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
419 go ty2 `thenM` \ ty2' ->
420 returnM (NoteTy (SynNote ty1') ty2')
422 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
424 go (PredTy p) = go_pred p `thenM` \ p' ->
427 go (FunTy arg res) = go arg `thenM` \ arg' ->
428 go res `thenM` \ res' ->
429 returnM (FunTy arg' res')
431 go (AppTy fun arg) = go fun `thenM` \ fun' ->
432 go arg `thenM` \ arg' ->
433 returnM (mkAppTy fun' arg')
434 -- NB the mkAppTy; we might have instantiated a
435 -- type variable to a type constructor, so we need
436 -- to pull the TyConApp to the top.
438 -- The two interesting cases!
439 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
441 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenM` \ tyvar' ->
442 go ty `thenM` \ ty' ->
443 returnM (ForAllTy tyvar' ty')
445 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
446 returnM (ClassP c tys')
447 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
448 returnM (IParam n ty')
450 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
451 -> TcTyVar -> TcM TcType
452 zonkTyVar unbound_var_fn tyvar
453 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
454 -- zonking a forall type, when the bound type variable
455 -- needn't be mutable
456 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
457 returnM (TyVarTy tyvar)
460 = getTcTyVar tyvar `thenM` \ maybe_ty ->
462 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
463 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
468 %************************************************************************
470 \subsection{Checking a user type}
472 %************************************************************************
474 When dealing with a user-written type, we first translate it from an HsType
475 to a Type, performing kind checking, and then check various things that should
476 be true about it. We don't want to perform these checks at the same time
477 as the initial translation because (a) they are unnecessary for interface-file
478 types and (b) when checking a mutually recursive group of type and class decls,
479 we can't "look" at the tycons/classes yet. Also, the checks are are rather
480 diverse, and used to really mess up the other code.
482 One thing we check for is 'rank'.
484 Rank 0: monotypes (no foralls)
485 Rank 1: foralls at the front only, Rank 0 inside
486 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
488 basic ::= tyvar | T basic ... basic
490 r2 ::= forall tvs. cxt => r2a
491 r2a ::= r1 -> r2a | basic
492 r1 ::= forall tvs. cxt => r0
493 r0 ::= r0 -> r0 | basic
495 Another thing is to check that type synonyms are saturated.
496 This might not necessarily show up in kind checking.
498 data T k = MkT (k Int)
504 = FunSigCtxt Name -- Function type signature
505 | ExprSigCtxt -- Expression type signature
506 | ConArgCtxt Name -- Data constructor argument
507 | TySynCtxt Name -- RHS of a type synonym decl
508 | GenPatCtxt -- Pattern in generic decl
509 -- f{| a+b |} (Inl x) = ...
510 | PatSigCtxt -- Type sig in pattern
512 | ResSigCtxt -- Result type sig
514 | ForSigCtxt Name -- Foreign inport or export signature
515 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
516 | DefaultDeclCtxt -- Types in a default declaration
518 -- Notes re TySynCtxt
519 -- We allow type synonyms that aren't types; e.g. type List = []
521 -- If the RHS mentions tyvars that aren't in scope, we'll
522 -- quantify over them:
523 -- e.g. type T = a->a
524 -- will become type T = forall a. a->a
526 -- With gla-exts that's right, but for H98 we should complain.
529 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
530 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
531 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
532 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
533 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
534 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
535 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
536 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
537 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
538 pprUserTypeCtxt DefaultDeclCtxt = ptext SLIT("a `default' declaration")
542 checkValidType :: UserTypeCtxt -> Type -> TcM ()
543 -- Checks that the type is valid for the given context
544 checkValidType ctxt ty
545 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
546 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
548 rank | gla_exts = Arbitrary
550 = case ctxt of -- Haskell 98
553 DefaultDeclCtxt-> Rank 0
555 TySynCtxt _ -> Rank 0
556 ExprSigCtxt -> Rank 1
557 FunSigCtxt _ -> Rank 1
558 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
559 -- constructor, hence rank 1
560 ForSigCtxt _ -> Rank 1
561 RuleSigCtxt _ -> Rank 1
563 actual_kind = typeKind ty
565 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
567 kind_ok = case ctxt of
568 TySynCtxt _ -> True -- Any kind will do
569 GenPatCtxt -> actual_kind_is_lifted
570 ForSigCtxt _ -> actual_kind_is_lifted
571 other -> isTypeKind actual_kind
573 ubx_tup | not gla_exts = UT_NotOk
574 | otherwise = case ctxt of
577 -- Unboxed tuples ok in function results,
578 -- but for type synonyms we allow them even at
581 -- Check that the thing has kind Type, and is lifted if necessary
582 checkTc kind_ok (kindErr actual_kind) `thenM_`
584 -- Check the internal validity of the type itself
585 check_poly_type rank ubx_tup ty `thenM_`
587 traceTc (text "checkValidType done" <+> ppr ty)
592 data Rank = Rank Int | Arbitrary
594 decRank :: Rank -> Rank
595 decRank Arbitrary = Arbitrary
596 decRank (Rank n) = Rank (n-1)
598 ----------------------------------------
599 data UbxTupFlag = UT_Ok | UT_NotOk
600 -- The "Ok" version means "ok if -fglasgow-exts is on"
602 ----------------------------------------
603 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
604 check_poly_type (Rank 0) ubx_tup ty
605 = check_tau_type (Rank 0) ubx_tup ty
607 check_poly_type rank ubx_tup ty
609 (tvs, theta, tau) = tcSplitSigmaTy ty
611 check_valid_theta SigmaCtxt theta `thenM_`
612 check_tau_type (decRank rank) ubx_tup tau `thenM_`
613 checkFreeness tvs theta `thenM_`
614 checkAmbiguity tvs theta (tyVarsOfType tau)
616 ----------------------------------------
617 check_arg_type :: Type -> TcM ()
618 -- The sort of type that can instantiate a type variable,
619 -- or be the argument of a type constructor.
620 -- Not an unboxed tuple, not a forall.
621 -- Other unboxed types are very occasionally allowed as type
622 -- arguments depending on the kind of the type constructor
624 -- For example, we want to reject things like:
626 -- instance Ord a => Ord (forall s. T s a)
628 -- g :: T s (forall b.b)
630 -- NB: unboxed tuples can have polymorphic or unboxed args.
631 -- This happens in the workers for functions returning
632 -- product types with polymorphic components.
633 -- But not in user code.
634 -- Anyway, they are dealt with by a special case in check_tau_type
637 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
638 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
640 ----------------------------------------
641 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
642 -- Rank is allowed rank for function args
643 -- No foralls otherwise
645 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
646 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
647 check_source_ty dflags TypeCtxt sty
648 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
649 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
650 = check_poly_type rank UT_NotOk arg_ty `thenM_`
651 check_tau_type rank UT_Ok res_ty
653 check_tau_type rank ubx_tup (AppTy ty1 ty2)
654 = check_arg_type ty1 `thenM_` check_arg_type ty2
656 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
657 -- Synonym notes are built only when the synonym is
658 -- saturated (see Type.mkSynTy)
659 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
661 -- If -fglasgow-exts then don't check the 'note' part.
662 -- This allows us to instantiate a synonym defn with a
663 -- for-all type, or with a partially-applied type synonym.
664 -- e.g. type T a b = a
667 -- Here, T is partially applied, so it's illegal in H98.
668 -- But if you expand S first, then T we get just
673 -- For H98, do check the un-expanded part
674 check_tau_type rank ubx_tup syn
677 check_tau_type rank ubx_tup ty
679 check_tau_type rank ubx_tup (NoteTy other_note ty)
680 = check_tau_type rank ubx_tup ty
682 check_tau_type rank ubx_tup (NewTcApp tc tys)
683 = mappM_ check_arg_type tys
685 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
687 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
688 -- synonym application, leaving it to checkValidType (i.e. right here)
690 checkTc syn_arity_ok arity_msg `thenM_`
691 mappM_ check_arg_type tys
693 | isUnboxedTupleTyCon tc
694 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
695 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
696 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
697 -- Args are allowed to be unlifted, or
698 -- more unboxed tuples, so can't use check_arg_ty
701 = mappM_ check_arg_type tys
704 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
706 syn_arity_ok = tc_arity <= n_args
707 -- It's OK to have an *over-applied* type synonym
708 -- data Tree a b = ...
709 -- type Foo a = Tree [a]
710 -- f :: Foo a b -> ...
712 tc_arity = tyConArity tc
714 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
715 ubx_tup_msg = ubxArgTyErr ty
717 ----------------------------------------
718 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr ty
719 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
720 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
721 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
726 %************************************************************************
728 \subsection{Checking a theta or source type}
730 %************************************************************************
733 -- Enumerate the contexts in which a "source type", <S>, can occur
737 -- or (N a) where N is a newtype
740 = ClassSCCtxt Name -- Superclasses of clas
741 -- class <S> => C a where ...
742 | SigmaCtxt -- Theta part of a normal for-all type
743 -- f :: <S> => a -> a
744 | DataTyCtxt Name -- Theta part of a data decl
745 -- data <S> => T a = MkT a
746 | TypeCtxt -- Source type in an ordinary type
748 | InstThetaCtxt -- Context of an instance decl
749 -- instance <S> => C [a] where ...
750 | InstHeadCtxt -- Head of an instance decl
751 -- instance ... => Eq a where ...
753 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
754 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
755 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
756 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
757 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
758 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
762 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
763 checkValidTheta ctxt theta
764 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
766 -------------------------
767 check_valid_theta ctxt []
769 check_valid_theta ctxt theta
770 = getDOpts `thenM` \ dflags ->
771 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
772 -- Actually, in instance decls and type signatures,
773 -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
774 -- so this error can only fire for the context of a class or
776 mappM_ (check_source_ty dflags ctxt) theta
778 (_,dups) = removeDups tcCmpPred theta
780 -------------------------
781 check_source_ty dflags ctxt pred@(ClassP cls tys)
782 = -- Class predicates are valid in all contexts
783 checkTc (arity == n_tys) arity_err `thenM_`
785 -- Check the form of the argument types
786 mappM_ check_arg_type tys `thenM_`
787 checkTc (check_class_pred_tys dflags ctxt tys)
788 (predTyVarErr pred $$ how_to_allow)
791 class_name = className cls
792 arity = classArity cls
794 arity_err = arityErr "Class" class_name arity n_tys
796 how_to_allow = case ctxt of
797 InstHeadCtxt -> empty -- Should not happen
798 InstThetaCtxt -> parens undecidableMsg
799 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
801 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
802 -- Implicit parameters only allows in type
803 -- signatures; not in instance decls, superclasses etc
804 -- The reason for not allowing implicit params in instances is a bit subtle
805 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
806 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
807 -- discharge all the potential usas of the ?x in e. For example, a
808 -- constraint Foo [Int] might come out of e,and applying the
809 -- instance decl would show up two uses of ?x.
812 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
814 -------------------------
815 check_class_pred_tys dflags ctxt tys
817 InstHeadCtxt -> True -- We check for instance-head
818 -- formation in checkValidInstHead
819 InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
820 other -> gla_exts || all tyvar_head tys
822 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
823 gla_exts = dopt Opt_GlasgowExts dflags
825 -------------------------
826 tyvar_head ty -- Haskell 98 allows predicates of form
827 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
828 | otherwise -- where a is a type variable
829 = case tcSplitAppTy_maybe ty of
830 Just (ty, _) -> tyvar_head ty
837 is ambiguous if P contains generic variables
838 (i.e. one of the Vs) that are not mentioned in tau
840 However, we need to take account of functional dependencies
841 when we speak of 'mentioned in tau'. Example:
842 class C a b | a -> b where ...
844 forall x y. (C x y) => x
845 is not ambiguous because x is mentioned and x determines y
847 NB; the ambiguity check is only used for *user* types, not for types
848 coming from inteface files. The latter can legitimately have
849 ambiguous types. Example
851 class S a where s :: a -> (Int,Int)
852 instance S Char where s _ = (1,1)
853 f:: S a => [a] -> Int -> (Int,Int)
854 f (_::[a]) x = (a*x,b)
855 where (a,b) = s (undefined::a)
857 Here the worker for f gets the type
858 fw :: forall a. S a => Int -> (# Int, Int #)
860 If the list of tv_names is empty, we have a monotype, and then we
861 don't need to check for ambiguity either, because the test can't fail
865 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
866 checkAmbiguity forall_tyvars theta tau_tyvars
867 = mappM_ complain (filter is_ambig theta)
869 complain pred = addErrTc (ambigErr pred)
870 extended_tau_vars = grow theta tau_tyvars
872 -- Only a *class* predicate can give rise to ambiguity
873 -- An *implicit parameter* cannot. For example:
874 -- foo :: (?x :: [a]) => Int
876 -- is fine. The call site will suppply a particular 'x'
877 is_ambig pred = isClassPred pred &&
878 any ambig_var (varSetElems (tyVarsOfPred pred))
880 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
881 not (ct_var `elemVarSet` extended_tau_vars)
884 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
885 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
886 ptext SLIT("must be reachable from the type after the '=>'"))]
889 In addition, GHC insists that at least one type variable
890 in each constraint is in V. So we disallow a type like
891 forall a. Eq b => b -> b
892 even in a scope where b is in scope.
895 checkFreeness forall_tyvars theta
896 = mappM_ complain (filter is_free theta)
898 is_free pred = not (isIPPred pred)
899 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
900 bound_var ct_var = ct_var `elem` forall_tyvars
901 complain pred = addErrTc (freeErr pred)
904 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
905 ptext SLIT("are already in scope"),
906 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
911 checkThetaCtxt ctxt theta
912 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
913 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
915 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
916 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
917 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
919 arityErr kind name n m
920 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
921 n_arguments <> comma, text "but has been given", int m]
923 n_arguments | n == 0 = ptext SLIT("no arguments")
924 | n == 1 = ptext SLIT("1 argument")
925 | True = hsep [int n, ptext SLIT("arguments")]
929 %************************************************************************
931 \subsection{Checking for a decent instance head type}
933 %************************************************************************
935 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
936 it must normally look like: @instance Foo (Tycon a b c ...) ...@
938 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
939 flag is on, or (2)~the instance is imported (they must have been
940 compiled elsewhere). In these cases, we let them go through anyway.
942 We can also have instances for functions: @instance Foo (a -> b) ...@.
945 checkValidInstHead :: Type -> TcM (Class, [TcType])
947 checkValidInstHead ty -- Should be a source type
948 = case tcSplitPredTy_maybe ty of {
949 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
952 case getClassPredTys_maybe pred of {
953 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
956 getDOpts `thenM` \ dflags ->
957 mappM_ check_arg_type tys `thenM_`
958 check_inst_head dflags clas tys `thenM_`
962 check_inst_head dflags clas tys
963 -- If GlasgowExts then check at least one isn't a type variable
964 | dopt Opt_GlasgowExts dflags
965 = check_tyvars dflags clas tys
967 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
969 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
970 not (isSynTyCon tycon), -- ...but not a synonym
971 all tcIsTyVarTy arg_tys, -- Applied to type variables
972 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
973 -- This last condition checks that all the type variables are distinct
977 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
982 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
983 text "where T is not a synonym, and a,b,c are distinct type variables")
985 check_tyvars dflags clas tys
986 -- Check that at least one isn't a type variable
987 -- unless -fallow-undecideable-instances
988 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
989 | not (all tcIsTyVarTy tys) = returnM ()
990 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
992 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
995 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
999 instTypeErr pp_ty msg
1000 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,