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, instTypeErr, checkAmbiguity,
39 --------------------------------
41 zonkType, zonkTcPredType,
42 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
43 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
44 zonkTcKindToKind, zonkTcKind,
46 readKindVar, writeKindVar
50 #include "HsVersions.h"
54 import TypeRep ( Type(..), PredType(..), -- Friend; can see representation
57 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
58 TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
59 MetaDetails(..), SkolemInfo(..), BoxInfo(..),
60 BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType,
62 isMetaTyVar, isSigTyVar, metaTvRef,
63 tcCmpPred, isClassPred, tcEqType, tcGetTyVar,
64 tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
65 tcValidInstHeadTy, tcSplitForAllTys,
66 tcIsTyVarTy, tcSplitSigmaTy,
67 isUnLiftedType, isIPPred,
68 typeKind, isSkolemTyVar,
69 mkAppTy, mkTyVarTy, mkTyVarTys,
70 tyVarsOfPred, getClassPredTys_maybe,
71 tyVarsOfType, tyVarsOfTypes, tcView,
72 pprPred, pprTheta, pprClassPred )
73 import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar,
74 isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
75 liftedTypeKind, defaultKind
77 import Type ( TvSubst, zipTopTvSubst, substTy )
78 import Class ( Class, classArity, className )
79 import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
80 tyConArity, tyConName )
81 import Var ( TyVar, tyVarKind, tyVarName, isTcTyVar,
82 mkTyVar, mkTcTyVar, tcTyVarDetails )
86 import TcType ( isFlexi, isBoxyTyVar, isImmutableTyVar )
87 import Kind ( isSubKind )
91 import TcRnMonad -- TcType, amongst others
92 import FunDeps ( grow )
93 import Name ( Name, setNameUnique, mkSysTvName )
95 import DynFlags ( dopt, DynFlag(..) )
96 import Util ( nOfThem, isSingleton, notNull )
97 import ListSetOps ( removeDups, findDupsEq )
102 %************************************************************************
104 Instantiation in general
106 %************************************************************************
109 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
110 -> TcType -- Type to instantiate
111 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
112 tcInstType inst_tyvars ty
113 = case tcSplitForAllTys ty of
114 ([], rho) -> let -- There may be overloading despite no type variables;
115 -- (?x :: Int) => Int -> Int
116 (theta, tau) = tcSplitPhiTy rho
118 return ([], theta, tau)
120 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
122 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
123 -- Either the tyvars are freshly made, by inst_tyvars,
124 -- or (in the call from tcSkolSigType) any nested foralls
125 -- have different binders. Either way, zipTopTvSubst is ok
127 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
128 ; return (tyvars', theta, tau) }
132 %************************************************************************
136 %************************************************************************
139 newKindVar :: TcM TcKind
140 newKindVar = do { uniq <- newUnique
141 ; ref <- newMutVar Nothing
142 ; return (KindVar (mkKindVar uniq ref)) }
144 newKindVars :: Int -> TcM [TcKind]
145 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
149 %************************************************************************
151 SkolemTvs (immutable)
153 %************************************************************************
156 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
157 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
159 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
160 -- Instantiate a type signature with skolem constants, but
161 -- do *not* give them fresh names, because we want the name to
162 -- be in the type environment -- it is lexically scoped.
163 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
165 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
166 -- Make skolem constants, but do *not* give them new names, as above
167 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
170 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
171 -- Instantiate a type with fresh skolem constants
172 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
174 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
175 tcInstSkolTyVar info tyvar
176 = do { uniq <- newUnique
177 ; let name = setNameUnique (tyVarName tyvar) uniq
178 kind = tyVarKind tyvar
179 ; return (mkSkolTyVar name kind info) }
181 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
182 tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
186 %************************************************************************
188 MetaTvs (meta type variables; mutable)
190 %************************************************************************
193 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
194 -- Make a new meta tyvar out of thin air
195 newMetaTyVar box_info kind
196 = do { uniq <- newUnique
197 ; ref <- newMutVar Flexi ;
198 ; let name = mkSysTvName uniq fs
199 fs = case box_info of
202 SigTv _ -> FSLIT("a")
203 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
205 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
206 -- Make a new meta tyvar whose Name and Kind
207 -- come from an existing TyVar
208 instMetaTyVar box_info tyvar
209 = do { uniq <- newUnique
210 ; ref <- newMutVar Flexi ;
211 ; let name = setNameUnique (tyVarName tyvar) uniq
212 kind = tyVarKind tyvar
213 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
215 readMetaTyVar :: TyVar -> TcM MetaDetails
216 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
217 readMutVar (metaTvRef tyvar)
219 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
221 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
223 writeMetaTyVar tyvar ty
224 | not (isMetaTyVar tyvar)
225 = pprTrace "writeMetaTyVar" (ppr tyvar) $
229 = ASSERT( isMetaTyVar tyvar )
230 ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
231 do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
232 ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
240 %************************************************************************
244 %************************************************************************
247 newFlexiTyVar :: Kind -> TcM TcTyVar
248 newFlexiTyVar kind = newMetaTyVar TauTv kind
250 newFlexiTyVarTy :: Kind -> TcM TcType
252 = newFlexiTyVar kind `thenM` \ tc_tyvar ->
253 returnM (TyVarTy tc_tyvar)
255 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
256 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
258 tcInstTyVar :: TyVar -> TcM TcTyVar
259 -- Instantiate with a META type variable
260 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
262 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
263 -- Instantiate with META type variables
265 = do { tc_tvs <- mapM tcInstTyVar tyvars
266 ; let tys = mkTyVarTys tc_tvs
267 ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
268 -- Since the tyvars are freshly made,
269 -- they cannot possibly be captured by
270 -- any existing for-alls. Hence zipTopTvSubst
274 %************************************************************************
278 %************************************************************************
281 tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
282 -- Instantiate with meta SigTvs
283 tcInstSigTyVars skol_info tyvars
284 = mapM (instMetaTyVar (SigTv skol_info)) tyvars
286 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
288 | isSkolemTyVar sig_tv
289 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
291 = ASSERT( isSigTyVar sig_tv )
292 do { ty <- zonkTcTyVar sig_tv
293 ; return (tcGetTyVar "zonkSigTyVar" ty) }
294 -- 'ty' is bound to be a type variable, because SigTvs
295 -- can only be unified with type variables
299 %************************************************************************
303 %************************************************************************
306 newBoxyTyVar :: Kind -> TcM BoxyTyVar
307 newBoxyTyVar kind = newMetaTyVar BoxTv kind
309 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
310 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
312 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
313 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
315 readFilledBox :: BoxyTyVar -> TcM TcType
316 -- Read the contents of the box, which should be filled in by now
317 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
318 do { cts <- readMetaTyVar box_tv
320 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
321 Indirect ty -> return ty }
323 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
324 -- Instantiate with a BOXY type variable
325 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
327 tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType)
328 -- tcInstType instantiates the outer-level for-alls of a TcType with
329 -- fresh BOXY type variables, splits off the dictionary part,
330 -- and returns the pieces.
331 tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty
335 %************************************************************************
337 \subsection{Putting and getting mutable type variables}
339 %************************************************************************
341 But it's more fun to short out indirections on the way: If this
342 version returns a TyVar, then that TyVar is unbound. If it returns
343 any other type, then there might be bound TyVars embedded inside it.
345 We return Nothing iff the original box was unbound.
348 data LookupTyVarResult -- The result of a lookupTcTyVar call
349 = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
352 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
355 SkolemTv _ -> return (DoneTv details)
356 MetaTv _ ref -> do { meta_details <- readMutVar ref
357 ; case meta_details of
358 Indirect ty -> return (IndirectTv ty)
359 Flexi -> return (DoneTv details) }
361 details = tcTyVarDetails tyvar
364 -- gaw 2004 We aren't shorting anything out anymore, at least for now
366 | not (isTcTyVar tyvar)
367 = pprTrace "getTcTyVar" (ppr tyvar) $
368 returnM (Just (mkTyVarTy tyvar))
371 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
372 readMetaTyVar tyvar `thenM` \ maybe_ty ->
374 Just ty -> short_out ty `thenM` \ ty' ->
375 writeMetaTyVar tyvar (Just ty') `thenM_`
378 Nothing -> returnM Nothing
380 short_out :: TcType -> TcM TcType
381 short_out ty@(TyVarTy tyvar)
382 | not (isTcTyVar tyvar)
386 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
388 Just ty' -> short_out ty' `thenM` \ ty' ->
389 writeMetaTyVar tyvar (Just ty') `thenM_`
394 short_out other_ty = returnM other_ty
399 %************************************************************************
401 \subsection{Zonking -- the exernal interfaces}
403 %************************************************************************
405 ----------------- Type variables
408 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
409 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
411 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
412 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
413 returnM (tyVarsOfTypes tys)
415 zonkTcTyVar :: TcTyVar -> TcM TcType
416 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
417 zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
420 ----------------- Types
423 zonkTcType :: TcType -> TcM TcType
424 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
426 zonkTcTypes :: [TcType] -> TcM [TcType]
427 zonkTcTypes tys = mappM zonkTcType tys
429 zonkTcClassConstraints cts = mappM zonk cts
430 where zonk (clas, tys)
431 = zonkTcTypes tys `thenM` \ new_tys ->
432 returnM (clas, new_tys)
434 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
435 zonkTcThetaType theta = mappM zonkTcPredType theta
437 zonkTcPredType :: TcPredType -> TcM TcPredType
438 zonkTcPredType (ClassP c ts)
439 = zonkTcTypes ts `thenM` \ new_ts ->
440 returnM (ClassP c new_ts)
441 zonkTcPredType (IParam n t)
442 = zonkTcType t `thenM` \ new_t ->
443 returnM (IParam n new_t)
446 ------------------- These ...ToType, ...ToKind versions
447 are used at the end of type checking
450 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
451 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
452 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
453 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
454 -- The meta tyvar is updated to point to the new regular TyVar. Now any
455 -- bound occurences of the original type variable will get zonked to
456 -- the immutable version.
458 -- We leave skolem TyVars alone; they are immutable.
459 zonkQuantifiedTyVar tv
460 | isSkolemTyVar tv = return tv
461 -- It might be a skolem type variable,
462 -- for example from a user type signature
464 | otherwise -- It's a meta-type-variable
465 = do { details <- readMetaTyVar tv
467 -- Create the new, frozen, regular type variable
468 ; let final_kind = defaultKind (tyVarKind tv)
469 final_tv = mkTyVar (tyVarName tv) final_kind
471 -- Bind the meta tyvar to the new tyvar
473 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
475 -- [Sept 04] I don't think this should happen
476 -- See note [Silly Type Synonym]
478 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
480 -- Return the new tyvar
484 [Silly Type Synonyms]
487 type C u a = u -- Note 'a' unused
489 foo :: (forall a. C u a -> C u a) -> u
493 bar = foo (\t -> t + t)
495 * From the (\t -> t+t) we get type {Num d} => d -> d
498 * Now unify with type of foo's arg, and we get:
499 {Num (C d a)} => C d a -> C d a
502 * Now abstract over the 'a', but float out the Num (C d a) constraint
503 because it does not 'really' mention a. (see exactTyVarsOfType)
504 The arg to foo becomes
507 * So we get a dict binding for Num (C d a), which is zonked to give
509 [Note Sept 04: now that we are zonking quantified type variables
510 on construction, the 'a' will be frozen as a regular tyvar on
511 quantification, so the floated dict will still have type (C d a).
512 Which renders this whole note moot; happily!]
514 * Then the /\a abstraction has a zonked 'a' in it.
516 All very silly. I think its harmless to ignore the problem. We'll end up with
517 a /\a in the final result but all the occurrences of a will be zonked to ()
520 %************************************************************************
522 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
524 %* For internal use only! *
526 %************************************************************************
529 -- For unbound, mutable tyvars, zonkType uses the function given to it
530 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
531 -- type variable and zonks the kind too
533 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
534 -- see zonkTcType, and zonkTcTypeToType
537 zonkType unbound_var_fn ty
540 go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
542 go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
543 returnM (TyConApp tc tys')
545 go (PredTy p) = go_pred p `thenM` \ p' ->
548 go (FunTy arg res) = go arg `thenM` \ arg' ->
549 go res `thenM` \ res' ->
550 returnM (FunTy arg' res')
552 go (AppTy fun arg) = go fun `thenM` \ fun' ->
553 go arg `thenM` \ arg' ->
554 returnM (mkAppTy fun' arg')
555 -- NB the mkAppTy; we might have instantiated a
556 -- type variable to a type constructor, so we need
557 -- to pull the TyConApp to the top.
559 -- The two interesting cases!
560 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
561 | otherwise = return (TyVarTy tyvar)
562 -- Ordinary (non Tc) tyvars occur inside quantified types
564 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
565 go ty `thenM` \ ty' ->
566 returnM (ForAllTy tyvar ty')
568 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
569 returnM (ClassP c tys')
570 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
571 returnM (IParam n ty')
573 zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
574 -> TcTyVar -> TcM TcType
575 zonk_tc_tyvar unbound_var_fn tyvar
576 | not (isMetaTyVar tyvar) -- Skolems
577 = returnM (TyVarTy tyvar)
579 | otherwise -- Mutables
580 = do { cts <- readMetaTyVar tyvar
582 Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
583 Indirect ty -> zonkType unbound_var_fn ty }
588 %************************************************************************
592 %************************************************************************
595 readKindVar :: KindVar -> TcM (Maybe TcKind)
596 writeKindVar :: KindVar -> TcKind -> TcM ()
597 readKindVar kv = readMutVar (kindVarRef kv)
598 writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
601 zonkTcKind :: TcKind -> TcM TcKind
602 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
603 ; k2' <- zonkTcKind k2
604 ; returnM (FunKind k1' k2') }
605 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
608 Just k -> zonkTcKind k }
609 zonkTcKind other_kind = returnM other_kind
612 zonkTcKindToKind :: TcKind -> TcM Kind
613 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
614 ; k2' <- zonkTcKindToKind k2
615 ; returnM (FunKind k1' k2') }
617 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
619 Nothing -> return liftedTypeKind
620 Just k -> zonkTcKindToKind k }
622 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
623 zonkTcKindToKind other_kind = returnM other_kind
626 %************************************************************************
628 \subsection{Checking a user type}
630 %************************************************************************
632 When dealing with a user-written type, we first translate it from an HsType
633 to a Type, performing kind checking, and then check various things that should
634 be true about it. We don't want to perform these checks at the same time
635 as the initial translation because (a) they are unnecessary for interface-file
636 types and (b) when checking a mutually recursive group of type and class decls,
637 we can't "look" at the tycons/classes yet. Also, the checks are are rather
638 diverse, and used to really mess up the other code.
640 One thing we check for is 'rank'.
642 Rank 0: monotypes (no foralls)
643 Rank 1: foralls at the front only, Rank 0 inside
644 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
646 basic ::= tyvar | T basic ... basic
648 r2 ::= forall tvs. cxt => r2a
649 r2a ::= r1 -> r2a | basic
650 r1 ::= forall tvs. cxt => r0
651 r0 ::= r0 -> r0 | basic
653 Another thing is to check that type synonyms are saturated.
654 This might not necessarily show up in kind checking.
656 data T k = MkT (k Int)
661 checkValidType :: UserTypeCtxt -> Type -> TcM ()
662 -- Checks that the type is valid for the given context
663 checkValidType ctxt ty
664 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
665 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
667 rank | gla_exts = Arbitrary
669 = case ctxt of -- Haskell 98
671 LamPatSigCtxt -> Rank 0
672 BindPatSigCtxt -> Rank 0
673 DefaultDeclCtxt-> Rank 0
675 TySynCtxt _ -> Rank 0
676 ExprSigCtxt -> Rank 1
677 FunSigCtxt _ -> Rank 1
678 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
679 -- constructor, hence rank 1
680 ForSigCtxt _ -> Rank 1
681 RuleSigCtxt _ -> Rank 1
682 SpecInstCtxt -> Rank 1
684 actual_kind = typeKind ty
686 kind_ok = case ctxt of
687 TySynCtxt _ -> True -- Any kind will do
688 ResSigCtxt -> isOpenTypeKind actual_kind
689 ExprSigCtxt -> isOpenTypeKind actual_kind
690 GenPatCtxt -> isLiftedTypeKind actual_kind
691 ForSigCtxt _ -> isLiftedTypeKind actual_kind
692 other -> isArgTypeKind actual_kind
694 ubx_tup | not gla_exts = UT_NotOk
695 | otherwise = case ctxt of
699 -- Unboxed tuples ok in function results,
700 -- but for type synonyms we allow them even at
703 -- Check that the thing has kind Type, and is lifted if necessary
704 checkTc kind_ok (kindErr actual_kind) `thenM_`
706 -- Check the internal validity of the type itself
707 check_poly_type rank ubx_tup ty `thenM_`
709 traceTc (text "checkValidType done" <+> ppr ty)
714 data Rank = Rank Int | Arbitrary
716 decRank :: Rank -> Rank
717 decRank Arbitrary = Arbitrary
718 decRank (Rank n) = Rank (n-1)
720 ----------------------------------------
721 data UbxTupFlag = UT_Ok | UT_NotOk
722 -- The "Ok" version means "ok if -fglasgow-exts is on"
724 ----------------------------------------
725 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
726 check_poly_type (Rank 0) ubx_tup ty
727 = check_tau_type (Rank 0) ubx_tup ty
729 check_poly_type rank ubx_tup ty
731 (tvs, theta, tau) = tcSplitSigmaTy ty
733 check_valid_theta SigmaCtxt theta `thenM_`
734 check_tau_type (decRank rank) ubx_tup tau `thenM_`
735 checkFreeness tvs theta `thenM_`
736 checkAmbiguity tvs theta (tyVarsOfType tau)
738 ----------------------------------------
739 check_arg_type :: Type -> TcM ()
740 -- The sort of type that can instantiate a type variable,
741 -- or be the argument of a type constructor.
742 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
743 -- Other unboxed types are very occasionally allowed as type
744 -- arguments depending on the kind of the type constructor
746 -- For example, we want to reject things like:
748 -- instance Ord a => Ord (forall s. T s a)
750 -- g :: T s (forall b.b)
752 -- NB: unboxed tuples can have polymorphic or unboxed args.
753 -- This happens in the workers for functions returning
754 -- product types with polymorphic components.
755 -- But not in user code.
756 -- Anyway, they are dealt with by a special case in check_tau_type
759 = check_poly_type Arbitrary UT_NotOk ty `thenM_`
760 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
762 ----------------------------------------
763 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
764 -- Rank is allowed rank for function args
765 -- No foralls otherwise
767 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
768 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
769 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
771 -- Naked PredTys don't usually show up, but they can as a result of
772 -- {-# SPECIALISE instance Ord Char #-}
773 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
774 -- are handled, but the quick thing is just to permit PredTys here.
775 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
776 check_source_ty dflags TypeCtxt sty
778 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
779 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
780 = check_poly_type rank UT_NotOk arg_ty `thenM_`
781 check_poly_type rank UT_Ok res_ty
783 check_tau_type rank ubx_tup (AppTy ty1 ty2)
784 = check_arg_type ty1 `thenM_` check_arg_type ty2
786 check_tau_type rank ubx_tup (NoteTy other_note ty)
787 = check_tau_type rank ubx_tup ty
789 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
791 = do { -- It's OK to have an *over-applied* type synonym
792 -- data Tree a b = ...
793 -- type Foo a = Tree [a]
794 -- f :: Foo a b -> ...
796 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
797 Nothing -> failWithTc arity_msg
799 ; gla_exts <- doptM Opt_GlasgowExts
801 -- If -fglasgow-exts then don't check the type arguments
802 -- This allows us to instantiate a synonym defn with a
803 -- for-all type, or with a partially-applied type synonym.
804 -- e.g. type T a b = a
807 -- Here, T is partially applied, so it's illegal in H98.
808 -- But if you expand S first, then T we get just
813 -- For H98, do check the type args
814 mappM_ check_arg_type tys
817 | isUnboxedTupleTyCon tc
818 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
819 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
820 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
821 -- Args are allowed to be unlifted, or
822 -- more unboxed tuples, so can't use check_arg_ty
825 = mappM_ check_arg_type tys
828 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
831 tc_arity = tyConArity tc
833 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
834 ubx_tup_msg = ubxArgTyErr ty
836 ----------------------------------------
837 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
838 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
839 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
840 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
845 %************************************************************************
847 \subsection{Checking a theta or source type}
849 %************************************************************************
852 -- Enumerate the contexts in which a "source type", <S>, can occur
856 -- or (N a) where N is a newtype
859 = ClassSCCtxt Name -- Superclasses of clas
860 -- class <S> => C a where ...
861 | SigmaCtxt -- Theta part of a normal for-all type
862 -- f :: <S> => a -> a
863 | DataTyCtxt Name -- Theta part of a data decl
864 -- data <S> => T a = MkT a
865 | TypeCtxt -- Source type in an ordinary type
867 | InstThetaCtxt -- Context of an instance decl
868 -- instance <S> => C [a] where ...
869 | InstHeadCtxt -- Head of an instance decl
870 -- instance ... => Eq a where ...
872 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
873 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
874 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
875 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
876 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
877 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
881 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
882 checkValidTheta ctxt theta
883 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
885 -------------------------
886 check_valid_theta ctxt []
888 check_valid_theta ctxt theta
889 = getDOpts `thenM` \ dflags ->
890 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
891 mappM_ (check_source_ty dflags ctxt) theta
893 (_,dups) = removeDups tcCmpPred theta
895 -------------------------
896 check_source_ty dflags ctxt pred@(ClassP cls tys)
897 = -- Class predicates are valid in all contexts
898 checkTc (arity == n_tys) arity_err `thenM_`
900 -- Check the form of the argument types
901 mappM_ check_arg_type tys `thenM_`
902 checkTc (check_class_pred_tys dflags ctxt tys)
903 (predTyVarErr pred $$ how_to_allow)
906 class_name = className cls
907 arity = classArity cls
909 arity_err = arityErr "Class" class_name arity n_tys
911 how_to_allow = case ctxt of
912 InstHeadCtxt -> empty -- Should not happen
913 InstThetaCtxt -> parens undecidableMsg
914 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
916 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
917 -- Implicit parameters only allows in type
918 -- signatures; not in instance decls, superclasses etc
919 -- The reason for not allowing implicit params in instances is a bit subtle
920 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
921 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
922 -- discharge all the potential usas of the ?x in e. For example, a
923 -- constraint Foo [Int] might come out of e,and applying the
924 -- instance decl would show up two uses of ?x.
927 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
929 -------------------------
930 check_class_pred_tys dflags ctxt tys
932 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
933 InstHeadCtxt -> True -- We check for instance-head
934 -- formation in checkValidInstHead
935 InstThetaCtxt -> undecidable_ok || distinct_tyvars tys
936 other -> gla_exts || all tyvar_head tys
938 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
939 gla_exts = dopt Opt_GlasgowExts dflags
941 -------------------------
942 distinct_tyvars tys -- Check that the types are all distinct type variables
943 = all tcIsTyVarTy tys && null (findDupsEq tcEqType tys)
945 -------------------------
946 tyvar_head ty -- Haskell 98 allows predicates of form
947 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
948 | otherwise -- where a is a type variable
949 = case tcSplitAppTy_maybe ty of
950 Just (ty, _) -> tyvar_head ty
957 is ambiguous if P contains generic variables
958 (i.e. one of the Vs) that are not mentioned in tau
960 However, we need to take account of functional dependencies
961 when we speak of 'mentioned in tau'. Example:
962 class C a b | a -> b where ...
964 forall x y. (C x y) => x
965 is not ambiguous because x is mentioned and x determines y
967 NB; the ambiguity check is only used for *user* types, not for types
968 coming from inteface files. The latter can legitimately have
969 ambiguous types. Example
971 class S a where s :: a -> (Int,Int)
972 instance S Char where s _ = (1,1)
973 f:: S a => [a] -> Int -> (Int,Int)
974 f (_::[a]) x = (a*x,b)
975 where (a,b) = s (undefined::a)
977 Here the worker for f gets the type
978 fw :: forall a. S a => Int -> (# Int, Int #)
980 If the list of tv_names is empty, we have a monotype, and then we
981 don't need to check for ambiguity either, because the test can't fail
985 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
986 checkAmbiguity forall_tyvars theta tau_tyvars
987 = mappM_ complain (filter is_ambig theta)
989 complain pred = addErrTc (ambigErr pred)
990 extended_tau_vars = grow theta tau_tyvars
992 -- Only a *class* predicate can give rise to ambiguity
993 -- An *implicit parameter* cannot. For example:
994 -- foo :: (?x :: [a]) => Int
996 -- is fine. The call site will suppply a particular 'x'
997 is_ambig pred = isClassPred pred &&
998 any ambig_var (varSetElems (tyVarsOfPred pred))
1000 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1001 not (ct_var `elemVarSet` extended_tau_vars)
1004 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1005 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1006 ptext SLIT("must be reachable from the type after the '=>'"))]
1009 In addition, GHC insists that at least one type variable
1010 in each constraint is in V. So we disallow a type like
1011 forall a. Eq b => b -> b
1012 even in a scope where b is in scope.
1015 checkFreeness forall_tyvars theta
1016 = mappM_ complain (filter is_free theta)
1018 is_free pred = not (isIPPred pred)
1019 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1020 bound_var ct_var = ct_var `elem` forall_tyvars
1021 complain pred = addErrTc (freeErr pred)
1024 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1025 ptext SLIT("are already in scope"),
1026 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1031 checkThetaCtxt ctxt theta
1032 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1033 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1035 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1036 predTyVarErr pred = sep [ptext SLIT("Non-type variables, or repeated type variables,"),
1037 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1038 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1040 arityErr kind name n m
1041 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1042 n_arguments <> comma, text "but has been given", int m]
1044 n_arguments | n == 0 = ptext SLIT("no arguments")
1045 | n == 1 = ptext SLIT("1 argument")
1046 | True = hsep [int n, ptext SLIT("arguments")]
1050 %************************************************************************
1052 \subsection{Checking for a decent instance head type}
1054 %************************************************************************
1056 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1057 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1059 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1060 flag is on, or (2)~the instance is imported (they must have been
1061 compiled elsewhere). In these cases, we let them go through anyway.
1063 We can also have instances for functions: @instance Foo (a -> b) ...@.
1066 checkValidInstHead :: Type -> TcM (Class, [TcType])
1068 checkValidInstHead ty -- Should be a source type
1069 = case tcSplitPredTy_maybe ty of {
1070 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1073 case getClassPredTys_maybe pred of {
1074 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1077 getDOpts `thenM` \ dflags ->
1078 mappM_ check_arg_type tys `thenM_`
1079 check_inst_head dflags clas tys `thenM_`
1083 check_inst_head dflags clas tys
1084 -- If GlasgowExts then check at least one isn't a type variable
1085 | dopt Opt_GlasgowExts dflags
1086 = check_tyvars dflags clas tys
1088 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1090 tcValidInstHeadTy first_ty
1094 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1097 (first_ty : _) = tys
1099 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1100 text "where T is not a synonym, and a,b,c are distinct type variables")
1102 check_tyvars dflags clas tys
1103 -- Check that at least one isn't a type variable
1104 -- unless -fallow-undecideable-instances
1105 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1106 | not (all tcIsTyVarTy tys) = returnM ()
1107 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1109 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1112 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1116 instTypeErr pp_ty msg
1117 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,