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, 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,
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 ->
140 %************************************************************************
142 \subsection{Type instantiation}
144 %************************************************************************
146 Instantiating a bunch of type variables
149 tcInstTyVars :: TyVarDetails -> [TyVar]
150 -> TcM ([TcTyVar], [TcType], Subst)
152 tcInstTyVars tv_details tyvars
153 = mappM (tcInstTyVar tv_details) tyvars `thenM` \ tc_tyvars ->
155 tys = mkTyVarTys tc_tyvars
157 returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
158 -- Since the tyvars are freshly made,
159 -- they cannot possibly be captured by
160 -- any existing for-alls. Hence mkTopTyVarSubst
162 tcInstTyVar tv_details tyvar
163 = newUnique `thenM` \ uniq ->
165 name = setNameUnique (tyVarName tyvar) uniq
166 -- Note that we don't change the print-name
167 -- This won't confuse the type checker but there's a chance
168 -- that two different tyvars will print the same way
169 -- in an error message. -dppr-debug will show up the difference
170 -- Better watch out for this. If worst comes to worst, just
173 newMutTyVar name (tyVarKind tyvar) tv_details
175 tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
176 -- tcInstType instantiates the outer-level for-alls of a TcType with
177 -- fresh (mutable) type variables, splits off the dictionary part,
178 -- and returns the pieces.
179 tcInstType tv_details ty
180 = case tcSplitForAllTys ty of
181 ([], rho) -> -- There may be overloading despite no type variables;
182 -- (?x :: Int) => Int -> Int
184 (theta, tau) = tcSplitPhiTy rho
186 returnM ([], theta, tau)
188 (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenM` \ (tyvars', _, tenv) ->
190 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
192 returnM (tyvars', theta, tau)
196 %************************************************************************
198 \subsection{Putting and getting mutable type variables}
200 %************************************************************************
203 putTcTyVar :: TcTyVar -> TcType -> TcM TcType
204 getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
211 | not (isMutTyVar tyvar)
212 = pprTrace "putTcTyVar" (ppr tyvar) $
216 = ASSERT( isMutTyVar tyvar )
217 writeMutTyVar tyvar (Just ty) `thenM_`
221 Getting is more interesting. The easy thing to do is just to read, thus:
224 getTcTyVar tyvar = readMutTyVar tyvar
227 But it's more fun to short out indirections on the way: If this
228 version returns a TyVar, then that TyVar is unbound. If it returns
229 any other type, then there might be bound TyVars embedded inside it.
231 We return Nothing iff the original box was unbound.
235 | not (isMutTyVar tyvar)
236 = pprTrace "getTcTyVar" (ppr tyvar) $
237 returnM (Just (mkTyVarTy tyvar))
240 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
241 readMutTyVar tyvar `thenM` \ maybe_ty ->
243 Just ty -> short_out ty `thenM` \ ty' ->
244 writeMutTyVar tyvar (Just ty') `thenM_`
247 Nothing -> returnM Nothing
249 short_out :: TcType -> TcM TcType
250 short_out ty@(TyVarTy tyvar)
251 | not (isMutTyVar tyvar)
255 = readMutTyVar tyvar `thenM` \ maybe_ty ->
257 Just ty' -> short_out ty' `thenM` \ ty' ->
258 writeMutTyVar tyvar (Just ty') `thenM_`
263 short_out other_ty = returnM other_ty
267 %************************************************************************
269 \subsection{Zonking -- the exernal interfaces}
271 %************************************************************************
273 ----------------- Type variables
276 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
277 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
279 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
280 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
281 returnM (tyVarsOfTypes tys)
283 zonkTcTyVar :: TcTyVar -> TcM TcType
284 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
287 ----------------- Types
290 zonkTcType :: TcType -> TcM TcType
291 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
293 zonkTcTypes :: [TcType] -> TcM [TcType]
294 zonkTcTypes tys = mappM zonkTcType tys
296 zonkTcClassConstraints cts = mappM zonk cts
297 where zonk (clas, tys)
298 = zonkTcTypes tys `thenM` \ new_tys ->
299 returnM (clas, new_tys)
301 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
302 zonkTcThetaType theta = mappM zonkTcPredType theta
304 zonkTcPredType :: TcPredType -> TcM TcPredType
305 zonkTcPredType (ClassP c ts)
306 = zonkTcTypes ts `thenM` \ new_ts ->
307 returnM (ClassP c new_ts)
308 zonkTcPredType (IParam n t)
309 = zonkTcType t `thenM` \ new_t ->
310 returnM (IParam n new_t)
313 ------------------- These ...ToType, ...ToKind versions
314 are used at the end of type checking
317 zonkTcKindToKind :: TcKind -> TcM Kind
318 zonkTcKindToKind tc_kind
319 = zonkType zonk_unbound_kind_var tc_kind
321 -- When zonking a kind, we want to
322 -- zonk a *kind* variable to (Type *)
323 -- zonk a *boxity* variable to *
324 zonk_unbound_kind_var kv
325 | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
326 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
327 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
329 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
330 -- of a type variable, at the *end* of type checking. It changes
331 -- the *mutable* type variable into an *immutable* one.
333 -- It does this by making an immutable version of tv and binds tv to it.
334 -- Now any bound occurences of the original type variable will get
335 -- zonked to the immutable version.
337 zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
338 zonkTcTyVarToTyVar tv
340 -- Make an immutable version, defaulting
341 -- the kind to lifted if necessary
342 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
343 immut_tv_ty = mkTyVarTy immut_tv
345 zap tv = putTcTyVar tv immut_tv_ty
346 -- Bind the mutable version to the immutable one
348 -- If the type variable is mutable, then bind it to immut_tv_ty
349 -- so that all other occurrences of the tyvar will get zapped too
350 zonkTyVar zap tv `thenM` \ ty2 ->
352 -- This warning shows up if the allegedly-unbound tyvar is
353 -- already bound to something. It can actually happen, and
354 -- in a harmless way (see [Silly Type Synonyms] below) so
355 -- it's only a warning
356 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
361 [Silly Type Synonyms]
364 type C u a = u -- Note 'a' unused
366 foo :: (forall a. C u a -> C u a) -> u
370 bar = foo (\t -> t + t)
372 * From the (\t -> t+t) we get type {Num d} => d -> d
375 * Now unify with type of foo's arg, and we get:
376 {Num (C d a)} => C d a -> C d a
379 * Now abstract over the 'a', but float out the Num (C d a) constraint
380 because it does not 'really' mention a. (see Type.tyVarsOfType)
381 The arg to foo becomes
384 * So we get a dict binding for Num (C d a), which is zonked to give
387 * Then the /\a abstraction has a zonked 'a' in it.
389 All very silly. I think its harmless to ignore the problem.
392 %************************************************************************
394 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
396 %* For internal use only! *
398 %************************************************************************
401 -- zonkType is used for Kinds as well
403 -- For unbound, mutable tyvars, zonkType uses the function given to it
404 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
405 -- type variable and zonks the kind too
407 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
408 -- see zonkTcType, and zonkTcTypeToType
411 zonkType unbound_var_fn ty
414 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
415 returnM (TyConApp tycon tys')
417 go (NewTcApp tycon tys) = mappM go tys `thenM` \ tys' ->
418 returnM (NewTcApp tycon tys')
420 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
421 go ty2 `thenM` \ ty2' ->
422 returnM (NoteTy (SynNote ty1') ty2')
424 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
426 go (PredTy p) = go_pred p `thenM` \ p' ->
429 go (FunTy arg res) = go arg `thenM` \ arg' ->
430 go res `thenM` \ res' ->
431 returnM (FunTy arg' res')
433 go (AppTy fun arg) = go fun `thenM` \ fun' ->
434 go arg `thenM` \ arg' ->
435 returnM (mkAppTy fun' arg')
436 -- NB the mkAppTy; we might have instantiated a
437 -- type variable to a type constructor, so we need
438 -- to pull the TyConApp to the top.
440 -- The two interesting cases!
441 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
443 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenM` \ tyvar' ->
444 go ty `thenM` \ ty' ->
445 returnM (ForAllTy tyvar' ty')
447 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
448 returnM (ClassP c tys')
449 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
450 returnM (IParam n ty')
452 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
453 -> TcTyVar -> TcM TcType
454 zonkTyVar unbound_var_fn tyvar
455 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
456 -- zonking a forall type, when the bound type variable
457 -- needn't be mutable
458 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
459 returnM (TyVarTy tyvar)
462 = getTcTyVar tyvar `thenM` \ maybe_ty ->
464 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
465 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
470 %************************************************************************
472 \subsection{Checking a user type}
474 %************************************************************************
476 When dealing with a user-written type, we first translate it from an HsType
477 to a Type, performing kind checking, and then check various things that should
478 be true about it. We don't want to perform these checks at the same time
479 as the initial translation because (a) they are unnecessary for interface-file
480 types and (b) when checking a mutually recursive group of type and class decls,
481 we can't "look" at the tycons/classes yet. Also, the checks are are rather
482 diverse, and used to really mess up the other code.
484 One thing we check for is 'rank'.
486 Rank 0: monotypes (no foralls)
487 Rank 1: foralls at the front only, Rank 0 inside
488 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
490 basic ::= tyvar | T basic ... basic
492 r2 ::= forall tvs. cxt => r2a
493 r2a ::= r1 -> r2a | basic
494 r1 ::= forall tvs. cxt => r0
495 r0 ::= r0 -> r0 | basic
497 Another thing is to check that type synonyms are saturated.
498 This might not necessarily show up in kind checking.
500 data T k = MkT (k Int)
506 = FunSigCtxt Name -- Function type signature
507 | ExprSigCtxt -- Expression type signature
508 | ConArgCtxt Name -- Data constructor argument
509 | TySynCtxt Name -- RHS of a type synonym decl
510 | GenPatCtxt -- Pattern in generic decl
511 -- f{| a+b |} (Inl x) = ...
512 | PatSigCtxt -- Type sig in pattern
514 | ResSigCtxt -- Result type sig
516 | ForSigCtxt Name -- Foreign inport or export signature
517 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
518 | DefaultDeclCtxt -- Types in a default declaration
520 -- Notes re TySynCtxt
521 -- We allow type synonyms that aren't types; e.g. type List = []
523 -- If the RHS mentions tyvars that aren't in scope, we'll
524 -- quantify over them:
525 -- e.g. type T = a->a
526 -- will become type T = forall a. a->a
528 -- With gla-exts that's right, but for H98 we should complain.
531 pprHsSigCtxt :: UserTypeCtxt -> HsType Name -> SDoc
532 pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt hs_ty ctxt
534 pprUserTypeCtxt ty (FunSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
535 pprUserTypeCtxt ty ExprSigCtxt = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
536 pprUserTypeCtxt ty (ConArgCtxt c) = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
537 pprUserTypeCtxt ty (TySynCtxt c) = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
538 nest 2 (ptext SLIT(", namely") <+> ppr ty)]
539 pprUserTypeCtxt ty GenPatCtxt = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
540 pprUserTypeCtxt ty PatSigCtxt = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
541 pprUserTypeCtxt ty ResSigCtxt = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
542 pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
543 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
544 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
546 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
550 checkValidType :: UserTypeCtxt -> Type -> TcM ()
551 -- Checks that the type is valid for the given context
552 checkValidType ctxt ty
553 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
554 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
556 rank | gla_exts = Arbitrary
558 = case ctxt of -- Haskell 98
561 DefaultDeclCtxt-> Rank 0
563 TySynCtxt _ -> Rank 0
564 ExprSigCtxt -> Rank 1
565 FunSigCtxt _ -> Rank 1
566 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
567 -- constructor, hence rank 1
568 ForSigCtxt _ -> Rank 1
569 RuleSigCtxt _ -> Rank 1
571 actual_kind = typeKind ty
573 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
575 kind_ok = case ctxt of
576 TySynCtxt _ -> True -- Any kind will do
577 GenPatCtxt -> actual_kind_is_lifted
578 ForSigCtxt _ -> actual_kind_is_lifted
579 other -> isTypeKind actual_kind
581 ubx_tup | not gla_exts = UT_NotOk
582 | otherwise = case ctxt of
585 -- Unboxed tuples ok in function results,
586 -- but for type synonyms we allow them even at
589 -- Check that the thing has kind Type, and is lifted if necessary
590 checkTc kind_ok (kindErr actual_kind) `thenM_`
592 -- Check the internal validity of the type itself
593 check_poly_type rank ubx_tup ty `thenM_`
595 traceTc (text "checkValidType done" <+> ppr ty)
600 data Rank = Rank Int | Arbitrary
602 decRank :: Rank -> Rank
603 decRank Arbitrary = Arbitrary
604 decRank (Rank n) = Rank (n-1)
606 ----------------------------------------
607 data UbxTupFlag = UT_Ok | UT_NotOk
608 -- The "Ok" version means "ok if -fglasgow-exts is on"
610 ----------------------------------------
611 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
612 check_poly_type (Rank 0) ubx_tup ty
613 = check_tau_type (Rank 0) ubx_tup ty
615 check_poly_type rank ubx_tup ty
617 (tvs, theta, tau) = tcSplitSigmaTy ty
619 check_valid_theta SigmaCtxt theta `thenM_`
620 check_tau_type (decRank rank) ubx_tup tau `thenM_`
621 checkFreeness tvs theta `thenM_`
622 checkAmbiguity tvs theta (tyVarsOfType tau)
624 ----------------------------------------
625 check_arg_type :: Type -> TcM ()
626 -- The sort of type that can instantiate a type variable,
627 -- or be the argument of a type constructor.
628 -- Not an unboxed tuple, not a forall.
629 -- Other unboxed types are very occasionally allowed as type
630 -- arguments depending on the kind of the type constructor
632 -- For example, we want to reject things like:
634 -- instance Ord a => Ord (forall s. T s a)
636 -- g :: T s (forall b.b)
638 -- NB: unboxed tuples can have polymorphic or unboxed args.
639 -- This happens in the workers for functions returning
640 -- product types with polymorphic components.
641 -- But not in user code.
642 -- Anyway, they are dealt with by a special case in check_tau_type
645 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
646 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
648 ----------------------------------------
649 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
650 -- Rank is allowed rank for function args
651 -- No foralls otherwise
653 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
654 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
655 check_source_ty dflags TypeCtxt sty
656 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
657 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
658 = check_poly_type rank UT_NotOk arg_ty `thenM_`
659 check_tau_type rank UT_Ok res_ty
661 check_tau_type rank ubx_tup (AppTy ty1 ty2)
662 = check_arg_type ty1 `thenM_` check_arg_type ty2
664 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
665 -- Synonym notes are built only when the synonym is
666 -- saturated (see Type.mkSynTy)
667 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
669 -- If -fglasgow-exts then don't check the 'note' part.
670 -- This allows us to instantiate a synonym defn with a
671 -- for-all type, or with a partially-applied type synonym.
672 -- e.g. type T a b = a
675 -- Here, T is partially applied, so it's illegal in H98.
676 -- But if you expand S first, then T we get just
681 -- For H98, do check the un-expanded part
682 check_tau_type rank ubx_tup syn
685 check_tau_type rank ubx_tup ty
687 check_tau_type rank ubx_tup (NoteTy other_note ty)
688 = check_tau_type rank ubx_tup ty
690 check_tau_type rank ubx_tup (NewTcApp tc tys)
691 = mappM_ check_arg_type tys
693 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
695 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
696 -- synonym application, leaving it to checkValidType (i.e. right here)
698 checkTc syn_arity_ok arity_msg `thenM_`
699 mappM_ check_arg_type tys
701 | isUnboxedTupleTyCon tc
702 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
703 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
704 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
705 -- Args are allowed to be unlifted, or
706 -- more unboxed tuples, so can't use check_arg_ty
709 = mappM_ check_arg_type tys
712 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
714 syn_arity_ok = tc_arity <= n_args
715 -- It's OK to have an *over-applied* type synonym
716 -- data Tree a b = ...
717 -- type Foo a = Tree [a]
718 -- f :: Foo a b -> ...
720 tc_arity = tyConArity tc
722 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
723 ubx_tup_msg = ubxArgTyErr ty
725 ----------------------------------------
726 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr ty
727 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
728 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
729 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
734 %************************************************************************
736 \subsection{Checking a theta or source type}
738 %************************************************************************
741 -- Enumerate the contexts in which a "source type", <S>, can occur
745 -- or (N a) where N is a newtype
748 = ClassSCCtxt Name -- Superclasses of clas
749 -- class <S> => C a where ...
750 | SigmaCtxt -- Theta part of a normal for-all type
751 -- f :: <S> => a -> a
752 | DataTyCtxt Name -- Theta part of a data decl
753 -- data <S> => T a = MkT a
754 | TypeCtxt -- Source type in an ordinary type
756 | InstThetaCtxt -- Context of an instance decl
757 -- instance <S> => C [a] where ...
758 | InstHeadCtxt -- Head of an instance decl
759 -- instance ... => Eq a where ...
761 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
762 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
763 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
764 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
765 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
766 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
770 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
771 checkValidTheta ctxt theta
772 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
774 -------------------------
775 check_valid_theta ctxt []
777 check_valid_theta ctxt theta
778 = getDOpts `thenM` \ dflags ->
779 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
780 -- Actually, in instance decls and type signatures,
781 -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
782 -- so this error can only fire for the context of a class or
784 mappM_ (check_source_ty dflags ctxt) theta
786 (_,dups) = removeDups tcCmpPred theta
788 -------------------------
789 check_source_ty dflags ctxt pred@(ClassP cls tys)
790 = -- Class predicates are valid in all contexts
791 checkTc (arity == n_tys) arity_err `thenM_`
793 -- Check the form of the argument types
794 mappM_ check_arg_type tys `thenM_`
795 checkTc (check_class_pred_tys dflags ctxt tys)
796 (predTyVarErr pred $$ how_to_allow)
799 class_name = className cls
800 arity = classArity cls
802 arity_err = arityErr "Class" class_name arity n_tys
804 how_to_allow = case ctxt of
805 InstHeadCtxt -> empty -- Should not happen
806 InstThetaCtxt -> parens undecidableMsg
807 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
809 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
810 -- Implicit parameters only allows in type
811 -- signatures; not in instance decls, superclasses etc
812 -- The reason for not allowing implicit params in instances is a bit subtle
813 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
814 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
815 -- discharge all the potential usas of the ?x in e. For example, a
816 -- constraint Foo [Int] might come out of e,and applying the
817 -- instance decl would show up two uses of ?x.
820 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
822 -------------------------
823 check_class_pred_tys dflags ctxt tys
825 InstHeadCtxt -> True -- We check for instance-head
826 -- formation in checkValidInstHead
827 InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
828 other -> gla_exts || all tyvar_head tys
830 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
831 gla_exts = dopt Opt_GlasgowExts dflags
833 -------------------------
834 tyvar_head ty -- Haskell 98 allows predicates of form
835 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
836 | otherwise -- where a is a type variable
837 = case tcSplitAppTy_maybe ty of
838 Just (ty, _) -> tyvar_head ty
845 is ambiguous if P contains generic variables
846 (i.e. one of the Vs) that are not mentioned in tau
848 However, we need to take account of functional dependencies
849 when we speak of 'mentioned in tau'. Example:
850 class C a b | a -> b where ...
852 forall x y. (C x y) => x
853 is not ambiguous because x is mentioned and x determines y
855 NB; the ambiguity check is only used for *user* types, not for types
856 coming from inteface files. The latter can legitimately have
857 ambiguous types. Example
859 class S a where s :: a -> (Int,Int)
860 instance S Char where s _ = (1,1)
861 f:: S a => [a] -> Int -> (Int,Int)
862 f (_::[a]) x = (a*x,b)
863 where (a,b) = s (undefined::a)
865 Here the worker for f gets the type
866 fw :: forall a. S a => Int -> (# Int, Int #)
868 If the list of tv_names is empty, we have a monotype, and then we
869 don't need to check for ambiguity either, because the test can't fail
873 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
874 checkAmbiguity forall_tyvars theta tau_tyvars
875 = mappM_ complain (filter is_ambig theta)
877 complain pred = addErrTc (ambigErr pred)
878 extended_tau_vars = grow theta tau_tyvars
880 -- Only a *class* predicate can give rise to ambiguity
881 -- An *implicit parameter* cannot. For example:
882 -- foo :: (?x :: [a]) => Int
884 -- is fine. The call site will suppply a particular 'x'
885 is_ambig pred = isClassPred pred &&
886 any ambig_var (varSetElems (tyVarsOfPred pred))
888 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
889 not (ct_var `elemVarSet` extended_tau_vars)
892 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
893 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
894 ptext SLIT("must be reachable from the type after the '=>'"))]
897 In addition, GHC insists that at least one type variable
898 in each constraint is in V. So we disallow a type like
899 forall a. Eq b => b -> b
900 even in a scope where b is in scope.
903 checkFreeness forall_tyvars theta
904 = mappM_ complain (filter is_free theta)
906 is_free pred = not (isIPPred pred)
907 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
908 bound_var ct_var = ct_var `elem` forall_tyvars
909 complain pred = addErrTc (freeErr pred)
912 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
913 ptext SLIT("are already in scope"),
914 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
919 checkThetaCtxt ctxt theta
920 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
921 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
923 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
924 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
925 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
927 arityErr kind name n m
928 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
929 n_arguments <> comma, text "but has been given", int m]
931 n_arguments | n == 0 = ptext SLIT("no arguments")
932 | n == 1 = ptext SLIT("1 argument")
933 | True = hsep [int n, ptext SLIT("arguments")]
937 %************************************************************************
939 \subsection{Checking for a decent instance head type}
941 %************************************************************************
943 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
944 it must normally look like: @instance Foo (Tycon a b c ...) ...@
946 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
947 flag is on, or (2)~the instance is imported (they must have been
948 compiled elsewhere). In these cases, we let them go through anyway.
950 We can also have instances for functions: @instance Foo (a -> b) ...@.
953 checkValidInstHead :: Type -> TcM (Class, [TcType])
955 checkValidInstHead ty -- Should be a source type
956 = case tcSplitPredTy_maybe ty of {
957 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
960 case getClassPredTys_maybe pred of {
961 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
964 getDOpts `thenM` \ dflags ->
965 mappM_ check_arg_type tys `thenM_`
966 check_inst_head dflags clas tys `thenM_`
970 check_inst_head dflags clas tys
971 -- If GlasgowExts then check at least one isn't a type variable
972 | dopt Opt_GlasgowExts dflags
973 = check_tyvars dflags clas tys
975 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
977 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
978 not (isSynTyCon tycon), -- ...but not a synonym
979 all tcIsTyVarTy arg_tys, -- Applied to type variables
980 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
981 -- This last condition checks that all the type variables are distinct
985 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
990 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
991 text "where T is not a synonym, and a,b,c are distinct type variables")
993 check_tyvars dflags clas tys
994 -- Check that at least one isn't a type variable
995 -- unless -fallow-undecideable-instances
996 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
997 | not (all tcIsTyVarTy tys) = returnM ()
998 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1000 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1003 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1007 instTypeErr pp_ty msg
1008 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,