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 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
208 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
209 -- Make a new meta tyvar whose Name and Kind
210 -- come from an existing TyVar
211 instMetaTyVar box_info tyvar
212 = do { uniq <- newUnique
213 ; ref <- newMutVar Flexi ;
214 ; let name = setNameUnique (tyVarName tyvar) uniq
215 kind = tyVarKind tyvar
216 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
218 readMetaTyVar :: TyVar -> TcM MetaDetails
219 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
220 readMutVar (metaTvRef tyvar)
222 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
224 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
226 writeMetaTyVar tyvar ty
227 | not (isMetaTyVar tyvar)
228 = pprTrace "writeMetaTyVar" (ppr tyvar) $
232 = ASSERT( isMetaTyVar tyvar )
233 ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
234 do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
235 ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
243 %************************************************************************
247 %************************************************************************
250 newFlexiTyVar :: Kind -> TcM TcTyVar
251 newFlexiTyVar kind = newMetaTyVar TauTv kind
253 newFlexiTyVarTy :: Kind -> TcM TcType
255 = newFlexiTyVar kind `thenM` \ tc_tyvar ->
256 returnM (TyVarTy tc_tyvar)
258 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
259 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
261 tcInstTyVar :: TyVar -> TcM TcTyVar
262 -- Instantiate with a META type variable
263 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
265 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
266 -- Instantiate with META type variables
268 = do { tc_tvs <- mapM tcInstTyVar tyvars
269 ; let tys = mkTyVarTys tc_tvs
270 ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
271 -- Since the tyvars are freshly made,
272 -- they cannot possibly be captured by
273 -- any existing for-alls. Hence zipTopTvSubst
277 %************************************************************************
281 %************************************************************************
284 tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
285 -- Instantiate with meta SigTvs
286 tcInstSigTyVars skol_info tyvars
287 = mapM (instMetaTyVar (SigTv skol_info)) tyvars
289 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
291 | isSkolemTyVar sig_tv
292 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
294 = ASSERT( isSigTyVar sig_tv )
295 do { ty <- zonkTcTyVar sig_tv
296 ; return (tcGetTyVar "zonkSigTyVar" ty) }
297 -- 'ty' is bound to be a type variable, because SigTvs
298 -- can only be unified with type variables
302 %************************************************************************
306 %************************************************************************
309 newBoxyTyVar :: Kind -> TcM BoxyTyVar
310 newBoxyTyVar kind = newMetaTyVar BoxTv kind
312 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
313 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
315 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
316 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
318 readFilledBox :: BoxyTyVar -> TcM TcType
319 -- Read the contents of the box, which should be filled in by now
320 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
321 do { cts <- readMetaTyVar box_tv
323 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
324 Indirect ty -> return ty }
326 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
327 -- Instantiate with a BOXY type variable
328 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
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
727 | null tvs && null theta
728 = check_tau_type rank ubx_tup ty
730 = do { check_valid_theta SigmaCtxt theta
731 ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow
732 ; checkFreeness tvs theta
733 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
735 (tvs, theta, tau) = tcSplitSigmaTy ty
737 ----------------------------------------
738 check_arg_type :: Type -> TcM ()
739 -- The sort of type that can instantiate a type variable,
740 -- or be the argument of a type constructor.
741 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
742 -- Other unboxed types are very occasionally allowed as type
743 -- arguments depending on the kind of the type constructor
745 -- For example, we want to reject things like:
747 -- instance Ord a => Ord (forall s. T s a)
749 -- g :: T s (forall b.b)
751 -- NB: unboxed tuples can have polymorphic or unboxed args.
752 -- This happens in the workers for functions returning
753 -- product types with polymorphic components.
754 -- But not in user code.
755 -- Anyway, they are dealt with by a special case in check_tau_type
758 = check_poly_type Arbitrary UT_NotOk ty `thenM_`
759 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
761 ----------------------------------------
762 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
763 -- Rank is allowed rank for function args
764 -- No foralls otherwise
766 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
767 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
768 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
770 -- Naked PredTys don't usually show up, but they can as a result of
771 -- {-# SPECIALISE instance Ord Char #-}
772 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
773 -- are handled, but the quick thing is just to permit PredTys here.
774 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
775 check_source_ty dflags TypeCtxt sty
777 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
778 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
779 = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_`
780 check_poly_type rank UT_Ok res_ty
782 check_tau_type rank ubx_tup (AppTy ty1 ty2)
783 = check_arg_type ty1 `thenM_` check_arg_type ty2
785 check_tau_type rank ubx_tup (NoteTy other_note ty)
786 = check_tau_type rank ubx_tup ty
788 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
790 = do { -- It's OK to have an *over-applied* type synonym
791 -- data Tree a b = ...
792 -- type Foo a = Tree [a]
793 -- f :: Foo a b -> ...
795 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
796 Nothing -> failWithTc arity_msg
798 ; gla_exts <- doptM Opt_GlasgowExts
800 -- If -fglasgow-exts then don't check the type arguments
801 -- This allows us to instantiate a synonym defn with a
802 -- for-all type, or with a partially-applied type synonym.
803 -- e.g. type T a b = a
806 -- Here, T is partially applied, so it's illegal in H98.
807 -- But if you expand S first, then T we get just
812 -- For H98, do check the type args
813 mappM_ check_arg_type tys
816 | isUnboxedTupleTyCon tc
817 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
818 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
819 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
820 -- Args are allowed to be unlifted, or
821 -- more unboxed tuples, so can't use check_arg_ty
824 = mappM_ check_arg_type tys
827 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
830 tc_arity = tyConArity tc
832 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
833 ubx_tup_msg = ubxArgTyErr ty
835 ----------------------------------------
836 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
837 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
838 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
839 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
844 %************************************************************************
846 \subsection{Checking a theta or source type}
848 %************************************************************************
851 -- Enumerate the contexts in which a "source type", <S>, can occur
855 -- or (N a) where N is a newtype
858 = ClassSCCtxt Name -- Superclasses of clas
859 -- class <S> => C a where ...
860 | SigmaCtxt -- Theta part of a normal for-all type
861 -- f :: <S> => a -> a
862 | DataTyCtxt Name -- Theta part of a data decl
863 -- data <S> => T a = MkT a
864 | TypeCtxt -- Source type in an ordinary type
866 | InstThetaCtxt -- Context of an instance decl
867 -- instance <S> => C [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 TypeCtxt = ptext SLIT("the context of a type")
877 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
878 checkValidTheta ctxt theta
879 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
881 -------------------------
882 check_valid_theta ctxt []
884 check_valid_theta ctxt theta
885 = getDOpts `thenM` \ dflags ->
886 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
887 mappM_ (check_source_ty dflags ctxt) theta
889 (_,dups) = removeDups tcCmpPred theta
891 -------------------------
892 check_source_ty dflags ctxt pred@(ClassP cls tys)
893 = -- Class predicates are valid in all contexts
894 checkTc (arity == n_tys) arity_err `thenM_`
896 -- Check the form of the argument types
897 mappM_ check_arg_type tys `thenM_`
898 checkTc (check_class_pred_tys dflags ctxt tys)
899 (predTyVarErr pred $$ how_to_allow)
902 class_name = className cls
903 arity = classArity cls
905 arity_err = arityErr "Class" class_name arity n_tys
906 how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
908 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
909 -- Implicit parameters only allows in type
910 -- signatures; not in instance decls, superclasses etc
911 -- The reason for not allowing implicit params in instances is a bit subtle
912 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
913 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
914 -- discharge all the potential usas of the ?x in e. For example, a
915 -- constraint Foo [Int] might come out of e,and applying the
916 -- instance decl would show up two uses of ?x.
919 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
921 -------------------------
922 check_class_pred_tys dflags ctxt tys
924 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
925 InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
926 -- Further checks on head and theta in
927 -- checkInstTermination
928 other -> gla_exts || all tyvar_head tys
930 gla_exts = dopt Opt_GlasgowExts dflags
931 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
933 -------------------------
934 tyvar_head ty -- Haskell 98 allows predicates of form
935 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
936 | otherwise -- where a is a type variable
937 = case tcSplitAppTy_maybe ty of
938 Just (ty, _) -> tyvar_head ty
945 is ambiguous if P contains generic variables
946 (i.e. one of the Vs) that are not mentioned in tau
948 However, we need to take account of functional dependencies
949 when we speak of 'mentioned in tau'. Example:
950 class C a b | a -> b where ...
952 forall x y. (C x y) => x
953 is not ambiguous because x is mentioned and x determines y
955 NB; the ambiguity check is only used for *user* types, not for types
956 coming from inteface files. The latter can legitimately have
957 ambiguous types. Example
959 class S a where s :: a -> (Int,Int)
960 instance S Char where s _ = (1,1)
961 f:: S a => [a] -> Int -> (Int,Int)
962 f (_::[a]) x = (a*x,b)
963 where (a,b) = s (undefined::a)
965 Here the worker for f gets the type
966 fw :: forall a. S a => Int -> (# Int, Int #)
968 If the list of tv_names is empty, we have a monotype, and then we
969 don't need to check for ambiguity either, because the test can't fail
973 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
974 checkAmbiguity forall_tyvars theta tau_tyvars
975 = mappM_ complain (filter is_ambig theta)
977 complain pred = addErrTc (ambigErr pred)
978 extended_tau_vars = grow theta tau_tyvars
980 -- Only a *class* predicate can give rise to ambiguity
981 -- An *implicit parameter* cannot. For example:
982 -- foo :: (?x :: [a]) => Int
984 -- is fine. The call site will suppply a particular 'x'
985 is_ambig pred = isClassPred pred &&
986 any ambig_var (varSetElems (tyVarsOfPred pred))
988 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
989 not (ct_var `elemVarSet` extended_tau_vars)
992 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
993 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
994 ptext SLIT("must be reachable from the type after the '=>'"))]
997 In addition, GHC insists that at least one type variable
998 in each constraint is in V. So we disallow a type like
999 forall a. Eq b => b -> b
1000 even in a scope where b is in scope.
1003 checkFreeness forall_tyvars theta
1004 = mappM_ complain (filter is_free theta)
1006 is_free pred = not (isIPPred pred)
1007 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1008 bound_var ct_var = ct_var `elem` forall_tyvars
1009 complain pred = addErrTc (freeErr pred)
1012 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1013 ptext SLIT("are already in scope"),
1014 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1019 checkThetaCtxt ctxt theta
1020 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1021 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1023 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1024 predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
1025 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1026 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1028 arityErr kind name n m
1029 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1030 n_arguments <> comma, text "but has been given", int m]
1032 n_arguments | n == 0 = ptext SLIT("no arguments")
1033 | n == 1 = ptext SLIT("1 argument")
1034 | True = hsep [int n, ptext SLIT("arguments")]
1038 %************************************************************************
1040 \subsection{Checking for a decent instance head type}
1042 %************************************************************************
1044 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1045 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1047 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1048 flag is on, or (2)~the instance is imported (they must have been
1049 compiled elsewhere). In these cases, we let them go through anyway.
1051 We can also have instances for functions: @instance Foo (a -> b) ...@.
1054 checkValidInstHead :: Type -> TcM (Class, [TcType])
1056 checkValidInstHead ty -- Should be a source type
1057 = case tcSplitPredTy_maybe ty of {
1058 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1061 case getClassPredTys_maybe pred of {
1062 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1065 getDOpts `thenM` \ dflags ->
1066 mappM_ check_arg_type tys `thenM_`
1067 check_inst_head dflags clas tys `thenM_`
1071 check_inst_head dflags clas tys
1072 -- If GlasgowExts then check at least one isn't a type variable
1073 | dopt Opt_GlasgowExts dflags
1074 = mapM_ check_one tys
1076 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1078 = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
1079 (instTypeErr (pprClassPred clas tys) head_shape_msg)
1082 (first_ty : _) = tys
1084 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1085 text "where T is not a synonym, and a,b,c are distinct type variables")
1087 -- For now, I only allow tau-types (not polytypes) in
1088 -- the head of an instance decl.
1089 -- E.g. instance C (forall a. a->a) is rejected
1090 -- One could imagine generalising that, but I'm not sure
1091 -- what all the consequences might be
1092 check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1093 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1095 instTypeErr pp_ty msg
1096 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1101 %************************************************************************
1103 \subsection{Checking instance for termination}
1105 %************************************************************************
1109 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1110 checkValidInstance tyvars theta clas inst_tys
1111 = do { gla_exts <- doptM Opt_GlasgowExts
1112 ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
1114 ; checkValidTheta InstThetaCtxt theta
1115 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1117 -- Check that instance inference will terminate (if we care)
1118 -- For Haskell 98, checkValidTheta has already done that
1119 ; when (gla_exts && not undecidable_ok) $
1120 checkInstTermination theta inst_tys
1122 -- The Coverage Condition
1123 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1124 (instTypeErr (pprClassPred clas inst_tys) msg)
1127 msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
1130 Termination test: each assertion in the context satisfies
1131 (1) no variable has more occurrences in the assertion than in the head, and
1132 (2) the assertion has fewer constructors and variables (taken together
1133 and counting repetitions) than the head.
1134 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1135 (which have already been checked) guarantee termination.
1137 The underlying idea is that
1139 for any ground substitution, each assertion in the
1140 context has fewer type constructors than the head.
1144 checkInstTermination :: ThetaType -> [TcType] -> TcM ()
1145 checkInstTermination theta tys
1146 = do { mappM_ (check_nomore (fvTypes tys)) theta
1147 ; mappM_ (check_smaller (sizeTypes tys)) theta }
1149 check_nomore :: [TyVar] -> PredType -> TcM ()
1150 check_nomore fvs pred
1151 = checkTc (null (fvPred pred \\ fvs))
1152 (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1154 check_smaller :: Int -> PredType -> TcM ()
1155 check_smaller n pred
1156 = checkTc (sizePred pred < n)
1157 (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1159 predUndecErr pred msg = sep [msg,
1160 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1162 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1163 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1164 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1166 -- Free variables of a type, retaining repetitions, and expanding synonyms
1167 fvType :: Type -> [TyVar]
1168 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1169 fvType (TyVarTy tv) = [tv]
1170 fvType (TyConApp _ tys) = fvTypes tys
1171 fvType (NoteTy _ ty) = fvType ty
1172 fvType (PredTy pred) = fvPred pred
1173 fvType (FunTy arg res) = fvType arg ++ fvType res
1174 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1175 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1177 fvTypes :: [Type] -> [TyVar]
1178 fvTypes tys = concat (map fvType tys)
1180 fvPred :: PredType -> [TyVar]
1181 fvPred (ClassP _ tys') = fvTypes tys'
1182 fvPred (IParam _ ty) = fvType ty
1184 -- Size of a type: the number of variables and constructors
1185 sizeType :: Type -> Int
1186 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1187 sizeType (TyVarTy _) = 1
1188 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1189 sizeType (NoteTy _ ty) = sizeType ty
1190 sizeType (PredTy pred) = sizePred pred
1191 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1192 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1193 sizeType (ForAllTy _ ty) = sizeType ty
1195 sizeTypes :: [Type] -> Int
1196 sizeTypes xs = sum (map sizeType xs)
1198 sizePred :: PredType -> Int
1199 sizePred (ClassP _ tys') = sizeTypes tys'
1200 sizePred (IParam _ ty) = sizeType ty