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, 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, UserTypeCtxt(..),
62 isMetaTyVar, isSigTyVar, metaTvRef,
63 tcCmpPred, isClassPred, 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, checkInstCoverage )
93 import Name ( Name, setNameUnique, mkSysTvName )
95 import DynFlags ( dopt, DynFlag(..) )
96 import Util ( nOfThem, isSingleton, notNull )
97 import ListSetOps ( removeDups )
100 import Control.Monad ( when )
101 import Data.List ( (\\) )
105 %************************************************************************
107 Instantiation in general
109 %************************************************************************
112 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
113 -> TcType -- Type to instantiate
114 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
115 tcInstType inst_tyvars ty
116 = case tcSplitForAllTys ty of
117 ([], rho) -> let -- There may be overloading despite no type variables;
118 -- (?x :: Int) => Int -> Int
119 (theta, tau) = tcSplitPhiTy rho
121 return ([], theta, tau)
123 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
125 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
126 -- Either the tyvars are freshly made, by inst_tyvars,
127 -- or (in the call from tcSkolSigType) any nested foralls
128 -- have different binders. Either way, zipTopTvSubst is ok
130 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
131 ; return (tyvars', theta, tau) }
135 %************************************************************************
139 %************************************************************************
142 newKindVar :: TcM TcKind
143 newKindVar = do { uniq <- newUnique
144 ; ref <- newMutVar Nothing
145 ; return (KindVar (mkKindVar uniq ref)) }
147 newKindVars :: Int -> TcM [TcKind]
148 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
152 %************************************************************************
154 SkolemTvs (immutable)
156 %************************************************************************
159 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
160 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
162 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
163 -- Instantiate a type signature with skolem constants, but
164 -- do *not* give them fresh names, because we want the name to
165 -- be in the type environment -- it is lexically scoped.
166 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
168 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
169 -- Make skolem constants, but do *not* give them new names, as above
170 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
173 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
174 -- Instantiate a type with fresh skolem constants
175 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
177 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
178 tcInstSkolTyVar info tyvar
179 = do { uniq <- newUnique
180 ; let name = setNameUnique (tyVarName tyvar) uniq
181 kind = tyVarKind tyvar
182 ; return (mkSkolTyVar name kind info) }
184 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
185 tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
189 %************************************************************************
191 MetaTvs (meta type variables; mutable)
193 %************************************************************************
196 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
197 -- Make a new meta tyvar out of thin air
198 newMetaTyVar box_info kind
199 = do { uniq <- newUnique
200 ; ref <- newMutVar Flexi ;
201 ; let name = mkSysTvName uniq fs
202 fs = case box_info of
205 SigTv _ -> FSLIT("a")
206 -- We give BoxTv and TauTv the same string, because
207 -- otherwise we get user-visible differences in error
208 -- messages, which are confusing. If you want to see
209 -- the box_info of each tyvar, use -dppr-debug
210 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
212 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
213 -- Make a new meta tyvar whose Name and Kind
214 -- come from an existing TyVar
215 instMetaTyVar box_info tyvar
216 = do { uniq <- newUnique
217 ; ref <- newMutVar Flexi ;
218 ; let name = setNameUnique (tyVarName tyvar) uniq
219 kind = tyVarKind tyvar
220 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
222 readMetaTyVar :: TyVar -> TcM MetaDetails
223 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
224 readMutVar (metaTvRef tyvar)
226 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
228 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
230 writeMetaTyVar tyvar ty
231 | not (isMetaTyVar tyvar)
232 = pprTrace "writeMetaTyVar" (ppr tyvar) $
236 = ASSERT( isMetaTyVar tyvar )
237 ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
238 do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
239 ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
247 %************************************************************************
251 %************************************************************************
254 newFlexiTyVar :: Kind -> TcM TcTyVar
255 newFlexiTyVar kind = newMetaTyVar TauTv kind
257 newFlexiTyVarTy :: Kind -> TcM TcType
259 = newFlexiTyVar kind `thenM` \ tc_tyvar ->
260 returnM (TyVarTy tc_tyvar)
262 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
263 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
265 tcInstTyVar :: TyVar -> TcM TcTyVar
266 -- Instantiate with a META type variable
267 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
269 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
270 -- Instantiate with META type variables
272 = do { tc_tvs <- mapM tcInstTyVar tyvars
273 ; let tys = mkTyVarTys tc_tvs
274 ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
275 -- Since the tyvars are freshly made,
276 -- they cannot possibly be captured by
277 -- any existing for-alls. Hence zipTopTvSubst
281 %************************************************************************
285 %************************************************************************
288 tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
289 -- Instantiate with meta SigTvs
290 tcInstSigTyVars skol_info tyvars
291 = mapM (instMetaTyVar (SigTv skol_info)) tyvars
293 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
295 | isSkolemTyVar sig_tv
296 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
298 = ASSERT( isSigTyVar sig_tv )
299 do { ty <- zonkTcTyVar sig_tv
300 ; return (tcGetTyVar "zonkSigTyVar" ty) }
301 -- 'ty' is bound to be a type variable, because SigTvs
302 -- can only be unified with type variables
306 %************************************************************************
310 %************************************************************************
313 newBoxyTyVar :: Kind -> TcM BoxyTyVar
314 newBoxyTyVar kind = newMetaTyVar BoxTv kind
316 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
317 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
319 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
320 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
322 readFilledBox :: BoxyTyVar -> TcM TcType
323 -- Read the contents of the box, which should be filled in by now
324 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
325 do { cts <- readMetaTyVar box_tv
327 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
328 Indirect ty -> return ty }
330 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
331 -- Instantiate with a BOXY type variable
332 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
336 %************************************************************************
338 \subsection{Putting and getting mutable type variables}
340 %************************************************************************
342 But it's more fun to short out indirections on the way: If this
343 version returns a TyVar, then that TyVar is unbound. If it returns
344 any other type, then there might be bound TyVars embedded inside it.
346 We return Nothing iff the original box was unbound.
349 data LookupTyVarResult -- The result of a lookupTcTyVar call
350 = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
353 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
356 SkolemTv _ -> return (DoneTv details)
357 MetaTv _ ref -> do { meta_details <- readMutVar ref
358 ; case meta_details of
359 Indirect ty -> return (IndirectTv ty)
360 Flexi -> return (DoneTv details) }
362 details = tcTyVarDetails tyvar
365 -- gaw 2004 We aren't shorting anything out anymore, at least for now
367 | not (isTcTyVar tyvar)
368 = pprTrace "getTcTyVar" (ppr tyvar) $
369 returnM (Just (mkTyVarTy tyvar))
372 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
373 readMetaTyVar tyvar `thenM` \ maybe_ty ->
375 Just ty -> short_out ty `thenM` \ ty' ->
376 writeMetaTyVar tyvar (Just ty') `thenM_`
379 Nothing -> returnM Nothing
381 short_out :: TcType -> TcM TcType
382 short_out ty@(TyVarTy tyvar)
383 | not (isTcTyVar tyvar)
387 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
389 Just ty' -> short_out ty' `thenM` \ ty' ->
390 writeMetaTyVar tyvar (Just ty') `thenM_`
395 short_out other_ty = returnM other_ty
400 %************************************************************************
402 \subsection{Zonking -- the exernal interfaces}
404 %************************************************************************
406 ----------------- Type variables
409 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
410 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
412 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
413 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
414 returnM (tyVarsOfTypes tys)
416 zonkTcTyVar :: TcTyVar -> TcM TcType
417 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
418 zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
421 ----------------- Types
424 zonkTcType :: TcType -> TcM TcType
425 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
427 zonkTcTypes :: [TcType] -> TcM [TcType]
428 zonkTcTypes tys = mappM zonkTcType tys
430 zonkTcClassConstraints cts = mappM zonk cts
431 where zonk (clas, tys)
432 = zonkTcTypes tys `thenM` \ new_tys ->
433 returnM (clas, new_tys)
435 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
436 zonkTcThetaType theta = mappM zonkTcPredType theta
438 zonkTcPredType :: TcPredType -> TcM TcPredType
439 zonkTcPredType (ClassP c ts)
440 = zonkTcTypes ts `thenM` \ new_ts ->
441 returnM (ClassP c new_ts)
442 zonkTcPredType (IParam n t)
443 = zonkTcType t `thenM` \ new_t ->
444 returnM (IParam n new_t)
447 ------------------- These ...ToType, ...ToKind versions
448 are used at the end of type checking
451 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
452 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
453 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
454 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
455 -- The meta tyvar is updated to point to the new regular TyVar. Now any
456 -- bound occurences of the original type variable will get zonked to
457 -- the immutable version.
459 -- We leave skolem TyVars alone; they are immutable.
460 zonkQuantifiedTyVar tv
461 | isSkolemTyVar tv = return tv
462 -- It might be a skolem type variable,
463 -- for example from a user type signature
465 | otherwise -- It's a meta-type-variable
466 = do { details <- readMetaTyVar tv
468 -- Create the new, frozen, regular type variable
469 ; let final_kind = defaultKind (tyVarKind tv)
470 final_tv = mkTyVar (tyVarName tv) final_kind
472 -- Bind the meta tyvar to the new tyvar
474 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
476 -- [Sept 04] I don't think this should happen
477 -- See note [Silly Type Synonym]
479 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
481 -- Return the new tyvar
485 [Silly Type Synonyms]
488 type C u a = u -- Note 'a' unused
490 foo :: (forall a. C u a -> C u a) -> u
494 bar = foo (\t -> t + t)
496 * From the (\t -> t+t) we get type {Num d} => d -> d
499 * Now unify with type of foo's arg, and we get:
500 {Num (C d a)} => C d a -> C d a
503 * Now abstract over the 'a', but float out the Num (C d a) constraint
504 because it does not 'really' mention a. (see exactTyVarsOfType)
505 The arg to foo becomes
508 * So we get a dict binding for Num (C d a), which is zonked to give
510 [Note Sept 04: now that we are zonking quantified type variables
511 on construction, the 'a' will be frozen as a regular tyvar on
512 quantification, so the floated dict will still have type (C d a).
513 Which renders this whole note moot; happily!]
515 * Then the /\a abstraction has a zonked 'a' in it.
517 All very silly. I think its harmless to ignore the problem. We'll end up with
518 a /\a in the final result but all the occurrences of a will be zonked to ()
521 %************************************************************************
523 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
525 %* For internal use only! *
527 %************************************************************************
530 -- For unbound, mutable tyvars, zonkType uses the function given to it
531 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
532 -- type variable and zonks the kind too
534 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
535 -- see zonkTcType, and zonkTcTypeToType
538 zonkType unbound_var_fn ty
541 go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
543 go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
544 returnM (TyConApp tc tys')
546 go (PredTy p) = go_pred p `thenM` \ p' ->
549 go (FunTy arg res) = go arg `thenM` \ arg' ->
550 go res `thenM` \ res' ->
551 returnM (FunTy arg' res')
553 go (AppTy fun arg) = go fun `thenM` \ fun' ->
554 go arg `thenM` \ arg' ->
555 returnM (mkAppTy fun' arg')
556 -- NB the mkAppTy; we might have instantiated a
557 -- type variable to a type constructor, so we need
558 -- to pull the TyConApp to the top.
560 -- The two interesting cases!
561 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
562 | otherwise = return (TyVarTy tyvar)
563 -- Ordinary (non Tc) tyvars occur inside quantified types
565 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
566 go ty `thenM` \ ty' ->
567 returnM (ForAllTy tyvar ty')
569 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
570 returnM (ClassP c tys')
571 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
572 returnM (IParam n ty')
574 zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
575 -> TcTyVar -> TcM TcType
576 zonk_tc_tyvar unbound_var_fn tyvar
577 | not (isMetaTyVar tyvar) -- Skolems
578 = returnM (TyVarTy tyvar)
580 | otherwise -- Mutables
581 = do { cts <- readMetaTyVar tyvar
583 Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
584 Indirect ty -> zonkType unbound_var_fn ty }
589 %************************************************************************
593 %************************************************************************
596 readKindVar :: KindVar -> TcM (Maybe TcKind)
597 writeKindVar :: KindVar -> TcKind -> TcM ()
598 readKindVar kv = readMutVar (kindVarRef kv)
599 writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
602 zonkTcKind :: TcKind -> TcM TcKind
603 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
604 ; k2' <- zonkTcKind k2
605 ; returnM (FunKind k1' k2') }
606 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
609 Just k -> zonkTcKind k }
610 zonkTcKind other_kind = returnM other_kind
613 zonkTcKindToKind :: TcKind -> TcM Kind
614 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
615 ; k2' <- zonkTcKindToKind k2
616 ; returnM (FunKind k1' k2') }
618 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
620 Nothing -> return liftedTypeKind
621 Just k -> zonkTcKindToKind k }
623 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
624 zonkTcKindToKind other_kind = returnM other_kind
627 %************************************************************************
629 \subsection{Checking a user type}
631 %************************************************************************
633 When dealing with a user-written type, we first translate it from an HsType
634 to a Type, performing kind checking, and then check various things that should
635 be true about it. We don't want to perform these checks at the same time
636 as the initial translation because (a) they are unnecessary for interface-file
637 types and (b) when checking a mutually recursive group of type and class decls,
638 we can't "look" at the tycons/classes yet. Also, the checks are are rather
639 diverse, and used to really mess up the other code.
641 One thing we check for is 'rank'.
643 Rank 0: monotypes (no foralls)
644 Rank 1: foralls at the front only, Rank 0 inside
645 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
647 basic ::= tyvar | T basic ... basic
649 r2 ::= forall tvs. cxt => r2a
650 r2a ::= r1 -> r2a | basic
651 r1 ::= forall tvs. cxt => r0
652 r0 ::= r0 -> r0 | basic
654 Another thing is to check that type synonyms are saturated.
655 This might not necessarily show up in kind checking.
657 data T k = MkT (k Int)
662 checkValidType :: UserTypeCtxt -> Type -> TcM ()
663 -- Checks that the type is valid for the given context
664 checkValidType ctxt ty
665 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
666 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
668 rank | gla_exts = Arbitrary
670 = case ctxt of -- Haskell 98
672 LamPatSigCtxt -> Rank 0
673 BindPatSigCtxt -> Rank 0
674 DefaultDeclCtxt-> Rank 0
676 TySynCtxt _ -> Rank 0
677 ExprSigCtxt -> Rank 1
678 FunSigCtxt _ -> Rank 1
679 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
680 -- constructor, hence rank 1
681 ForSigCtxt _ -> Rank 1
682 RuleSigCtxt _ -> Rank 1
683 SpecInstCtxt -> Rank 1
685 actual_kind = typeKind ty
687 kind_ok = case ctxt of
688 TySynCtxt _ -> True -- Any kind will do
689 ResSigCtxt -> isOpenTypeKind actual_kind
690 ExprSigCtxt -> isOpenTypeKind actual_kind
691 GenPatCtxt -> isLiftedTypeKind actual_kind
692 ForSigCtxt _ -> isLiftedTypeKind actual_kind
693 other -> isArgTypeKind actual_kind
695 ubx_tup | not gla_exts = UT_NotOk
696 | otherwise = case ctxt of
700 -- Unboxed tuples ok in function results,
701 -- but for type synonyms we allow them even at
704 -- Check that the thing has kind Type, and is lifted if necessary
705 checkTc kind_ok (kindErr actual_kind) `thenM_`
707 -- Check the internal validity of the type itself
708 check_poly_type rank ubx_tup ty `thenM_`
710 traceTc (text "checkValidType done" <+> ppr ty)
715 data Rank = Rank Int | Arbitrary
717 decRank :: Rank -> Rank
718 decRank Arbitrary = Arbitrary
719 decRank (Rank n) = Rank (n-1)
721 ----------------------------------------
722 data UbxTupFlag = UT_Ok | UT_NotOk
723 -- The "Ok" version means "ok if -fglasgow-exts is on"
725 ----------------------------------------
726 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
727 check_poly_type (Rank 0) ubx_tup ty
728 = check_tau_type (Rank 0) ubx_tup ty
730 check_poly_type rank ubx_tup ty
731 | null tvs && null theta
732 = check_tau_type rank ubx_tup ty
734 = do { check_valid_theta SigmaCtxt theta
735 ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow
736 ; checkFreeness tvs theta
737 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
739 (tvs, theta, tau) = tcSplitSigmaTy ty
741 ----------------------------------------
742 check_arg_type :: Type -> TcM ()
743 -- The sort of type that can instantiate a type variable,
744 -- or be the argument of a type constructor.
745 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
746 -- Other unboxed types are very occasionally allowed as type
747 -- arguments depending on the kind of the type constructor
749 -- For example, we want to reject things like:
751 -- instance Ord a => Ord (forall s. T s a)
753 -- g :: T s (forall b.b)
755 -- NB: unboxed tuples can have polymorphic or unboxed args.
756 -- This happens in the workers for functions returning
757 -- product types with polymorphic components.
758 -- But not in user code.
759 -- Anyway, they are dealt with by a special case in check_tau_type
762 = check_poly_type Arbitrary UT_NotOk ty `thenM_`
763 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
765 ----------------------------------------
766 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
767 -- Rank is allowed rank for function args
768 -- No foralls otherwise
770 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
771 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
772 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
774 -- Naked PredTys don't usually show up, but they can as a result of
775 -- {-# SPECIALISE instance Ord Char #-}
776 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
777 -- are handled, but the quick thing is just to permit PredTys here.
778 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
779 check_source_ty dflags TypeCtxt sty
781 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
782 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
783 = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_`
784 check_poly_type rank UT_Ok res_ty
786 check_tau_type rank ubx_tup (AppTy ty1 ty2)
787 = check_arg_type ty1 `thenM_` check_arg_type ty2
789 check_tau_type rank ubx_tup (NoteTy other_note ty)
790 = check_tau_type rank ubx_tup ty
792 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
794 = do { -- It's OK to have an *over-applied* type synonym
795 -- data Tree a b = ...
796 -- type Foo a = Tree [a]
797 -- f :: Foo a b -> ...
799 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
800 Nothing -> failWithTc arity_msg
802 ; gla_exts <- doptM Opt_GlasgowExts
804 -- If -fglasgow-exts then don't check the type arguments
805 -- This allows us to instantiate a synonym defn with a
806 -- for-all type, or with a partially-applied type synonym.
807 -- e.g. type T a b = a
810 -- Here, T is partially applied, so it's illegal in H98.
811 -- But if you expand S first, then T we get just
816 -- For H98, do check the type args
817 mappM_ check_arg_type tys
820 | isUnboxedTupleTyCon tc
821 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
822 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
823 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
824 -- Args are allowed to be unlifted, or
825 -- more unboxed tuples, so can't use check_arg_ty
828 = mappM_ check_arg_type tys
831 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
834 tc_arity = tyConArity tc
836 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
837 ubx_tup_msg = ubxArgTyErr ty
839 ----------------------------------------
840 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
841 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
842 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
843 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
848 %************************************************************************
850 \subsection{Checking a theta or source type}
852 %************************************************************************
855 -- Enumerate the contexts in which a "source type", <S>, can occur
859 -- or (N a) where N is a newtype
862 = ClassSCCtxt Name -- Superclasses of clas
863 -- class <S> => C a where ...
864 | SigmaCtxt -- Theta part of a normal for-all type
865 -- f :: <S> => a -> a
866 | DataTyCtxt Name -- Theta part of a data decl
867 -- data <S> => T a = MkT a
868 | TypeCtxt -- Source type in an ordinary type
870 | InstThetaCtxt -- Context of an instance decl
871 -- instance <S> => C [a] where ...
873 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
874 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
875 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
876 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context 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
910 how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
912 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
913 -- Implicit parameters only allows in type
914 -- signatures; not in instance decls, superclasses etc
915 -- The reason for not allowing implicit params in instances is a bit subtle
916 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
917 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
918 -- discharge all the potential usas of the ?x in e. For example, a
919 -- constraint Foo [Int] might come out of e,and applying the
920 -- instance decl would show up two uses of ?x.
923 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
925 -------------------------
926 check_class_pred_tys dflags ctxt tys
928 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
929 InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
930 -- Further checks on head and theta in
931 -- checkInstTermination
932 other -> gla_exts || all tyvar_head tys
934 gla_exts = dopt Opt_GlasgowExts dflags
935 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
937 -------------------------
938 tyvar_head ty -- Haskell 98 allows predicates of form
939 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
940 | otherwise -- where a is a type variable
941 = case tcSplitAppTy_maybe ty of
942 Just (ty, _) -> tyvar_head ty
949 is ambiguous if P contains generic variables
950 (i.e. one of the Vs) that are not mentioned in tau
952 However, we need to take account of functional dependencies
953 when we speak of 'mentioned in tau'. Example:
954 class C a b | a -> b where ...
956 forall x y. (C x y) => x
957 is not ambiguous because x is mentioned and x determines y
959 NB; the ambiguity check is only used for *user* types, not for types
960 coming from inteface files. The latter can legitimately have
961 ambiguous types. Example
963 class S a where s :: a -> (Int,Int)
964 instance S Char where s _ = (1,1)
965 f:: S a => [a] -> Int -> (Int,Int)
966 f (_::[a]) x = (a*x,b)
967 where (a,b) = s (undefined::a)
969 Here the worker for f gets the type
970 fw :: forall a. S a => Int -> (# Int, Int #)
972 If the list of tv_names is empty, we have a monotype, and then we
973 don't need to check for ambiguity either, because the test can't fail
977 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
978 checkAmbiguity forall_tyvars theta tau_tyvars
979 = mappM_ complain (filter is_ambig theta)
981 complain pred = addErrTc (ambigErr pred)
982 extended_tau_vars = grow theta tau_tyvars
984 -- Only a *class* predicate can give rise to ambiguity
985 -- An *implicit parameter* cannot. For example:
986 -- foo :: (?x :: [a]) => Int
988 -- is fine. The call site will suppply a particular 'x'
989 is_ambig pred = isClassPred pred &&
990 any ambig_var (varSetElems (tyVarsOfPred pred))
992 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
993 not (ct_var `elemVarSet` extended_tau_vars)
996 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
997 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
998 ptext SLIT("must be reachable from the type after the '=>'"))]
1001 In addition, GHC insists that at least one type variable
1002 in each constraint is in V. So we disallow a type like
1003 forall a. Eq b => b -> b
1004 even in a scope where b is in scope.
1007 checkFreeness forall_tyvars theta
1008 = mappM_ complain (filter is_free theta)
1010 is_free pred = not (isIPPred pred)
1011 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1012 bound_var ct_var = ct_var `elem` forall_tyvars
1013 complain pred = addErrTc (freeErr pred)
1016 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1017 ptext SLIT("are already in scope"),
1018 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1023 checkThetaCtxt ctxt theta
1024 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1025 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1027 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1028 predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
1029 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1030 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1032 arityErr kind name n m
1033 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1034 n_arguments <> comma, text "but has been given", int m]
1036 n_arguments | n == 0 = ptext SLIT("no arguments")
1037 | n == 1 = ptext SLIT("1 argument")
1038 | True = hsep [int n, ptext SLIT("arguments")]
1042 %************************************************************************
1044 \subsection{Checking for a decent instance head type}
1046 %************************************************************************
1048 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1049 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1051 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1052 flag is on, or (2)~the instance is imported (they must have been
1053 compiled elsewhere). In these cases, we let them go through anyway.
1055 We can also have instances for functions: @instance Foo (a -> b) ...@.
1058 checkValidInstHead :: Type -> TcM (Class, [TcType])
1060 checkValidInstHead ty -- Should be a source type
1061 = case tcSplitPredTy_maybe ty of {
1062 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1065 case getClassPredTys_maybe pred of {
1066 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1069 getDOpts `thenM` \ dflags ->
1070 mappM_ check_arg_type tys `thenM_`
1071 check_inst_head dflags clas tys `thenM_`
1075 check_inst_head dflags clas tys
1076 -- If GlasgowExts then check at least one isn't a type variable
1077 | dopt Opt_GlasgowExts dflags
1078 = mapM_ check_one tys
1080 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1082 = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
1083 (instTypeErr (pprClassPred clas tys) head_shape_msg)
1086 (first_ty : _) = tys
1088 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1089 text "where T is not a synonym, and a,b,c are distinct type variables")
1091 -- For now, I only allow tau-types (not polytypes) in
1092 -- the head of an instance decl.
1093 -- E.g. instance C (forall a. a->a) is rejected
1094 -- One could imagine generalising that, but I'm not sure
1095 -- what all the consequences might be
1096 check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1097 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1099 instTypeErr pp_ty msg
1100 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1105 %************************************************************************
1107 \subsection{Checking instance for termination}
1109 %************************************************************************
1113 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1114 checkValidInstance tyvars theta clas inst_tys
1115 = do { gla_exts <- doptM Opt_GlasgowExts
1116 ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
1118 ; checkValidTheta InstThetaCtxt theta
1119 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1121 -- Check that instance inference will terminate (if we care)
1122 -- For Haskell 98, checkValidTheta has already done that
1123 ; when (gla_exts && not undecidable_ok) $
1124 checkInstTermination theta inst_tys
1126 -- The Coverage Condition
1127 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1128 (instTypeErr (pprClassPred clas inst_tys) msg)
1131 msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
1134 Termination test: each assertion in the context satisfies
1135 (1) no variable has more occurrences in the assertion than in the head, and
1136 (2) the assertion has fewer constructors and variables (taken together
1137 and counting repetitions) than the head.
1138 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1139 (which have already been checked) guarantee termination.
1141 The underlying idea is that
1143 for any ground substitution, each assertion in the
1144 context has fewer type constructors than the head.
1148 checkInstTermination :: ThetaType -> [TcType] -> TcM ()
1149 checkInstTermination theta tys
1150 = do { mappM_ (check_nomore (fvTypes tys)) theta
1151 ; mappM_ (check_smaller (sizeTypes tys)) theta }
1153 check_nomore :: [TyVar] -> PredType -> TcM ()
1154 check_nomore fvs pred
1155 = checkTc (null (fvPred pred \\ fvs))
1156 (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1158 check_smaller :: Int -> PredType -> TcM ()
1159 check_smaller n pred
1160 = checkTc (sizePred pred < n)
1161 (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1163 predUndecErr pred msg = sep [msg,
1164 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1166 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1167 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1168 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1170 -- Free variables of a type, retaining repetitions, and expanding synonyms
1171 fvType :: Type -> [TyVar]
1172 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1173 fvType (TyVarTy tv) = [tv]
1174 fvType (TyConApp _ tys) = fvTypes tys
1175 fvType (NoteTy _ ty) = fvType ty
1176 fvType (PredTy pred) = fvPred pred
1177 fvType (FunTy arg res) = fvType arg ++ fvType res
1178 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1179 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1181 fvTypes :: [Type] -> [TyVar]
1182 fvTypes tys = concat (map fvType tys)
1184 fvPred :: PredType -> [TyVar]
1185 fvPred (ClassP _ tys') = fvTypes tys'
1186 fvPred (IParam _ ty) = fvType ty
1188 -- Size of a type: the number of variables and constructors
1189 sizeType :: Type -> Int
1190 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1191 sizeType (TyVarTy _) = 1
1192 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1193 sizeType (NoteTy _ ty) = sizeType ty
1194 sizeType (PredTy pred) = sizePred pred
1195 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1196 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1197 sizeType (ForAllTy _ ty) = sizeType ty
1199 sizeTypes :: [Type] -> Int
1200 sizeTypes xs = sum (map sizeType xs)
1202 sizePred :: PredType -> Int
1203 sizePred (ClassP _ tys') = sizeTypes tys'
1204 sizePred (IParam _ ty) = sizeType ty