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, 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, 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, openTypeKind, 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 :: TcM BoxyTyVar -- Of openTypeKind
307 newBoxyTyVar = newMetaTyVar BoxTv openTypeKind
309 newBoxyTyVars :: Int -> TcM [BoxyTyVar] -- Of openTypeKind
310 newBoxyTyVars n = sequenceM [newMetaTyVar BoxTv openTypeKind | i <- [1..n]]
312 readFilledBox :: BoxyTyVar -> TcM TcType
313 -- Read the contents of the box, which should be filled in by now
314 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
315 do { cts <- readMetaTyVar box_tv
317 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
318 Indirect ty -> return ty }
320 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
321 -- Instantiate with a BOXY type variable
322 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
324 tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType)
325 -- tcInstType instantiates the outer-level for-alls of a TcType with
326 -- fresh BOXY type variables, splits off the dictionary part,
327 -- and returns the pieces.
328 tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty
332 %************************************************************************
334 \subsection{Putting and getting mutable type variables}
336 %************************************************************************
338 But it's more fun to short out indirections on the way: If this
339 version returns a TyVar, then that TyVar is unbound. If it returns
340 any other type, then there might be bound TyVars embedded inside it.
342 We return Nothing iff the original box was unbound.
345 data LookupTyVarResult -- The result of a lookupTcTyVar call
346 = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
349 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
352 SkolemTv _ -> return (DoneTv details)
353 MetaTv _ ref -> do { meta_details <- readMutVar ref
354 ; case meta_details of
355 Indirect ty -> return (IndirectTv ty)
356 Flexi -> return (DoneTv details) }
358 details = tcTyVarDetails tyvar
361 -- gaw 2004 We aren't shorting anything out anymore, at least for now
363 | not (isTcTyVar tyvar)
364 = pprTrace "getTcTyVar" (ppr tyvar) $
365 returnM (Just (mkTyVarTy tyvar))
368 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
369 readMetaTyVar tyvar `thenM` \ maybe_ty ->
371 Just ty -> short_out ty `thenM` \ ty' ->
372 writeMetaTyVar tyvar (Just ty') `thenM_`
375 Nothing -> returnM Nothing
377 short_out :: TcType -> TcM TcType
378 short_out ty@(TyVarTy tyvar)
379 | not (isTcTyVar tyvar)
383 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
385 Just ty' -> short_out ty' `thenM` \ ty' ->
386 writeMetaTyVar tyvar (Just ty') `thenM_`
391 short_out other_ty = returnM other_ty
396 %************************************************************************
398 \subsection{Zonking -- the exernal interfaces}
400 %************************************************************************
402 ----------------- Type variables
405 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
406 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
408 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
409 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
410 returnM (tyVarsOfTypes tys)
412 zonkTcTyVar :: TcTyVar -> TcM TcType
413 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
414 zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
417 ----------------- Types
420 zonkTcType :: TcType -> TcM TcType
421 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
423 zonkTcTypes :: [TcType] -> TcM [TcType]
424 zonkTcTypes tys = mappM zonkTcType tys
426 zonkTcClassConstraints cts = mappM zonk cts
427 where zonk (clas, tys)
428 = zonkTcTypes tys `thenM` \ new_tys ->
429 returnM (clas, new_tys)
431 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
432 zonkTcThetaType theta = mappM zonkTcPredType theta
434 zonkTcPredType :: TcPredType -> TcM TcPredType
435 zonkTcPredType (ClassP c ts)
436 = zonkTcTypes ts `thenM` \ new_ts ->
437 returnM (ClassP c new_ts)
438 zonkTcPredType (IParam n t)
439 = zonkTcType t `thenM` \ new_t ->
440 returnM (IParam n new_t)
443 ------------------- These ...ToType, ...ToKind versions
444 are used at the end of type checking
447 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
448 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
449 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
450 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
451 -- The meta tyvar is updated to point to the new regular TyVar. Now any
452 -- bound occurences of the original type variable will get zonked to
453 -- the immutable version.
455 -- We leave skolem TyVars alone; they are immutable.
456 zonkQuantifiedTyVar tv
457 | isSkolemTyVar tv = return tv
458 -- It might be a skolem type variable,
459 -- for example from a user type signature
461 | otherwise -- It's a meta-type-variable
462 = do { details <- readMetaTyVar tv
464 -- Create the new, frozen, regular type variable
465 ; let final_kind = defaultKind (tyVarKind tv)
466 final_tv = mkTyVar (tyVarName tv) final_kind
468 -- Bind the meta tyvar to the new tyvar
470 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
472 -- [Sept 04] I don't think this should happen
473 -- See note [Silly Type Synonym]
475 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
477 -- Return the new tyvar
481 [Silly Type Synonyms]
484 type C u a = u -- Note 'a' unused
486 foo :: (forall a. C u a -> C u a) -> u
490 bar = foo (\t -> t + t)
492 * From the (\t -> t+t) we get type {Num d} => d -> d
495 * Now unify with type of foo's arg, and we get:
496 {Num (C d a)} => C d a -> C d a
499 * Now abstract over the 'a', but float out the Num (C d a) constraint
500 because it does not 'really' mention a. (see exactTyVarsOfType)
501 The arg to foo becomes
504 * So we get a dict binding for Num (C d a), which is zonked to give
506 [Note Sept 04: now that we are zonking quantified type variables
507 on construction, the 'a' will be frozen as a regular tyvar on
508 quantification, so the floated dict will still have type (C d a).
509 Which renders this whole note moot; happily!]
511 * Then the /\a abstraction has a zonked 'a' in it.
513 All very silly. I think its harmless to ignore the problem. We'll end up with
514 a /\a in the final result but all the occurrences of a will be zonked to ()
517 %************************************************************************
519 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
521 %* For internal use only! *
523 %************************************************************************
526 -- For unbound, mutable tyvars, zonkType uses the function given to it
527 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
528 -- type variable and zonks the kind too
530 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
531 -- see zonkTcType, and zonkTcTypeToType
534 zonkType unbound_var_fn ty
537 go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
539 go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
540 returnM (TyConApp tc tys')
542 go (PredTy p) = go_pred p `thenM` \ p' ->
545 go (FunTy arg res) = go arg `thenM` \ arg' ->
546 go res `thenM` \ res' ->
547 returnM (FunTy arg' res')
549 go (AppTy fun arg) = go fun `thenM` \ fun' ->
550 go arg `thenM` \ arg' ->
551 returnM (mkAppTy fun' arg')
552 -- NB the mkAppTy; we might have instantiated a
553 -- type variable to a type constructor, so we need
554 -- to pull the TyConApp to the top.
556 -- The two interesting cases!
557 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
558 | otherwise = return (TyVarTy tyvar)
559 -- Ordinary (non Tc) tyvars occur inside quantified types
561 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
562 go ty `thenM` \ ty' ->
563 returnM (ForAllTy tyvar ty')
565 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
566 returnM (ClassP c tys')
567 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
568 returnM (IParam n ty')
570 zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
571 -> TcTyVar -> TcM TcType
572 zonk_tc_tyvar unbound_var_fn tyvar
573 | not (isMetaTyVar tyvar) -- Skolems
574 = returnM (TyVarTy tyvar)
576 | otherwise -- Mutables
577 = do { cts <- readMetaTyVar tyvar
579 Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
580 Indirect ty -> zonkType unbound_var_fn ty }
585 %************************************************************************
589 %************************************************************************
592 readKindVar :: KindVar -> TcM (Maybe TcKind)
593 writeKindVar :: KindVar -> TcKind -> TcM ()
594 readKindVar kv = readMutVar (kindVarRef kv)
595 writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
598 zonkTcKind :: TcKind -> TcM TcKind
599 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
600 ; k2' <- zonkTcKind k2
601 ; returnM (FunKind k1' k2') }
602 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
605 Just k -> zonkTcKind k }
606 zonkTcKind other_kind = returnM other_kind
609 zonkTcKindToKind :: TcKind -> TcM Kind
610 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
611 ; k2' <- zonkTcKindToKind k2
612 ; returnM (FunKind k1' k2') }
614 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
616 Nothing -> return liftedTypeKind
617 Just k -> zonkTcKindToKind k }
619 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
620 zonkTcKindToKind other_kind = returnM other_kind
623 %************************************************************************
625 \subsection{Checking a user type}
627 %************************************************************************
629 When dealing with a user-written type, we first translate it from an HsType
630 to a Type, performing kind checking, and then check various things that should
631 be true about it. We don't want to perform these checks at the same time
632 as the initial translation because (a) they are unnecessary for interface-file
633 types and (b) when checking a mutually recursive group of type and class decls,
634 we can't "look" at the tycons/classes yet. Also, the checks are are rather
635 diverse, and used to really mess up the other code.
637 One thing we check for is 'rank'.
639 Rank 0: monotypes (no foralls)
640 Rank 1: foralls at the front only, Rank 0 inside
641 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
643 basic ::= tyvar | T basic ... basic
645 r2 ::= forall tvs. cxt => r2a
646 r2a ::= r1 -> r2a | basic
647 r1 ::= forall tvs. cxt => r0
648 r0 ::= r0 -> r0 | basic
650 Another thing is to check that type synonyms are saturated.
651 This might not necessarily show up in kind checking.
653 data T k = MkT (k Int)
658 checkValidType :: UserTypeCtxt -> Type -> TcM ()
659 -- Checks that the type is valid for the given context
660 checkValidType ctxt ty
661 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
662 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
664 rank | gla_exts = Arbitrary
666 = case ctxt of -- Haskell 98
668 LamPatSigCtxt -> Rank 0
669 BindPatSigCtxt -> Rank 0
670 DefaultDeclCtxt-> Rank 0
672 TySynCtxt _ -> Rank 0
673 ExprSigCtxt -> Rank 1
674 FunSigCtxt _ -> Rank 1
675 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
676 -- constructor, hence rank 1
677 ForSigCtxt _ -> Rank 1
678 RuleSigCtxt _ -> Rank 1
679 SpecInstCtxt -> Rank 1
681 actual_kind = typeKind ty
683 kind_ok = case ctxt of
684 TySynCtxt _ -> True -- Any kind will do
685 ResSigCtxt -> isOpenTypeKind actual_kind
686 ExprSigCtxt -> isOpenTypeKind actual_kind
687 GenPatCtxt -> isLiftedTypeKind actual_kind
688 ForSigCtxt _ -> isLiftedTypeKind actual_kind
689 other -> isArgTypeKind actual_kind
691 ubx_tup | not gla_exts = UT_NotOk
692 | otherwise = case ctxt of
696 -- Unboxed tuples ok in function results,
697 -- but for type synonyms we allow them even at
700 -- Check that the thing has kind Type, and is lifted if necessary
701 checkTc kind_ok (kindErr actual_kind) `thenM_`
703 -- Check the internal validity of the type itself
704 check_poly_type rank ubx_tup ty `thenM_`
706 traceTc (text "checkValidType done" <+> ppr ty)
711 data Rank = Rank Int | Arbitrary
713 decRank :: Rank -> Rank
714 decRank Arbitrary = Arbitrary
715 decRank (Rank n) = Rank (n-1)
717 ----------------------------------------
718 data UbxTupFlag = UT_Ok | UT_NotOk
719 -- The "Ok" version means "ok if -fglasgow-exts is on"
721 ----------------------------------------
722 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
723 check_poly_type (Rank 0) ubx_tup ty
724 = check_tau_type (Rank 0) ubx_tup ty
726 check_poly_type rank ubx_tup ty
728 (tvs, theta, tau) = tcSplitSigmaTy ty
730 check_valid_theta SigmaCtxt theta `thenM_`
731 check_tau_type (decRank rank) ubx_tup tau `thenM_`
732 checkFreeness tvs theta `thenM_`
733 checkAmbiguity tvs theta (tyVarsOfType tau)
735 ----------------------------------------
736 check_arg_type :: Type -> TcM ()
737 -- The sort of type that can instantiate a type variable,
738 -- or be the argument of a type constructor.
739 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
740 -- Other unboxed types are very occasionally allowed as type
741 -- arguments depending on the kind of the type constructor
743 -- For example, we want to reject things like:
745 -- instance Ord a => Ord (forall s. T s a)
747 -- g :: T s (forall b.b)
749 -- NB: unboxed tuples can have polymorphic or unboxed args.
750 -- This happens in the workers for functions returning
751 -- product types with polymorphic components.
752 -- But not in user code.
753 -- Anyway, they are dealt with by a special case in check_tau_type
756 = check_poly_type Arbitrary UT_NotOk ty `thenM_`
757 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
759 ----------------------------------------
760 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
761 -- Rank is allowed rank for function args
762 -- No foralls otherwise
764 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
765 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
766 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
768 -- Naked PredTys don't usually show up, but they can as a result of
769 -- {-# SPECIALISE instance Ord Char #-}
770 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
771 -- are handled, but the quick thing is just to permit PredTys here.
772 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
773 check_source_ty dflags TypeCtxt sty
775 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
776 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
777 = check_poly_type rank UT_NotOk arg_ty `thenM_`
778 check_poly_type rank UT_Ok res_ty
780 check_tau_type rank ubx_tup (AppTy ty1 ty2)
781 = check_arg_type ty1 `thenM_` check_arg_type ty2
783 check_tau_type rank ubx_tup (NoteTy other_note ty)
784 = check_tau_type rank ubx_tup ty
786 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
788 = do { -- It's OK to have an *over-applied* type synonym
789 -- data Tree a b = ...
790 -- type Foo a = Tree [a]
791 -- f :: Foo a b -> ...
793 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
794 Nothing -> failWithTc arity_msg
796 ; gla_exts <- doptM Opt_GlasgowExts
798 -- If -fglasgow-exts then don't check the type arguments
799 -- This allows us to instantiate a synonym defn with a
800 -- for-all type, or with a partially-applied type synonym.
801 -- e.g. type T a b = a
804 -- Here, T is partially applied, so it's illegal in H98.
805 -- But if you expand S first, then T we get just
810 -- For H98, do check the type args
811 mappM_ check_arg_type tys
814 | isUnboxedTupleTyCon tc
815 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
816 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
817 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
818 -- Args are allowed to be unlifted, or
819 -- more unboxed tuples, so can't use check_arg_ty
822 = mappM_ check_arg_type tys
825 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
828 tc_arity = tyConArity tc
830 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
831 ubx_tup_msg = ubxArgTyErr ty
833 ----------------------------------------
834 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
835 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
836 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
837 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
842 %************************************************************************
844 \subsection{Checking a theta or source type}
846 %************************************************************************
849 -- Enumerate the contexts in which a "source type", <S>, can occur
853 -- or (N a) where N is a newtype
856 = ClassSCCtxt Name -- Superclasses of clas
857 -- class <S> => C a where ...
858 | SigmaCtxt -- Theta part of a normal for-all type
859 -- f :: <S> => a -> a
860 | DataTyCtxt Name -- Theta part of a data decl
861 -- data <S> => T a = MkT a
862 | TypeCtxt -- Source type in an ordinary type
864 | InstThetaCtxt -- Context of an instance decl
865 -- instance <S> => C [a] where ...
866 | InstHeadCtxt -- Head of an instance decl
867 -- instance ... => Eq a where ...
869 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
870 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
871 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
872 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
873 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
874 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
878 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
879 checkValidTheta ctxt theta
880 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
882 -------------------------
883 check_valid_theta ctxt []
885 check_valid_theta ctxt theta
886 = getDOpts `thenM` \ dflags ->
887 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
888 mappM_ (check_source_ty dflags ctxt) theta
890 (_,dups) = removeDups tcCmpPred theta
892 -------------------------
893 check_source_ty dflags ctxt pred@(ClassP cls tys)
894 = -- Class predicates are valid in all contexts
895 checkTc (arity == n_tys) arity_err `thenM_`
897 -- Check the form of the argument types
898 mappM_ check_arg_type tys `thenM_`
899 checkTc (check_class_pred_tys dflags ctxt tys)
900 (predTyVarErr pred $$ how_to_allow)
903 class_name = className cls
904 arity = classArity cls
906 arity_err = arityErr "Class" class_name arity n_tys
908 how_to_allow = case ctxt of
909 InstHeadCtxt -> empty -- Should not happen
910 InstThetaCtxt -> parens undecidableMsg
911 other -> 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 InstHeadCtxt -> True -- We check for instance-head
931 -- formation in checkValidInstHead
932 InstThetaCtxt -> undecidable_ok || distinct_tyvars tys
933 other -> gla_exts || all tyvar_head tys
935 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
936 gla_exts = dopt Opt_GlasgowExts dflags
938 -------------------------
939 distinct_tyvars tys -- Check that the types are all distinct type variables
940 = all tcIsTyVarTy tys && null (findDupsEq tcEqType tys)
942 -------------------------
943 tyvar_head ty -- Haskell 98 allows predicates of form
944 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
945 | otherwise -- where a is a type variable
946 = case tcSplitAppTy_maybe ty of
947 Just (ty, _) -> tyvar_head ty
954 is ambiguous if P contains generic variables
955 (i.e. one of the Vs) that are not mentioned in tau
957 However, we need to take account of functional dependencies
958 when we speak of 'mentioned in tau'. Example:
959 class C a b | a -> b where ...
961 forall x y. (C x y) => x
962 is not ambiguous because x is mentioned and x determines y
964 NB; the ambiguity check is only used for *user* types, not for types
965 coming from inteface files. The latter can legitimately have
966 ambiguous types. Example
968 class S a where s :: a -> (Int,Int)
969 instance S Char where s _ = (1,1)
970 f:: S a => [a] -> Int -> (Int,Int)
971 f (_::[a]) x = (a*x,b)
972 where (a,b) = s (undefined::a)
974 Here the worker for f gets the type
975 fw :: forall a. S a => Int -> (# Int, Int #)
977 If the list of tv_names is empty, we have a monotype, and then we
978 don't need to check for ambiguity either, because the test can't fail
982 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
983 checkAmbiguity forall_tyvars theta tau_tyvars
984 = mappM_ complain (filter is_ambig theta)
986 complain pred = addErrTc (ambigErr pred)
987 extended_tau_vars = grow theta tau_tyvars
989 -- Only a *class* predicate can give rise to ambiguity
990 -- An *implicit parameter* cannot. For example:
991 -- foo :: (?x :: [a]) => Int
993 -- is fine. The call site will suppply a particular 'x'
994 is_ambig pred = isClassPred pred &&
995 any ambig_var (varSetElems (tyVarsOfPred pred))
997 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
998 not (ct_var `elemVarSet` extended_tau_vars)
1001 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1002 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1003 ptext SLIT("must be reachable from the type after the '=>'"))]
1006 In addition, GHC insists that at least one type variable
1007 in each constraint is in V. So we disallow a type like
1008 forall a. Eq b => b -> b
1009 even in a scope where b is in scope.
1012 checkFreeness forall_tyvars theta
1013 = mappM_ complain (filter is_free theta)
1015 is_free pred = not (isIPPred pred)
1016 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1017 bound_var ct_var = ct_var `elem` forall_tyvars
1018 complain pred = addErrTc (freeErr pred)
1021 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1022 ptext SLIT("are already in scope"),
1023 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1028 checkThetaCtxt ctxt theta
1029 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1030 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1032 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1033 predTyVarErr pred = sep [ptext SLIT("Non-type variables, or repeated type variables,"),
1034 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1035 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1037 arityErr kind name n m
1038 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1039 n_arguments <> comma, text "but has been given", int m]
1041 n_arguments | n == 0 = ptext SLIT("no arguments")
1042 | n == 1 = ptext SLIT("1 argument")
1043 | True = hsep [int n, ptext SLIT("arguments")]
1047 %************************************************************************
1049 \subsection{Checking for a decent instance head type}
1051 %************************************************************************
1053 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1054 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1056 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1057 flag is on, or (2)~the instance is imported (they must have been
1058 compiled elsewhere). In these cases, we let them go through anyway.
1060 We can also have instances for functions: @instance Foo (a -> b) ...@.
1063 checkValidInstHead :: Type -> TcM (Class, [TcType])
1065 checkValidInstHead ty -- Should be a source type
1066 = case tcSplitPredTy_maybe ty of {
1067 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1070 case getClassPredTys_maybe pred of {
1071 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1074 getDOpts `thenM` \ dflags ->
1075 mappM_ check_arg_type tys `thenM_`
1076 check_inst_head dflags clas tys `thenM_`
1080 check_inst_head dflags clas tys
1081 -- If GlasgowExts then check at least one isn't a type variable
1082 | dopt Opt_GlasgowExts dflags
1083 = check_tyvars dflags clas tys
1085 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1087 tcValidInstHeadTy first_ty
1091 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1094 (first_ty : _) = tys
1096 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1097 text "where T is not a synonym, and a,b,c are distinct type variables")
1099 check_tyvars dflags clas tys
1100 -- Check that at least one isn't a type variable
1101 -- unless -fallow-undecideable-instances
1102 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1103 | not (all tcIsTyVarTy tys) = returnM ()
1104 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1106 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1109 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1113 instTypeErr pp_ty msg
1114 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,