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
372 SkolemTv _ -> return (DoneTv details)
373 MetaTv _ ref -> do { meta_details <- readMutVar ref
374 ; case meta_details of
375 Indirect ty -> return (IndirectTv ty)
376 Flexi -> return (DoneTv details) }
378 details = tcTyVarDetails tyvar
381 -- gaw 2004 We aren't shorting anything out anymore, at least for now
383 | not (isTcTyVar tyvar)
384 = pprTrace "getTcTyVar" (ppr tyvar) $
385 returnM (Just (mkTyVarTy tyvar))
388 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
389 readMetaTyVar tyvar `thenM` \ maybe_ty ->
391 Just ty -> short_out ty `thenM` \ ty' ->
392 writeMetaTyVar tyvar (Just ty') `thenM_`
395 Nothing -> returnM Nothing
397 short_out :: TcType -> TcM TcType
398 short_out ty@(TyVarTy tyvar)
399 | not (isTcTyVar tyvar)
403 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
405 Just ty' -> short_out ty' `thenM` \ ty' ->
406 writeMetaTyVar tyvar (Just ty') `thenM_`
411 short_out other_ty = returnM other_ty
416 %************************************************************************
418 \subsection{Zonking -- the exernal interfaces}
420 %************************************************************************
422 ----------------- Type variables
425 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
426 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
428 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
429 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
430 returnM (tyVarsOfTypes tys)
432 zonkTcTyVar :: TcTyVar -> TcM TcType
433 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
434 zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
437 ----------------- Types
440 zonkTcType :: TcType -> TcM TcType
441 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
443 zonkTcTypes :: [TcType] -> TcM [TcType]
444 zonkTcTypes tys = mappM zonkTcType tys
446 zonkTcClassConstraints cts = mappM zonk cts
447 where zonk (clas, tys)
448 = zonkTcTypes tys `thenM` \ new_tys ->
449 returnM (clas, new_tys)
451 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
452 zonkTcThetaType theta = mappM zonkTcPredType theta
454 zonkTcPredType :: TcPredType -> TcM TcPredType
455 zonkTcPredType (ClassP c ts)
456 = zonkTcTypes ts `thenM` \ new_ts ->
457 returnM (ClassP c new_ts)
458 zonkTcPredType (IParam n t)
459 = zonkTcType t `thenM` \ new_t ->
460 returnM (IParam n new_t)
461 zonkTcPredType (EqPred t1 t2)
462 = zonkTcType t1 `thenM` \ new_t1 ->
463 zonkTcType t2 `thenM` \ new_t2 ->
464 returnM (EqPred new_t1 new_t2)
467 ------------------- These ...ToType, ...ToKind versions
468 are used at the end of type checking
471 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
472 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
473 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
474 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
475 -- The meta tyvar is updated to point to the new regular TyVar. Now any
476 -- bound occurences of the original type variable will get zonked to
477 -- the immutable version.
479 -- We leave skolem TyVars alone; they are immutable.
480 zonkQuantifiedTyVar tv
481 | isSkolemTyVar tv = return tv
482 -- It might be a skolem type variable,
483 -- for example from a user type signature
485 | otherwise -- It's a meta-type-variable
486 = do { details <- readMetaTyVar tv
488 -- Create the new, frozen, regular type variable
489 ; let final_kind = defaultKind (tyVarKind tv)
490 final_tv = mkTyVar (tyVarName tv) final_kind
492 -- Bind the meta tyvar to the new tyvar
494 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
496 -- [Sept 04] I don't think this should happen
497 -- See note [Silly Type Synonym]
499 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
501 -- Return the new tyvar
505 [Silly Type Synonyms]
508 type C u a = u -- Note 'a' unused
510 foo :: (forall a. C u a -> C u a) -> u
514 bar = foo (\t -> t + t)
516 * From the (\t -> t+t) we get type {Num d} => d -> d
519 * Now unify with type of foo's arg, and we get:
520 {Num (C d a)} => C d a -> C d a
523 * Now abstract over the 'a', but float out the Num (C d a) constraint
524 because it does not 'really' mention a. (see exactTyVarsOfType)
525 The arg to foo becomes
528 * So we get a dict binding for Num (C d a), which is zonked to give
530 [Note Sept 04: now that we are zonking quantified type variables
531 on construction, the 'a' will be frozen as a regular tyvar on
532 quantification, so the floated dict will still have type (C d a).
533 Which renders this whole note moot; happily!]
535 * Then the /\a abstraction has a zonked 'a' in it.
537 All very silly. I think its harmless to ignore the problem. We'll end up with
538 a /\a in the final result but all the occurrences of a will be zonked to ()
541 %************************************************************************
543 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
545 %* For internal use only! *
547 %************************************************************************
550 -- For unbound, mutable tyvars, zonkType uses the function given to it
551 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
552 -- type variable and zonks the kind too
554 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
555 -- see zonkTcType, and zonkTcTypeToType
558 zonkType unbound_var_fn ty
561 go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
563 go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
564 returnM (TyConApp tc tys')
566 go (PredTy p) = go_pred p `thenM` \ p' ->
569 go (FunTy arg res) = go arg `thenM` \ arg' ->
570 go res `thenM` \ res' ->
571 returnM (FunTy arg' res')
573 go (AppTy fun arg) = go fun `thenM` \ fun' ->
574 go arg `thenM` \ arg' ->
575 returnM (mkAppTy fun' arg')
576 -- NB the mkAppTy; we might have instantiated a
577 -- type variable to a type constructor, so we need
578 -- to pull the TyConApp to the top.
580 -- The two interesting cases!
581 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
582 | otherwise = return (TyVarTy tyvar)
583 -- Ordinary (non Tc) tyvars occur inside quantified types
585 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
586 go ty `thenM` \ ty' ->
587 returnM (ForAllTy tyvar ty')
589 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
590 returnM (ClassP c tys')
591 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
592 returnM (IParam n ty')
593 go_pred (EqPred ty1 ty2) = go ty1 `thenM` \ ty1' ->
594 go ty2 `thenM` \ ty2' ->
595 returnM (EqPred ty1' ty2')
597 zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
598 -> TcTyVar -> TcM TcType
599 zonk_tc_tyvar unbound_var_fn tyvar
600 | not (isMetaTyVar tyvar) -- Skolems
601 = returnM (TyVarTy tyvar)
603 | otherwise -- Mutables
604 = do { cts <- readMetaTyVar tyvar
606 Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
607 Indirect ty -> zonkType unbound_var_fn ty }
612 %************************************************************************
616 %************************************************************************
619 readKindVar :: KindVar -> TcM (MetaDetails)
620 writeKindVar :: KindVar -> TcKind -> TcM ()
621 readKindVar kv = readMutVar (kindVarRef kv)
622 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
625 zonkTcKind :: TcKind -> TcM TcKind
626 zonkTcKind k = zonkTcType k
629 zonkTcKindToKind :: TcKind -> TcM Kind
630 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
631 -- Haskell specifies that * is to be used, so we follow that.
632 zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
635 %************************************************************************
637 \subsection{Checking a user type}
639 %************************************************************************
641 When dealing with a user-written type, we first translate it from an HsType
642 to a Type, performing kind checking, and then check various things that should
643 be true about it. We don't want to perform these checks at the same time
644 as the initial translation because (a) they are unnecessary for interface-file
645 types and (b) when checking a mutually recursive group of type and class decls,
646 we can't "look" at the tycons/classes yet. Also, the checks are are rather
647 diverse, and used to really mess up the other code.
649 One thing we check for is 'rank'.
651 Rank 0: monotypes (no foralls)
652 Rank 1: foralls at the front only, Rank 0 inside
653 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
655 basic ::= tyvar | T basic ... basic
657 r2 ::= forall tvs. cxt => r2a
658 r2a ::= r1 -> r2a | basic
659 r1 ::= forall tvs. cxt => r0
660 r0 ::= r0 -> r0 | basic
662 Another thing is to check that type synonyms are saturated.
663 This might not necessarily show up in kind checking.
665 data T k = MkT (k Int)
670 checkValidType :: UserTypeCtxt -> Type -> TcM ()
671 -- Checks that the type is valid for the given context
672 checkValidType ctxt ty
673 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
674 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
676 rank | gla_exts = Arbitrary
678 = case ctxt of -- Haskell 98
680 LamPatSigCtxt -> Rank 0
681 BindPatSigCtxt -> Rank 0
682 DefaultDeclCtxt-> Rank 0
684 TySynCtxt _ -> Rank 0
685 ExprSigCtxt -> Rank 1
686 FunSigCtxt _ -> Rank 1
687 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
688 -- constructor, hence rank 1
689 ForSigCtxt _ -> Rank 1
690 RuleSigCtxt _ -> Rank 1
691 SpecInstCtxt -> Rank 1
693 actual_kind = typeKind ty
695 kind_ok = case ctxt of
696 TySynCtxt _ -> True -- Any kind will do
697 ResSigCtxt -> isSubOpenTypeKind actual_kind
698 ExprSigCtxt -> isSubOpenTypeKind actual_kind
699 GenPatCtxt -> isLiftedTypeKind actual_kind
700 ForSigCtxt _ -> isLiftedTypeKind actual_kind
701 other -> isSubArgTypeKind actual_kind
703 ubx_tup | not gla_exts = UT_NotOk
704 | otherwise = case ctxt of
708 -- Unboxed tuples ok in function results,
709 -- but for type synonyms we allow them even at
712 -- Check that the thing has kind Type, and is lifted if necessary
713 checkTc kind_ok (kindErr actual_kind) `thenM_`
715 -- Check the internal validity of the type itself
716 check_poly_type rank ubx_tup ty `thenM_`
718 traceTc (text "checkValidType done" <+> ppr ty)
723 data Rank = Rank Int | Arbitrary
725 decRank :: Rank -> Rank
726 decRank Arbitrary = Arbitrary
727 decRank (Rank n) = Rank (n-1)
729 ----------------------------------------
730 data UbxTupFlag = UT_Ok | UT_NotOk
731 -- The "Ok" version means "ok if -fglasgow-exts is on"
733 ----------------------------------------
734 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
735 check_poly_type (Rank 0) ubx_tup ty
736 = check_tau_type (Rank 0) ubx_tup ty
738 check_poly_type rank ubx_tup ty
739 | null tvs && null theta
740 = check_tau_type rank ubx_tup ty
742 = do { check_valid_theta SigmaCtxt theta
743 ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow
744 ; checkFreeness tvs theta
745 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
747 (tvs, theta, tau) = tcSplitSigmaTy ty
749 ----------------------------------------
750 check_arg_type :: Type -> TcM ()
751 -- The sort of type that can instantiate a type variable,
752 -- or be the argument of a type constructor.
753 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
754 -- Other unboxed types are very occasionally allowed as type
755 -- arguments depending on the kind of the type constructor
757 -- For example, we want to reject things like:
759 -- instance Ord a => Ord (forall s. T s a)
761 -- g :: T s (forall b.b)
763 -- NB: unboxed tuples can have polymorphic or unboxed args.
764 -- This happens in the workers for functions returning
765 -- product types with polymorphic components.
766 -- But not in user code.
767 -- Anyway, they are dealt with by a special case in check_tau_type
770 = check_poly_type Arbitrary UT_NotOk ty `thenM_`
771 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
773 ----------------------------------------
774 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
775 -- Rank is allowed rank for function args
776 -- No foralls otherwise
778 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
779 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
780 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
782 -- Naked PredTys don't usually show up, but they can as a result of
783 -- {-# SPECIALISE instance Ord Char #-}
784 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
785 -- are handled, but the quick thing is just to permit PredTys here.
786 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
787 check_pred_ty dflags TypeCtxt sty
789 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
790 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
791 = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_`
792 check_poly_type rank UT_Ok res_ty
794 check_tau_type rank ubx_tup (AppTy ty1 ty2)
795 = check_arg_type ty1 `thenM_` check_arg_type ty2
797 check_tau_type rank ubx_tup (NoteTy other_note ty)
798 = check_tau_type rank ubx_tup ty
800 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
802 = do { -- It's OK to have an *over-applied* type synonym
803 -- data Tree a b = ...
804 -- type Foo a = Tree [a]
805 -- f :: Foo a b -> ...
807 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
808 Nothing -> failWithTc arity_msg
810 ; gla_exts <- doptM Opt_GlasgowExts
812 -- If -fglasgow-exts then don't check the type arguments
813 -- This allows us to instantiate a synonym defn with a
814 -- for-all type, or with a partially-applied type synonym.
815 -- e.g. type T a b = a
818 -- Here, T is partially applied, so it's illegal in H98.
819 -- But if you expand S first, then T we get just
824 -- For H98, do check the type args
825 mappM_ check_arg_type tys
828 | isUnboxedTupleTyCon tc
829 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
830 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
831 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
832 -- Args are allowed to be unlifted, or
833 -- more unboxed tuples, so can't use check_arg_ty
836 = mappM_ check_arg_type tys
839 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
842 tc_arity = tyConArity tc
844 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
845 ubx_tup_msg = ubxArgTyErr ty
847 ----------------------------------------
848 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
849 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
850 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
851 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
856 %************************************************************************
858 \subsection{Checking a theta or source type}
860 %************************************************************************
863 -- Enumerate the contexts in which a "source type", <S>, can occur
867 -- or (N a) where N is a newtype
870 = ClassSCCtxt Name -- Superclasses of clas
871 -- class <S> => C a where ...
872 | SigmaCtxt -- Theta part of a normal for-all type
873 -- f :: <S> => a -> a
874 | DataTyCtxt Name -- Theta part of a data decl
875 -- data <S> => T a = MkT a
876 | TypeCtxt -- Source type in an ordinary type
878 | InstThetaCtxt -- Context of an instance decl
879 -- instance <S> => C [a] where ...
881 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
882 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
883 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
884 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
885 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
889 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
890 checkValidTheta ctxt theta
891 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
893 -------------------------
894 check_valid_theta ctxt []
896 check_valid_theta ctxt theta
897 = getDOpts `thenM` \ dflags ->
898 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
899 mappM_ (check_pred_ty dflags ctxt) theta
901 (_,dups) = removeDups tcCmpPred theta
903 -------------------------
904 check_pred_ty dflags ctxt pred@(ClassP cls tys)
905 = -- Class predicates are valid in all contexts
906 checkTc (arity == n_tys) arity_err `thenM_`
908 -- Check the form of the argument types
909 mappM_ check_arg_type tys `thenM_`
910 checkTc (check_class_pred_tys dflags ctxt tys)
911 (predTyVarErr pred $$ how_to_allow)
914 class_name = className cls
915 arity = classArity cls
917 arity_err = arityErr "Class" class_name arity n_tys
918 how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
920 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
921 -- Implicit parameters only allows in type
922 -- signatures; not in instance decls, superclasses etc
923 -- The reason for not allowing implicit params in instances is a bit subtle
924 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
925 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
926 -- discharge all the potential usas of the ?x in e. For example, a
927 -- constraint Foo [Int] might come out of e,and applying the
928 -- instance decl would show up two uses of ?x.
931 check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
933 -------------------------
934 check_class_pred_tys dflags ctxt tys
936 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
937 InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
938 -- Further checks on head and theta in
939 -- checkInstTermination
940 other -> gla_exts || all tyvar_head tys
942 gla_exts = dopt Opt_GlasgowExts dflags
943 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
945 -------------------------
946 tyvar_head ty -- Haskell 98 allows predicates of form
947 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
948 | otherwise -- where a is a type variable
949 = case tcSplitAppTy_maybe ty of
950 Just (ty, _) -> tyvar_head ty
957 is ambiguous if P contains generic variables
958 (i.e. one of the Vs) that are not mentioned in tau
960 However, we need to take account of functional dependencies
961 when we speak of 'mentioned in tau'. Example:
962 class C a b | a -> b where ...
964 forall x y. (C x y) => x
965 is not ambiguous because x is mentioned and x determines y
967 NB; the ambiguity check is only used for *user* types, not for types
968 coming from inteface files. The latter can legitimately have
969 ambiguous types. Example
971 class S a where s :: a -> (Int,Int)
972 instance S Char where s _ = (1,1)
973 f:: S a => [a] -> Int -> (Int,Int)
974 f (_::[a]) x = (a*x,b)
975 where (a,b) = s (undefined::a)
977 Here the worker for f gets the type
978 fw :: forall a. S a => Int -> (# Int, Int #)
980 If the list of tv_names is empty, we have a monotype, and then we
981 don't need to check for ambiguity either, because the test can't fail
985 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
986 checkAmbiguity forall_tyvars theta tau_tyvars
987 = mappM_ complain (filter is_ambig theta)
989 complain pred = addErrTc (ambigErr pred)
990 extended_tau_vars = grow theta tau_tyvars
992 -- Only a *class* predicate can give rise to ambiguity
993 -- An *implicit parameter* cannot. For example:
994 -- foo :: (?x :: [a]) => Int
996 -- is fine. The call site will suppply a particular 'x'
997 is_ambig pred = isClassPred pred &&
998 any ambig_var (varSetElems (tyVarsOfPred pred))
1000 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1001 not (ct_var `elemVarSet` extended_tau_vars)
1004 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1005 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1006 ptext SLIT("must be reachable from the type after the '=>'"))]
1009 In addition, GHC insists that at least one type variable
1010 in each constraint is in V. So we disallow a type like
1011 forall a. Eq b => b -> b
1012 even in a scope where b is in scope.
1015 checkFreeness forall_tyvars theta
1016 = mappM_ complain (filter is_free theta)
1018 is_free pred = not (isIPPred pred)
1019 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1020 bound_var ct_var = ct_var `elem` forall_tyvars
1021 complain pred = addErrTc (freeErr pred)
1024 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1025 ptext SLIT("are already in scope"),
1026 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1031 checkThetaCtxt ctxt theta
1032 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1033 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1035 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1036 predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
1037 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1038 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1040 arityErr kind name n m
1041 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1042 n_arguments <> comma, text "but has been given", int m]
1044 n_arguments | n == 0 = ptext SLIT("no arguments")
1045 | n == 1 = ptext SLIT("1 argument")
1046 | True = hsep [int n, ptext SLIT("arguments")]
1050 %************************************************************************
1052 \subsection{Checking for a decent instance head type}
1054 %************************************************************************
1056 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1057 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1059 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1060 flag is on, or (2)~the instance is imported (they must have been
1061 compiled elsewhere). In these cases, we let them go through anyway.
1063 We can also have instances for functions: @instance Foo (a -> b) ...@.
1066 checkValidInstHead :: Type -> TcM (Class, [TcType])
1068 checkValidInstHead ty -- Should be a source type
1069 = case tcSplitPredTy_maybe ty of {
1070 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1073 case getClassPredTys_maybe pred of {
1074 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1077 getDOpts `thenM` \ dflags ->
1078 mappM_ check_arg_type tys `thenM_`
1079 check_inst_head dflags clas tys `thenM_`
1083 check_inst_head dflags clas tys
1084 -- If GlasgowExts then check at least one isn't a type variable
1085 | dopt Opt_GlasgowExts dflags
1086 = mapM_ check_one tys
1088 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1090 = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
1091 (instTypeErr (pprClassPred clas tys) head_shape_msg)
1094 (first_ty : _) = tys
1096 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1097 text "where T is not a synonym, and a,b,c are distinct type variables")
1099 -- For now, I only allow tau-types (not polytypes) in
1100 -- the head of an instance decl.
1101 -- E.g. instance C (forall a. a->a) is rejected
1102 -- One could imagine generalising that, but I'm not sure
1103 -- what all the consequences might be
1104 check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1105 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1107 instTypeErr pp_ty msg
1108 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1113 %************************************************************************
1115 \subsection{Checking instance for termination}
1117 %************************************************************************
1121 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1122 checkValidInstance tyvars theta clas inst_tys
1123 = do { gla_exts <- doptM Opt_GlasgowExts
1124 ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
1126 ; checkValidTheta InstThetaCtxt theta
1127 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1129 -- Check that instance inference will terminate (if we care)
1130 -- For Haskell 98, checkValidTheta has already done that
1131 ; when (gla_exts && not undecidable_ok) $
1132 checkInstTermination theta inst_tys
1134 -- The Coverage Condition
1135 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1136 (instTypeErr (pprClassPred clas inst_tys) msg)
1139 msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
1142 Termination test: each assertion in the context satisfies
1143 (1) no variable has more occurrences in the assertion than in the head, and
1144 (2) the assertion has fewer constructors and variables (taken together
1145 and counting repetitions) than the head.
1146 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1147 (which have already been checked) guarantee termination.
1149 The underlying idea is that
1151 for any ground substitution, each assertion in the
1152 context has fewer type constructors than the head.
1156 checkInstTermination :: ThetaType -> [TcType] -> TcM ()
1157 checkInstTermination theta tys
1158 = do { mappM_ (check_nomore (fvTypes tys)) theta
1159 ; mappM_ (check_smaller (sizeTypes tys)) theta }
1161 check_nomore :: [TyVar] -> PredType -> TcM ()
1162 check_nomore fvs pred
1163 = checkTc (null (fvPred pred \\ fvs))
1164 (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1166 check_smaller :: Int -> PredType -> TcM ()
1167 check_smaller n pred
1168 = checkTc (sizePred pred < n)
1169 (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1171 predUndecErr pred msg = sep [msg,
1172 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1174 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1175 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1176 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1178 -- Free variables of a type, retaining repetitions, and expanding synonyms
1179 fvType :: Type -> [TyVar]
1180 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1181 fvType (TyVarTy tv) = [tv]
1182 fvType (TyConApp _ tys) = fvTypes tys
1183 fvType (NoteTy _ ty) = fvType ty
1184 fvType (PredTy pred) = fvPred pred
1185 fvType (FunTy arg res) = fvType arg ++ fvType res
1186 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1187 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1189 fvTypes :: [Type] -> [TyVar]
1190 fvTypes tys = concat (map fvType tys)
1192 fvPred :: PredType -> [TyVar]
1193 fvPred (ClassP _ tys') = fvTypes tys'
1194 fvPred (IParam _ ty) = fvType ty
1195 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1197 -- Size of a type: the number of variables and constructors
1198 sizeType :: Type -> Int
1199 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1200 sizeType (TyVarTy _) = 1
1201 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1202 sizeType (NoteTy _ ty) = sizeType ty
1203 sizeType (PredTy pred) = sizePred pred
1204 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1205 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1206 sizeType (ForAllTy _ ty) = sizeType ty
1208 sizeTypes :: [Type] -> Int
1209 sizeTypes xs = sum (map sizeType xs)
1211 sizePred :: PredType -> Int
1212 sizePred (ClassP _ tys') = sizeTypes tys'
1213 sizePred (IParam _ ty) = sizeType ty
1214 sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2