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, tcInstSigType,
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, mkSystemName, getOccName )
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
180 tcInstTyVar tyvar -- Use the OccName of the tyvar we are instantiating
181 -- but make a System Name, so that it's updated in
182 -- preference to a tcInstSigTyVar
183 = do { uniq <- newUnique
184 ; newMetaTyVar (mkSystemName uniq (getOccName tyvar))
185 (tyVarKind tyvar) Flexi }
187 tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
188 -- tcInstType instantiates the outer-level for-alls of a TcType with
189 -- fresh (mutable) type variables, splits off the dictionary part,
190 -- and returns the pieces.
191 tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty
194 ---------------------------------------------
195 tcInstSigType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
196 -- Instantiate a type with fresh meta type variables, but
197 -- ones which have the same Name as the original type
198 -- variable. This is used for type signatures, where we must
199 -- instantiate with meta type variables, but we'd like to avoid
200 -- instantiating them were possible; and the unifier unifies
201 -- tyvars with System Names by preference
203 -- We don't need a fresh unique, because the renamer has made them
204 -- unique, and it's better not to do so because we extend the envt
205 -- with them as scoped type variables, and we'd like to avoid spurious
206 -- 's = s' bindings in error messages
207 tcInstSigType ty = tc_inst_type tcInstSigTyVars ty
209 tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
210 tcInstSigTyVars tyvars
213 new_tv tv = newMetaTyVar (tyVarName tv) (tyVarKind tv) Flexi
216 ---------------------------------------------
217 tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
218 -- Instantiate a type with fresh skolem constants
219 tcSkolType info ty = tc_inst_type (tcSkolTyVars info) ty
221 tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
222 tcSkolTyVars info tyvars
223 = do { us <- newUniqueSupply
224 ; return (zipWith skol_tv tyvars (uniqsFromSupply us)) }
226 skol_tv tv uniq = mkTcTyVar (setNameUnique (tyVarName tv) uniq)
227 (tyVarKind tv) (SkolemTv info)
228 -- See Note [TyVarName]
231 ---------------------------------------------
232 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
233 -- Instantiate a type signature with skolem constants, but
234 -- do *not* give them fresh names, because we want the name to
235 -- be in the type environment -- it is lexically scoped.
236 tcSkolSigType info ty
237 = tc_inst_type (\tvs -> return (tcSkolSigTyVars info tvs)) ty
239 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
240 tcSkolSigTyVars info tyvars = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info)
243 -----------------------
244 tc_inst_type :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
245 -> TcType -- Type to instantiate
246 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
247 tc_inst_type inst_tyvars ty
248 = case tcSplitForAllTys ty of
249 ([], rho) -> let -- There may be overloading despite no type variables;
250 -- (?x :: Int) => Int -> Int
251 (theta, tau) = tcSplitPhiTy rho
253 return ([], theta, tau)
255 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
257 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
258 -- Either the tyvars are freshly made, by inst_tyvars,
259 -- or (in the call from tcSkolSigType) any nested foralls
260 -- have different binders. Either way, zipTopTvSubst is ok
262 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
263 ; return (tyvars', theta, tau) }
267 %************************************************************************
269 \subsection{Putting and getting mutable type variables}
271 %************************************************************************
274 putMetaTyVar :: TcTyVar -> TcType -> TcM ()
276 putMetaTyVar tyvar ty = writeMetaTyVar tyvar (Indirect ty)
278 putMetaTyVar tyvar ty
279 | not (isMetaTyVar tyvar)
280 = pprTrace "putTcTyVar" (ppr tyvar) $
284 = ASSERT( isMetaTyVar tyvar )
285 ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
286 do { ASSERTM( do { details <- readMetaTyVar tyvar; return (isFlexi details) } )
287 ; writeMetaTyVar tyvar (Indirect ty) }
294 But it's more fun to short out indirections on the way: If this
295 version returns a TyVar, then that TyVar is unbound. If it returns
296 any other type, then there might be bound TyVars embedded inside it.
298 We return Nothing iff the original box was unbound.
301 data LookupTyVarResult -- The result of a lookupTcTyVar call
304 | IndirectTv Bool TcType
305 -- True => This is a non-wobbly type refinement,
306 -- gotten from GADT match unification
307 -- False => This is a wobbly type,
308 -- gotten from inference unification
310 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
311 -- This function is the ONLY PLACE that we consult the
312 -- type refinement carried by the monad
314 -- The boolean returned with Indirect
316 = case tcTyVarDetails tyvar of
317 SkolemTv _ -> do { type_reft <- getTypeRefinement
318 ; case lookupVarEnv type_reft tyvar of
319 Just ty -> return (IndirectTv True ty)
320 Nothing -> return RigidTv
322 MetaTv ref -> do { details <- readMutVar ref
324 Indirect ty -> return (IndirectTv False ty)
325 Flexi -> return FlexiTv
328 -- Look up a meta type variable, conditionally consulting
329 -- the current type refinement
330 condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
331 condLookupTcTyVar use_refinement tyvar
332 | use_refinement = lookupTcTyVar tyvar
334 = case tcTyVarDetails tyvar of
335 SkolemTv _ -> return RigidTv
336 MetaTv ref -> do { details <- readMutVar ref
338 Indirect ty -> return (IndirectTv False ty)
339 Flexi -> return FlexiTv
343 -- gaw 2004 We aren't shorting anything out anymore, at least for now
345 | not (isTcTyVar tyvar)
346 = pprTrace "getTcTyVar" (ppr tyvar) $
347 returnM (Just (mkTyVarTy tyvar))
350 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
351 readMetaTyVar tyvar `thenM` \ maybe_ty ->
353 Just ty -> short_out ty `thenM` \ ty' ->
354 writeMetaTyVar tyvar (Just ty') `thenM_`
357 Nothing -> returnM Nothing
359 short_out :: TcType -> TcM TcType
360 short_out ty@(TyVarTy tyvar)
361 | not (isTcTyVar tyvar)
365 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
367 Just ty' -> short_out ty' `thenM` \ ty' ->
368 writeMetaTyVar tyvar (Just ty') `thenM_`
373 short_out other_ty = returnM other_ty
378 %************************************************************************
380 \subsection{Zonking -- the exernal interfaces}
382 %************************************************************************
384 ----------------- Type variables
387 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
388 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
390 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
391 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
392 returnM (tyVarsOfTypes tys)
394 zonkTcTyVar :: TcTyVar -> TcM TcType
395 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) True tyvar
398 ----------------- Types
401 zonkTcType :: TcType -> TcM TcType
402 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) True ty
404 zonkTcTypes :: [TcType] -> TcM [TcType]
405 zonkTcTypes tys = mappM zonkTcType tys
407 zonkTcClassConstraints cts = mappM zonk cts
408 where zonk (clas, tys)
409 = zonkTcTypes tys `thenM` \ new_tys ->
410 returnM (clas, new_tys)
412 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
413 zonkTcThetaType theta = mappM zonkTcPredType theta
415 zonkTcPredType :: TcPredType -> TcM TcPredType
416 zonkTcPredType (ClassP c ts)
417 = zonkTcTypes ts `thenM` \ new_ts ->
418 returnM (ClassP c new_ts)
419 zonkTcPredType (IParam n t)
420 = zonkTcType t `thenM` \ new_t ->
421 returnM (IParam n new_t)
424 ------------------- These ...ToType, ...ToKind versions
425 are used at the end of type checking
428 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
429 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
430 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
431 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
432 -- The meta tyvar is updated to point to the new regular TyVar. Now any
433 -- bound occurences of the original type variable will get zonked to
434 -- the immutable version.
436 -- We leave skolem TyVars alone; they are immutable.
437 zonkQuantifiedTyVar tv
438 | isSkolemTyVar tv = return tv
439 -- It might be a skolem type variable,
440 -- for example from a user type signature
442 | otherwise -- It's a meta-type-variable
443 = do { details <- readMetaTyVar tv
445 -- Create the new, frozen, regular type variable
446 ; let final_kind = defaultKind (tyVarKind tv)
447 final_tv = mkTyVar (tyVarName tv) final_kind
449 -- Bind the meta tyvar to the new tyvar
451 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
453 -- [Sept 04] I don't think this should happen
454 -- See note [Silly Type Synonym]
456 other -> writeMetaTyVar tv (Indirect (mkTyVarTy final_tv))
458 -- Return the new tyvar
462 [Silly Type Synonyms]
465 type C u a = u -- Note 'a' unused
467 foo :: (forall a. C u a -> C u a) -> u
471 bar = foo (\t -> t + t)
473 * From the (\t -> t+t) we get type {Num d} => d -> d
476 * Now unify with type of foo's arg, and we get:
477 {Num (C d a)} => C d a -> C d a
480 * Now abstract over the 'a', but float out the Num (C d a) constraint
481 because it does not 'really' mention a. (see Type.tyVarsOfType)
482 The arg to foo becomes
485 * So we get a dict binding for Num (C d a), which is zonked to give
487 [Note Sept 04: now that we are zonking quantified type variables
488 on construction, the 'a' will be frozen as a regular tyvar on
489 quantification, so the floated dict will still have type (C d a).
490 Which renders this whole note moot; happily!]
492 * Then the /\a abstraction has a zonked 'a' in it.
494 All very silly. I think its harmless to ignore the problem. We'll end up with
495 a /\a in the final result but all the occurrences of a will be zonked to ()
498 %************************************************************************
500 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
502 %* For internal use only! *
504 %************************************************************************
507 -- For unbound, mutable tyvars, zonkType uses the function given to it
508 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
509 -- type variable and zonks the kind too
511 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
512 -- see zonkTcType, and zonkTcTypeToType
513 -> Bool -- Should we consult the current type refinement?
516 zonkType unbound_var_fn rflag ty
519 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
520 returnM (TyConApp tycon tys')
522 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
523 go ty2 `thenM` \ ty2' ->
524 returnM (NoteTy (SynNote ty1') ty2')
526 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
528 go (PredTy p) = go_pred p `thenM` \ p' ->
531 go (FunTy arg res) = go arg `thenM` \ arg' ->
532 go res `thenM` \ res' ->
533 returnM (FunTy arg' res')
535 go (AppTy fun arg) = go fun `thenM` \ fun' ->
536 go arg `thenM` \ arg' ->
537 returnM (mkAppTy fun' arg')
538 -- NB the mkAppTy; we might have instantiated a
539 -- type variable to a type constructor, so we need
540 -- to pull the TyConApp to the top.
542 -- The two interesting cases!
543 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn rflag tyvar
545 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
546 go ty `thenM` \ ty' ->
547 returnM (ForAllTy tyvar ty')
549 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
550 returnM (ClassP c tys')
551 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
552 returnM (IParam n ty')
554 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
555 -> Bool -- Consult the type refinement?
556 -> TcTyVar -> TcM TcType
557 zonkTyVar unbound_var_fn rflag tyvar
558 | not (isTcTyVar tyvar) -- When zonking (forall a. ...a...), the occurrences of
559 -- the quantified variable 'a' are TyVars not TcTyVars
560 = returnM (TyVarTy tyvar)
563 = condLookupTcTyVar rflag tyvar `thenM` \ details ->
565 -- If b is true, the variable was refined, and therefore it is okay
566 -- to continue refining inside. Otherwise it was wobbly and we should
567 -- not refine further inside.
568 IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
569 FlexiTv -> unbound_var_fn tyvar -- Unbound flexi
570 RigidTv -> return (TyVarTy tyvar) -- Rigid, no zonking necessary
575 %************************************************************************
579 %************************************************************************
582 readKindVar :: KindVar -> TcM (Maybe TcKind)
583 writeKindVar :: KindVar -> TcKind -> TcM ()
584 readKindVar (KVar _ ref) = readMutVar ref
585 writeKindVar (KVar _ ref) val = writeMutVar ref (Just val)
588 zonkTcKind :: TcKind -> TcM TcKind
589 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
590 ; k2' <- zonkTcKind k2
591 ; returnM (FunKind k1' k2') }
592 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
595 Just k -> zonkTcKind k }
596 zonkTcKind other_kind = returnM other_kind
599 zonkTcKindToKind :: TcKind -> TcM Kind
600 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
601 ; k2' <- zonkTcKindToKind k2
602 ; returnM (FunKind k1' k2') }
604 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
606 Nothing -> return liftedTypeKind
607 Just k -> zonkTcKindToKind k }
609 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
610 zonkTcKindToKind other_kind = returnM other_kind
613 %************************************************************************
615 \subsection{Checking a user type}
617 %************************************************************************
619 When dealing with a user-written type, we first translate it from an HsType
620 to a Type, performing kind checking, and then check various things that should
621 be true about it. We don't want to perform these checks at the same time
622 as the initial translation because (a) they are unnecessary for interface-file
623 types and (b) when checking a mutually recursive group of type and class decls,
624 we can't "look" at the tycons/classes yet. Also, the checks are are rather
625 diverse, and used to really mess up the other code.
627 One thing we check for is 'rank'.
629 Rank 0: monotypes (no foralls)
630 Rank 1: foralls at the front only, Rank 0 inside
631 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
633 basic ::= tyvar | T basic ... basic
635 r2 ::= forall tvs. cxt => r2a
636 r2a ::= r1 -> r2a | basic
637 r1 ::= forall tvs. cxt => r0
638 r0 ::= r0 -> r0 | basic
640 Another thing is to check that type synonyms are saturated.
641 This might not necessarily show up in kind checking.
643 data T k = MkT (k Int)
649 = FunSigCtxt Name -- Function type signature
650 | ExprSigCtxt -- Expression type signature
651 | ConArgCtxt Name -- Data constructor argument
652 | TySynCtxt Name -- RHS of a type synonym decl
653 | GenPatCtxt -- Pattern in generic decl
654 -- f{| a+b |} (Inl x) = ...
655 | PatSigCtxt -- Type sig in pattern
657 | ResSigCtxt -- Result type sig
659 | ForSigCtxt Name -- Foreign inport or export signature
660 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
661 | DefaultDeclCtxt -- Types in a default declaration
663 -- Notes re TySynCtxt
664 -- We allow type synonyms that aren't types; e.g. type List = []
666 -- If the RHS mentions tyvars that aren't in scope, we'll
667 -- quantify over them:
668 -- e.g. type T = a->a
669 -- will become type T = forall a. a->a
671 -- With gla-exts that's right, but for H98 we should complain.
674 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
675 pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt
677 pprUserTypeCtxt ty (FunSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
678 pprUserTypeCtxt ty ExprSigCtxt = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
679 pprUserTypeCtxt ty (ConArgCtxt c) = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
680 pprUserTypeCtxt ty (TySynCtxt c) = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
681 nest 2 (ptext SLIT(", namely") <+> ppr ty)]
682 pprUserTypeCtxt ty GenPatCtxt = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
683 pprUserTypeCtxt ty PatSigCtxt = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
684 pprUserTypeCtxt ty ResSigCtxt = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
685 pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
686 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
687 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
689 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
693 checkValidType :: UserTypeCtxt -> Type -> TcM ()
694 -- Checks that the type is valid for the given context
695 checkValidType ctxt ty
696 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
697 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
699 rank | gla_exts = Arbitrary
701 = case ctxt of -- Haskell 98
704 DefaultDeclCtxt-> Rank 0
706 TySynCtxt _ -> Rank 0
707 ExprSigCtxt -> Rank 1
708 FunSigCtxt _ -> Rank 1
709 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
710 -- constructor, hence rank 1
711 ForSigCtxt _ -> Rank 1
712 RuleSigCtxt _ -> Rank 1
714 actual_kind = typeKind ty
716 kind_ok = case ctxt of
717 TySynCtxt _ -> True -- Any kind will do
718 ResSigCtxt -> isOpenTypeKind actual_kind
719 ExprSigCtxt -> isOpenTypeKind actual_kind
720 GenPatCtxt -> isLiftedTypeKind actual_kind
721 ForSigCtxt _ -> isLiftedTypeKind actual_kind
722 other -> isArgTypeKind actual_kind
724 ubx_tup | not gla_exts = UT_NotOk
725 | otherwise = case ctxt of
729 -- Unboxed tuples ok in function results,
730 -- but for type synonyms we allow them even at
733 -- Check that the thing has kind Type, and is lifted if necessary
734 checkTc kind_ok (kindErr actual_kind) `thenM_`
736 -- Check the internal validity of the type itself
737 check_poly_type rank ubx_tup ty `thenM_`
739 traceTc (text "checkValidType done" <+> ppr ty)
744 data Rank = Rank Int | Arbitrary
746 decRank :: Rank -> Rank
747 decRank Arbitrary = Arbitrary
748 decRank (Rank n) = Rank (n-1)
750 ----------------------------------------
751 data UbxTupFlag = UT_Ok | UT_NotOk
752 -- The "Ok" version means "ok if -fglasgow-exts is on"
754 ----------------------------------------
755 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
756 check_poly_type (Rank 0) ubx_tup ty
757 = check_tau_type (Rank 0) ubx_tup ty
759 check_poly_type rank ubx_tup ty
761 (tvs, theta, tau) = tcSplitSigmaTy ty
763 check_valid_theta SigmaCtxt theta `thenM_`
764 check_tau_type (decRank rank) ubx_tup tau `thenM_`
765 checkFreeness tvs theta `thenM_`
766 checkAmbiguity tvs theta (tyVarsOfType tau)
768 ----------------------------------------
769 check_arg_type :: Type -> TcM ()
770 -- The sort of type that can instantiate a type variable,
771 -- or be the argument of a type constructor.
772 -- Not an unboxed tuple, not a forall.
773 -- Other unboxed types are very occasionally allowed as type
774 -- arguments depending on the kind of the type constructor
776 -- For example, we want to reject things like:
778 -- instance Ord a => Ord (forall s. T s a)
780 -- g :: T s (forall b.b)
782 -- NB: unboxed tuples can have polymorphic or unboxed args.
783 -- This happens in the workers for functions returning
784 -- product types with polymorphic components.
785 -- But not in user code.
786 -- Anyway, they are dealt with by a special case in check_tau_type
789 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
790 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
792 ----------------------------------------
793 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
794 -- Rank is allowed rank for function args
795 -- No foralls otherwise
797 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
798 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
799 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
801 -- Naked PredTys don't usually show up, but they can as a result of
802 -- {-# SPECIALISE instance Ord Char #-}
803 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
804 -- are handled, but the quick thing is just to permit PredTys here.
805 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
806 check_source_ty dflags TypeCtxt sty
808 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
809 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
810 = check_poly_type rank UT_NotOk arg_ty `thenM_`
811 check_tau_type rank UT_Ok res_ty
813 check_tau_type rank ubx_tup (AppTy ty1 ty2)
814 = check_arg_type ty1 `thenM_` check_arg_type ty2
816 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
817 -- Synonym notes are built only when the synonym is
818 -- saturated (see Type.mkSynTy)
819 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
821 -- If -fglasgow-exts then don't check the 'note' part.
822 -- This allows us to instantiate a synonym defn with a
823 -- for-all type, or with a partially-applied type synonym.
824 -- e.g. type T a b = a
827 -- Here, T is partially applied, so it's illegal in H98.
828 -- But if you expand S first, then T we get just
833 -- For H98, do check the un-expanded part
834 check_tau_type rank ubx_tup syn
837 check_tau_type rank ubx_tup ty
839 check_tau_type rank ubx_tup (NoteTy other_note ty)
840 = check_tau_type rank ubx_tup ty
842 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
844 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
845 -- synonym application, leaving it to checkValidType (i.e. right here)
847 checkTc syn_arity_ok arity_msg `thenM_`
848 mappM_ check_arg_type tys
850 | isUnboxedTupleTyCon tc
851 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
852 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
853 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
854 -- Args are allowed to be unlifted, or
855 -- more unboxed tuples, so can't use check_arg_ty
858 = mappM_ check_arg_type tys
861 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
863 syn_arity_ok = tc_arity <= n_args
864 -- It's OK to have an *over-applied* type synonym
865 -- data Tree a b = ...
866 -- type Foo a = Tree [a]
867 -- f :: Foo a b -> ...
869 tc_arity = tyConArity tc
871 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
872 ubx_tup_msg = ubxArgTyErr ty
874 ----------------------------------------
875 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
876 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
877 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
878 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
883 %************************************************************************
885 \subsection{Checking a theta or source type}
887 %************************************************************************
890 -- Enumerate the contexts in which a "source type", <S>, can occur
894 -- or (N a) where N is a newtype
897 = ClassSCCtxt Name -- Superclasses of clas
898 -- class <S> => C a where ...
899 | SigmaCtxt -- Theta part of a normal for-all type
900 -- f :: <S> => a -> a
901 | DataTyCtxt Name -- Theta part of a data decl
902 -- data <S> => T a = MkT a
903 | TypeCtxt -- Source type in an ordinary type
905 | InstThetaCtxt -- Context of an instance decl
906 -- instance <S> => C [a] where ...
907 | InstHeadCtxt -- Head of an instance decl
908 -- instance ... => Eq a where ...
910 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
911 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
912 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
913 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
914 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
915 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
919 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
920 checkValidTheta ctxt theta
921 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
923 -------------------------
924 check_valid_theta ctxt []
926 check_valid_theta ctxt theta
927 = getDOpts `thenM` \ dflags ->
928 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
929 -- Actually, in instance decls and type signatures,
930 -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
931 -- so this error can only fire for the context of a class or
933 mappM_ (check_source_ty dflags ctxt) theta
935 (_,dups) = removeDups tcCmpPred theta
937 -------------------------
938 check_source_ty dflags ctxt pred@(ClassP cls tys)
939 = -- Class predicates are valid in all contexts
940 checkTc (arity == n_tys) arity_err `thenM_`
942 -- Check the form of the argument types
943 mappM_ check_arg_type tys `thenM_`
944 checkTc (check_class_pred_tys dflags ctxt tys)
945 (predTyVarErr pred $$ how_to_allow)
948 class_name = className cls
949 arity = classArity cls
951 arity_err = arityErr "Class" class_name arity n_tys
953 how_to_allow = case ctxt of
954 InstHeadCtxt -> empty -- Should not happen
955 InstThetaCtxt -> parens undecidableMsg
956 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
958 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
959 -- Implicit parameters only allows in type
960 -- signatures; not in instance decls, superclasses etc
961 -- The reason for not allowing implicit params in instances is a bit subtle
962 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
963 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
964 -- discharge all the potential usas of the ?x in e. For example, a
965 -- constraint Foo [Int] might come out of e,and applying the
966 -- instance decl would show up two uses of ?x.
969 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
971 -------------------------
972 check_class_pred_tys dflags ctxt tys
974 InstHeadCtxt -> True -- We check for instance-head
975 -- formation in checkValidInstHead
976 InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
977 other -> gla_exts || all tyvar_head tys
979 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
980 gla_exts = dopt Opt_GlasgowExts dflags
982 -------------------------
983 tyvar_head ty -- Haskell 98 allows predicates of form
984 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
985 | otherwise -- where a is a type variable
986 = case tcSplitAppTy_maybe ty of
987 Just (ty, _) -> tyvar_head ty
994 is ambiguous if P contains generic variables
995 (i.e. one of the Vs) that are not mentioned in tau
997 However, we need to take account of functional dependencies
998 when we speak of 'mentioned in tau'. Example:
999 class C a b | a -> b where ...
1001 forall x y. (C x y) => x
1002 is not ambiguous because x is mentioned and x determines y
1004 NB; the ambiguity check is only used for *user* types, not for types
1005 coming from inteface files. The latter can legitimately have
1006 ambiguous types. Example
1008 class S a where s :: a -> (Int,Int)
1009 instance S Char where s _ = (1,1)
1010 f:: S a => [a] -> Int -> (Int,Int)
1011 f (_::[a]) x = (a*x,b)
1012 where (a,b) = s (undefined::a)
1014 Here the worker for f gets the type
1015 fw :: forall a. S a => Int -> (# Int, Int #)
1017 If the list of tv_names is empty, we have a monotype, and then we
1018 don't need to check for ambiguity either, because the test can't fail
1022 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1023 checkAmbiguity forall_tyvars theta tau_tyvars
1024 = mappM_ complain (filter is_ambig theta)
1026 complain pred = addErrTc (ambigErr pred)
1027 extended_tau_vars = grow theta tau_tyvars
1029 -- Only a *class* predicate can give rise to ambiguity
1030 -- An *implicit parameter* cannot. For example:
1031 -- foo :: (?x :: [a]) => Int
1033 -- is fine. The call site will suppply a particular 'x'
1034 is_ambig pred = isClassPred pred &&
1035 any ambig_var (varSetElems (tyVarsOfPred pred))
1037 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1038 not (ct_var `elemVarSet` extended_tau_vars)
1041 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1042 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1043 ptext SLIT("must be reachable from the type after the '=>'"))]
1046 In addition, GHC insists that at least one type variable
1047 in each constraint is in V. So we disallow a type like
1048 forall a. Eq b => b -> b
1049 even in a scope where b is in scope.
1052 checkFreeness forall_tyvars theta
1053 = mappM_ complain (filter is_free theta)
1055 is_free pred = not (isIPPred pred)
1056 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1057 bound_var ct_var = ct_var `elem` forall_tyvars
1058 complain pred = addErrTc (freeErr pred)
1061 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1062 ptext SLIT("are already in scope"),
1063 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1068 checkThetaCtxt ctxt theta
1069 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1070 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1072 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1073 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
1074 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1076 arityErr kind name n m
1077 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1078 n_arguments <> comma, text "but has been given", int m]
1080 n_arguments | n == 0 = ptext SLIT("no arguments")
1081 | n == 1 = ptext SLIT("1 argument")
1082 | True = hsep [int n, ptext SLIT("arguments")]
1086 %************************************************************************
1088 \subsection{Checking for a decent instance head type}
1090 %************************************************************************
1092 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1093 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1095 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1096 flag is on, or (2)~the instance is imported (they must have been
1097 compiled elsewhere). In these cases, we let them go through anyway.
1099 We can also have instances for functions: @instance Foo (a -> b) ...@.
1102 checkValidInstHead :: Type -> TcM (Class, [TcType])
1104 checkValidInstHead ty -- Should be a source type
1105 = case tcSplitPredTy_maybe ty of {
1106 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1109 case getClassPredTys_maybe pred of {
1110 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1113 getDOpts `thenM` \ dflags ->
1114 mappM_ check_arg_type tys `thenM_`
1115 check_inst_head dflags clas tys `thenM_`
1119 check_inst_head dflags clas tys
1120 -- If GlasgowExts then check at least one isn't a type variable
1121 | dopt Opt_GlasgowExts dflags
1122 = check_tyvars dflags clas tys
1124 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1126 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1127 not (isSynTyCon tycon), -- ...but not a synonym
1128 all tcIsTyVarTy arg_tys, -- Applied to type variables
1129 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1130 -- This last condition checks that all the type variables are distinct
1134 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1137 (first_ty : _) = tys
1139 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1140 text "where T is not a synonym, and a,b,c are distinct type variables")
1142 check_tyvars dflags clas tys
1143 -- Check that at least one isn't a type variable
1144 -- unless -fallow-undecideable-instances
1145 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1146 | not (all tcIsTyVarTy tys) = returnM ()
1147 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1149 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1152 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1156 instTypeErr pp_ty msg
1157 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,