2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Monadic type operations}
6 This module contains monadic operations over types that contain mutable type variables
10 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
12 --------------------------------
13 -- Creating new mutable type variables
15 newFlexiTyVarTy, -- Kind -> TcM TcType
16 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
17 newKindVar, newKindVars,
18 lookupTcTyVar, LookupTyVarResult(..),
19 newMetaTyVar, readMetaTyVar, writeMetaTyVar,
21 --------------------------------
22 -- Boxy type variables
23 newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
25 --------------------------------
27 tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar,
28 tcInstSigTyVars, zonkSigTyVar,
29 tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
30 tcSkolSigType, tcSkolSigTyVars,
32 --------------------------------
33 -- Checking type validity
34 Rank, UserTypeCtxt(..), checkValidType,
35 SourceTyCtxt(..), checkValidTheta, checkFreeness,
36 checkValidInstHead, checkValidInstance, checkAmbiguity,
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, 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(..), DynFlags )
96 import Util ( nOfThem, isSingleton, notNull )
97 import ListSetOps ( removeDups )
100 import Data.List ( (\\) )
104 %************************************************************************
106 Instantiation in general
108 %************************************************************************
111 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
112 -> TcType -- Type to instantiate
113 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
114 tcInstType inst_tyvars ty
115 = case tcSplitForAllTys ty of
116 ([], rho) -> let -- There may be overloading despite no type variables;
117 -- (?x :: Int) => Int -> Int
118 (theta, tau) = tcSplitPhiTy rho
120 return ([], theta, tau)
122 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
124 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
125 -- Either the tyvars are freshly made, by inst_tyvars,
126 -- or (in the call from tcSkolSigType) any nested foralls
127 -- have different binders. Either way, zipTopTvSubst is ok
129 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
130 ; return (tyvars', theta, tau) }
134 %************************************************************************
138 %************************************************************************
141 newKindVar :: TcM TcKind
142 newKindVar = do { uniq <- newUnique
143 ; ref <- newMutVar Nothing
144 ; return (KindVar (mkKindVar uniq ref)) }
146 newKindVars :: Int -> TcM [TcKind]
147 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
151 %************************************************************************
153 SkolemTvs (immutable)
155 %************************************************************************
158 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
159 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
161 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
162 -- Instantiate a type signature with skolem constants, but
163 -- do *not* give them fresh names, because we want the name to
164 -- be in the type environment -- it is lexically scoped.
165 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
167 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
168 -- Make skolem constants, but do *not* give them new names, as above
169 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
172 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
173 -- Instantiate a type with fresh skolem constants
174 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
176 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
177 tcInstSkolTyVar info tyvar
178 = do { uniq <- newUnique
179 ; let name = setNameUnique (tyVarName tyvar) uniq
180 kind = tyVarKind tyvar
181 ; return (mkSkolTyVar name kind info) }
183 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
184 tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
188 %************************************************************************
190 MetaTvs (meta type variables; mutable)
192 %************************************************************************
195 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
196 -- Make a new meta tyvar out of thin air
197 newMetaTyVar box_info kind
198 = do { uniq <- newUnique
199 ; ref <- newMutVar Flexi ;
200 ; let name = mkSysTvName uniq fs
201 fs = case box_info of
204 SigTv _ -> FSLIT("a")
205 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
207 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
208 -- Make a new meta tyvar whose Name and Kind
209 -- come from an existing TyVar
210 instMetaTyVar box_info tyvar
211 = do { uniq <- newUnique
212 ; ref <- newMutVar Flexi ;
213 ; let name = setNameUnique (tyVarName tyvar) uniq
214 kind = tyVarKind tyvar
215 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
217 readMetaTyVar :: TyVar -> TcM MetaDetails
218 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
219 readMutVar (metaTvRef tyvar)
221 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
223 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
225 writeMetaTyVar tyvar ty
226 | not (isMetaTyVar tyvar)
227 = pprTrace "writeMetaTyVar" (ppr tyvar) $
231 = ASSERT( isMetaTyVar tyvar )
232 ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
233 do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
234 ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
242 %************************************************************************
246 %************************************************************************
249 newFlexiTyVar :: Kind -> TcM TcTyVar
250 newFlexiTyVar kind = newMetaTyVar TauTv kind
252 newFlexiTyVarTy :: Kind -> TcM TcType
254 = newFlexiTyVar kind `thenM` \ tc_tyvar ->
255 returnM (TyVarTy tc_tyvar)
257 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
258 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
260 tcInstTyVar :: TyVar -> TcM TcTyVar
261 -- Instantiate with a META type variable
262 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
264 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
265 -- Instantiate with META type variables
267 = do { tc_tvs <- mapM tcInstTyVar tyvars
268 ; let tys = mkTyVarTys tc_tvs
269 ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
270 -- Since the tyvars are freshly made,
271 -- they cannot possibly be captured by
272 -- any existing for-alls. Hence zipTopTvSubst
276 %************************************************************************
280 %************************************************************************
283 tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
284 -- Instantiate with meta SigTvs
285 tcInstSigTyVars skol_info tyvars
286 = mapM (instMetaTyVar (SigTv skol_info)) tyvars
288 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
290 | isSkolemTyVar sig_tv
291 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
293 = ASSERT( isSigTyVar sig_tv )
294 do { ty <- zonkTcTyVar sig_tv
295 ; return (tcGetTyVar "zonkSigTyVar" ty) }
296 -- 'ty' is bound to be a type variable, because SigTvs
297 -- can only be unified with type variables
301 %************************************************************************
305 %************************************************************************
308 newBoxyTyVar :: Kind -> TcM BoxyTyVar
309 newBoxyTyVar kind = newMetaTyVar BoxTv kind
311 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
312 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
314 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
315 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
317 readFilledBox :: BoxyTyVar -> TcM TcType
318 -- Read the contents of the box, which should be filled in by now
319 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
320 do { cts <- readMetaTyVar box_tv
322 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
323 Indirect ty -> return ty }
325 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
326 -- Instantiate with a BOXY type variable
327 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
329 tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType)
330 -- tcInstType instantiates the outer-level for-alls of a TcType with
331 -- fresh BOXY type variables, splits off the dictionary part,
332 -- and returns the pieces.
333 tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty
337 %************************************************************************
339 \subsection{Putting and getting mutable type variables}
341 %************************************************************************
343 But it's more fun to short out indirections on the way: If this
344 version returns a TyVar, then that TyVar is unbound. If it returns
345 any other type, then there might be bound TyVars embedded inside it.
347 We return Nothing iff the original box was unbound.
350 data LookupTyVarResult -- The result of a lookupTcTyVar call
351 = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
354 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
357 SkolemTv _ -> return (DoneTv details)
358 MetaTv _ ref -> do { meta_details <- readMutVar ref
359 ; case meta_details of
360 Indirect ty -> return (IndirectTv ty)
361 Flexi -> return (DoneTv details) }
363 details = tcTyVarDetails tyvar
366 -- gaw 2004 We aren't shorting anything out anymore, at least for now
368 | not (isTcTyVar tyvar)
369 = pprTrace "getTcTyVar" (ppr tyvar) $
370 returnM (Just (mkTyVarTy tyvar))
373 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
374 readMetaTyVar tyvar `thenM` \ maybe_ty ->
376 Just ty -> short_out ty `thenM` \ ty' ->
377 writeMetaTyVar tyvar (Just ty') `thenM_`
380 Nothing -> returnM Nothing
382 short_out :: TcType -> TcM TcType
383 short_out ty@(TyVarTy tyvar)
384 | not (isTcTyVar tyvar)
388 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
390 Just ty' -> short_out ty' `thenM` \ ty' ->
391 writeMetaTyVar tyvar (Just ty') `thenM_`
396 short_out other_ty = returnM other_ty
401 %************************************************************************
403 \subsection{Zonking -- the exernal interfaces}
405 %************************************************************************
407 ----------------- Type variables
410 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
411 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
413 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
414 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
415 returnM (tyVarsOfTypes tys)
417 zonkTcTyVar :: TcTyVar -> TcM TcType
418 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
419 zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
422 ----------------- Types
425 zonkTcType :: TcType -> TcM TcType
426 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
428 zonkTcTypes :: [TcType] -> TcM [TcType]
429 zonkTcTypes tys = mappM zonkTcType tys
431 zonkTcClassConstraints cts = mappM zonk cts
432 where zonk (clas, tys)
433 = zonkTcTypes tys `thenM` \ new_tys ->
434 returnM (clas, new_tys)
436 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
437 zonkTcThetaType theta = mappM zonkTcPredType theta
439 zonkTcPredType :: TcPredType -> TcM TcPredType
440 zonkTcPredType (ClassP c ts)
441 = zonkTcTypes ts `thenM` \ new_ts ->
442 returnM (ClassP c new_ts)
443 zonkTcPredType (IParam n t)
444 = zonkTcType t `thenM` \ new_t ->
445 returnM (IParam n new_t)
448 ------------------- These ...ToType, ...ToKind versions
449 are used at the end of type checking
452 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
453 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
454 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
455 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
456 -- The meta tyvar is updated to point to the new regular TyVar. Now any
457 -- bound occurences of the original type variable will get zonked to
458 -- the immutable version.
460 -- We leave skolem TyVars alone; they are immutable.
461 zonkQuantifiedTyVar tv
462 | isSkolemTyVar tv = return tv
463 -- It might be a skolem type variable,
464 -- for example from a user type signature
466 | otherwise -- It's a meta-type-variable
467 = do { details <- readMetaTyVar tv
469 -- Create the new, frozen, regular type variable
470 ; let final_kind = defaultKind (tyVarKind tv)
471 final_tv = mkTyVar (tyVarName tv) final_kind
473 -- Bind the meta tyvar to the new tyvar
475 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
477 -- [Sept 04] I don't think this should happen
478 -- See note [Silly Type Synonym]
480 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
482 -- Return the new tyvar
486 [Silly Type Synonyms]
489 type C u a = u -- Note 'a' unused
491 foo :: (forall a. C u a -> C u a) -> u
495 bar = foo (\t -> t + t)
497 * From the (\t -> t+t) we get type {Num d} => d -> d
500 * Now unify with type of foo's arg, and we get:
501 {Num (C d a)} => C d a -> C d a
504 * Now abstract over the 'a', but float out the Num (C d a) constraint
505 because it does not 'really' mention a. (see exactTyVarsOfType)
506 The arg to foo becomes
509 * So we get a dict binding for Num (C d a), which is zonked to give
511 [Note Sept 04: now that we are zonking quantified type variables
512 on construction, the 'a' will be frozen as a regular tyvar on
513 quantification, so the floated dict will still have type (C d a).
514 Which renders this whole note moot; happily!]
516 * Then the /\a abstraction has a zonked 'a' in it.
518 All very silly. I think its harmless to ignore the problem. We'll end up with
519 a /\a in the final result but all the occurrences of a will be zonked to ()
522 %************************************************************************
524 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
526 %* For internal use only! *
528 %************************************************************************
531 -- For unbound, mutable tyvars, zonkType uses the function given to it
532 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
533 -- type variable and zonks the kind too
535 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
536 -- see zonkTcType, and zonkTcTypeToType
539 zonkType unbound_var_fn ty
542 go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
544 go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
545 returnM (TyConApp tc tys')
547 go (PredTy p) = go_pred p `thenM` \ p' ->
550 go (FunTy arg res) = go arg `thenM` \ arg' ->
551 go res `thenM` \ res' ->
552 returnM (FunTy arg' res')
554 go (AppTy fun arg) = go fun `thenM` \ fun' ->
555 go arg `thenM` \ arg' ->
556 returnM (mkAppTy fun' arg')
557 -- NB the mkAppTy; we might have instantiated a
558 -- type variable to a type constructor, so we need
559 -- to pull the TyConApp to the top.
561 -- The two interesting cases!
562 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
563 | otherwise = return (TyVarTy tyvar)
564 -- Ordinary (non Tc) tyvars occur inside quantified types
566 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
567 go ty `thenM` \ ty' ->
568 returnM (ForAllTy tyvar ty')
570 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
571 returnM (ClassP c tys')
572 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
573 returnM (IParam n ty')
575 zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
576 -> TcTyVar -> TcM TcType
577 zonk_tc_tyvar unbound_var_fn tyvar
578 | not (isMetaTyVar tyvar) -- Skolems
579 = returnM (TyVarTy tyvar)
581 | otherwise -- Mutables
582 = do { cts <- readMetaTyVar tyvar
584 Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
585 Indirect ty -> zonkType unbound_var_fn ty }
590 %************************************************************************
594 %************************************************************************
597 readKindVar :: KindVar -> TcM (Maybe TcKind)
598 writeKindVar :: KindVar -> TcKind -> TcM ()
599 readKindVar kv = readMutVar (kindVarRef kv)
600 writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
603 zonkTcKind :: TcKind -> TcM TcKind
604 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
605 ; k2' <- zonkTcKind k2
606 ; returnM (FunKind k1' k2') }
607 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
610 Just k -> zonkTcKind k }
611 zonkTcKind other_kind = returnM other_kind
614 zonkTcKindToKind :: TcKind -> TcM Kind
615 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
616 ; k2' <- zonkTcKindToKind k2
617 ; returnM (FunKind k1' k2') }
619 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
621 Nothing -> return liftedTypeKind
622 Just k -> zonkTcKindToKind k }
624 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
625 zonkTcKindToKind other_kind = returnM other_kind
628 %************************************************************************
630 \subsection{Checking a user type}
632 %************************************************************************
634 When dealing with a user-written type, we first translate it from an HsType
635 to a Type, performing kind checking, and then check various things that should
636 be true about it. We don't want to perform these checks at the same time
637 as the initial translation because (a) they are unnecessary for interface-file
638 types and (b) when checking a mutually recursive group of type and class decls,
639 we can't "look" at the tycons/classes yet. Also, the checks are are rather
640 diverse, and used to really mess up the other code.
642 One thing we check for is 'rank'.
644 Rank 0: monotypes (no foralls)
645 Rank 1: foralls at the front only, Rank 0 inside
646 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
648 basic ::= tyvar | T basic ... basic
650 r2 ::= forall tvs. cxt => r2a
651 r2a ::= r1 -> r2a | basic
652 r1 ::= forall tvs. cxt => r0
653 r0 ::= r0 -> r0 | basic
655 Another thing is to check that type synonyms are saturated.
656 This might not necessarily show up in kind checking.
658 data T k = MkT (k Int)
663 checkValidType :: UserTypeCtxt -> Type -> TcM ()
664 -- Checks that the type is valid for the given context
665 checkValidType ctxt ty
666 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
667 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
669 rank | gla_exts = Arbitrary
671 = case ctxt of -- Haskell 98
673 LamPatSigCtxt -> Rank 0
674 BindPatSigCtxt -> Rank 0
675 DefaultDeclCtxt-> Rank 0
677 TySynCtxt _ -> Rank 0
678 ExprSigCtxt -> Rank 1
679 FunSigCtxt _ -> Rank 1
680 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
681 -- constructor, hence rank 1
682 ForSigCtxt _ -> Rank 1
683 RuleSigCtxt _ -> Rank 1
684 SpecInstCtxt -> Rank 1
686 actual_kind = typeKind ty
688 kind_ok = case ctxt of
689 TySynCtxt _ -> True -- Any kind will do
690 ResSigCtxt -> isOpenTypeKind actual_kind
691 ExprSigCtxt -> isOpenTypeKind actual_kind
692 GenPatCtxt -> isLiftedTypeKind actual_kind
693 ForSigCtxt _ -> isLiftedTypeKind actual_kind
694 other -> isArgTypeKind actual_kind
696 ubx_tup | not gla_exts = UT_NotOk
697 | otherwise = case ctxt of
701 -- Unboxed tuples ok in function results,
702 -- but for type synonyms we allow them even at
705 -- Check that the thing has kind Type, and is lifted if necessary
706 checkTc kind_ok (kindErr actual_kind) `thenM_`
708 -- Check the internal validity of the type itself
709 check_poly_type rank ubx_tup ty `thenM_`
711 traceTc (text "checkValidType done" <+> ppr ty)
716 data Rank = Rank Int | Arbitrary
718 decRank :: Rank -> Rank
719 decRank Arbitrary = Arbitrary
720 decRank (Rank n) = Rank (n-1)
722 ----------------------------------------
723 data UbxTupFlag = UT_Ok | UT_NotOk
724 -- The "Ok" version means "ok if -fglasgow-exts is on"
726 ----------------------------------------
727 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
728 check_poly_type (Rank 0) ubx_tup ty
729 = check_tau_type (Rank 0) ubx_tup ty
731 check_poly_type rank ubx_tup ty
733 (tvs, theta, tau) = tcSplitSigmaTy ty
735 check_valid_theta SigmaCtxt theta `thenM_`
736 check_tau_type (decRank rank) ubx_tup tau `thenM_`
737 checkFreeness tvs theta `thenM_`
738 checkAmbiguity tvs theta (tyVarsOfType tau)
740 ----------------------------------------
741 check_arg_type :: Type -> TcM ()
742 -- The sort of type that can instantiate a type variable,
743 -- or be the argument of a type constructor.
744 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
745 -- Other unboxed types are very occasionally allowed as type
746 -- arguments depending on the kind of the type constructor
748 -- For example, we want to reject things like:
750 -- instance Ord a => Ord (forall s. T s a)
752 -- g :: T s (forall b.b)
754 -- NB: unboxed tuples can have polymorphic or unboxed args.
755 -- This happens in the workers for functions returning
756 -- product types with polymorphic components.
757 -- But not in user code.
758 -- Anyway, they are dealt with by a special case in check_tau_type
761 = check_poly_type Arbitrary UT_NotOk ty `thenM_`
762 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
764 ----------------------------------------
765 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
766 -- Rank is allowed rank for function args
767 -- No foralls otherwise
769 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
770 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
771 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
773 -- Naked PredTys don't usually show up, but they can as a result of
774 -- {-# SPECIALISE instance Ord Char #-}
775 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
776 -- are handled, but the quick thing is just to permit PredTys here.
777 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
778 check_source_ty dflags TypeCtxt sty
780 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
781 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
782 = check_poly_type rank UT_NotOk arg_ty `thenM_`
783 check_poly_type rank UT_Ok res_ty
785 check_tau_type rank ubx_tup (AppTy ty1 ty2)
786 = check_arg_type ty1 `thenM_` check_arg_type ty2
788 check_tau_type rank ubx_tup (NoteTy other_note ty)
789 = check_tau_type rank ubx_tup ty
791 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
793 = do { -- It's OK to have an *over-applied* type synonym
794 -- data Tree a b = ...
795 -- type Foo a = Tree [a]
796 -- f :: Foo a b -> ...
798 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
799 Nothing -> failWithTc arity_msg
801 ; gla_exts <- doptM Opt_GlasgowExts
803 -- If -fglasgow-exts then don't check the type arguments
804 -- This allows us to instantiate a synonym defn with a
805 -- for-all type, or with a partially-applied type synonym.
806 -- e.g. type T a b = a
809 -- Here, T is partially applied, so it's illegal in H98.
810 -- But if you expand S first, then T we get just
815 -- For H98, do check the type args
816 mappM_ check_arg_type tys
819 | isUnboxedTupleTyCon tc
820 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
821 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
822 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
823 -- Args are allowed to be unlifted, or
824 -- more unboxed tuples, so can't use check_arg_ty
827 = mappM_ check_arg_type tys
830 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
833 tc_arity = tyConArity tc
835 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
836 ubx_tup_msg = ubxArgTyErr ty
838 ----------------------------------------
839 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
840 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
841 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
842 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
847 %************************************************************************
849 \subsection{Checking a theta or source type}
851 %************************************************************************
854 -- Enumerate the contexts in which a "source type", <S>, can occur
858 -- or (N a) where N is a newtype
861 = ClassSCCtxt Name -- Superclasses of clas
862 -- class <S> => C a where ...
863 | SigmaCtxt -- Theta part of a normal for-all type
864 -- f :: <S> => a -> a
865 | DataTyCtxt Name -- Theta part of a data decl
866 -- data <S> => T a = MkT a
867 | TypeCtxt -- Source type in an ordinary type
869 | InstThetaCtxt -- Context of an instance decl
870 -- instance <S> => C [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 TypeCtxt = ptext SLIT("the context of a type")
880 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
881 checkValidTheta ctxt theta
882 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
884 -------------------------
885 check_valid_theta ctxt []
887 check_valid_theta ctxt theta
888 = getDOpts `thenM` \ dflags ->
889 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
890 mappM_ (check_source_ty dflags ctxt) theta
892 (_,dups) = removeDups tcCmpPred theta
894 -------------------------
895 check_source_ty dflags ctxt pred@(ClassP cls tys)
896 = -- Class predicates are valid in all contexts
897 checkTc (arity == n_tys) arity_err `thenM_`
899 -- Check the form of the argument types
900 mappM_ check_arg_type tys `thenM_`
901 checkTc (check_class_pred_tys dflags ctxt tys)
902 (predTyVarErr pred $$ how_to_allow)
905 class_name = className cls
906 arity = classArity cls
908 arity_err = arityErr "Class" class_name arity n_tys
909 how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
911 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
912 -- Implicit parameters only allows in type
913 -- signatures; not in instance decls, superclasses etc
914 -- The reason for not allowing implicit params in instances is a bit subtle
915 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
916 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
917 -- discharge all the potential usas of the ?x in e. For example, a
918 -- constraint Foo [Int] might come out of e,and applying the
919 -- instance decl would show up two uses of ?x.
922 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
924 -------------------------
925 check_class_pred_tys dflags ctxt tys
927 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
928 InstThetaCtxt -> gla_exts || all tcIsTyVarTy tys
929 -- Further checks on head and theta in
930 -- checkInstTermination
931 other -> gla_exts || all tyvar_head tys
933 gla_exts = dopt Opt_GlasgowExts dflags
935 -------------------------
936 tyvar_head ty -- Haskell 98 allows predicates of form
937 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
938 | otherwise -- where a is a type variable
939 = case tcSplitAppTy_maybe ty of
940 Just (ty, _) -> tyvar_head ty
947 is ambiguous if P contains generic variables
948 (i.e. one of the Vs) that are not mentioned in tau
950 However, we need to take account of functional dependencies
951 when we speak of 'mentioned in tau'. Example:
952 class C a b | a -> b where ...
954 forall x y. (C x y) => x
955 is not ambiguous because x is mentioned and x determines y
957 NB; the ambiguity check is only used for *user* types, not for types
958 coming from inteface files. The latter can legitimately have
959 ambiguous types. Example
961 class S a where s :: a -> (Int,Int)
962 instance S Char where s _ = (1,1)
963 f:: S a => [a] -> Int -> (Int,Int)
964 f (_::[a]) x = (a*x,b)
965 where (a,b) = s (undefined::a)
967 Here the worker for f gets the type
968 fw :: forall a. S a => Int -> (# Int, Int #)
970 If the list of tv_names is empty, we have a monotype, and then we
971 don't need to check for ambiguity either, because the test can't fail
975 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
976 checkAmbiguity forall_tyvars theta tau_tyvars
977 = mappM_ complain (filter is_ambig theta)
979 complain pred = addErrTc (ambigErr pred)
980 extended_tau_vars = grow theta tau_tyvars
982 -- Only a *class* predicate can give rise to ambiguity
983 -- An *implicit parameter* cannot. For example:
984 -- foo :: (?x :: [a]) => Int
986 -- is fine. The call site will suppply a particular 'x'
987 is_ambig pred = isClassPred pred &&
988 any ambig_var (varSetElems (tyVarsOfPred pred))
990 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
991 not (ct_var `elemVarSet` extended_tau_vars)
994 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
995 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
996 ptext SLIT("must be reachable from the type after the '=>'"))]
999 In addition, GHC insists that at least one type variable
1000 in each constraint is in V. So we disallow a type like
1001 forall a. Eq b => b -> b
1002 even in a scope where b is in scope.
1005 checkFreeness forall_tyvars theta
1006 = mappM_ complain (filter is_free theta)
1008 is_free pred = not (isIPPred pred)
1009 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1010 bound_var ct_var = ct_var `elem` forall_tyvars
1011 complain pred = addErrTc (freeErr pred)
1014 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1015 ptext SLIT("are already in scope"),
1016 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1021 checkThetaCtxt ctxt theta
1022 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1023 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1025 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1026 predTyVarErr pred = sep [ptext SLIT("Non-type variable argument"),
1027 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1028 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1030 arityErr kind name n m
1031 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1032 n_arguments <> comma, text "but has been given", int m]
1034 n_arguments | n == 0 = ptext SLIT("no arguments")
1035 | n == 1 = ptext SLIT("1 argument")
1036 | True = hsep [int n, ptext SLIT("arguments")]
1040 %************************************************************************
1042 \subsection{Checking for a decent instance head type}
1044 %************************************************************************
1046 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1047 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1049 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1050 flag is on, or (2)~the instance is imported (they must have been
1051 compiled elsewhere). In these cases, we let them go through anyway.
1053 We can also have instances for functions: @instance Foo (a -> b) ...@.
1056 checkValidInstHead :: Type -> TcM (Class, [TcType])
1058 checkValidInstHead ty -- Should be a source type
1059 = case tcSplitPredTy_maybe ty of {
1060 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1063 case getClassPredTys_maybe pred of {
1064 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1067 getDOpts `thenM` \ dflags ->
1068 mappM_ check_arg_type tys `thenM_`
1069 check_inst_head dflags clas tys `thenM_`
1073 check_inst_head dflags clas tys
1074 -- If GlasgowExts then check at least one isn't a type variable
1075 | dopt Opt_GlasgowExts dflags
1078 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1080 tcValidInstHeadTy first_ty
1084 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1087 (first_ty : _) = tys
1089 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1090 text "where T is not a synonym, and a,b,c are distinct type variables")
1094 instTypeErr pp_ty msg
1095 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1100 %************************************************************************
1102 \subsection{Checking instance for termination}
1104 %************************************************************************
1108 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1109 checkValidInstance tyvars theta clas inst_tys
1110 = do { dflags <- getDOpts
1112 ; checkValidTheta InstThetaCtxt theta
1113 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1115 -- Check that instance inference will termainate
1116 -- For Haskell 98, checkValidTheta has already done that
1117 ; checkInstTermination dflags theta inst_tys
1119 -- The Coverage Condition
1120 ; checkTc (dopt Opt_AllowUndecidableInstances dflags ||
1121 checkInstCoverage clas inst_tys)
1122 (instTypeErr (pprClassPred clas inst_tys) msg)
1125 msg = parens (ptext SLIT("the instance types do not agree with the functional dependencies of the class"))
1128 Termination test: each assertion in the context satisfies
1129 (1) no variable has more occurrences in the assertion than in the head, and
1130 (2) the assertion has fewer constructors and variables (taken together
1131 and counting repetitions) than the head.
1132 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1133 (which have already been checked) guarantee termination.
1136 checkInstTermination :: DynFlags -> ThetaType -> [TcType] -> TcM ()
1137 checkInstTermination dflags theta tys
1138 | not (dopt Opt_GlasgowExts dflags) = returnM ()
1139 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1141 mappM_ (check_nomore (fvTypes tys)) theta
1142 mappM_ (check_smaller (sizeTypes tys)) theta
1144 check_nomore :: [TyVar] -> PredType -> TcM ()
1145 check_nomore fvs pred
1146 = checkTc (null (fvPred pred \\ fvs))
1147 (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1149 check_smaller :: Int -> PredType -> TcM ()
1150 check_smaller n pred
1151 = checkTc (sizePred pred < n)
1152 (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1154 predUndecErr pred msg = sep [msg,
1155 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1157 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1158 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1159 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1161 -- Free variables of a type, retaining repetitions, and expanding synonyms
1162 fvType :: Type -> [TyVar]
1163 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1164 fvType (TyVarTy tv) = [tv]
1165 fvType (TyConApp _ tys) = fvTypes tys
1166 fvType (NoteTy _ ty) = fvType ty
1167 fvType (PredTy pred) = fvPred pred
1168 fvType (FunTy arg res) = fvType arg ++ fvType res
1169 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1170 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1172 fvTypes :: [Type] -> [TyVar]
1173 fvTypes tys = concat (map fvType tys)
1175 fvPred :: PredType -> [TyVar]
1176 fvPred (ClassP _ tys') = fvTypes tys'
1177 fvPred (IParam _ ty) = fvType ty
1179 -- Size of a type: the number of variables and constructors
1180 sizeType :: Type -> Int
1181 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1182 sizeType (TyVarTy _) = 1
1183 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1184 sizeType (NoteTy _ ty) = sizeType ty
1185 sizeType (PredTy pred) = sizePred pred
1186 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1187 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1188 sizeType (ForAllTy _ ty) = sizeType ty
1190 sizeTypes :: [Type] -> Int
1191 sizeTypes xs = sum (map sizeType xs)
1193 sizePred :: PredType -> Int
1194 sizePred (ClassP _ tys') = sizeTypes tys'
1195 sizePred (IParam _ ty) = sizeType ty