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 --------------------------------
26 -- Creating new coercion variables
29 --------------------------------
31 tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
32 tcInstSigTyVars, zonkSigTyVar,
33 tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
34 tcSkolSigType, tcSkolSigTyVars,
36 --------------------------------
37 -- Checking type validity
38 Rank, UserTypeCtxt(..), checkValidType,
39 SourceTyCtxt(..), checkValidTheta, checkFreeness,
40 checkValidInstHead, checkValidInstance, checkAmbiguity,
44 --------------------------------
46 zonkType, zonkTcPredType,
47 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
48 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
49 zonkTcKindToKind, zonkTcKind,
51 readKindVar, writeKindVar
55 #include "HsVersions.h"
59 import TypeRep ( Type(..), PredType(..), -- Friend; can see representation
62 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
63 TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
64 MetaDetails(..), SkolemInfo(..), BoxInfo(..),
65 BoxyTyVar, BoxyType, UserTypeCtxt(..), kindVarRef,
66 mkKindVar, isMetaTyVar, isSigTyVar, metaTvRef,
67 tcCmpPred, isClassPred, tcGetTyVar,
68 tcSplitPhiTy, tcSplitPredTy_maybe,
70 tcValidInstHeadTy, tcSplitForAllTys,
71 tcIsTyVarTy, tcSplitSigmaTy,
72 isUnLiftedType, isIPPred,
73 typeKind, isSkolemTyVar,
74 mkAppTy, mkTyVarTy, mkTyVarTys,
75 tyVarsOfPred, getClassPredTys_maybe,
76 tyVarsOfType, tyVarsOfTypes, tcView,
77 pprPred, pprTheta, pprClassPred )
78 import Type ( Kind, KindVar,
79 isLiftedTypeKind, isSubArgTypeKind, isSubOpenTypeKind,
80 liftedTypeKind, defaultKind
82 import Type ( TvSubst, zipTopTvSubst, substTy )
83 import Coercion ( mkCoKind )
84 import Class ( Class, classArity, className )
85 import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
86 tyConArity, tyConName )
87 import Var ( TyVar, tyVarKind, tyVarName, isTcTyVar,
88 mkTyVar, mkTcTyVar, tcTyVarDetails,
93 import TcType ( isFlexi, isBoxyTyVar, isImmutableTyVar )
94 import Type ( isSubKind )
98 import TcRnMonad -- TcType, amongst others
99 import FunDeps ( grow, checkInstCoverage )
100 import Name ( Name, setNameUnique, mkSysTvName )
102 import DynFlags ( dopt, DynFlag(..) )
103 import Util ( nOfThem, isSingleton, notNull )
104 import ListSetOps ( removeDups )
105 import UniqSupply ( uniqsFromSupply )
108 import Control.Monad ( when )
109 import Data.List ( (\\) )
113 %************************************************************************
115 Instantiation in general
117 %************************************************************************
120 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
121 -> TcType -- Type to instantiate
122 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
123 tcInstType inst_tyvars ty
124 = case tcSplitForAllTys ty of
125 ([], rho) -> let -- There may be overloading despite no type variables;
126 -- (?x :: Int) => Int -> Int
127 (theta, tau) = tcSplitPhiTy rho
129 return ([], theta, tau)
131 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
133 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
134 -- Either the tyvars are freshly made, by inst_tyvars,
135 -- or (in the call from tcSkolSigType) any nested foralls
136 -- have different binders. Either way, zipTopTvSubst is ok
138 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
139 ; return (tyvars', theta, tau) }
143 %************************************************************************
147 %************************************************************************
150 newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
152 = do { us <- newUniqueSupply
153 ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
155 | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
157 newKindVar :: TcM TcKind
158 newKindVar = do { uniq <- newUnique
159 ; ref <- newMutVar Flexi
160 ; return (mkTyVarTy (mkKindVar uniq ref)) }
162 newKindVars :: Int -> TcM [TcKind]
163 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
167 %************************************************************************
169 SkolemTvs (immutable)
171 %************************************************************************
174 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
175 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
177 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
178 -- Instantiate a type signature with skolem constants, but
179 -- do *not* give them fresh names, because we want the name to
180 -- be in the type environment -- it is lexically scoped.
181 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
183 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
184 -- Make skolem constants, but do *not* give them new names, as above
185 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
188 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
189 -- Instantiate a type with fresh skolem constants
190 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
192 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
193 tcInstSkolTyVar info tyvar
194 = do { uniq <- newUnique
195 ; let name = setNameUnique (tyVarName tyvar) uniq
196 kind = tyVarKind tyvar
197 ; return (mkSkolTyVar name kind info) }
199 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
200 tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
204 %************************************************************************
206 MetaTvs (meta type variables; mutable)
208 %************************************************************************
211 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
212 -- Make a new meta tyvar out of thin air
213 newMetaTyVar box_info kind
214 = do { uniq <- newUnique
215 ; ref <- newMutVar Flexi ;
216 ; let name = mkSysTvName uniq fs
217 fs = case box_info of
220 SigTv _ -> FSLIT("a")
221 -- We give BoxTv and TauTv the same string, because
222 -- otherwise we get user-visible differences in error
223 -- messages, which are confusing. If you want to see
224 -- the box_info of each tyvar, use -dppr-debug
225 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
227 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
228 -- Make a new meta tyvar whose Name and Kind
229 -- come from an existing TyVar
230 instMetaTyVar box_info tyvar
231 = do { uniq <- newUnique
232 ; ref <- newMutVar Flexi ;
233 ; let name = setNameUnique (tyVarName tyvar) uniq
234 kind = tyVarKind tyvar
235 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
237 readMetaTyVar :: TyVar -> TcM MetaDetails
238 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
239 readMutVar (metaTvRef tyvar)
241 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
243 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
245 writeMetaTyVar tyvar ty
246 | not (isMetaTyVar tyvar)
247 = pprTrace "writeMetaTyVar" (ppr tyvar) $
251 = ASSERT( isMetaTyVar tyvar )
252 ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
253 do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
254 ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
262 %************************************************************************
266 %************************************************************************
269 newFlexiTyVar :: Kind -> TcM TcTyVar
270 newFlexiTyVar kind = newMetaTyVar TauTv kind
272 newFlexiTyVarTy :: Kind -> TcM TcType
274 = newFlexiTyVar kind `thenM` \ tc_tyvar ->
275 returnM (TyVarTy tc_tyvar)
277 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
278 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
280 tcInstTyVar :: TyVar -> TcM TcTyVar
281 -- Instantiate with a META type variable
282 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
284 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
285 -- Instantiate with META type variables
287 = do { tc_tvs <- mapM tcInstTyVar tyvars
288 ; let tys = mkTyVarTys tc_tvs
289 ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
290 -- Since the tyvars are freshly made,
291 -- they cannot possibly be captured by
292 -- any existing for-alls. Hence zipTopTvSubst
296 %************************************************************************
300 %************************************************************************
303 tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
304 -- Instantiate with meta SigTvs
305 tcInstSigTyVars skol_info tyvars
306 = mapM (instMetaTyVar (SigTv skol_info)) tyvars
308 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
310 | isSkolemTyVar sig_tv
311 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
313 = ASSERT( isSigTyVar sig_tv )
314 do { ty <- zonkTcTyVar sig_tv
315 ; return (tcGetTyVar "zonkSigTyVar" ty) }
316 -- 'ty' is bound to be a type variable, because SigTvs
317 -- can only be unified with type variables
321 %************************************************************************
325 %************************************************************************
328 newBoxyTyVar :: Kind -> TcM BoxyTyVar
329 newBoxyTyVar kind = newMetaTyVar BoxTv kind
331 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
332 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
334 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
335 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
337 readFilledBox :: BoxyTyVar -> TcM TcType
338 -- Read the contents of the box, which should be filled in by now
339 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
340 do { cts <- readMetaTyVar box_tv
342 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
343 Indirect ty -> return ty }
345 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
346 -- Instantiate with a BOXY type variable
347 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
351 %************************************************************************
353 \subsection{Putting and getting mutable type variables}
355 %************************************************************************
357 But it's more fun to short out indirections on the way: If this
358 version returns a TyVar, then that TyVar is unbound. If it returns
359 any other type, then there might be bound TyVars embedded inside it.
361 We return Nothing iff the original box was unbound.
364 data LookupTyVarResult -- The result of a lookupTcTyVar call
365 = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
368 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
371 SkolemTv _ -> return (DoneTv details)
372 MetaTv _ ref -> do { meta_details <- readMutVar ref
373 ; case meta_details of
374 Indirect ty -> return (IndirectTv ty)
375 Flexi -> return (DoneTv details) }
377 details = tcTyVarDetails tyvar
380 -- gaw 2004 We aren't shorting anything out anymore, at least for now
382 | not (isTcTyVar tyvar)
383 = pprTrace "getTcTyVar" (ppr tyvar) $
384 returnM (Just (mkTyVarTy tyvar))
387 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
388 readMetaTyVar tyvar `thenM` \ maybe_ty ->
390 Just ty -> short_out ty `thenM` \ ty' ->
391 writeMetaTyVar tyvar (Just ty') `thenM_`
394 Nothing -> returnM Nothing
396 short_out :: TcType -> TcM TcType
397 short_out ty@(TyVarTy tyvar)
398 | not (isTcTyVar tyvar)
402 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
404 Just ty' -> short_out ty' `thenM` \ ty' ->
405 writeMetaTyVar tyvar (Just ty') `thenM_`
410 short_out other_ty = returnM other_ty
415 %************************************************************************
417 \subsection{Zonking -- the exernal interfaces}
419 %************************************************************************
421 ----------------- Type variables
424 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
425 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
427 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
428 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
429 returnM (tyVarsOfTypes tys)
431 zonkTcTyVar :: TcTyVar -> TcM TcType
432 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
433 zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
436 ----------------- Types
439 zonkTcType :: TcType -> TcM TcType
440 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
442 zonkTcTypes :: [TcType] -> TcM [TcType]
443 zonkTcTypes tys = mappM zonkTcType tys
445 zonkTcClassConstraints cts = mappM zonk cts
446 where zonk (clas, tys)
447 = zonkTcTypes tys `thenM` \ new_tys ->
448 returnM (clas, new_tys)
450 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
451 zonkTcThetaType theta = mappM zonkTcPredType theta
453 zonkTcPredType :: TcPredType -> TcM TcPredType
454 zonkTcPredType (ClassP c ts)
455 = zonkTcTypes ts `thenM` \ new_ts ->
456 returnM (ClassP c new_ts)
457 zonkTcPredType (IParam n t)
458 = zonkTcType t `thenM` \ new_t ->
459 returnM (IParam n new_t)
460 zonkTcPredType (EqPred t1 t2)
461 = zonkTcType t1 `thenM` \ new_t1 ->
462 zonkTcType t2 `thenM` \ new_t2 ->
463 returnM (EqPred new_t1 new_t2)
466 ------------------- These ...ToType, ...ToKind versions
467 are used at the end of type checking
470 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
471 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
472 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
473 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
474 -- The meta tyvar is updated to point to the new regular TyVar. Now any
475 -- bound occurences of the original type variable will get zonked to
476 -- the immutable version.
478 -- We leave skolem TyVars alone; they are immutable.
479 zonkQuantifiedTyVar tv
480 | isSkolemTyVar tv = return tv
481 -- It might be a skolem type variable,
482 -- for example from a user type signature
484 | otherwise -- It's a meta-type-variable
485 = do { details <- readMetaTyVar tv
487 -- Create the new, frozen, regular type variable
488 ; let final_kind = defaultKind (tyVarKind tv)
489 final_tv = mkTyVar (tyVarName tv) final_kind
491 -- Bind the meta tyvar to the new tyvar
493 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
495 -- [Sept 04] I don't think this should happen
496 -- See note [Silly Type Synonym]
498 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
500 -- Return the new tyvar
504 [Silly Type Synonyms]
507 type C u a = u -- Note 'a' unused
509 foo :: (forall a. C u a -> C u a) -> u
513 bar = foo (\t -> t + t)
515 * From the (\t -> t+t) we get type {Num d} => d -> d
518 * Now unify with type of foo's arg, and we get:
519 {Num (C d a)} => C d a -> C d a
522 * Now abstract over the 'a', but float out the Num (C d a) constraint
523 because it does not 'really' mention a. (see exactTyVarsOfType)
524 The arg to foo becomes
527 * So we get a dict binding for Num (C d a), which is zonked to give
529 [Note Sept 04: now that we are zonking quantified type variables
530 on construction, the 'a' will be frozen as a regular tyvar on
531 quantification, so the floated dict will still have type (C d a).
532 Which renders this whole note moot; happily!]
534 * Then the /\a abstraction has a zonked 'a' in it.
536 All very silly. I think its harmless to ignore the problem. We'll end up with
537 a /\a in the final result but all the occurrences of a will be zonked to ()
540 %************************************************************************
542 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
544 %* For internal use only! *
546 %************************************************************************
549 -- For unbound, mutable tyvars, zonkType uses the function given to it
550 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
551 -- type variable and zonks the kind too
553 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
554 -- see zonkTcType, and zonkTcTypeToType
557 zonkType unbound_var_fn ty
560 go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
562 go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
563 returnM (TyConApp tc tys')
565 go (PredTy p) = go_pred p `thenM` \ p' ->
568 go (FunTy arg res) = go arg `thenM` \ arg' ->
569 go res `thenM` \ res' ->
570 returnM (FunTy arg' res')
572 go (AppTy fun arg) = go fun `thenM` \ fun' ->
573 go arg `thenM` \ arg' ->
574 returnM (mkAppTy fun' arg')
575 -- NB the mkAppTy; we might have instantiated a
576 -- type variable to a type constructor, so we need
577 -- to pull the TyConApp to the top.
579 -- The two interesting cases!
580 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
581 | otherwise = return (TyVarTy tyvar)
582 -- Ordinary (non Tc) tyvars occur inside quantified types
584 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
585 go ty `thenM` \ ty' ->
586 returnM (ForAllTy tyvar ty')
588 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
589 returnM (ClassP c tys')
590 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
591 returnM (IParam n ty')
592 go_pred (EqPred ty1 ty2) = go ty1 `thenM` \ ty1' ->
593 go ty2 `thenM` \ ty2' ->
594 returnM (EqPred ty1' ty2')
596 zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
597 -> TcTyVar -> TcM TcType
598 zonk_tc_tyvar unbound_var_fn tyvar
599 | not (isMetaTyVar tyvar) -- Skolems
600 = returnM (TyVarTy tyvar)
602 | otherwise -- Mutables
603 = do { cts <- readMetaTyVar tyvar
605 Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
606 Indirect ty -> zonkType unbound_var_fn ty }
611 %************************************************************************
615 %************************************************************************
618 readKindVar :: KindVar -> TcM (MetaDetails)
619 writeKindVar :: KindVar -> TcKind -> TcM ()
620 readKindVar kv = readMutVar (kindVarRef kv)
621 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
624 zonkTcKind :: TcKind -> TcM TcKind
625 zonkTcKind k = zonkTcType k
628 zonkTcKindToKind :: TcKind -> TcM Kind
629 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
630 -- Haskell specifies that * is to be used, so we follow that.
631 zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
634 %************************************************************************
636 \subsection{Checking a user type}
638 %************************************************************************
640 When dealing with a user-written type, we first translate it from an HsType
641 to a Type, performing kind checking, and then check various things that should
642 be true about it. We don't want to perform these checks at the same time
643 as the initial translation because (a) they are unnecessary for interface-file
644 types and (b) when checking a mutually recursive group of type and class decls,
645 we can't "look" at the tycons/classes yet. Also, the checks are are rather
646 diverse, and used to really mess up the other code.
648 One thing we check for is 'rank'.
650 Rank 0: monotypes (no foralls)
651 Rank 1: foralls at the front only, Rank 0 inside
652 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
654 basic ::= tyvar | T basic ... basic
656 r2 ::= forall tvs. cxt => r2a
657 r2a ::= r1 -> r2a | basic
658 r1 ::= forall tvs. cxt => r0
659 r0 ::= r0 -> r0 | basic
661 Another thing is to check that type synonyms are saturated.
662 This might not necessarily show up in kind checking.
664 data T k = MkT (k Int)
669 checkValidType :: UserTypeCtxt -> Type -> TcM ()
670 -- Checks that the type is valid for the given context
671 checkValidType ctxt ty
672 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
673 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
675 rank | gla_exts = Arbitrary
677 = case ctxt of -- Haskell 98
679 LamPatSigCtxt -> Rank 0
680 BindPatSigCtxt -> Rank 0
681 DefaultDeclCtxt-> Rank 0
683 TySynCtxt _ -> Rank 0
684 ExprSigCtxt -> Rank 1
685 FunSigCtxt _ -> Rank 1
686 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
687 -- constructor, hence rank 1
688 ForSigCtxt _ -> Rank 1
689 RuleSigCtxt _ -> Rank 1
690 SpecInstCtxt -> Rank 1
692 actual_kind = typeKind ty
694 kind_ok = case ctxt of
695 TySynCtxt _ -> True -- Any kind will do
696 ResSigCtxt -> isSubOpenTypeKind actual_kind
697 ExprSigCtxt -> isSubOpenTypeKind actual_kind
698 GenPatCtxt -> isLiftedTypeKind actual_kind
699 ForSigCtxt _ -> isLiftedTypeKind actual_kind
700 other -> isSubArgTypeKind actual_kind
702 ubx_tup | not gla_exts = UT_NotOk
703 | otherwise = case ctxt of
707 -- Unboxed tuples ok in function results,
708 -- but for type synonyms we allow them even at
711 -- Check that the thing has kind Type, and is lifted if necessary
712 checkTc kind_ok (kindErr actual_kind) `thenM_`
714 -- Check the internal validity of the type itself
715 check_poly_type rank ubx_tup ty `thenM_`
717 traceTc (text "checkValidType done" <+> ppr ty)
722 data Rank = Rank Int | Arbitrary
724 decRank :: Rank -> Rank
725 decRank Arbitrary = Arbitrary
726 decRank (Rank n) = Rank (n-1)
728 ----------------------------------------
729 data UbxTupFlag = UT_Ok | UT_NotOk
730 -- The "Ok" version means "ok if -fglasgow-exts is on"
732 ----------------------------------------
733 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
734 check_poly_type (Rank 0) ubx_tup ty
735 = check_tau_type (Rank 0) ubx_tup ty
737 check_poly_type rank ubx_tup ty
738 | null tvs && null theta
739 = check_tau_type rank ubx_tup ty
741 = do { check_valid_theta SigmaCtxt theta
742 ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow
743 ; checkFreeness tvs theta
744 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
746 (tvs, theta, tau) = tcSplitSigmaTy ty
748 ----------------------------------------
749 check_arg_type :: Type -> TcM ()
750 -- The sort of type that can instantiate a type variable,
751 -- or be the argument of a type constructor.
752 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
753 -- Other unboxed types are very occasionally allowed as type
754 -- arguments depending on the kind of the type constructor
756 -- For example, we want to reject things like:
758 -- instance Ord a => Ord (forall s. T s a)
760 -- g :: T s (forall b.b)
762 -- NB: unboxed tuples can have polymorphic or unboxed args.
763 -- This happens in the workers for functions returning
764 -- product types with polymorphic components.
765 -- But not in user code.
766 -- Anyway, they are dealt with by a special case in check_tau_type
769 = check_poly_type Arbitrary UT_NotOk ty `thenM_`
770 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
772 ----------------------------------------
773 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
774 -- Rank is allowed rank for function args
775 -- No foralls otherwise
777 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
778 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
779 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
781 -- Naked PredTys don't usually show up, but they can as a result of
782 -- {-# SPECIALISE instance Ord Char #-}
783 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
784 -- are handled, but the quick thing is just to permit PredTys here.
785 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
786 check_pred_ty dflags TypeCtxt sty
788 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
789 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
790 = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_`
791 check_poly_type rank UT_Ok res_ty
793 check_tau_type rank ubx_tup (AppTy ty1 ty2)
794 = check_arg_type ty1 `thenM_` check_arg_type ty2
796 check_tau_type rank ubx_tup (NoteTy other_note ty)
797 = check_tau_type rank ubx_tup ty
799 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
801 = do { -- It's OK to have an *over-applied* type synonym
802 -- data Tree a b = ...
803 -- type Foo a = Tree [a]
804 -- f :: Foo a b -> ...
806 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
807 Nothing -> failWithTc arity_msg
809 ; gla_exts <- doptM Opt_GlasgowExts
811 -- If -fglasgow-exts then don't check the type arguments
812 -- This allows us to instantiate a synonym defn with a
813 -- for-all type, or with a partially-applied type synonym.
814 -- e.g. type T a b = a
817 -- Here, T is partially applied, so it's illegal in H98.
818 -- But if you expand S first, then T we get just
823 -- For H98, do check the type args
824 mappM_ check_arg_type tys
827 | isUnboxedTupleTyCon tc
828 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
829 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
830 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
831 -- Args are allowed to be unlifted, or
832 -- more unboxed tuples, so can't use check_arg_ty
835 = mappM_ check_arg_type tys
838 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
841 tc_arity = tyConArity tc
843 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
844 ubx_tup_msg = ubxArgTyErr ty
846 ----------------------------------------
847 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
848 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
849 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
850 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
855 %************************************************************************
857 \subsection{Checking a theta or source type}
859 %************************************************************************
862 -- Enumerate the contexts in which a "source type", <S>, can occur
866 -- or (N a) where N is a newtype
869 = ClassSCCtxt Name -- Superclasses of clas
870 -- class <S> => C a where ...
871 | SigmaCtxt -- Theta part of a normal for-all type
872 -- f :: <S> => a -> a
873 | DataTyCtxt Name -- Theta part of a data decl
874 -- data <S> => T a = MkT a
875 | TypeCtxt -- Source type in an ordinary type
877 | InstThetaCtxt -- Context of an instance decl
878 -- instance <S> => C [a] where ...
880 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
881 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
882 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
883 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
884 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
888 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
889 checkValidTheta ctxt theta
890 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
892 -------------------------
893 check_valid_theta ctxt []
895 check_valid_theta ctxt theta
896 = getDOpts `thenM` \ dflags ->
897 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
898 mappM_ (check_pred_ty dflags ctxt) theta
900 (_,dups) = removeDups tcCmpPred theta
902 -------------------------
903 check_pred_ty dflags ctxt pred@(ClassP cls tys)
904 = -- Class predicates are valid in all contexts
905 checkTc (arity == n_tys) arity_err `thenM_`
907 -- Check the form of the argument types
908 mappM_ check_arg_type tys `thenM_`
909 checkTc (check_class_pred_tys dflags ctxt tys)
910 (predTyVarErr pred $$ how_to_allow)
913 class_name = className cls
914 arity = classArity cls
916 arity_err = arityErr "Class" class_name arity n_tys
917 how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
919 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
920 -- Implicit parameters only allows in type
921 -- signatures; not in instance decls, superclasses etc
922 -- The reason for not allowing implicit params in instances is a bit subtle
923 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
924 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
925 -- discharge all the potential usas of the ?x in e. For example, a
926 -- constraint Foo [Int] might come out of e,and applying the
927 -- instance decl would show up two uses of ?x.
930 check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
932 -------------------------
933 check_class_pred_tys dflags ctxt tys
935 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
936 InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
937 -- Further checks on head and theta in
938 -- checkInstTermination
939 other -> gla_exts || all tyvar_head tys
941 gla_exts = dopt Opt_GlasgowExts dflags
942 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
944 -------------------------
945 tyvar_head ty -- Haskell 98 allows predicates of form
946 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
947 | otherwise -- where a is a type variable
948 = case tcSplitAppTy_maybe ty of
949 Just (ty, _) -> tyvar_head ty
956 is ambiguous if P contains generic variables
957 (i.e. one of the Vs) that are not mentioned in tau
959 However, we need to take account of functional dependencies
960 when we speak of 'mentioned in tau'. Example:
961 class C a b | a -> b where ...
963 forall x y. (C x y) => x
964 is not ambiguous because x is mentioned and x determines y
966 NB; the ambiguity check is only used for *user* types, not for types
967 coming from inteface files. The latter can legitimately have
968 ambiguous types. Example
970 class S a where s :: a -> (Int,Int)
971 instance S Char where s _ = (1,1)
972 f:: S a => [a] -> Int -> (Int,Int)
973 f (_::[a]) x = (a*x,b)
974 where (a,b) = s (undefined::a)
976 Here the worker for f gets the type
977 fw :: forall a. S a => Int -> (# Int, Int #)
979 If the list of tv_names is empty, we have a monotype, and then we
980 don't need to check for ambiguity either, because the test can't fail
984 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
985 checkAmbiguity forall_tyvars theta tau_tyvars
986 = mappM_ complain (filter is_ambig theta)
988 complain pred = addErrTc (ambigErr pred)
989 extended_tau_vars = grow theta tau_tyvars
991 -- Only a *class* predicate can give rise to ambiguity
992 -- An *implicit parameter* cannot. For example:
993 -- foo :: (?x :: [a]) => Int
995 -- is fine. The call site will suppply a particular 'x'
996 is_ambig pred = isClassPred pred &&
997 any ambig_var (varSetElems (tyVarsOfPred pred))
999 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1000 not (ct_var `elemVarSet` extended_tau_vars)
1003 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1004 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1005 ptext SLIT("must be reachable from the type after the '=>'"))]
1008 In addition, GHC insists that at least one type variable
1009 in each constraint is in V. So we disallow a type like
1010 forall a. Eq b => b -> b
1011 even in a scope where b is in scope.
1014 checkFreeness forall_tyvars theta
1015 = mappM_ complain (filter is_free theta)
1017 is_free pred = not (isIPPred pred)
1018 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1019 bound_var ct_var = ct_var `elem` forall_tyvars
1020 complain pred = addErrTc (freeErr pred)
1023 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1024 ptext SLIT("are already in scope"),
1025 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1030 checkThetaCtxt ctxt theta
1031 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1032 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1034 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1035 predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
1036 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1037 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1039 arityErr kind name n m
1040 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1041 n_arguments <> comma, text "but has been given", int m]
1043 n_arguments | n == 0 = ptext SLIT("no arguments")
1044 | n == 1 = ptext SLIT("1 argument")
1045 | True = hsep [int n, ptext SLIT("arguments")]
1049 %************************************************************************
1051 \subsection{Checking for a decent instance head type}
1053 %************************************************************************
1055 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1056 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1058 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1059 flag is on, or (2)~the instance is imported (they must have been
1060 compiled elsewhere). In these cases, we let them go through anyway.
1062 We can also have instances for functions: @instance Foo (a -> b) ...@.
1065 checkValidInstHead :: Type -> TcM (Class, [TcType])
1067 checkValidInstHead ty -- Should be a source type
1068 = case tcSplitPredTy_maybe ty of {
1069 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1072 case getClassPredTys_maybe pred of {
1073 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1076 getDOpts `thenM` \ dflags ->
1077 mappM_ check_arg_type tys `thenM_`
1078 check_inst_head dflags clas tys `thenM_`
1082 check_inst_head dflags clas tys
1083 -- If GlasgowExts then check at least one isn't a type variable
1084 | dopt Opt_GlasgowExts dflags
1085 = mapM_ check_one tys
1087 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1089 = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
1090 (instTypeErr (pprClassPred clas tys) head_shape_msg)
1093 (first_ty : _) = tys
1095 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1096 text "where T is not a synonym, and a,b,c are distinct type variables")
1098 -- For now, I only allow tau-types (not polytypes) in
1099 -- the head of an instance decl.
1100 -- E.g. instance C (forall a. a->a) is rejected
1101 -- One could imagine generalising that, but I'm not sure
1102 -- what all the consequences might be
1103 check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1104 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1106 instTypeErr pp_ty msg
1107 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1112 %************************************************************************
1114 \subsection{Checking instance for termination}
1116 %************************************************************************
1120 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1121 checkValidInstance tyvars theta clas inst_tys
1122 = do { gla_exts <- doptM Opt_GlasgowExts
1123 ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
1125 ; checkValidTheta InstThetaCtxt theta
1126 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1128 -- Check that instance inference will terminate (if we care)
1129 -- For Haskell 98, checkValidTheta has already done that
1130 ; when (gla_exts && not undecidable_ok) $
1131 checkInstTermination theta inst_tys
1133 -- The Coverage Condition
1134 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1135 (instTypeErr (pprClassPred clas inst_tys) msg)
1138 msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
1141 Termination test: each assertion in the context satisfies
1142 (1) no variable has more occurrences in the assertion than in the head, and
1143 (2) the assertion has fewer constructors and variables (taken together
1144 and counting repetitions) than the head.
1145 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1146 (which have already been checked) guarantee termination.
1148 The underlying idea is that
1150 for any ground substitution, each assertion in the
1151 context has fewer type constructors than the head.
1155 checkInstTermination :: ThetaType -> [TcType] -> TcM ()
1156 checkInstTermination theta tys
1157 = do { mappM_ (check_nomore (fvTypes tys)) theta
1158 ; mappM_ (check_smaller (sizeTypes tys)) theta }
1160 check_nomore :: [TyVar] -> PredType -> TcM ()
1161 check_nomore fvs pred
1162 = checkTc (null (fvPred pred \\ fvs))
1163 (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1165 check_smaller :: Int -> PredType -> TcM ()
1166 check_smaller n pred
1167 = checkTc (sizePred pred < n)
1168 (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1170 predUndecErr pred msg = sep [msg,
1171 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1173 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1174 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1175 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1177 -- Free variables of a type, retaining repetitions, and expanding synonyms
1178 fvType :: Type -> [TyVar]
1179 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1180 fvType (TyVarTy tv) = [tv]
1181 fvType (TyConApp _ tys) = fvTypes tys
1182 fvType (NoteTy _ ty) = fvType ty
1183 fvType (PredTy pred) = fvPred pred
1184 fvType (FunTy arg res) = fvType arg ++ fvType res
1185 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1186 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1188 fvTypes :: [Type] -> [TyVar]
1189 fvTypes tys = concat (map fvType tys)
1191 fvPred :: PredType -> [TyVar]
1192 fvPred (ClassP _ tys') = fvTypes tys'
1193 fvPred (IParam _ ty) = fvType ty
1194 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1196 -- Size of a type: the number of variables and constructors
1197 sizeType :: Type -> Int
1198 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1199 sizeType (TyVarTy _) = 1
1200 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1201 sizeType (NoteTy _ ty) = sizeType ty
1202 sizeType (PredTy pred) = sizePred pred
1203 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1204 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1205 sizeType (ForAllTy _ ty) = sizeType ty
1207 sizeTypes :: [Type] -> Int
1208 sizeTypes xs = sum (map sizeType xs)
1210 sizePred :: PredType -> Int
1211 sizePred (ClassP _ tys') = sizeTypes tys'
1212 sizePred (IParam _ ty) = sizeType ty
1213 sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2