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,
64 eqKind, isTypeKind, pprThetaArrow,
65 pprPred, pprTheta, pprClassPred )
66 import Subst ( Subst, mkTopTyVarSubst, substTy )
67 import Class ( Class, classArity, className )
68 import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
69 tyConArity, tyConName )
70 import Var ( TyVar, tyVarKind, tyVarName, isTyVar,
71 mkTyVar, mkMutTyVar, isMutTyVar, mutTyVarRef )
74 import TcRnMonad -- TcType, amongst others
75 import FunDeps ( grow )
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 ->
136 newOpenTypeKind :: TcM TcKind
137 newOpenTypeKind = newBoxityVar `thenM` \ bx_var ->
138 returnM (mkTyConApp typeCon [bx_var])
142 %************************************************************************
144 \subsection{Type instantiation}
146 %************************************************************************
148 Instantiating a bunch of type variables
151 tcInstTyVars :: TyVarDetails -> [TyVar]
152 -> TcM ([TcTyVar], [TcType], Subst)
154 tcInstTyVars tv_details tyvars
155 = mappM (tcInstTyVar tv_details) tyvars `thenM` \ tc_tyvars ->
157 tys = mkTyVarTys tc_tyvars
159 returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
160 -- Since the tyvars are freshly made,
161 -- they cannot possibly be captured by
162 -- any existing for-alls. Hence mkTopTyVarSubst
164 tcInstTyVar tv_details tyvar
165 = newUnique `thenM` \ uniq ->
167 name = setNameUnique (tyVarName tyvar) uniq
168 -- Note that we don't change the print-name
169 -- This won't confuse the type checker but there's a chance
170 -- that two different tyvars will print the same way
171 -- in an error message. -dppr-debug will show up the difference
172 -- Better watch out for this. If worst comes to worst, just
175 newMutTyVar name (tyVarKind tyvar) tv_details
177 tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
178 -- tcInstType instantiates the outer-level for-alls of a TcType with
179 -- fresh (mutable) type variables, splits off the dictionary part,
180 -- and returns the pieces.
181 tcInstType tv_details ty
182 = case tcSplitForAllTys ty of
183 ([], rho) -> -- There may be overloading despite no type variables;
184 -- (?x :: Int) => Int -> Int
186 (theta, tau) = tcSplitPhiTy rho
188 returnM ([], theta, tau)
190 (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenM` \ (tyvars', _, tenv) ->
192 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
194 returnM (tyvars', theta, tau)
198 %************************************************************************
200 \subsection{Putting and getting mutable type variables}
202 %************************************************************************
205 putTcTyVar :: TcTyVar -> TcType -> TcM TcType
206 getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
213 | not (isMutTyVar tyvar)
214 = pprTrace "putTcTyVar" (ppr tyvar) $
218 = ASSERT( isMutTyVar tyvar )
219 writeMutTyVar tyvar (Just ty) `thenM_`
223 Getting is more interesting. The easy thing to do is just to read, thus:
226 getTcTyVar tyvar = readMutTyVar tyvar
229 But it's more fun to short out indirections on the way: If this
230 version returns a TyVar, then that TyVar is unbound. If it returns
231 any other type, then there might be bound TyVars embedded inside it.
233 We return Nothing iff the original box was unbound.
237 | not (isMutTyVar tyvar)
238 = pprTrace "getTcTyVar" (ppr tyvar) $
239 returnM (Just (mkTyVarTy tyvar))
242 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
243 readMutTyVar tyvar `thenM` \ maybe_ty ->
245 Just ty -> short_out ty `thenM` \ ty' ->
246 writeMutTyVar tyvar (Just ty') `thenM_`
249 Nothing -> returnM Nothing
251 short_out :: TcType -> TcM TcType
252 short_out ty@(TyVarTy tyvar)
253 | not (isMutTyVar tyvar)
257 = readMutTyVar tyvar `thenM` \ maybe_ty ->
259 Just ty' -> short_out ty' `thenM` \ ty' ->
260 writeMutTyVar tyvar (Just ty') `thenM_`
265 short_out other_ty = returnM other_ty
269 %************************************************************************
271 \subsection{Zonking -- the exernal interfaces}
273 %************************************************************************
275 ----------------- Type variables
278 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
279 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
281 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
282 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
283 returnM (tyVarsOfTypes tys)
285 zonkTcTyVar :: TcTyVar -> TcM TcType
286 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
289 ----------------- Types
292 zonkTcType :: TcType -> TcM TcType
293 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
295 zonkTcTypes :: [TcType] -> TcM [TcType]
296 zonkTcTypes tys = mappM zonkTcType tys
298 zonkTcClassConstraints cts = mappM zonk cts
299 where zonk (clas, tys)
300 = zonkTcTypes tys `thenM` \ new_tys ->
301 returnM (clas, new_tys)
303 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
304 zonkTcThetaType theta = mappM zonkTcPredType theta
306 zonkTcPredType :: TcPredType -> TcM TcPredType
307 zonkTcPredType (ClassP c ts)
308 = zonkTcTypes ts `thenM` \ new_ts ->
309 returnM (ClassP c new_ts)
310 zonkTcPredType (IParam n t)
311 = zonkTcType t `thenM` \ new_t ->
312 returnM (IParam n new_t)
315 ------------------- These ...ToType, ...ToKind versions
316 are used at the end of type checking
319 zonkTcKindToKind :: TcKind -> TcM Kind
320 zonkTcKindToKind tc_kind
321 = zonkType zonk_unbound_kind_var tc_kind
323 -- When zonking a kind, we want to
324 -- zonk a *kind* variable to (Type *)
325 -- zonk a *boxity* variable to *
326 zonk_unbound_kind_var kv
327 | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
328 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
329 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
331 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
332 -- of a type variable, at the *end* of type checking. It changes
333 -- the *mutable* type variable into an *immutable* one.
335 -- It does this by making an immutable version of tv and binds tv to it.
336 -- Now any bound occurences of the original type variable will get
337 -- zonked to the immutable version.
339 zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
340 zonkTcTyVarToTyVar tv
342 -- Make an immutable version, defaulting
343 -- the kind to lifted if necessary
344 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
345 immut_tv_ty = mkTyVarTy immut_tv
347 zap tv = putTcTyVar tv immut_tv_ty
348 -- Bind the mutable version to the immutable one
350 -- If the type variable is mutable, then bind it to immut_tv_ty
351 -- so that all other occurrences of the tyvar will get zapped too
352 zonkTyVar zap tv `thenM` \ ty2 ->
354 -- This warning shows up if the allegedly-unbound tyvar is
355 -- already bound to something. It can actually happen, and
356 -- in a harmless way (see [Silly Type Synonyms] below) so
357 -- it's only a warning
358 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
363 [Silly Type Synonyms]
366 type C u a = u -- Note 'a' unused
368 foo :: (forall a. C u a -> C u a) -> u
372 bar = foo (\t -> t + t)
374 * From the (\t -> t+t) we get type {Num d} => d -> d
377 * Now unify with type of foo's arg, and we get:
378 {Num (C d a)} => C d a -> C d a
381 * Now abstract over the 'a', but float out the Num (C d a) constraint
382 because it does not 'really' mention a. (see Type.tyVarsOfType)
383 The arg to foo becomes
386 * So we get a dict binding for Num (C d a), which is zonked to give
389 * Then the /\a abstraction has a zonked 'a' in it.
391 All very silly. I think its harmless to ignore the problem.
394 %************************************************************************
396 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
398 %* For internal use only! *
400 %************************************************************************
403 -- zonkType is used for Kinds as well
405 -- For unbound, mutable tyvars, zonkType uses the function given to it
406 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
407 -- type variable and zonks the kind too
409 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
410 -- see zonkTcType, and zonkTcTypeToType
413 zonkType unbound_var_fn ty
416 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
417 returnM (TyConApp tycon tys')
419 go (NewTcApp tycon tys) = mappM go tys `thenM` \ tys' ->
420 returnM (NewTcApp tycon tys')
422 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
423 go ty2 `thenM` \ ty2' ->
424 returnM (NoteTy (SynNote ty1') ty2')
426 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
428 go (PredTy p) = go_pred p `thenM` \ p' ->
431 go (FunTy arg res) = go arg `thenM` \ arg' ->
432 go res `thenM` \ res' ->
433 returnM (FunTy arg' res')
435 go (AppTy fun arg) = go fun `thenM` \ fun' ->
436 go arg `thenM` \ arg' ->
437 returnM (mkAppTy fun' arg')
438 -- NB the mkAppTy; we might have instantiated a
439 -- type variable to a type constructor, so we need
440 -- to pull the TyConApp to the top.
442 -- The two interesting cases!
443 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
445 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenM` \ tyvar' ->
446 go ty `thenM` \ ty' ->
447 returnM (ForAllTy tyvar' ty')
449 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
450 returnM (ClassP c tys')
451 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
452 returnM (IParam n ty')
454 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
455 -> TcTyVar -> TcM TcType
456 zonkTyVar unbound_var_fn tyvar
457 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
458 -- zonking a forall type, when the bound type variable
459 -- needn't be mutable
460 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
461 returnM (TyVarTy tyvar)
464 = getTcTyVar tyvar `thenM` \ maybe_ty ->
466 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
467 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
472 %************************************************************************
474 \subsection{Checking a user type}
476 %************************************************************************
478 When dealing with a user-written type, we first translate it from an HsType
479 to a Type, performing kind checking, and then check various things that should
480 be true about it. We don't want to perform these checks at the same time
481 as the initial translation because (a) they are unnecessary for interface-file
482 types and (b) when checking a mutually recursive group of type and class decls,
483 we can't "look" at the tycons/classes yet. Also, the checks are are rather
484 diverse, and used to really mess up the other code.
486 One thing we check for is 'rank'.
488 Rank 0: monotypes (no foralls)
489 Rank 1: foralls at the front only, Rank 0 inside
490 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
492 basic ::= tyvar | T basic ... basic
494 r2 ::= forall tvs. cxt => r2a
495 r2a ::= r1 -> r2a | basic
496 r1 ::= forall tvs. cxt => r0
497 r0 ::= r0 -> r0 | basic
499 Another thing is to check that type synonyms are saturated.
500 This might not necessarily show up in kind checking.
502 data T k = MkT (k Int)
508 = FunSigCtxt Name -- Function type signature
509 | ExprSigCtxt -- Expression type signature
510 | ConArgCtxt Name -- Data constructor argument
511 | TySynCtxt Name -- RHS of a type synonym decl
512 | GenPatCtxt -- Pattern in generic decl
513 -- f{| a+b |} (Inl x) = ...
514 | PatSigCtxt -- Type sig in pattern
516 | ResSigCtxt -- Result type sig
518 | ForSigCtxt Name -- Foreign inport or export signature
519 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
520 | DefaultDeclCtxt -- Types in a default declaration
522 -- Notes re TySynCtxt
523 -- We allow type synonyms that aren't types; e.g. type List = []
525 -- If the RHS mentions tyvars that aren't in scope, we'll
526 -- quantify over them:
527 -- e.g. type T = a->a
528 -- will become type T = forall a. a->a
530 -- With gla-exts that's right, but for H98 we should complain.
533 pprHsSigCtxt :: UserTypeCtxt -> HsType Name -> SDoc
534 pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt hs_ty ctxt
536 pprUserTypeCtxt ty (FunSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
537 pprUserTypeCtxt ty ExprSigCtxt = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
538 pprUserTypeCtxt ty (ConArgCtxt c) = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
539 pprUserTypeCtxt ty (TySynCtxt c) = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
540 nest 2 (ptext SLIT(", namely") <+> ppr ty)]
541 pprUserTypeCtxt ty GenPatCtxt = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
542 pprUserTypeCtxt ty PatSigCtxt = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
543 pprUserTypeCtxt ty ResSigCtxt = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
544 pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
545 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
546 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
548 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
552 checkValidType :: UserTypeCtxt -> Type -> TcM ()
553 -- Checks that the type is valid for the given context
554 checkValidType ctxt ty
555 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
556 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
558 rank | gla_exts = Arbitrary
560 = case ctxt of -- Haskell 98
563 DefaultDeclCtxt-> Rank 0
565 TySynCtxt _ -> Rank 0
566 ExprSigCtxt -> Rank 1
567 FunSigCtxt _ -> Rank 1
568 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
569 -- constructor, hence rank 1
570 ForSigCtxt _ -> Rank 1
571 RuleSigCtxt _ -> Rank 1
573 actual_kind = typeKind ty
575 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
577 kind_ok = case ctxt of
578 TySynCtxt _ -> True -- Any kind will do
579 GenPatCtxt -> actual_kind_is_lifted
580 ForSigCtxt _ -> actual_kind_is_lifted
581 other -> isTypeKind actual_kind
583 ubx_tup | not gla_exts = UT_NotOk
584 | otherwise = case ctxt of
587 -- Unboxed tuples ok in function results,
588 -- but for type synonyms we allow them even at
591 -- Check that the thing has kind Type, and is lifted if necessary
592 checkTc kind_ok (kindErr actual_kind) `thenM_`
594 -- Check the internal validity of the type itself
595 check_poly_type rank ubx_tup ty `thenM_`
597 traceTc (text "checkValidType done" <+> ppr ty)
602 data Rank = Rank Int | Arbitrary
604 decRank :: Rank -> Rank
605 decRank Arbitrary = Arbitrary
606 decRank (Rank n) = Rank (n-1)
608 ----------------------------------------
609 data UbxTupFlag = UT_Ok | UT_NotOk
610 -- The "Ok" version means "ok if -fglasgow-exts is on"
612 ----------------------------------------
613 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
614 check_poly_type (Rank 0) ubx_tup ty
615 = check_tau_type (Rank 0) ubx_tup ty
617 check_poly_type rank ubx_tup ty
619 (tvs, theta, tau) = tcSplitSigmaTy ty
621 check_valid_theta SigmaCtxt theta `thenM_`
622 check_tau_type (decRank rank) ubx_tup tau `thenM_`
623 checkFreeness tvs theta `thenM_`
624 checkAmbiguity tvs theta (tyVarsOfType tau)
626 ----------------------------------------
627 check_arg_type :: Type -> TcM ()
628 -- The sort of type that can instantiate a type variable,
629 -- or be the argument of a type constructor.
630 -- Not an unboxed tuple, not a forall.
631 -- Other unboxed types are very occasionally allowed as type
632 -- arguments depending on the kind of the type constructor
634 -- For example, we want to reject things like:
636 -- instance Ord a => Ord (forall s. T s a)
638 -- g :: T s (forall b.b)
640 -- NB: unboxed tuples can have polymorphic or unboxed args.
641 -- This happens in the workers for functions returning
642 -- product types with polymorphic components.
643 -- But not in user code.
644 -- Anyway, they are dealt with by a special case in check_tau_type
647 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
648 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
650 ----------------------------------------
651 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
652 -- Rank is allowed rank for function args
653 -- No foralls otherwise
655 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
656 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
657 check_source_ty dflags TypeCtxt sty
658 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
659 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
660 = check_poly_type rank UT_NotOk arg_ty `thenM_`
661 check_tau_type rank UT_Ok res_ty
663 check_tau_type rank ubx_tup (AppTy ty1 ty2)
664 = check_arg_type ty1 `thenM_` check_arg_type ty2
666 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
667 -- Synonym notes are built only when the synonym is
668 -- saturated (see Type.mkSynTy)
669 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
671 -- If -fglasgow-exts then don't check the 'note' part.
672 -- This allows us to instantiate a synonym defn with a
673 -- for-all type, or with a partially-applied type synonym.
674 -- e.g. type T a b = a
677 -- Here, T is partially applied, so it's illegal in H98.
678 -- But if you expand S first, then T we get just
683 -- For H98, do check the un-expanded part
684 check_tau_type rank ubx_tup syn
687 check_tau_type rank ubx_tup ty
689 check_tau_type rank ubx_tup (NoteTy other_note ty)
690 = check_tau_type rank ubx_tup ty
692 check_tau_type rank ubx_tup (NewTcApp tc tys)
693 = mappM_ check_arg_type tys
695 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
697 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
698 -- synonym application, leaving it to checkValidType (i.e. right here)
700 checkTc syn_arity_ok arity_msg `thenM_`
701 mappM_ check_arg_type tys
703 | isUnboxedTupleTyCon tc
704 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
705 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
706 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
707 -- Args are allowed to be unlifted, or
708 -- more unboxed tuples, so can't use check_arg_ty
711 = mappM_ check_arg_type tys
714 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
716 syn_arity_ok = tc_arity <= n_args
717 -- It's OK to have an *over-applied* type synonym
718 -- data Tree a b = ...
719 -- type Foo a = Tree [a]
720 -- f :: Foo a b -> ...
722 tc_arity = tyConArity tc
724 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
725 ubx_tup_msg = ubxArgTyErr ty
727 ----------------------------------------
728 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr ty
729 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
730 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
731 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
736 %************************************************************************
738 \subsection{Checking a theta or source type}
740 %************************************************************************
743 -- Enumerate the contexts in which a "source type", <S>, can occur
747 -- or (N a) where N is a newtype
750 = ClassSCCtxt Name -- Superclasses of clas
751 -- class <S> => C a where ...
752 | SigmaCtxt -- Theta part of a normal for-all type
753 -- f :: <S> => a -> a
754 | DataTyCtxt Name -- Theta part of a data decl
755 -- data <S> => T a = MkT a
756 | TypeCtxt -- Source type in an ordinary type
758 | InstThetaCtxt -- Context of an instance decl
759 -- instance <S> => C [a] where ...
760 | InstHeadCtxt -- Head of an instance decl
761 -- instance ... => Eq a where ...
763 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
764 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
765 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
766 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
767 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
768 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
772 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
773 checkValidTheta ctxt theta
774 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
776 -------------------------
777 check_valid_theta ctxt []
779 check_valid_theta ctxt theta
780 = getDOpts `thenM` \ dflags ->
781 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
782 -- Actually, in instance decls and type signatures,
783 -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
784 -- so this error can only fire for the context of a class or
786 mappM_ (check_source_ty dflags ctxt) theta
788 (_,dups) = removeDups tcCmpPred theta
790 -------------------------
791 check_source_ty dflags ctxt pred@(ClassP cls tys)
792 = -- Class predicates are valid in all contexts
793 checkTc (arity == n_tys) arity_err `thenM_`
795 -- Check the form of the argument types
796 mappM_ check_arg_type tys `thenM_`
797 checkTc (check_class_pred_tys dflags ctxt tys)
798 (predTyVarErr pred $$ how_to_allow)
801 class_name = className cls
802 arity = classArity cls
804 arity_err = arityErr "Class" class_name arity n_tys
806 how_to_allow = case ctxt of
807 InstHeadCtxt -> empty -- Should not happen
808 InstThetaCtxt -> parens undecidableMsg
809 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
811 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
812 -- Implicit parameters only allows in type
813 -- signatures; not in instance decls, superclasses etc
814 -- The reason for not allowing implicit params in instances is a bit subtle
815 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
816 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
817 -- discharge all the potential usas of the ?x in e. For example, a
818 -- constraint Foo [Int] might come out of e,and applying the
819 -- instance decl would show up two uses of ?x.
822 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
824 -------------------------
825 check_class_pred_tys dflags ctxt tys
827 InstHeadCtxt -> True -- We check for instance-head
828 -- formation in checkValidInstHead
829 InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
830 other -> gla_exts || all tyvar_head tys
832 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
833 gla_exts = dopt Opt_GlasgowExts dflags
835 -------------------------
836 tyvar_head ty -- Haskell 98 allows predicates of form
837 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
838 | otherwise -- where a is a type variable
839 = case tcSplitAppTy_maybe ty of
840 Just (ty, _) -> tyvar_head ty
847 is ambiguous if P contains generic variables
848 (i.e. one of the Vs) that are not mentioned in tau
850 However, we need to take account of functional dependencies
851 when we speak of 'mentioned in tau'. Example:
852 class C a b | a -> b where ...
854 forall x y. (C x y) => x
855 is not ambiguous because x is mentioned and x determines y
857 NB; the ambiguity check is only used for *user* types, not for types
858 coming from inteface files. The latter can legitimately have
859 ambiguous types. Example
861 class S a where s :: a -> (Int,Int)
862 instance S Char where s _ = (1,1)
863 f:: S a => [a] -> Int -> (Int,Int)
864 f (_::[a]) x = (a*x,b)
865 where (a,b) = s (undefined::a)
867 Here the worker for f gets the type
868 fw :: forall a. S a => Int -> (# Int, Int #)
870 If the list of tv_names is empty, we have a monotype, and then we
871 don't need to check for ambiguity either, because the test can't fail
875 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
876 checkAmbiguity forall_tyvars theta tau_tyvars
877 = mappM_ complain (filter is_ambig theta)
879 complain pred = addErrTc (ambigErr pred)
880 extended_tau_vars = grow theta tau_tyvars
882 -- Only a *class* predicate can give rise to ambiguity
883 -- An *implicit parameter* cannot. For example:
884 -- foo :: (?x :: [a]) => Int
886 -- is fine. The call site will suppply a particular 'x'
887 is_ambig pred = isClassPred pred &&
888 any ambig_var (varSetElems (tyVarsOfPred pred))
890 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
891 not (ct_var `elemVarSet` extended_tau_vars)
894 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
895 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
896 ptext SLIT("must be reachable from the type after the '=>'"))]
899 In addition, GHC insists that at least one type variable
900 in each constraint is in V. So we disallow a type like
901 forall a. Eq b => b -> b
902 even in a scope where b is in scope.
905 checkFreeness forall_tyvars theta
906 = mappM_ complain (filter is_free theta)
908 is_free pred = not (isIPPred pred)
909 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
910 bound_var ct_var = ct_var `elem` forall_tyvars
911 complain pred = addErrTc (freeErr pred)
914 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
915 ptext SLIT("are already in scope"),
916 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
921 checkThetaCtxt ctxt theta
922 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
923 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
925 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
926 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
927 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
929 arityErr kind name n m
930 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
931 n_arguments <> comma, text "but has been given", int m]
933 n_arguments | n == 0 = ptext SLIT("no arguments")
934 | n == 1 = ptext SLIT("1 argument")
935 | True = hsep [int n, ptext SLIT("arguments")]
939 %************************************************************************
941 \subsection{Checking for a decent instance head type}
943 %************************************************************************
945 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
946 it must normally look like: @instance Foo (Tycon a b c ...) ...@
948 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
949 flag is on, or (2)~the instance is imported (they must have been
950 compiled elsewhere). In these cases, we let them go through anyway.
952 We can also have instances for functions: @instance Foo (a -> b) ...@.
955 checkValidInstHead :: Type -> TcM (Class, [TcType])
957 checkValidInstHead ty -- Should be a source type
958 = case tcSplitPredTy_maybe ty of {
959 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
962 case getClassPredTys_maybe pred of {
963 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
966 getDOpts `thenM` \ dflags ->
967 mappM_ check_arg_type tys `thenM_`
968 check_inst_head dflags clas tys `thenM_`
972 check_inst_head dflags clas tys
973 -- If GlasgowExts then check at least one isn't a type variable
974 | dopt Opt_GlasgowExts dflags
975 = check_tyvars dflags clas tys
977 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
979 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
980 not (isSynTyCon tycon), -- ...but not a synonym
981 all tcIsTyVarTy arg_tys, -- Applied to type variables
982 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
983 -- This last condition checks that all the type variables are distinct
987 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
992 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
993 text "where T is not a synonym, and a,b,c are distinct type variables")
995 check_tyvars dflags clas tys
996 -- Check that at least one isn't a type variable
997 -- unless -fallow-undecideable-instances
998 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
999 | not (all tcIsTyVarTy tys) = returnM ()
1000 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1002 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1005 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1009 instTypeErr pp_ty msg
1010 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,