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 newTyFlexiVarTy, -- Kind -> TcM TcType
16 newTyFlexiVarTys, -- Int -> Kind -> TcM [TcType]
17 newKindVar, newKindVars,
18 lookupTcTyVar, condLookupTcTyVar, LookupTyVarResult(..),
19 newMetaTyVar, readMetaTyVar, writeMetaTyVar, putMetaTyVar,
21 --------------------------------
23 tcInstTyVar, tcInstTyVars, tcInstType,
24 tcSkolType, tcSkolTyVars,
25 tcSkolSigType, tcSkolSigTyVars,
27 --------------------------------
28 -- Checking type validity
29 Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
30 SourceTyCtxt(..), checkValidTheta, checkFreeness,
31 checkValidInstHead, instTypeErr, checkAmbiguity,
32 arityErr, isRigidType,
34 --------------------------------
36 zonkType, zonkTcPredType,
37 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
38 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
39 zonkTcKindToKind, zonkTcKind,
41 readKindVar, writeKindVar
45 #include "HsVersions.h"
49 import HsSyn ( LHsType )
50 import TypeRep ( Type(..), PredType(..), TyNote(..), -- Friend; can see representation
53 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
54 TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
55 MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef,
56 tcCmpPred, isClassPred,
57 tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
58 tcSplitTyConApp_maybe, tcSplitForAllTys,
59 tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy,
60 isUnLiftedType, isIPPred, isImmutableTyVar,
61 typeKind, isFlexi, isSkolemTyVar,
62 mkAppTy, mkTyVarTy, mkTyVarTys,
63 tyVarsOfPred, getClassPredTys_maybe,
64 tyVarsOfType, tyVarsOfTypes,
65 pprPred, pprTheta, pprClassPred )
66 import Kind ( Kind(..), KindVar(..), mkKindVar, isSubKind,
67 isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
68 liftedTypeKind, defaultKind
70 import Type ( TvSubst, zipTopTvSubst, substTy )
71 import Class ( Class, classArity, className )
72 import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
73 tyConArity, tyConName )
74 import Var ( TyVar, tyVarKind, tyVarName,
75 mkTyVar, mkTcTyVar, tcTyVarDetails, isTcTyVar )
78 import TcRnMonad -- TcType, amongst others
79 import FunDeps ( grow )
80 import Name ( Name, setNameUnique, mkSysTvName )
83 import CmdLineOpts ( dopt, DynFlag(..) )
84 import UniqSupply ( uniqsFromSupply )
85 import Util ( nOfThem, isSingleton, equalLength, notNull )
86 import ListSetOps ( removeDups )
87 import SrcLoc ( unLoc )
92 %************************************************************************
94 \subsection{New type variables}
96 %************************************************************************
99 newMetaTyVar :: Name -> Kind -> MetaDetails -> TcM TyVar
100 newMetaTyVar name kind details
101 = do { ref <- newMutVar details ;
102 return (mkTcTyVar name kind (MetaTv ref)) }
104 readMetaTyVar :: TyVar -> TcM MetaDetails
105 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
106 readMutVar (metaTvRef tyvar)
108 writeMetaTyVar :: TyVar -> MetaDetails -> TcM ()
109 writeMetaTyVar tyvar val = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
110 writeMutVar (metaTvRef tyvar) val
112 newFlexiTyVar :: Kind -> TcM TcTyVar
114 = newUnique `thenM` \ uniq ->
115 newMetaTyVar (mkSysTvName uniq FSLIT("t")) kind Flexi
117 newTyFlexiVarTy :: Kind -> TcM TcType
119 = newFlexiTyVar kind `thenM` \ tc_tyvar ->
120 returnM (TyVarTy tc_tyvar)
122 newTyFlexiVarTys :: Int -> Kind -> TcM [TcType]
123 newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind)
125 isRigidType :: TcType -> TcM Bool
126 -- Check that the type is rigid, *taking the type refinement into account*
127 -- In other words if a rigid type variable tv is refined to a wobbly type,
128 -- the answer should be False
129 -- ToDo: can this happen?
131 = do { rigids <- mapM is_rigid (varSetElems (tyVarsOfType ty))
132 ; return (and rigids) }
134 is_rigid tv = do { details <- lookupTcTyVar tv
136 RigidTv -> return True
137 IndirectTv True ty -> isRigidType ty
138 other -> return False
141 newKindVar :: TcM TcKind
142 newKindVar = do { uniq <- newUnique
143 ; ref <- newMutVar Nothing
144 ; return (KindVar (mkKindVar uniq ref)) }
146 newKindVars :: Int -> TcM [TcKind]
147 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
151 %************************************************************************
153 \subsection{Type instantiation}
155 %************************************************************************
157 Instantiating a bunch of type variables
161 Note that we don't change the print-name
162 This won't confuse the type checker but there's a chance
163 that two different tyvars will print the same way
164 in an error message. -dppr-debug will show up the difference
165 Better watch out for this. If worst comes to worst, just
170 -----------------------
171 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
173 = do { tc_tvs <- mappM tcInstTyVar tyvars
174 ; let tys = mkTyVarTys tc_tvs
175 ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
176 -- Since the tyvars are freshly made,
177 -- they cannot possibly be captured by
178 -- any existing for-alls. Hence zipTopTvSubst
181 = do { uniq <- newUnique
182 ; let name = setNameUnique (tyVarName tyvar) uniq
183 -- See Note [TyVarName]
184 ; newMetaTyVar name (tyVarKind tyvar) Flexi }
186 tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
187 -- tcInstType instantiates the outer-level for-alls of a TcType with
188 -- fresh (mutable) type variables, splits off the dictionary part,
189 -- and returns the pieces.
190 tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty
193 ---------------------------------------------
194 tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
195 -- Instantiate a type with fresh skolem constants
196 tcSkolType info ty = tc_inst_type (tcSkolTyVars info) ty
198 tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
199 tcSkolTyVars info tyvars
200 = do { us <- newUniqueSupply
201 ; return (zipWith skol_tv tyvars (uniqsFromSupply us)) }
203 skol_tv tv uniq = mkTcTyVar (setNameUnique (tyVarName tv) uniq)
204 (tyVarKind tv) (SkolemTv info)
205 -- See Note [TyVarName]
208 ---------------------------------------------
209 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
210 -- Instantiate a type signature with skolem constants, but
211 -- do *not* give them fresh names, because we want the name to
212 -- be in the type environment -- it is lexically scoped.
213 tcSkolSigType info ty
214 = tc_inst_type (\tvs -> return (tcSkolSigTyVars info tvs)) ty
216 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
217 tcSkolSigTyVars info tyvars = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info)
220 -----------------------
221 tc_inst_type :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
222 -> TcType -- Type to instantiate
223 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
224 tc_inst_type inst_tyvars ty
225 = case tcSplitForAllTys ty of
226 ([], rho) -> let -- There may be overloading despite no type variables;
227 -- (?x :: Int) => Int -> Int
228 (theta, tau) = tcSplitPhiTy rho
230 return ([], theta, tau)
232 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
234 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
235 -- Either the tyvars are freshly made, by inst_tyvars,
236 -- or (in the call from tcSkolSigType) any nested foralls
237 -- have different binders. Either way, zipTopTvSubst is ok
239 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
240 ; return (tyvars', theta, tau) }
244 %************************************************************************
246 \subsection{Putting and getting mutable type variables}
248 %************************************************************************
251 putMetaTyVar :: TcTyVar -> TcType -> TcM ()
253 putMetaTyVar tyvar ty = writeMetaTyVar tyvar (Indirect ty)
255 putMetaTyVar tyvar ty
256 | not (isMetaTyVar tyvar)
257 = pprTrace "putTcTyVar" (ppr tyvar) $
261 = ASSERT( isMetaTyVar tyvar )
262 ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
263 do { ASSERTM( do { details <- readMetaTyVar tyvar; return (isFlexi details) } )
264 ; writeMetaTyVar tyvar (Indirect ty) }
271 But it's more fun to short out indirections on the way: If this
272 version returns a TyVar, then that TyVar is unbound. If it returns
273 any other type, then there might be bound TyVars embedded inside it.
275 We return Nothing iff the original box was unbound.
278 data LookupTyVarResult -- The result of a lookupTcTyVar call
281 | IndirectTv Bool TcType
282 -- True => This is a non-wobbly type refinement,
283 -- gotten from GADT match unification
284 -- False => This is a wobbly type,
285 -- gotten from inference unification
287 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
288 -- This function is the ONLY PLACE that we consult the
289 -- type refinement carried by the monad
291 -- The boolean returned with Indirect
293 = case tcTyVarDetails tyvar of
294 SkolemTv _ -> do { type_reft <- getTypeRefinement
295 ; case lookupVarEnv type_reft tyvar of
296 Just ty -> return (IndirectTv True ty)
297 Nothing -> return RigidTv
299 MetaTv ref -> do { details <- readMutVar ref
301 Indirect ty -> return (IndirectTv False ty)
302 Flexi -> return FlexiTv
305 -- Look up a meta type variable, conditionally consulting
306 -- the current type refinement
307 condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
308 condLookupTcTyVar use_refinement tyvar
309 | use_refinement = lookupTcTyVar tyvar
311 = case tcTyVarDetails tyvar of
312 SkolemTv _ -> return RigidTv
313 MetaTv ref -> do { details <- readMutVar ref
315 Indirect ty -> return (IndirectTv False ty)
316 Flexi -> return FlexiTv
320 -- gaw 2004 We aren't shorting anything out anymore, at least for now
322 | not (isTcTyVar tyvar)
323 = pprTrace "getTcTyVar" (ppr tyvar) $
324 returnM (Just (mkTyVarTy tyvar))
327 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
328 readMetaTyVar tyvar `thenM` \ maybe_ty ->
330 Just ty -> short_out ty `thenM` \ ty' ->
331 writeMetaTyVar tyvar (Just ty') `thenM_`
334 Nothing -> returnM Nothing
336 short_out :: TcType -> TcM TcType
337 short_out ty@(TyVarTy tyvar)
338 | not (isTcTyVar tyvar)
342 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
344 Just ty' -> short_out ty' `thenM` \ ty' ->
345 writeMetaTyVar tyvar (Just ty') `thenM_`
350 short_out other_ty = returnM other_ty
355 %************************************************************************
357 \subsection{Zonking -- the exernal interfaces}
359 %************************************************************************
361 ----------------- Type variables
364 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
365 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
367 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
368 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
369 returnM (tyVarsOfTypes tys)
371 zonkTcTyVar :: TcTyVar -> TcM TcType
372 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) True tyvar
375 ----------------- Types
378 zonkTcType :: TcType -> TcM TcType
379 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) True ty
381 zonkTcTypes :: [TcType] -> TcM [TcType]
382 zonkTcTypes tys = mappM zonkTcType tys
384 zonkTcClassConstraints cts = mappM zonk cts
385 where zonk (clas, tys)
386 = zonkTcTypes tys `thenM` \ new_tys ->
387 returnM (clas, new_tys)
389 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
390 zonkTcThetaType theta = mappM zonkTcPredType theta
392 zonkTcPredType :: TcPredType -> TcM TcPredType
393 zonkTcPredType (ClassP c ts)
394 = zonkTcTypes ts `thenM` \ new_ts ->
395 returnM (ClassP c new_ts)
396 zonkTcPredType (IParam n t)
397 = zonkTcType t `thenM` \ new_t ->
398 returnM (IParam n new_t)
401 ------------------- These ...ToType, ...ToKind versions
402 are used at the end of type checking
405 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
406 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
407 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
408 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
409 -- The meta tyvar is updated to point to the new regular TyVar. Now any
410 -- bound occurences of the original type variable will get zonked to
411 -- the immutable version.
413 -- We leave skolem TyVars alone; they are imutable.
414 zonkQuantifiedTyVar tv
415 | isSkolemTyVar tv = return tv
416 -- It might be a skolem type variable,
417 -- for example from a user type signature
419 | otherwise -- It's a meta-type-variable
420 = do { details <- readMetaTyVar tv
422 -- Create the new, frozen, regular type variable
423 ; let final_kind = defaultKind (tyVarKind tv)
424 final_tv = mkTyVar (tyVarName tv) final_kind
426 -- Bind the meta tyvar to the new tyvar
428 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
430 -- [Sept 04] I don't think this should happen
431 -- See note [Silly Type Synonym]
433 other -> writeMetaTyVar tv (Indirect (mkTyVarTy final_tv))
435 -- Return the new tyvar
439 [Silly Type Synonyms]
442 type C u a = u -- Note 'a' unused
444 foo :: (forall a. C u a -> C u a) -> u
448 bar = foo (\t -> t + t)
450 * From the (\t -> t+t) we get type {Num d} => d -> d
453 * Now unify with type of foo's arg, and we get:
454 {Num (C d a)} => C d a -> C d a
457 * Now abstract over the 'a', but float out the Num (C d a) constraint
458 because it does not 'really' mention a. (see Type.tyVarsOfType)
459 The arg to foo becomes
462 * So we get a dict binding for Num (C d a), which is zonked to give
464 [Note Sept 04: now that we are zonking quantified type variables
465 on construction, the 'a' will be frozen as a regular tyvar on
466 quantification, so the floated dict will still have type (C d a).
467 Which renders this whole note moot; happily!]
469 * Then the /\a abstraction has a zonked 'a' in it.
471 All very silly. I think its harmless to ignore the problem. We'll end up with
472 a /\a in the final result but all the occurrences of a will be zonked to ()
475 %************************************************************************
477 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
479 %* For internal use only! *
481 %************************************************************************
484 -- For unbound, mutable tyvars, zonkType uses the function given to it
485 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
486 -- type variable and zonks the kind too
488 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
489 -- see zonkTcType, and zonkTcTypeToType
490 -> Bool -- Should we consult the current type refinement?
493 zonkType unbound_var_fn rflag ty
496 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
497 returnM (TyConApp tycon tys')
499 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
500 go ty2 `thenM` \ ty2' ->
501 returnM (NoteTy (SynNote ty1') ty2')
503 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
505 go (PredTy p) = go_pred p `thenM` \ p' ->
508 go (FunTy arg res) = go arg `thenM` \ arg' ->
509 go res `thenM` \ res' ->
510 returnM (FunTy arg' res')
512 go (AppTy fun arg) = go fun `thenM` \ fun' ->
513 go arg `thenM` \ arg' ->
514 returnM (mkAppTy fun' arg')
515 -- NB the mkAppTy; we might have instantiated a
516 -- type variable to a type constructor, so we need
517 -- to pull the TyConApp to the top.
519 -- The two interesting cases!
520 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn rflag tyvar
522 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
523 go ty `thenM` \ ty' ->
524 returnM (ForAllTy tyvar ty')
526 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
527 returnM (ClassP c tys')
528 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
529 returnM (IParam n ty')
531 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
532 -> Bool -- Consult the type refinement?
533 -> TcTyVar -> TcM TcType
534 zonkTyVar unbound_var_fn rflag tyvar
535 | not (isTcTyVar tyvar) -- When zonking (forall a. ...a...), the occurrences of
536 -- the quantified variable a are TyVars not TcTyVars
537 = returnM (TyVarTy tyvar)
540 = condLookupTcTyVar rflag tyvar `thenM` \ details ->
542 -- If b is true, the variable was refined, and therefore it is okay
543 -- to continue refining inside. Otherwise it was wobbly and we should
544 -- not refine further inside.
545 IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
546 FlexiTv -> unbound_var_fn tyvar -- Unbound flexi
547 RigidTv -> return (TyVarTy tyvar) -- Rigid, no zonking necessary
552 %************************************************************************
556 %************************************************************************
559 readKindVar :: KindVar -> TcM (Maybe TcKind)
560 writeKindVar :: KindVar -> TcKind -> TcM ()
561 readKindVar (KVar _ ref) = readMutVar ref
562 writeKindVar (KVar _ ref) val = writeMutVar ref (Just val)
565 zonkTcKind :: TcKind -> TcM TcKind
566 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
567 ; k2' <- zonkTcKind k2
568 ; returnM (FunKind k1' k2') }
569 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
572 Just k -> zonkTcKind k }
573 zonkTcKind other_kind = returnM other_kind
576 zonkTcKindToKind :: TcKind -> TcM Kind
577 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
578 ; k2' <- zonkTcKindToKind k2
579 ; returnM (FunKind k1' k2') }
581 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
583 Nothing -> return liftedTypeKind
584 Just k -> zonkTcKindToKind k }
586 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
587 zonkTcKindToKind other_kind = returnM other_kind
590 %************************************************************************
592 \subsection{Checking a user type}
594 %************************************************************************
596 When dealing with a user-written type, we first translate it from an HsType
597 to a Type, performing kind checking, and then check various things that should
598 be true about it. We don't want to perform these checks at the same time
599 as the initial translation because (a) they are unnecessary for interface-file
600 types and (b) when checking a mutually recursive group of type and class decls,
601 we can't "look" at the tycons/classes yet. Also, the checks are are rather
602 diverse, and used to really mess up the other code.
604 One thing we check for is 'rank'.
606 Rank 0: monotypes (no foralls)
607 Rank 1: foralls at the front only, Rank 0 inside
608 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
610 basic ::= tyvar | T basic ... basic
612 r2 ::= forall tvs. cxt => r2a
613 r2a ::= r1 -> r2a | basic
614 r1 ::= forall tvs. cxt => r0
615 r0 ::= r0 -> r0 | basic
617 Another thing is to check that type synonyms are saturated.
618 This might not necessarily show up in kind checking.
620 data T k = MkT (k Int)
626 = FunSigCtxt Name -- Function type signature
627 | ExprSigCtxt -- Expression type signature
628 | ConArgCtxt Name -- Data constructor argument
629 | TySynCtxt Name -- RHS of a type synonym decl
630 | GenPatCtxt -- Pattern in generic decl
631 -- f{| a+b |} (Inl x) = ...
632 | PatSigCtxt -- Type sig in pattern
634 | ResSigCtxt -- Result type sig
636 | ForSigCtxt Name -- Foreign inport or export signature
637 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
638 | DefaultDeclCtxt -- Types in a default declaration
640 -- Notes re TySynCtxt
641 -- We allow type synonyms that aren't types; e.g. type List = []
643 -- If the RHS mentions tyvars that aren't in scope, we'll
644 -- quantify over them:
645 -- e.g. type T = a->a
646 -- will become type T = forall a. a->a
648 -- With gla-exts that's right, but for H98 we should complain.
651 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
652 pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt
654 pprUserTypeCtxt ty (FunSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
655 pprUserTypeCtxt ty ExprSigCtxt = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
656 pprUserTypeCtxt ty (ConArgCtxt c) = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
657 pprUserTypeCtxt ty (TySynCtxt c) = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
658 nest 2 (ptext SLIT(", namely") <+> ppr ty)]
659 pprUserTypeCtxt ty GenPatCtxt = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
660 pprUserTypeCtxt ty PatSigCtxt = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
661 pprUserTypeCtxt ty ResSigCtxt = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
662 pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
663 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
664 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
666 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
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
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
691 actual_kind = typeKind ty
693 kind_ok = case ctxt of
694 TySynCtxt _ -> True -- Any kind will do
695 ResSigCtxt -> isOpenTypeKind actual_kind
696 ExprSigCtxt -> isOpenTypeKind actual_kind
697 GenPatCtxt -> isLiftedTypeKind actual_kind
698 ForSigCtxt _ -> isLiftedTypeKind actual_kind
699 other -> isArgTypeKind actual_kind
701 ubx_tup | not gla_exts = UT_NotOk
702 | otherwise = case ctxt of
706 -- Unboxed tuples ok in function results,
707 -- but for type synonyms we allow them even at
710 -- Check that the thing has kind Type, and is lifted if necessary
711 checkTc kind_ok (kindErr actual_kind) `thenM_`
713 -- Check the internal validity of the type itself
714 check_poly_type rank ubx_tup ty `thenM_`
716 traceTc (text "checkValidType done" <+> ppr ty)
721 data Rank = Rank Int | Arbitrary
723 decRank :: Rank -> Rank
724 decRank Arbitrary = Arbitrary
725 decRank (Rank n) = Rank (n-1)
727 ----------------------------------------
728 data UbxTupFlag = UT_Ok | UT_NotOk
729 -- The "Ok" version means "ok if -fglasgow-exts is on"
731 ----------------------------------------
732 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
733 check_poly_type (Rank 0) ubx_tup ty
734 = check_tau_type (Rank 0) ubx_tup ty
736 check_poly_type rank ubx_tup ty
738 (tvs, theta, tau) = tcSplitSigmaTy ty
740 check_valid_theta SigmaCtxt theta `thenM_`
741 check_tau_type (decRank rank) ubx_tup tau `thenM_`
742 checkFreeness tvs theta `thenM_`
743 checkAmbiguity tvs theta (tyVarsOfType tau)
745 ----------------------------------------
746 check_arg_type :: Type -> TcM ()
747 -- The sort of type that can instantiate a type variable,
748 -- or be the argument of a type constructor.
749 -- Not an unboxed tuple, not a forall.
750 -- Other unboxed types are very occasionally allowed as type
751 -- arguments depending on the kind of the type constructor
753 -- For example, we want to reject things like:
755 -- instance Ord a => Ord (forall s. T s a)
757 -- g :: T s (forall b.b)
759 -- NB: unboxed tuples can have polymorphic or unboxed args.
760 -- This happens in the workers for functions returning
761 -- product types with polymorphic components.
762 -- But not in user code.
763 -- Anyway, they are dealt with by a special case in check_tau_type
766 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
767 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
769 ----------------------------------------
770 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
771 -- Rank is allowed rank for function args
772 -- No foralls otherwise
774 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
775 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
776 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
778 -- Naked PredTys don't usually show up, but they can as a result of
779 -- {-# SPECIALISE instance Ord Char #-}
780 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
781 -- are handled, but the quick thing is just to permit PredTys here.
782 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
783 check_source_ty dflags TypeCtxt sty
785 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
786 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
787 = check_poly_type rank UT_NotOk arg_ty `thenM_`
788 check_tau_type rank UT_Ok res_ty
790 check_tau_type rank ubx_tup (AppTy ty1 ty2)
791 = check_arg_type ty1 `thenM_` check_arg_type ty2
793 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
794 -- Synonym notes are built only when the synonym is
795 -- saturated (see Type.mkSynTy)
796 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
798 -- If -fglasgow-exts then don't check the 'note' part.
799 -- This allows us to instantiate a synonym defn with a
800 -- for-all type, or with a partially-applied type synonym.
801 -- e.g. type T a b = a
804 -- Here, T is partially applied, so it's illegal in H98.
805 -- But if you expand S first, then T we get just
810 -- For H98, do check the un-expanded part
811 check_tau_type rank ubx_tup syn
814 check_tau_type rank ubx_tup ty
816 check_tau_type rank ubx_tup (NoteTy other_note ty)
817 = check_tau_type rank ubx_tup ty
819 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
821 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
822 -- synonym application, leaving it to checkValidType (i.e. right here)
824 checkTc syn_arity_ok arity_msg `thenM_`
825 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 }
840 syn_arity_ok = tc_arity <= n_args
841 -- It's OK to have an *over-applied* type synonym
842 -- data Tree a b = ...
843 -- type Foo a = Tree [a]
844 -- f :: Foo a b -> ...
846 tc_arity = tyConArity tc
848 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
849 ubx_tup_msg = ubxArgTyErr ty
851 ----------------------------------------
852 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
853 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
854 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
855 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
860 %************************************************************************
862 \subsection{Checking a theta or source type}
864 %************************************************************************
867 -- Enumerate the contexts in which a "source type", <S>, can occur
871 -- or (N a) where N is a newtype
874 = ClassSCCtxt Name -- Superclasses of clas
875 -- class <S> => C a where ...
876 | SigmaCtxt -- Theta part of a normal for-all type
877 -- f :: <S> => a -> a
878 | DataTyCtxt Name -- Theta part of a data decl
879 -- data <S> => T a = MkT a
880 | TypeCtxt -- Source type in an ordinary type
882 | InstThetaCtxt -- Context of an instance decl
883 -- instance <S> => C [a] where ...
884 | InstHeadCtxt -- Head of an instance decl
885 -- instance ... => Eq a where ...
887 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
888 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
889 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
890 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
891 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
892 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
896 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
897 checkValidTheta ctxt theta
898 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
900 -------------------------
901 check_valid_theta ctxt []
903 check_valid_theta ctxt theta
904 = getDOpts `thenM` \ dflags ->
905 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
906 -- Actually, in instance decls and type signatures,
907 -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
908 -- so this error can only fire for the context of a class or
910 mappM_ (check_source_ty dflags ctxt) theta
912 (_,dups) = removeDups tcCmpPred theta
914 -------------------------
915 check_source_ty dflags ctxt pred@(ClassP cls tys)
916 = -- Class predicates are valid in all contexts
917 checkTc (arity == n_tys) arity_err `thenM_`
919 -- Check the form of the argument types
920 mappM_ check_arg_type tys `thenM_`
921 checkTc (check_class_pred_tys dflags ctxt tys)
922 (predTyVarErr pred $$ how_to_allow)
925 class_name = className cls
926 arity = classArity cls
928 arity_err = arityErr "Class" class_name arity n_tys
930 how_to_allow = case ctxt of
931 InstHeadCtxt -> empty -- Should not happen
932 InstThetaCtxt -> parens undecidableMsg
933 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
935 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
936 -- Implicit parameters only allows in type
937 -- signatures; not in instance decls, superclasses etc
938 -- The reason for not allowing implicit params in instances is a bit subtle
939 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
940 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
941 -- discharge all the potential usas of the ?x in e. For example, a
942 -- constraint Foo [Int] might come out of e,and applying the
943 -- instance decl would show up two uses of ?x.
946 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
948 -------------------------
949 check_class_pred_tys dflags ctxt tys
951 InstHeadCtxt -> True -- We check for instance-head
952 -- formation in checkValidInstHead
953 InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
954 other -> gla_exts || all tyvar_head tys
956 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
957 gla_exts = dopt Opt_GlasgowExts dflags
959 -------------------------
960 tyvar_head ty -- Haskell 98 allows predicates of form
961 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
962 | otherwise -- where a is a type variable
963 = case tcSplitAppTy_maybe ty of
964 Just (ty, _) -> tyvar_head ty
971 is ambiguous if P contains generic variables
972 (i.e. one of the Vs) that are not mentioned in tau
974 However, we need to take account of functional dependencies
975 when we speak of 'mentioned in tau'. Example:
976 class C a b | a -> b where ...
978 forall x y. (C x y) => x
979 is not ambiguous because x is mentioned and x determines y
981 NB; the ambiguity check is only used for *user* types, not for types
982 coming from inteface files. The latter can legitimately have
983 ambiguous types. Example
985 class S a where s :: a -> (Int,Int)
986 instance S Char where s _ = (1,1)
987 f:: S a => [a] -> Int -> (Int,Int)
988 f (_::[a]) x = (a*x,b)
989 where (a,b) = s (undefined::a)
991 Here the worker for f gets the type
992 fw :: forall a. S a => Int -> (# Int, Int #)
994 If the list of tv_names is empty, we have a monotype, and then we
995 don't need to check for ambiguity either, because the test can't fail
999 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1000 checkAmbiguity forall_tyvars theta tau_tyvars
1001 = mappM_ complain (filter is_ambig theta)
1003 complain pred = addErrTc (ambigErr pred)
1004 extended_tau_vars = grow theta tau_tyvars
1006 -- Only a *class* predicate can give rise to ambiguity
1007 -- An *implicit parameter* cannot. For example:
1008 -- foo :: (?x :: [a]) => Int
1010 -- is fine. The call site will suppply a particular 'x'
1011 is_ambig pred = isClassPred pred &&
1012 any ambig_var (varSetElems (tyVarsOfPred pred))
1014 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1015 not (ct_var `elemVarSet` extended_tau_vars)
1018 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1019 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1020 ptext SLIT("must be reachable from the type after the '=>'"))]
1023 In addition, GHC insists that at least one type variable
1024 in each constraint is in V. So we disallow a type like
1025 forall a. Eq b => b -> b
1026 even in a scope where b is in scope.
1029 checkFreeness forall_tyvars theta
1030 = mappM_ complain (filter is_free theta)
1032 is_free pred = not (isIPPred pred)
1033 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1034 bound_var ct_var = ct_var `elem` forall_tyvars
1035 complain pred = addErrTc (freeErr pred)
1038 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1039 ptext SLIT("are already in scope"),
1040 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1045 checkThetaCtxt ctxt theta
1046 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1047 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1049 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1050 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
1051 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1053 arityErr kind name n m
1054 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1055 n_arguments <> comma, text "but has been given", int m]
1057 n_arguments | n == 0 = ptext SLIT("no arguments")
1058 | n == 1 = ptext SLIT("1 argument")
1059 | True = hsep [int n, ptext SLIT("arguments")]
1063 %************************************************************************
1065 \subsection{Checking for a decent instance head type}
1067 %************************************************************************
1069 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1070 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1072 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1073 flag is on, or (2)~the instance is imported (they must have been
1074 compiled elsewhere). In these cases, we let them go through anyway.
1076 We can also have instances for functions: @instance Foo (a -> b) ...@.
1079 checkValidInstHead :: Type -> TcM (Class, [TcType])
1081 checkValidInstHead ty -- Should be a source type
1082 = case tcSplitPredTy_maybe ty of {
1083 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1086 case getClassPredTys_maybe pred of {
1087 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1090 getDOpts `thenM` \ dflags ->
1091 mappM_ check_arg_type tys `thenM_`
1092 check_inst_head dflags clas tys `thenM_`
1096 check_inst_head dflags clas tys
1097 -- If GlasgowExts then check at least one isn't a type variable
1098 | dopt Opt_GlasgowExts dflags
1099 = check_tyvars dflags clas tys
1101 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1103 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1104 not (isSynTyCon tycon), -- ...but not a synonym
1105 all tcIsTyVarTy arg_tys, -- Applied to type variables
1106 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1107 -- This last condition checks that all the type variables are distinct
1111 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1114 (first_ty : _) = tys
1116 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1117 text "where T is not a synonym, and a,b,c are distinct type variables")
1119 check_tyvars dflags clas tys
1120 -- Check that at least one isn't a type variable
1121 -- unless -fallow-undecideable-instances
1122 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1123 | not (all tcIsTyVarTy tys) = returnM ()
1124 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1126 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1129 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1133 instTypeErr pp_ty msg
1134 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,