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
734 | null tvs && null theta
735 = check_tau_type rank ubx_tup ty
737 = do { check_valid_theta SigmaCtxt theta
738 ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow
739 ; checkFreeness tvs theta
740 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
742 (tvs, theta, tau) = tcSplitSigmaTy ty
744 ----------------------------------------
745 check_arg_type :: Type -> TcM ()
746 -- The sort of type that can instantiate a type variable,
747 -- or be the argument of a type constructor.
748 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
749 -- Other unboxed types are very occasionally allowed as type
750 -- arguments depending on the kind of the type constructor
752 -- For example, we want to reject things like:
754 -- instance Ord a => Ord (forall s. T s a)
756 -- g :: T s (forall b.b)
758 -- NB: unboxed tuples can have polymorphic or unboxed args.
759 -- This happens in the workers for functions returning
760 -- product types with polymorphic components.
761 -- But not in user code.
762 -- Anyway, they are dealt with by a special case in check_tau_type
765 = check_poly_type Arbitrary UT_NotOk ty `thenM_`
766 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
768 ----------------------------------------
769 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
770 -- Rank is allowed rank for function args
771 -- No foralls otherwise
773 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
774 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
775 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
777 -- Naked PredTys don't usually show up, but they can as a result of
778 -- {-# SPECIALISE instance Ord Char #-}
779 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
780 -- are handled, but the quick thing is just to permit PredTys here.
781 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
782 check_source_ty dflags TypeCtxt sty
784 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
785 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
786 = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_`
787 check_poly_type rank UT_Ok res_ty
789 check_tau_type rank ubx_tup (AppTy ty1 ty2)
790 = check_arg_type ty1 `thenM_` check_arg_type ty2
792 check_tau_type rank ubx_tup (NoteTy other_note ty)
793 = check_tau_type rank ubx_tup ty
795 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
797 = do { -- It's OK to have an *over-applied* type synonym
798 -- data Tree a b = ...
799 -- type Foo a = Tree [a]
800 -- f :: Foo a b -> ...
802 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
803 Nothing -> failWithTc arity_msg
805 ; gla_exts <- doptM Opt_GlasgowExts
807 -- If -fglasgow-exts then don't check the type arguments
808 -- This allows us to instantiate a synonym defn with a
809 -- for-all type, or with a partially-applied type synonym.
810 -- e.g. type T a b = a
813 -- Here, T is partially applied, so it's illegal in H98.
814 -- But if you expand S first, then T we get just
819 -- For H98, do check the type args
820 mappM_ check_arg_type tys
823 | isUnboxedTupleTyCon tc
824 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
825 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
826 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
827 -- Args are allowed to be unlifted, or
828 -- more unboxed tuples, so can't use check_arg_ty
831 = mappM_ check_arg_type tys
834 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
837 tc_arity = tyConArity tc
839 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
840 ubx_tup_msg = ubxArgTyErr ty
842 ----------------------------------------
843 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
844 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
845 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
846 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
851 %************************************************************************
853 \subsection{Checking a theta or source type}
855 %************************************************************************
858 -- Enumerate the contexts in which a "source type", <S>, can occur
862 -- or (N a) where N is a newtype
865 = ClassSCCtxt Name -- Superclasses of clas
866 -- class <S> => C a where ...
867 | SigmaCtxt -- Theta part of a normal for-all type
868 -- f :: <S> => a -> a
869 | DataTyCtxt Name -- Theta part of a data decl
870 -- data <S> => T a = MkT a
871 | TypeCtxt -- Source type in an ordinary type
873 | InstThetaCtxt -- Context of an instance decl
874 -- instance <S> => C [a] where ...
876 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
877 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
878 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
879 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
880 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
884 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
885 checkValidTheta ctxt theta
886 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
888 -------------------------
889 check_valid_theta ctxt []
891 check_valid_theta ctxt theta
892 = getDOpts `thenM` \ dflags ->
893 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
894 mappM_ (check_source_ty dflags ctxt) theta
896 (_,dups) = removeDups tcCmpPred theta
898 -------------------------
899 check_source_ty dflags ctxt pred@(ClassP cls tys)
900 = -- Class predicates are valid in all contexts
901 checkTc (arity == n_tys) arity_err `thenM_`
903 -- Check the form of the argument types
904 mappM_ check_arg_type tys `thenM_`
905 checkTc (check_class_pred_tys dflags ctxt tys)
906 (predTyVarErr pred $$ how_to_allow)
909 class_name = className cls
910 arity = classArity cls
912 arity_err = arityErr "Class" class_name arity n_tys
913 how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
915 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
916 -- Implicit parameters only allows in type
917 -- signatures; not in instance decls, superclasses etc
918 -- The reason for not allowing implicit params in instances is a bit subtle
919 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
920 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
921 -- discharge all the potential usas of the ?x in e. For example, a
922 -- constraint Foo [Int] might come out of e,and applying the
923 -- instance decl would show up two uses of ?x.
926 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
928 -------------------------
929 check_class_pred_tys dflags ctxt tys
931 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
932 InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
933 -- Further checks on head and theta in
934 -- checkInstTermination
935 other -> gla_exts || all tyvar_head tys
937 gla_exts = dopt Opt_GlasgowExts dflags
938 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
940 -------------------------
941 tyvar_head ty -- Haskell 98 allows predicates of form
942 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
943 | otherwise -- where a is a type variable
944 = case tcSplitAppTy_maybe ty of
945 Just (ty, _) -> tyvar_head ty
952 is ambiguous if P contains generic variables
953 (i.e. one of the Vs) that are not mentioned in tau
955 However, we need to take account of functional dependencies
956 when we speak of 'mentioned in tau'. Example:
957 class C a b | a -> b where ...
959 forall x y. (C x y) => x
960 is not ambiguous because x is mentioned and x determines y
962 NB; the ambiguity check is only used for *user* types, not for types
963 coming from inteface files. The latter can legitimately have
964 ambiguous types. Example
966 class S a where s :: a -> (Int,Int)
967 instance S Char where s _ = (1,1)
968 f:: S a => [a] -> Int -> (Int,Int)
969 f (_::[a]) x = (a*x,b)
970 where (a,b) = s (undefined::a)
972 Here the worker for f gets the type
973 fw :: forall a. S a => Int -> (# Int, Int #)
975 If the list of tv_names is empty, we have a monotype, and then we
976 don't need to check for ambiguity either, because the test can't fail
980 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
981 checkAmbiguity forall_tyvars theta tau_tyvars
982 = mappM_ complain (filter is_ambig theta)
984 complain pred = addErrTc (ambigErr pred)
985 extended_tau_vars = grow theta tau_tyvars
987 -- Only a *class* predicate can give rise to ambiguity
988 -- An *implicit parameter* cannot. For example:
989 -- foo :: (?x :: [a]) => Int
991 -- is fine. The call site will suppply a particular 'x'
992 is_ambig pred = isClassPred pred &&
993 any ambig_var (varSetElems (tyVarsOfPred pred))
995 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
996 not (ct_var `elemVarSet` extended_tau_vars)
999 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1000 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1001 ptext SLIT("must be reachable from the type after the '=>'"))]
1004 In addition, GHC insists that at least one type variable
1005 in each constraint is in V. So we disallow a type like
1006 forall a. Eq b => b -> b
1007 even in a scope where b is in scope.
1010 checkFreeness forall_tyvars theta
1011 = mappM_ complain (filter is_free theta)
1013 is_free pred = not (isIPPred pred)
1014 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1015 bound_var ct_var = ct_var `elem` forall_tyvars
1016 complain pred = addErrTc (freeErr pred)
1019 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1020 ptext SLIT("are already in scope"),
1021 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1026 checkThetaCtxt ctxt theta
1027 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1028 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1030 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1031 predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
1032 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1033 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1035 arityErr kind name n m
1036 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1037 n_arguments <> comma, text "but has been given", int m]
1039 n_arguments | n == 0 = ptext SLIT("no arguments")
1040 | n == 1 = ptext SLIT("1 argument")
1041 | True = hsep [int n, ptext SLIT("arguments")]
1045 %************************************************************************
1047 \subsection{Checking for a decent instance head type}
1049 %************************************************************************
1051 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1052 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1054 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1055 flag is on, or (2)~the instance is imported (they must have been
1056 compiled elsewhere). In these cases, we let them go through anyway.
1058 We can also have instances for functions: @instance Foo (a -> b) ...@.
1061 checkValidInstHead :: Type -> TcM (Class, [TcType])
1063 checkValidInstHead ty -- Should be a source type
1064 = case tcSplitPredTy_maybe ty of {
1065 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1068 case getClassPredTys_maybe pred of {
1069 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1072 getDOpts `thenM` \ dflags ->
1073 mappM_ check_arg_type tys `thenM_`
1074 check_inst_head dflags clas tys `thenM_`
1078 check_inst_head dflags clas tys
1079 -- If GlasgowExts then check at least one isn't a type variable
1080 | dopt Opt_GlasgowExts dflags
1081 = mapM_ check_one tys
1083 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1085 = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
1086 (instTypeErr (pprClassPred clas tys) head_shape_msg)
1089 (first_ty : _) = tys
1091 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1092 text "where T is not a synonym, and a,b,c are distinct type variables")
1094 -- For now, I only allow tau-types (not polytypes) in
1095 -- the head of an instance decl.
1096 -- E.g. instance C (forall a. a->a) is rejected
1097 -- One could imagine generalising that, but I'm not sure
1098 -- what all the consequences might be
1099 check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1100 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1102 instTypeErr pp_ty msg
1103 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1108 %************************************************************************
1110 \subsection{Checking instance for termination}
1112 %************************************************************************
1116 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1117 checkValidInstance tyvars theta clas inst_tys
1118 = do { gla_exts <- doptM Opt_GlasgowExts
1119 ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
1121 ; checkValidTheta InstThetaCtxt theta
1122 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1124 -- Check that instance inference will terminate (if we care)
1125 -- For Haskell 98, checkValidTheta has already done that
1126 ; when (gla_exts && not undecidable_ok) $
1127 checkInstTermination theta inst_tys
1129 -- The Coverage Condition
1130 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1131 (instTypeErr (pprClassPred clas inst_tys) msg)
1134 msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
1137 Termination test: each assertion in the context satisfies
1138 (1) no variable has more occurrences in the assertion than in the head, and
1139 (2) the assertion has fewer constructors and variables (taken together
1140 and counting repetitions) than the head.
1141 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1142 (which have already been checked) guarantee termination.
1144 The underlying idea is that
1146 for any ground substitution, each assertion in the
1147 context has fewer type constructors than the head.
1151 checkInstTermination :: ThetaType -> [TcType] -> TcM ()
1152 checkInstTermination theta tys
1153 = do { mappM_ (check_nomore (fvTypes tys)) theta
1154 ; mappM_ (check_smaller (sizeTypes tys)) theta }
1156 check_nomore :: [TyVar] -> PredType -> TcM ()
1157 check_nomore fvs pred
1158 = checkTc (null (fvPred pred \\ fvs))
1159 (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1161 check_smaller :: Int -> PredType -> TcM ()
1162 check_smaller n pred
1163 = checkTc (sizePred pred < n)
1164 (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1166 predUndecErr pred msg = sep [msg,
1167 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1169 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1170 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1171 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1173 -- Free variables of a type, retaining repetitions, and expanding synonyms
1174 fvType :: Type -> [TyVar]
1175 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1176 fvType (TyVarTy tv) = [tv]
1177 fvType (TyConApp _ tys) = fvTypes tys
1178 fvType (NoteTy _ ty) = fvType ty
1179 fvType (PredTy pred) = fvPred pred
1180 fvType (FunTy arg res) = fvType arg ++ fvType res
1181 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1182 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1184 fvTypes :: [Type] -> [TyVar]
1185 fvTypes tys = concat (map fvType tys)
1187 fvPred :: PredType -> [TyVar]
1188 fvPred (ClassP _ tys') = fvTypes tys'
1189 fvPred (IParam _ ty) = fvType ty
1191 -- Size of a type: the number of variables and constructors
1192 sizeType :: Type -> Int
1193 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1194 sizeType (TyVarTy _) = 1
1195 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1196 sizeType (NoteTy _ ty) = sizeType ty
1197 sizeType (PredTy pred) = sizePred pred
1198 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1199 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1200 sizeType (ForAllTy _ ty) = sizeType ty
1202 sizeTypes :: [Type] -> Int
1203 sizeTypes xs = sum (map sizeType xs)
1205 sizePred :: PredType -> Int
1206 sizePred (ClassP _ tys') = sizeTypes tys'
1207 sizePred (IParam _ ty) = sizeType ty