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 ( (\\) )
114 %************************************************************************
116 Instantiation in general
118 %************************************************************************
121 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
122 -> TcType -- Type to instantiate
123 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
124 tcInstType inst_tyvars ty
125 = case tcSplitForAllTys ty of
126 ([], rho) -> let -- There may be overloading despite no type variables;
127 -- (?x :: Int) => Int -> Int
128 (theta, tau) = tcSplitPhiTy rho
130 return ([], theta, tau)
132 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
134 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
135 -- Either the tyvars are freshly made, by inst_tyvars,
136 -- or (in the call from tcSkolSigType) any nested foralls
137 -- have different binders. Either way, zipTopTvSubst is ok
139 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
140 ; return (tyvars', theta, tau) }
144 %************************************************************************
148 %************************************************************************
151 newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
153 = do { us <- newUniqueSupply
154 ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
156 | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
158 newKindVar :: TcM TcKind
159 newKindVar = do { uniq <- newUnique
160 ; ref <- newMutVar Flexi
161 ; return (mkTyVarTy (mkKindVar uniq ref)) }
163 newKindVars :: Int -> TcM [TcKind]
164 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
168 %************************************************************************
170 SkolemTvs (immutable)
172 %************************************************************************
175 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
176 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
178 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
179 -- Instantiate a type signature with skolem constants, but
180 -- do *not* give them fresh names, because we want the name to
181 -- be in the type environment -- it is lexically scoped.
182 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
184 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
185 -- Make skolem constants, but do *not* give them new names, as above
186 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
189 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
190 -- Instantiate a type with fresh skolem constants
191 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
193 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
194 tcInstSkolTyVar info tyvar
195 = do { uniq <- newUnique
196 ; let name = setNameUnique (tyVarName tyvar) uniq
197 kind = tyVarKind tyvar
198 ; return (mkSkolTyVar name kind info) }
200 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
201 tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
205 %************************************************************************
207 MetaTvs (meta type variables; mutable)
209 %************************************************************************
212 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
213 -- Make a new meta tyvar out of thin air
214 newMetaTyVar box_info kind
215 = do { uniq <- newUnique
216 ; ref <- newMutVar Flexi ;
217 ; let name = mkSysTvName uniq fs
218 fs = case box_info of
221 SigTv _ -> FSLIT("a")
222 -- We give BoxTv and TauTv the same string, because
223 -- otherwise we get user-visible differences in error
224 -- messages, which are confusing. If you want to see
225 -- the box_info of each tyvar, use -dppr-debug
226 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
228 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
229 -- Make a new meta tyvar whose Name and Kind
230 -- come from an existing TyVar
231 instMetaTyVar box_info tyvar
232 = do { uniq <- newUnique
233 ; ref <- newMutVar Flexi ;
234 ; let name = setNameUnique (tyVarName tyvar) uniq
235 kind = tyVarKind tyvar
236 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
238 readMetaTyVar :: TyVar -> TcM MetaDetails
239 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
240 readMutVar (metaTvRef tyvar)
242 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
244 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
246 writeMetaTyVar tyvar ty
247 | not (isMetaTyVar tyvar)
248 = pprTrace "writeMetaTyVar" (ppr tyvar) $
252 = ASSERT( isMetaTyVar tyvar )
253 ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
254 do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
255 ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
263 %************************************************************************
267 %************************************************************************
270 newFlexiTyVar :: Kind -> TcM TcTyVar
271 newFlexiTyVar kind = newMetaTyVar TauTv kind
273 newFlexiTyVarTy :: Kind -> TcM TcType
275 = newFlexiTyVar kind `thenM` \ tc_tyvar ->
276 returnM (TyVarTy tc_tyvar)
278 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
279 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
281 tcInstTyVar :: TyVar -> TcM TcTyVar
282 -- Instantiate with a META type variable
283 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
285 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
286 -- Instantiate with META type variables
288 = do { tc_tvs <- mapM tcInstTyVar tyvars
289 ; let tys = mkTyVarTys tc_tvs
290 ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
291 -- Since the tyvars are freshly made,
292 -- they cannot possibly be captured by
293 -- any existing for-alls. Hence zipTopTvSubst
297 %************************************************************************
301 %************************************************************************
304 tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
305 -- Instantiate with meta SigTvs
306 tcInstSigTyVars skol_info tyvars
307 = mapM (instMetaTyVar (SigTv skol_info)) tyvars
309 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
311 | isSkolemTyVar sig_tv
312 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
314 = ASSERT( isSigTyVar sig_tv )
315 do { ty <- zonkTcTyVar sig_tv
316 ; return (tcGetTyVar "zonkSigTyVar" ty) }
317 -- 'ty' is bound to be a type variable, because SigTvs
318 -- can only be unified with type variables
322 %************************************************************************
326 %************************************************************************
329 newBoxyTyVar :: Kind -> TcM BoxyTyVar
330 newBoxyTyVar kind = newMetaTyVar BoxTv kind
332 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
333 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
335 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
336 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
338 readFilledBox :: BoxyTyVar -> TcM TcType
339 -- Read the contents of the box, which should be filled in by now
340 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
341 do { cts <- readMetaTyVar box_tv
343 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
344 Indirect ty -> return ty }
346 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
347 -- Instantiate with a BOXY type variable
348 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
352 %************************************************************************
354 \subsection{Putting and getting mutable type variables}
356 %************************************************************************
358 But it's more fun to short out indirections on the way: If this
359 version returns a TyVar, then that TyVar is unbound. If it returns
360 any other type, then there might be bound TyVars embedded inside it.
362 We return Nothing iff the original box was unbound.
365 data LookupTyVarResult -- The result of a lookupTcTyVar call
366 = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
369 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
371 = ASSERT( isTcTyVar tyvar )
373 SkolemTv _ -> return (DoneTv details)
374 MetaTv _ ref -> do { meta_details <- readMutVar ref
375 ; case meta_details of
376 Indirect ty -> return (IndirectTv ty)
377 Flexi -> return (DoneTv details) }
379 details = tcTyVarDetails tyvar
382 -- gaw 2004 We aren't shorting anything out anymore, at least for now
384 | not (isTcTyVar tyvar)
385 = pprTrace "getTcTyVar" (ppr tyvar) $
386 returnM (Just (mkTyVarTy tyvar))
389 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
390 readMetaTyVar tyvar `thenM` \ maybe_ty ->
392 Just ty -> short_out ty `thenM` \ ty' ->
393 writeMetaTyVar tyvar (Just ty') `thenM_`
396 Nothing -> returnM Nothing
398 short_out :: TcType -> TcM TcType
399 short_out ty@(TyVarTy tyvar)
400 | not (isTcTyVar tyvar)
404 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
406 Just ty' -> short_out ty' `thenM` \ ty' ->
407 writeMetaTyVar tyvar (Just ty') `thenM_`
412 short_out other_ty = returnM other_ty
417 %************************************************************************
419 \subsection{Zonking -- the exernal interfaces}
421 %************************************************************************
423 ----------------- Type variables
426 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
427 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
429 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
430 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
431 returnM (tyVarsOfTypes tys)
433 zonkTcTyVar :: TcTyVar -> TcM TcType
434 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
435 zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
438 ----------------- Types
441 zonkTcType :: TcType -> TcM TcType
442 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
444 zonkTcTypes :: [TcType] -> TcM [TcType]
445 zonkTcTypes tys = mappM zonkTcType tys
447 zonkTcClassConstraints cts = mappM zonk cts
448 where zonk (clas, tys)
449 = zonkTcTypes tys `thenM` \ new_tys ->
450 returnM (clas, new_tys)
452 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
453 zonkTcThetaType theta = mappM zonkTcPredType theta
455 zonkTcPredType :: TcPredType -> TcM TcPredType
456 zonkTcPredType (ClassP c ts)
457 = zonkTcTypes ts `thenM` \ new_ts ->
458 returnM (ClassP c new_ts)
459 zonkTcPredType (IParam n t)
460 = zonkTcType t `thenM` \ new_t ->
461 returnM (IParam n new_t)
462 zonkTcPredType (EqPred t1 t2)
463 = zonkTcType t1 `thenM` \ new_t1 ->
464 zonkTcType t2 `thenM` \ new_t2 ->
465 returnM (EqPred new_t1 new_t2)
468 ------------------- These ...ToType, ...ToKind versions
469 are used at the end of type checking
472 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
473 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
474 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
475 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
476 -- The meta tyvar is updated to point to the new regular TyVar. Now any
477 -- bound occurences of the original type variable will get zonked to
478 -- the immutable version.
480 -- We leave skolem TyVars alone; they are immutable.
481 zonkQuantifiedTyVar tv
482 | isSkolemTyVar tv = return tv
483 -- It might be a skolem type variable,
484 -- for example from a user type signature
486 | otherwise -- It's a meta-type-variable
487 = do { details <- readMetaTyVar tv
489 -- Create the new, frozen, regular type variable
490 ; let final_kind = defaultKind (tyVarKind tv)
491 final_tv = mkTyVar (tyVarName tv) final_kind
493 -- Bind the meta tyvar to the new tyvar
495 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
497 -- [Sept 04] I don't think this should happen
498 -- See note [Silly Type Synonym]
500 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
502 -- Return the new tyvar
506 [Silly Type Synonyms]
509 type C u a = u -- Note 'a' unused
511 foo :: (forall a. C u a -> C u a) -> u
515 bar = foo (\t -> t + t)
517 * From the (\t -> t+t) we get type {Num d} => d -> d
520 * Now unify with type of foo's arg, and we get:
521 {Num (C d a)} => C d a -> C d a
524 * Now abstract over the 'a', but float out the Num (C d a) constraint
525 because it does not 'really' mention a. (see exactTyVarsOfType)
526 The arg to foo becomes
529 * So we get a dict binding for Num (C d a), which is zonked to give
531 [Note Sept 04: now that we are zonking quantified type variables
532 on construction, the 'a' will be frozen as a regular tyvar on
533 quantification, so the floated dict will still have type (C d a).
534 Which renders this whole note moot; happily!]
536 * Then the /\a abstraction has a zonked 'a' in it.
538 All very silly. I think its harmless to ignore the problem. We'll end up with
539 a /\a in the final result but all the occurrences of a will be zonked to ()
542 %************************************************************************
544 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
546 %* For internal use only! *
548 %************************************************************************
551 -- For unbound, mutable tyvars, zonkType uses the function given to it
552 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
553 -- type variable and zonks the kind too
555 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
556 -- see zonkTcType, and zonkTcTypeToType
559 zonkType unbound_var_fn ty
562 go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
564 go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
565 returnM (TyConApp tc tys')
567 go (PredTy p) = go_pred p `thenM` \ p' ->
570 go (FunTy arg res) = go arg `thenM` \ arg' ->
571 go res `thenM` \ res' ->
572 returnM (FunTy arg' res')
574 go (AppTy fun arg) = go fun `thenM` \ fun' ->
575 go arg `thenM` \ arg' ->
576 returnM (mkAppTy fun' arg')
577 -- NB the mkAppTy; we might have instantiated a
578 -- type variable to a type constructor, so we need
579 -- to pull the TyConApp to the top.
581 -- The two interesting cases!
582 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
583 | otherwise = return (TyVarTy tyvar)
584 -- Ordinary (non Tc) tyvars occur inside quantified types
586 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
587 go ty `thenM` \ ty' ->
588 returnM (ForAllTy tyvar ty')
590 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
591 returnM (ClassP c tys')
592 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
593 returnM (IParam n ty')
594 go_pred (EqPred ty1 ty2) = go ty1 `thenM` \ ty1' ->
595 go ty2 `thenM` \ ty2' ->
596 returnM (EqPred ty1' ty2')
598 zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
599 -> TcTyVar -> TcM TcType
600 zonk_tc_tyvar unbound_var_fn tyvar
601 | not (isMetaTyVar tyvar) -- Skolems
602 = returnM (TyVarTy tyvar)
604 | otherwise -- Mutables
605 = do { cts <- readMetaTyVar tyvar
607 Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
608 Indirect ty -> zonkType unbound_var_fn ty }
613 %************************************************************************
617 %************************************************************************
620 readKindVar :: KindVar -> TcM (MetaDetails)
621 writeKindVar :: KindVar -> TcKind -> TcM ()
622 readKindVar kv = readMutVar (kindVarRef kv)
623 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
626 zonkTcKind :: TcKind -> TcM TcKind
627 zonkTcKind k = zonkTcType k
630 zonkTcKindToKind :: TcKind -> TcM Kind
631 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
632 -- Haskell specifies that * is to be used, so we follow that.
633 zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
636 %************************************************************************
638 \subsection{Checking a user type}
640 %************************************************************************
642 When dealing with a user-written type, we first translate it from an HsType
643 to a Type, performing kind checking, and then check various things that should
644 be true about it. We don't want to perform these checks at the same time
645 as the initial translation because (a) they are unnecessary for interface-file
646 types and (b) when checking a mutually recursive group of type and class decls,
647 we can't "look" at the tycons/classes yet. Also, the checks are are rather
648 diverse, and used to really mess up the other code.
650 One thing we check for is 'rank'.
652 Rank 0: monotypes (no foralls)
653 Rank 1: foralls at the front only, Rank 0 inside
654 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
656 basic ::= tyvar | T basic ... basic
658 r2 ::= forall tvs. cxt => r2a
659 r2a ::= r1 -> r2a | basic
660 r1 ::= forall tvs. cxt => r0
661 r0 ::= r0 -> r0 | basic
663 Another thing is to check that type synonyms are saturated.
664 This might not necessarily show up in kind checking.
666 data T k = MkT (k Int)
671 checkValidType :: UserTypeCtxt -> Type -> TcM ()
672 -- Checks that the type is valid for the given context
673 checkValidType ctxt ty
674 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
675 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
677 rank | gla_exts = Arbitrary
679 = case ctxt of -- Haskell 98
681 LamPatSigCtxt -> Rank 0
682 BindPatSigCtxt -> Rank 0
683 DefaultDeclCtxt-> Rank 0
685 TySynCtxt _ -> Rank 0
686 ExprSigCtxt -> Rank 1
687 FunSigCtxt _ -> Rank 1
688 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
689 -- constructor, hence rank 1
690 ForSigCtxt _ -> Rank 1
691 RuleSigCtxt _ -> Rank 1
692 SpecInstCtxt -> Rank 1
694 actual_kind = typeKind ty
696 kind_ok = case ctxt of
697 TySynCtxt _ -> True -- Any kind will do
698 ResSigCtxt -> isSubOpenTypeKind actual_kind
699 ExprSigCtxt -> isSubOpenTypeKind actual_kind
700 GenPatCtxt -> isLiftedTypeKind actual_kind
701 ForSigCtxt _ -> isLiftedTypeKind actual_kind
702 other -> isSubArgTypeKind actual_kind
704 ubx_tup | not gla_exts = UT_NotOk
705 | otherwise = case ctxt of
709 -- Unboxed tuples ok in function results,
710 -- but for type synonyms we allow them even at
713 -- Check that the thing has kind Type, and is lifted if necessary
714 checkTc kind_ok (kindErr actual_kind) `thenM_`
716 -- Check the internal validity of the type itself
717 check_poly_type rank ubx_tup ty `thenM_`
719 traceTc (text "checkValidType done" <+> ppr ty)
724 data Rank = Rank Int | Arbitrary
726 decRank :: Rank -> Rank
727 decRank Arbitrary = Arbitrary
728 decRank (Rank n) = Rank (n-1)
730 ----------------------------------------
731 data UbxTupFlag = UT_Ok | UT_NotOk
732 -- The "Ok" version means "ok if -fglasgow-exts is on"
734 ----------------------------------------
735 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
736 check_poly_type (Rank 0) ubx_tup ty
737 = check_tau_type (Rank 0) ubx_tup ty
739 check_poly_type rank ubx_tup ty
740 | null tvs && null theta
741 = check_tau_type rank ubx_tup ty
743 = do { check_valid_theta SigmaCtxt theta
744 ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow
745 ; checkFreeness tvs theta
746 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
748 (tvs, theta, tau) = tcSplitSigmaTy ty
750 ----------------------------------------
751 check_arg_type :: Type -> TcM ()
752 -- The sort of type that can instantiate a type variable,
753 -- or be the argument of a type constructor.
754 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
755 -- Other unboxed types are very occasionally allowed as type
756 -- arguments depending on the kind of the type constructor
758 -- For example, we want to reject things like:
760 -- instance Ord a => Ord (forall s. T s a)
762 -- g :: T s (forall b.b)
764 -- NB: unboxed tuples can have polymorphic or unboxed args.
765 -- This happens in the workers for functions returning
766 -- product types with polymorphic components.
767 -- But not in user code.
768 -- Anyway, they are dealt with by a special case in check_tau_type
771 = check_poly_type Arbitrary UT_NotOk ty `thenM_`
772 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
774 ----------------------------------------
775 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
776 -- Rank is allowed rank for function args
777 -- No foralls otherwise
779 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
780 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
781 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
783 -- Naked PredTys don't usually show up, but they can as a result of
784 -- {-# SPECIALISE instance Ord Char #-}
785 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
786 -- are handled, but the quick thing is just to permit PredTys here.
787 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
788 check_pred_ty dflags TypeCtxt sty
790 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
791 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
792 = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_`
793 check_poly_type rank UT_Ok res_ty
795 check_tau_type rank ubx_tup (AppTy ty1 ty2)
796 = check_arg_type ty1 `thenM_` check_arg_type ty2
798 check_tau_type rank ubx_tup (NoteTy other_note ty)
799 = check_tau_type rank ubx_tup ty
801 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
803 = do { -- It's OK to have an *over-applied* type synonym
804 -- data Tree a b = ...
805 -- type Foo a = Tree [a]
806 -- f :: Foo a b -> ...
808 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
809 Nothing -> failWithTc arity_msg
811 ; gla_exts <- doptM Opt_GlasgowExts
813 -- If -fglasgow-exts then don't check the type arguments
814 -- This allows us to instantiate a synonym defn with a
815 -- for-all type, or with a partially-applied type synonym.
816 -- e.g. type T a b = a
819 -- Here, T is partially applied, so it's illegal in H98.
820 -- But if you expand S first, then T we get just
825 -- For H98, do check the type args
826 mappM_ check_arg_type tys
829 | isUnboxedTupleTyCon tc
830 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
831 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
832 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
833 -- Args are allowed to be unlifted, or
834 -- more unboxed tuples, so can't use check_arg_ty
837 = mappM_ check_arg_type tys
840 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
843 tc_arity = tyConArity tc
845 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
846 ubx_tup_msg = ubxArgTyErr ty
848 ----------------------------------------
849 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
850 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
851 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
852 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
857 %************************************************************************
859 \subsection{Checking a theta or source type}
861 %************************************************************************
864 -- Enumerate the contexts in which a "source type", <S>, can occur
868 -- or (N a) where N is a newtype
871 = ClassSCCtxt Name -- Superclasses of clas
872 -- class <S> => C a where ...
873 | SigmaCtxt -- Theta part of a normal for-all type
874 -- f :: <S> => a -> a
875 | DataTyCtxt Name -- Theta part of a data decl
876 -- data <S> => T a = MkT a
877 | TypeCtxt -- Source type in an ordinary type
879 | InstThetaCtxt -- Context of an instance decl
880 -- instance <S> => C [a] where ...
882 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
883 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
884 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
885 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
886 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
890 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
891 checkValidTheta ctxt theta
892 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
894 -------------------------
895 check_valid_theta ctxt []
897 check_valid_theta ctxt theta
898 = getDOpts `thenM` \ dflags ->
899 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
900 mappM_ (check_pred_ty dflags ctxt) theta
902 (_,dups) = removeDups tcCmpPred theta
904 -------------------------
905 check_pred_ty dflags ctxt pred@(ClassP cls tys)
906 = -- Class predicates are valid in all contexts
907 checkTc (arity == n_tys) arity_err `thenM_`
909 -- Check the form of the argument types
910 mappM_ check_arg_type tys `thenM_`
911 checkTc (check_class_pred_tys dflags ctxt tys)
912 (predTyVarErr pred $$ how_to_allow)
915 class_name = className cls
916 arity = classArity cls
918 arity_err = arityErr "Class" class_name arity n_tys
919 how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
921 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
922 -- Implicit parameters only allows in type
923 -- signatures; not in instance decls, superclasses etc
924 -- The reason for not allowing implicit params in instances is a bit subtle
925 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
926 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
927 -- discharge all the potential usas of the ?x in e. For example, a
928 -- constraint Foo [Int] might come out of e,and applying the
929 -- instance decl would show up two uses of ?x.
932 check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
934 -------------------------
935 check_class_pred_tys dflags ctxt tys
937 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
938 InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
939 -- Further checks on head and theta in
940 -- checkInstTermination
941 other -> gla_exts || all tyvar_head tys
943 gla_exts = dopt Opt_GlasgowExts dflags
944 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
946 -------------------------
947 tyvar_head ty -- Haskell 98 allows predicates of form
948 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
949 | otherwise -- where a is a type variable
950 = case tcSplitAppTy_maybe ty of
951 Just (ty, _) -> tyvar_head ty
958 is ambiguous if P contains generic variables
959 (i.e. one of the Vs) that are not mentioned in tau
961 However, we need to take account of functional dependencies
962 when we speak of 'mentioned in tau'. Example:
963 class C a b | a -> b where ...
965 forall x y. (C x y) => x
966 is not ambiguous because x is mentioned and x determines y
968 NB; the ambiguity check is only used for *user* types, not for types
969 coming from inteface files. The latter can legitimately have
970 ambiguous types. Example
972 class S a where s :: a -> (Int,Int)
973 instance S Char where s _ = (1,1)
974 f:: S a => [a] -> Int -> (Int,Int)
975 f (_::[a]) x = (a*x,b)
976 where (a,b) = s (undefined::a)
978 Here the worker for f gets the type
979 fw :: forall a. S a => Int -> (# Int, Int #)
981 If the list of tv_names is empty, we have a monotype, and then we
982 don't need to check for ambiguity either, because the test can't fail
986 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
987 checkAmbiguity forall_tyvars theta tau_tyvars
988 = mappM_ complain (filter is_ambig theta)
990 complain pred = addErrTc (ambigErr pred)
991 extended_tau_vars = grow theta tau_tyvars
993 -- Only a *class* predicate can give rise to ambiguity
994 -- An *implicit parameter* cannot. For example:
995 -- foo :: (?x :: [a]) => Int
997 -- is fine. The call site will suppply a particular 'x'
998 is_ambig pred = isClassPred pred &&
999 any ambig_var (varSetElems (tyVarsOfPred pred))
1001 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1002 not (ct_var `elemVarSet` extended_tau_vars)
1005 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1006 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1007 ptext SLIT("must be reachable from the type after the '=>'"))]
1010 In addition, GHC insists that at least one type variable
1011 in each constraint is in V. So we disallow a type like
1012 forall a. Eq b => b -> b
1013 even in a scope where b is in scope.
1016 checkFreeness forall_tyvars theta
1017 = mappM_ complain (filter is_free theta)
1019 is_free pred = not (isIPPred pred)
1020 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1021 bound_var ct_var = ct_var `elem` forall_tyvars
1022 complain pred = addErrTc (freeErr pred)
1025 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1026 ptext SLIT("are already in scope"),
1027 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1032 checkThetaCtxt ctxt theta
1033 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1034 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1036 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1037 predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
1038 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1039 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1041 arityErr kind name n m
1042 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1043 n_arguments <> comma, text "but has been given", int m]
1045 n_arguments | n == 0 = ptext SLIT("no arguments")
1046 | n == 1 = ptext SLIT("1 argument")
1047 | True = hsep [int n, ptext SLIT("arguments")]
1051 %************************************************************************
1053 \subsection{Checking for a decent instance head type}
1055 %************************************************************************
1057 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1058 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1060 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1061 flag is on, or (2)~the instance is imported (they must have been
1062 compiled elsewhere). In these cases, we let them go through anyway.
1064 We can also have instances for functions: @instance Foo (a -> b) ...@.
1067 checkValidInstHead :: Type -> TcM (Class, [TcType])
1069 checkValidInstHead ty -- Should be a source type
1070 = case tcSplitPredTy_maybe ty of {
1071 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1074 case getClassPredTys_maybe pred of {
1075 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1078 getDOpts `thenM` \ dflags ->
1079 mappM_ check_arg_type tys `thenM_`
1080 check_inst_head dflags clas tys `thenM_`
1084 check_inst_head dflags clas tys
1085 -- If GlasgowExts then check at least one isn't a type variable
1086 | dopt Opt_GlasgowExts dflags
1087 = mapM_ check_one tys
1089 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1091 = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
1092 (instTypeErr (pprClassPred clas tys) head_shape_msg)
1095 (first_ty : _) = tys
1097 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1098 text "where T is not a synonym, and a,b,c are distinct type variables")
1100 -- For now, I only allow tau-types (not polytypes) in
1101 -- the head of an instance decl.
1102 -- E.g. instance C (forall a. a->a) is rejected
1103 -- One could imagine generalising that, but I'm not sure
1104 -- what all the consequences might be
1105 check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1106 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1108 instTypeErr pp_ty msg
1109 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1114 %************************************************************************
1116 \subsection{Checking instance for termination}
1118 %************************************************************************
1122 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1123 checkValidInstance tyvars theta clas inst_tys
1124 = do { gla_exts <- doptM Opt_GlasgowExts
1125 ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
1127 ; checkValidTheta InstThetaCtxt theta
1128 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1130 -- Check that instance inference will terminate (if we care)
1131 -- For Haskell 98, checkValidTheta has already done that
1132 ; when (gla_exts && not undecidable_ok) $
1133 checkInstTermination theta inst_tys
1135 -- The Coverage Condition
1136 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1137 (instTypeErr (pprClassPred clas inst_tys) msg)
1140 msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
1143 Termination test: each assertion in the context satisfies
1144 (1) no variable has more occurrences in the assertion than in the head, and
1145 (2) the assertion has fewer constructors and variables (taken together
1146 and counting repetitions) than the head.
1147 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1148 (which have already been checked) guarantee termination.
1150 The underlying idea is that
1152 for any ground substitution, each assertion in the
1153 context has fewer type constructors than the head.
1157 checkInstTermination :: ThetaType -> [TcType] -> TcM ()
1158 checkInstTermination theta tys
1159 = do { mappM_ (check_nomore (fvTypes tys)) theta
1160 ; mappM_ (check_smaller (sizeTypes tys)) theta }
1162 check_nomore :: [TyVar] -> PredType -> TcM ()
1163 check_nomore fvs pred
1164 = checkTc (null (fvPred pred \\ fvs))
1165 (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1167 check_smaller :: Int -> PredType -> TcM ()
1168 check_smaller n pred
1169 = checkTc (sizePred pred < n)
1170 (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1172 predUndecErr pred msg = sep [msg,
1173 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1175 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1176 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1177 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1179 -- Free variables of a type, retaining repetitions, and expanding synonyms
1180 fvType :: Type -> [TyVar]
1181 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1182 fvType (TyVarTy tv) = [tv]
1183 fvType (TyConApp _ tys) = fvTypes tys
1184 fvType (NoteTy _ ty) = fvType ty
1185 fvType (PredTy pred) = fvPred pred
1186 fvType (FunTy arg res) = fvType arg ++ fvType res
1187 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1188 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1190 fvTypes :: [Type] -> [TyVar]
1191 fvTypes tys = concat (map fvType tys)
1193 fvPred :: PredType -> [TyVar]
1194 fvPred (ClassP _ tys') = fvTypes tys'
1195 fvPred (IParam _ ty) = fvType ty
1196 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1198 -- Size of a type: the number of variables and constructors
1199 sizeType :: Type -> Int
1200 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1201 sizeType (TyVarTy _) = 1
1202 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1203 sizeType (NoteTy _ ty) = sizeType ty
1204 sizeType (PredTy pred) = sizePred pred
1205 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1206 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1207 sizeType (ForAllTy _ ty) = sizeType ty
1209 sizeTypes :: [Type] -> Int
1210 sizeTypes xs = sum (map sizeType xs)
1212 sizePred :: PredType -> Int
1213 sizePred (ClassP _ tys') = sizeTypes tys'
1214 sizePred (IParam _ ty) = sizeType ty
1215 sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2