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
15 newFlexiTyVarTy, -- Kind -> TcM TcType
16 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
17 newKindVar, newKindVars,
18 lookupTcTyVar, LookupTyVarResult(..),
19 newMetaTyVar, readMetaTyVar, writeMetaTyVar,
21 --------------------------------
22 -- Boxy type variables
23 newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
25 --------------------------------
27 tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar,
28 tcInstSigTyVars, zonkSigTyVar,
29 tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
30 tcSkolSigType, tcSkolSigTyVars,
32 --------------------------------
33 -- Checking type validity
34 Rank, UserTypeCtxt(..), checkValidType,
35 SourceTyCtxt(..), checkValidTheta, checkFreeness,
36 checkValidInstHead, checkValidInstance, checkAmbiguity,
40 --------------------------------
42 zonkType, zonkTcPredType,
43 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
44 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
45 zonkTcKindToKind, zonkTcKind,
47 readKindVar, writeKindVar
51 #include "HsVersions.h"
55 import TypeRep ( Type(..), PredType(..), -- Friend; can see representation
58 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
59 TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
60 MetaDetails(..), SkolemInfo(..), BoxInfo(..),
61 BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType,
63 isMetaTyVar, isSigTyVar, metaTvRef,
64 tcCmpPred, isClassPred, tcGetTyVar,
65 tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
66 tcValidInstHeadTy, tcSplitForAllTys,
67 tcIsTyVarTy, tcSplitSigmaTy,
68 isUnLiftedType, isIPPred,
69 typeKind, isSkolemTyVar,
70 mkAppTy, mkTyVarTy, mkTyVarTys,
71 tyVarsOfPred, getClassPredTys_maybe,
72 tyVarsOfType, tyVarsOfTypes, tcView,
73 pprPred, pprTheta, pprClassPred )
74 import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar,
75 isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
76 liftedTypeKind, defaultKind
78 import Type ( TvSubst, zipTopTvSubst, substTy )
79 import Class ( Class, classArity, className )
80 import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
81 tyConArity, tyConName )
82 import Var ( TyVar, tyVarKind, tyVarName, isTcTyVar,
83 mkTyVar, mkTcTyVar, tcTyVarDetails )
87 import TcType ( isFlexi, isBoxyTyVar, isImmutableTyVar )
88 import Kind ( isSubKind )
92 import TcRnMonad -- TcType, amongst others
93 import FunDeps ( grow, checkInstCoverage )
94 import Name ( Name, setNameUnique, mkSysTvName )
96 import DynFlags ( dopt, DynFlag(..) )
97 import Util ( nOfThem, isSingleton, notNull )
98 import ListSetOps ( removeDups )
101 import Control.Monad ( when )
102 import Data.List ( (\\) )
106 %************************************************************************
108 Instantiation in general
110 %************************************************************************
113 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
114 -> TcType -- Type to instantiate
115 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
116 tcInstType inst_tyvars ty
117 = case tcSplitForAllTys ty of
118 ([], rho) -> let -- There may be overloading despite no type variables;
119 -- (?x :: Int) => Int -> Int
120 (theta, tau) = tcSplitPhiTy rho
122 return ([], theta, tau)
124 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
126 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
127 -- Either the tyvars are freshly made, by inst_tyvars,
128 -- or (in the call from tcSkolSigType) any nested foralls
129 -- have different binders. Either way, zipTopTvSubst is ok
131 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
132 ; return (tyvars', theta, tau) }
136 %************************************************************************
140 %************************************************************************
143 newKindVar :: TcM TcKind
144 newKindVar = do { uniq <- newUnique
145 ; ref <- newMutVar Nothing
146 ; return (KindVar (mkKindVar uniq ref)) }
148 newKindVars :: Int -> TcM [TcKind]
149 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
153 %************************************************************************
155 SkolemTvs (immutable)
157 %************************************************************************
160 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
161 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
163 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
164 -- Instantiate a type signature with skolem constants, but
165 -- do *not* give them fresh names, because we want the name to
166 -- be in the type environment -- it is lexically scoped.
167 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
169 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
170 -- Make skolem constants, but do *not* give them new names, as above
171 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
174 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
175 -- Instantiate a type with fresh skolem constants
176 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
178 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
179 tcInstSkolTyVar info tyvar
180 = do { uniq <- newUnique
181 ; let name = setNameUnique (tyVarName tyvar) uniq
182 kind = tyVarKind tyvar
183 ; return (mkSkolTyVar name kind info) }
185 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
186 tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
190 %************************************************************************
192 MetaTvs (meta type variables; mutable)
194 %************************************************************************
197 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
198 -- Make a new meta tyvar out of thin air
199 newMetaTyVar box_info kind
200 = do { uniq <- newUnique
201 ; ref <- newMutVar Flexi ;
202 ; let name = mkSysTvName uniq fs
203 fs = case box_info of
206 SigTv _ -> FSLIT("a")
207 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
209 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
210 -- Make a new meta tyvar whose Name and Kind
211 -- come from an existing TyVar
212 instMetaTyVar box_info tyvar
213 = do { uniq <- newUnique
214 ; ref <- newMutVar Flexi ;
215 ; let name = setNameUnique (tyVarName tyvar) uniq
216 kind = tyVarKind tyvar
217 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
219 readMetaTyVar :: TyVar -> TcM MetaDetails
220 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
221 readMutVar (metaTvRef tyvar)
223 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
225 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
227 writeMetaTyVar tyvar ty
228 | not (isMetaTyVar tyvar)
229 = pprTrace "writeMetaTyVar" (ppr tyvar) $
233 = ASSERT( isMetaTyVar tyvar )
234 ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
235 do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
236 ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
244 %************************************************************************
248 %************************************************************************
251 newFlexiTyVar :: Kind -> TcM TcTyVar
252 newFlexiTyVar kind = newMetaTyVar TauTv kind
254 newFlexiTyVarTy :: Kind -> TcM TcType
256 = newFlexiTyVar kind `thenM` \ tc_tyvar ->
257 returnM (TyVarTy tc_tyvar)
259 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
260 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
262 tcInstTyVar :: TyVar -> TcM TcTyVar
263 -- Instantiate with a META type variable
264 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
266 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
267 -- Instantiate with META type variables
269 = do { tc_tvs <- mapM tcInstTyVar tyvars
270 ; let tys = mkTyVarTys tc_tvs
271 ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
272 -- Since the tyvars are freshly made,
273 -- they cannot possibly be captured by
274 -- any existing for-alls. Hence zipTopTvSubst
278 %************************************************************************
282 %************************************************************************
285 tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
286 -- Instantiate with meta SigTvs
287 tcInstSigTyVars skol_info tyvars
288 = mapM (instMetaTyVar (SigTv skol_info)) tyvars
290 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
292 | isSkolemTyVar sig_tv
293 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
295 = ASSERT( isSigTyVar sig_tv )
296 do { ty <- zonkTcTyVar sig_tv
297 ; return (tcGetTyVar "zonkSigTyVar" ty) }
298 -- 'ty' is bound to be a type variable, because SigTvs
299 -- can only be unified with type variables
303 %************************************************************************
307 %************************************************************************
310 newBoxyTyVar :: Kind -> TcM BoxyTyVar
311 newBoxyTyVar kind = newMetaTyVar BoxTv kind
313 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
314 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
316 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
317 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
319 readFilledBox :: BoxyTyVar -> TcM TcType
320 -- Read the contents of the box, which should be filled in by now
321 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
322 do { cts <- readMetaTyVar box_tv
324 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
325 Indirect ty -> return ty }
327 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
328 -- Instantiate with a BOXY type variable
329 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
331 tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType)
332 -- tcInstType instantiates the outer-level for-alls of a TcType with
333 -- fresh BOXY type variables, splits off the dictionary part,
334 -- and returns the pieces.
335 tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty
339 %************************************************************************
341 \subsection{Putting and getting mutable type variables}
343 %************************************************************************
345 But it's more fun to short out indirections on the way: If this
346 version returns a TyVar, then that TyVar is unbound. If it returns
347 any other type, then there might be bound TyVars embedded inside it.
349 We return Nothing iff the original box was unbound.
352 data LookupTyVarResult -- The result of a lookupTcTyVar call
353 = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
356 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
359 SkolemTv _ -> return (DoneTv details)
360 MetaTv _ ref -> do { meta_details <- readMutVar ref
361 ; case meta_details of
362 Indirect ty -> return (IndirectTv ty)
363 Flexi -> return (DoneTv details) }
365 details = tcTyVarDetails tyvar
368 -- gaw 2004 We aren't shorting anything out anymore, at least for now
370 | not (isTcTyVar tyvar)
371 = pprTrace "getTcTyVar" (ppr tyvar) $
372 returnM (Just (mkTyVarTy tyvar))
375 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
376 readMetaTyVar tyvar `thenM` \ maybe_ty ->
378 Just ty -> short_out ty `thenM` \ ty' ->
379 writeMetaTyVar tyvar (Just ty') `thenM_`
382 Nothing -> returnM Nothing
384 short_out :: TcType -> TcM TcType
385 short_out ty@(TyVarTy tyvar)
386 | not (isTcTyVar tyvar)
390 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
392 Just ty' -> short_out ty' `thenM` \ ty' ->
393 writeMetaTyVar tyvar (Just ty') `thenM_`
398 short_out other_ty = returnM other_ty
403 %************************************************************************
405 \subsection{Zonking -- the exernal interfaces}
407 %************************************************************************
409 ----------------- Type variables
412 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
413 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
415 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
416 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
417 returnM (tyVarsOfTypes tys)
419 zonkTcTyVar :: TcTyVar -> TcM TcType
420 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
421 zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
424 ----------------- Types
427 zonkTcType :: TcType -> TcM TcType
428 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
430 zonkTcTypes :: [TcType] -> TcM [TcType]
431 zonkTcTypes tys = mappM zonkTcType tys
433 zonkTcClassConstraints cts = mappM zonk cts
434 where zonk (clas, tys)
435 = zonkTcTypes tys `thenM` \ new_tys ->
436 returnM (clas, new_tys)
438 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
439 zonkTcThetaType theta = mappM zonkTcPredType theta
441 zonkTcPredType :: TcPredType -> TcM TcPredType
442 zonkTcPredType (ClassP c ts)
443 = zonkTcTypes ts `thenM` \ new_ts ->
444 returnM (ClassP c new_ts)
445 zonkTcPredType (IParam n t)
446 = zonkTcType t `thenM` \ new_t ->
447 returnM (IParam n new_t)
450 ------------------- These ...ToType, ...ToKind versions
451 are used at the end of type checking
454 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
455 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
456 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
457 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
458 -- The meta tyvar is updated to point to the new regular TyVar. Now any
459 -- bound occurences of the original type variable will get zonked to
460 -- the immutable version.
462 -- We leave skolem TyVars alone; they are immutable.
463 zonkQuantifiedTyVar tv
464 | isSkolemTyVar tv = return tv
465 -- It might be a skolem type variable,
466 -- for example from a user type signature
468 | otherwise -- It's a meta-type-variable
469 = do { details <- readMetaTyVar tv
471 -- Create the new, frozen, regular type variable
472 ; let final_kind = defaultKind (tyVarKind tv)
473 final_tv = mkTyVar (tyVarName tv) final_kind
475 -- Bind the meta tyvar to the new tyvar
477 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
479 -- [Sept 04] I don't think this should happen
480 -- See note [Silly Type Synonym]
482 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
484 -- Return the new tyvar
488 [Silly Type Synonyms]
491 type C u a = u -- Note 'a' unused
493 foo :: (forall a. C u a -> C u a) -> u
497 bar = foo (\t -> t + t)
499 * From the (\t -> t+t) we get type {Num d} => d -> d
502 * Now unify with type of foo's arg, and we get:
503 {Num (C d a)} => C d a -> C d a
506 * Now abstract over the 'a', but float out the Num (C d a) constraint
507 because it does not 'really' mention a. (see exactTyVarsOfType)
508 The arg to foo becomes
511 * So we get a dict binding for Num (C d a), which is zonked to give
513 [Note Sept 04: now that we are zonking quantified type variables
514 on construction, the 'a' will be frozen as a regular tyvar on
515 quantification, so the floated dict will still have type (C d a).
516 Which renders this whole note moot; happily!]
518 * Then the /\a abstraction has a zonked 'a' in it.
520 All very silly. I think its harmless to ignore the problem. We'll end up with
521 a /\a in the final result but all the occurrences of a will be zonked to ()
524 %************************************************************************
526 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
528 %* For internal use only! *
530 %************************************************************************
533 -- For unbound, mutable tyvars, zonkType uses the function given to it
534 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
535 -- type variable and zonks the kind too
537 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
538 -- see zonkTcType, and zonkTcTypeToType
541 zonkType unbound_var_fn ty
544 go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
546 go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
547 returnM (TyConApp tc tys')
549 go (PredTy p) = go_pred p `thenM` \ p' ->
552 go (FunTy arg res) = go arg `thenM` \ arg' ->
553 go res `thenM` \ res' ->
554 returnM (FunTy arg' res')
556 go (AppTy fun arg) = go fun `thenM` \ fun' ->
557 go arg `thenM` \ arg' ->
558 returnM (mkAppTy fun' arg')
559 -- NB the mkAppTy; we might have instantiated a
560 -- type variable to a type constructor, so we need
561 -- to pull the TyConApp to the top.
563 -- The two interesting cases!
564 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
565 | otherwise = return (TyVarTy tyvar)
566 -- Ordinary (non Tc) tyvars occur inside quantified types
568 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
569 go ty `thenM` \ ty' ->
570 returnM (ForAllTy tyvar ty')
572 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
573 returnM (ClassP c tys')
574 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
575 returnM (IParam n ty')
577 zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
578 -> TcTyVar -> TcM TcType
579 zonk_tc_tyvar unbound_var_fn tyvar
580 | not (isMetaTyVar tyvar) -- Skolems
581 = returnM (TyVarTy tyvar)
583 | otherwise -- Mutables
584 = do { cts <- readMetaTyVar tyvar
586 Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
587 Indirect ty -> zonkType unbound_var_fn ty }
592 %************************************************************************
596 %************************************************************************
599 readKindVar :: KindVar -> TcM (Maybe TcKind)
600 writeKindVar :: KindVar -> TcKind -> TcM ()
601 readKindVar kv = readMutVar (kindVarRef kv)
602 writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
605 zonkTcKind :: TcKind -> TcM TcKind
606 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
607 ; k2' <- zonkTcKind k2
608 ; returnM (FunKind k1' k2') }
609 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
612 Just k -> zonkTcKind k }
613 zonkTcKind other_kind = returnM other_kind
616 zonkTcKindToKind :: TcKind -> TcM Kind
617 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
618 ; k2' <- zonkTcKindToKind k2
619 ; returnM (FunKind k1' k2') }
621 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
623 Nothing -> return liftedTypeKind
624 Just k -> zonkTcKindToKind k }
626 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
627 zonkTcKindToKind other_kind = returnM other_kind
630 %************************************************************************
632 \subsection{Checking a user type}
634 %************************************************************************
636 When dealing with a user-written type, we first translate it from an HsType
637 to a Type, performing kind checking, and then check various things that should
638 be true about it. We don't want to perform these checks at the same time
639 as the initial translation because (a) they are unnecessary for interface-file
640 types and (b) when checking a mutually recursive group of type and class decls,
641 we can't "look" at the tycons/classes yet. Also, the checks are are rather
642 diverse, and used to really mess up the other code.
644 One thing we check for is 'rank'.
646 Rank 0: monotypes (no foralls)
647 Rank 1: foralls at the front only, Rank 0 inside
648 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
650 basic ::= tyvar | T basic ... basic
652 r2 ::= forall tvs. cxt => r2a
653 r2a ::= r1 -> r2a | basic
654 r1 ::= forall tvs. cxt => r0
655 r0 ::= r0 -> r0 | basic
657 Another thing is to check that type synonyms are saturated.
658 This might not necessarily show up in kind checking.
660 data T k = MkT (k Int)
665 checkValidType :: UserTypeCtxt -> Type -> TcM ()
666 -- Checks that the type is valid for the given context
667 checkValidType ctxt ty
668 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
669 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
671 rank | gla_exts = Arbitrary
673 = case ctxt of -- Haskell 98
675 LamPatSigCtxt -> Rank 0
676 BindPatSigCtxt -> Rank 0
677 DefaultDeclCtxt-> Rank 0
679 TySynCtxt _ -> Rank 0
680 ExprSigCtxt -> Rank 1
681 FunSigCtxt _ -> Rank 1
682 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
683 -- constructor, hence rank 1
684 ForSigCtxt _ -> Rank 1
685 RuleSigCtxt _ -> Rank 1
686 SpecInstCtxt -> Rank 1
688 actual_kind = typeKind ty
690 kind_ok = case ctxt of
691 TySynCtxt _ -> True -- Any kind will do
692 ResSigCtxt -> isOpenTypeKind actual_kind
693 ExprSigCtxt -> isOpenTypeKind actual_kind
694 GenPatCtxt -> isLiftedTypeKind actual_kind
695 ForSigCtxt _ -> isLiftedTypeKind actual_kind
696 other -> isArgTypeKind actual_kind
698 ubx_tup | not gla_exts = UT_NotOk
699 | otherwise = case ctxt of
703 -- Unboxed tuples ok in function results,
704 -- but for type synonyms we allow them even at
707 -- Check that the thing has kind Type, and is lifted if necessary
708 checkTc kind_ok (kindErr actual_kind) `thenM_`
710 -- Check the internal validity of the type itself
711 check_poly_type rank ubx_tup ty `thenM_`
713 traceTc (text "checkValidType done" <+> ppr ty)
718 data Rank = Rank Int | Arbitrary
720 decRank :: Rank -> Rank
721 decRank Arbitrary = Arbitrary
722 decRank (Rank n) = Rank (n-1)
724 ----------------------------------------
725 data UbxTupFlag = UT_Ok | UT_NotOk
726 -- The "Ok" version means "ok if -fglasgow-exts is on"
728 ----------------------------------------
729 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
730 check_poly_type (Rank 0) ubx_tup ty
731 = check_tau_type (Rank 0) ubx_tup ty
733 check_poly_type rank ubx_tup ty
735 (tvs, theta, tau) = tcSplitSigmaTy ty
737 check_valid_theta SigmaCtxt theta `thenM_`
738 check_tau_type (decRank rank) ubx_tup tau `thenM_`
739 checkFreeness tvs theta `thenM_`
740 checkAmbiguity tvs theta (tyVarsOfType tau)
742 ----------------------------------------
743 check_arg_type :: Type -> TcM ()
744 -- The sort of type that can instantiate a type variable,
745 -- or be the argument of a type constructor.
746 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
747 -- Other unboxed types are very occasionally allowed as type
748 -- arguments depending on the kind of the type constructor
750 -- For example, we want to reject things like:
752 -- instance Ord a => Ord (forall s. T s a)
754 -- g :: T s (forall b.b)
756 -- NB: unboxed tuples can have polymorphic or unboxed args.
757 -- This happens in the workers for functions returning
758 -- product types with polymorphic components.
759 -- But not in user code.
760 -- Anyway, they are dealt with by a special case in check_tau_type
763 = check_poly_type Arbitrary UT_NotOk ty `thenM_`
764 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
766 ----------------------------------------
767 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
768 -- Rank is allowed rank for function args
769 -- No foralls otherwise
771 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
772 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
773 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
775 -- Naked PredTys don't usually show up, but they can as a result of
776 -- {-# SPECIALISE instance Ord Char #-}
777 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
778 -- are handled, but the quick thing is just to permit PredTys here.
779 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
780 check_source_ty dflags TypeCtxt sty
782 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
783 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
784 = check_poly_type rank UT_NotOk arg_ty `thenM_`
785 check_poly_type rank UT_Ok res_ty
787 check_tau_type rank ubx_tup (AppTy ty1 ty2)
788 = check_arg_type ty1 `thenM_` check_arg_type ty2
790 check_tau_type rank ubx_tup (NoteTy other_note ty)
791 = check_tau_type rank ubx_tup ty
793 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
795 = do { -- It's OK to have an *over-applied* type synonym
796 -- data Tree a b = ...
797 -- type Foo a = Tree [a]
798 -- f :: Foo a b -> ...
800 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
801 Nothing -> failWithTc arity_msg
803 ; gla_exts <- doptM Opt_GlasgowExts
805 -- If -fglasgow-exts then don't check the type arguments
806 -- This allows us to instantiate a synonym defn with a
807 -- for-all type, or with a partially-applied type synonym.
808 -- e.g. type T a b = a
811 -- Here, T is partially applied, so it's illegal in H98.
812 -- But if you expand S first, then T we get just
817 -- For H98, do check the type args
818 mappM_ check_arg_type tys
821 | isUnboxedTupleTyCon tc
822 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
823 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
824 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
825 -- Args are allowed to be unlifted, or
826 -- more unboxed tuples, so can't use check_arg_ty
829 = mappM_ check_arg_type tys
832 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
835 tc_arity = tyConArity tc
837 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
838 ubx_tup_msg = ubxArgTyErr ty
840 ----------------------------------------
841 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
842 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
843 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
844 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
849 %************************************************************************
851 \subsection{Checking a theta or source type}
853 %************************************************************************
856 -- Enumerate the contexts in which a "source type", <S>, can occur
860 -- or (N a) where N is a newtype
863 = ClassSCCtxt Name -- Superclasses of clas
864 -- class <S> => C a where ...
865 | SigmaCtxt -- Theta part of a normal for-all type
866 -- f :: <S> => a -> a
867 | DataTyCtxt Name -- Theta part of a data decl
868 -- data <S> => T a = MkT a
869 | TypeCtxt -- Source type in an ordinary type
871 | InstThetaCtxt -- Context of an instance decl
872 -- instance <S> => C [a] where ...
874 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
875 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
876 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
877 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
878 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
882 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
883 checkValidTheta ctxt theta
884 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
886 -------------------------
887 check_valid_theta ctxt []
889 check_valid_theta ctxt theta
890 = getDOpts `thenM` \ dflags ->
891 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
892 mappM_ (check_source_ty dflags ctxt) theta
894 (_,dups) = removeDups tcCmpPred theta
896 -------------------------
897 check_source_ty dflags ctxt pred@(ClassP cls tys)
898 = -- Class predicates are valid in all contexts
899 checkTc (arity == n_tys) arity_err `thenM_`
901 -- Check the form of the argument types
902 mappM_ check_arg_type tys `thenM_`
903 checkTc (check_class_pred_tys dflags ctxt tys)
904 (predTyVarErr pred $$ how_to_allow)
907 class_name = className cls
908 arity = classArity cls
910 arity_err = arityErr "Class" class_name arity n_tys
911 how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
913 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
914 -- Implicit parameters only allows in type
915 -- signatures; not in instance decls, superclasses etc
916 -- The reason for not allowing implicit params in instances is a bit subtle
917 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
918 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
919 -- discharge all the potential usas of the ?x in e. For example, a
920 -- constraint Foo [Int] might come out of e,and applying the
921 -- instance decl would show up two uses of ?x.
924 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
926 -------------------------
927 check_class_pred_tys dflags ctxt tys
929 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
930 InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
931 -- Further checks on head and theta in
932 -- checkInstTermination
933 other -> gla_exts || all tyvar_head tys
935 gla_exts = dopt Opt_GlasgowExts dflags
936 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
938 -------------------------
939 tyvar_head ty -- Haskell 98 allows predicates of form
940 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
941 | otherwise -- where a is a type variable
942 = case tcSplitAppTy_maybe ty of
943 Just (ty, _) -> tyvar_head ty
950 is ambiguous if P contains generic variables
951 (i.e. one of the Vs) that are not mentioned in tau
953 However, we need to take account of functional dependencies
954 when we speak of 'mentioned in tau'. Example:
955 class C a b | a -> b where ...
957 forall x y. (C x y) => x
958 is not ambiguous because x is mentioned and x determines y
960 NB; the ambiguity check is only used for *user* types, not for types
961 coming from inteface files. The latter can legitimately have
962 ambiguous types. Example
964 class S a where s :: a -> (Int,Int)
965 instance S Char where s _ = (1,1)
966 f:: S a => [a] -> Int -> (Int,Int)
967 f (_::[a]) x = (a*x,b)
968 where (a,b) = s (undefined::a)
970 Here the worker for f gets the type
971 fw :: forall a. S a => Int -> (# Int, Int #)
973 If the list of tv_names is empty, we have a monotype, and then we
974 don't need to check for ambiguity either, because the test can't fail
978 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
979 checkAmbiguity forall_tyvars theta tau_tyvars
980 = mappM_ complain (filter is_ambig theta)
982 complain pred = addErrTc (ambigErr pred)
983 extended_tau_vars = grow theta tau_tyvars
985 -- Only a *class* predicate can give rise to ambiguity
986 -- An *implicit parameter* cannot. For example:
987 -- foo :: (?x :: [a]) => Int
989 -- is fine. The call site will suppply a particular 'x'
990 is_ambig pred = isClassPred pred &&
991 any ambig_var (varSetElems (tyVarsOfPred pred))
993 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
994 not (ct_var `elemVarSet` extended_tau_vars)
997 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
998 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
999 ptext SLIT("must be reachable from the type after the '=>'"))]
1002 In addition, GHC insists that at least one type variable
1003 in each constraint is in V. So we disallow a type like
1004 forall a. Eq b => b -> b
1005 even in a scope where b is in scope.
1008 checkFreeness forall_tyvars theta
1009 = mappM_ complain (filter is_free theta)
1011 is_free pred = not (isIPPred pred)
1012 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1013 bound_var ct_var = ct_var `elem` forall_tyvars
1014 complain pred = addErrTc (freeErr pred)
1017 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1018 ptext SLIT("are already in scope"),
1019 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1024 checkThetaCtxt ctxt theta
1025 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1026 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1028 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1029 predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
1030 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1031 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1033 arityErr kind name n m
1034 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1035 n_arguments <> comma, text "but has been given", int m]
1037 n_arguments | n == 0 = ptext SLIT("no arguments")
1038 | n == 1 = ptext SLIT("1 argument")
1039 | True = hsep [int n, ptext SLIT("arguments")]
1043 %************************************************************************
1045 \subsection{Checking for a decent instance head type}
1047 %************************************************************************
1049 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1050 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1052 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1053 flag is on, or (2)~the instance is imported (they must have been
1054 compiled elsewhere). In these cases, we let them go through anyway.
1056 We can also have instances for functions: @instance Foo (a -> b) ...@.
1059 checkValidInstHead :: Type -> TcM (Class, [TcType])
1061 checkValidInstHead ty -- Should be a source type
1062 = case tcSplitPredTy_maybe ty of {
1063 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1066 case getClassPredTys_maybe pred of {
1067 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1070 getDOpts `thenM` \ dflags ->
1071 mappM_ check_arg_type tys `thenM_`
1072 check_inst_head dflags clas tys `thenM_`
1076 check_inst_head dflags clas tys
1077 -- If GlasgowExts then check at least one isn't a type variable
1078 | dopt Opt_GlasgowExts dflags
1079 = mapM_ check_one tys
1081 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1083 = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
1084 (instTypeErr (pprClassPred clas tys) head_shape_msg)
1087 (first_ty : _) = tys
1089 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1090 text "where T is not a synonym, and a,b,c are distinct type variables")
1092 -- For now, I only allow tau-types (not polytypes) in
1093 -- the head of an instance decl.
1094 -- E.g. instance C (forall a. a->a) is rejected
1095 -- One could imagine generalising that, but I'm not sure
1096 -- what all the consequences might be
1097 check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1098 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1100 instTypeErr pp_ty msg
1101 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1106 %************************************************************************
1108 \subsection{Checking instance for termination}
1110 %************************************************************************
1114 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1115 checkValidInstance tyvars theta clas inst_tys
1116 = do { gla_exts <- doptM Opt_GlasgowExts
1117 ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
1119 ; checkValidTheta InstThetaCtxt theta
1120 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1122 -- Check that instance inference will terminate (if we care)
1123 -- For Haskell 98, checkValidTheta has already done that
1124 ; when (gla_exts && not undecidable_ok) $
1125 checkInstTermination theta inst_tys
1127 -- The Coverage Condition
1128 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1129 (instTypeErr (pprClassPred clas inst_tys) msg)
1132 msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
1135 Termination test: each assertion in the context satisfies
1136 (1) no variable has more occurrences in the assertion than in the head, and
1137 (2) the assertion has fewer constructors and variables (taken together
1138 and counting repetitions) than the head.
1139 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1140 (which have already been checked) guarantee termination.
1142 The underlying idea is that
1144 for any ground substitution, each assertion in the
1145 context has fewer type constructors than the head.
1149 checkInstTermination :: ThetaType -> [TcType] -> TcM ()
1150 checkInstTermination theta tys
1151 = do { mappM_ (check_nomore (fvTypes tys)) theta
1152 ; mappM_ (check_smaller (sizeTypes tys)) theta }
1154 check_nomore :: [TyVar] -> PredType -> TcM ()
1155 check_nomore fvs pred
1156 = checkTc (null (fvPred pred \\ fvs))
1157 (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1159 check_smaller :: Int -> PredType -> TcM ()
1160 check_smaller n pred
1161 = checkTc (sizePred pred < n)
1162 (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1164 predUndecErr pred msg = sep [msg,
1165 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1167 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1168 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1169 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1171 -- Free variables of a type, retaining repetitions, and expanding synonyms
1172 fvType :: Type -> [TyVar]
1173 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1174 fvType (TyVarTy tv) = [tv]
1175 fvType (TyConApp _ tys) = fvTypes tys
1176 fvType (NoteTy _ ty) = fvType ty
1177 fvType (PredTy pred) = fvPred pred
1178 fvType (FunTy arg res) = fvType arg ++ fvType res
1179 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1180 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1182 fvTypes :: [Type] -> [TyVar]
1183 fvTypes tys = concat (map fvType tys)
1185 fvPred :: PredType -> [TyVar]
1186 fvPred (ClassP _ tys') = fvTypes tys'
1187 fvPred (IParam _ ty) = fvType ty
1189 -- Size of a type: the number of variables and constructors
1190 sizeType :: Type -> Int
1191 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1192 sizeType (TyVarTy _) = 1
1193 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1194 sizeType (NoteTy _ ty) = sizeType ty
1195 sizeType (PredTy pred) = sizePred pred
1196 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1197 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1198 sizeType (ForAllTy _ ty) = sizeType ty
1200 sizeTypes :: [Type] -> Int
1201 sizeTypes xs = sum (map sizeType xs)
1203 sizePred :: PredType -> Int
1204 sizePred (ClassP _ tys') = sizeTypes tys'
1205 sizePred (IParam _ ty) = sizeType ty