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 tcSkolTyVar, tcSkolTyVars, tcSkolType,
26 --------------------------------
27 -- Checking type validity
28 Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
29 SourceTyCtxt(..), checkValidTheta, checkFreeness,
30 checkValidInstHead, instTypeErr, checkAmbiguity,
31 arityErr, isRigidType,
33 --------------------------------
35 zonkType, zonkTcPredType,
36 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
37 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
38 zonkTcKindToKind, zonkTcKind,
40 readKindVar, writeKindVar
44 #include "HsVersions.h"
48 import HsSyn ( LHsType )
49 import TypeRep ( Type(..), PredType(..), TyNote(..), -- Friend; can see representation
52 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
53 TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
54 MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef,
55 tcCmpPred, isClassPred,
56 tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
57 tcSplitTyConApp_maybe, tcSplitForAllTys,
58 tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy,
59 isUnLiftedType, isIPPred, isImmutableTyVar,
60 typeKind, isFlexi, isSkolemTyVar,
61 mkAppTy, mkTyVarTy, mkTyVarTys,
62 tyVarsOfPred, getClassPredTys_maybe,
63 tyVarsOfType, tyVarsOfTypes,
64 pprPred, pprTheta, pprClassPred )
65 import Kind ( Kind(..), KindVar(..), mkKindVar, isSubKind,
66 isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
67 liftedTypeKind, defaultKind
69 import Type ( TvSubst, zipTopTvSubst, substTy )
70 import Class ( Class, classArity, className )
71 import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
72 tyConArity, tyConName )
73 import Var ( TyVar, tyVarKind, tyVarName,
74 mkTyVar, mkTcTyVar, tcTyVarDetails, isTcTyVar )
77 import TcRnMonad -- TcType, amongst others
78 import FunDeps ( grow )
79 import Name ( Name, setNameUnique, mkSysTvName )
82 import CmdLineOpts ( dopt, DynFlag(..) )
83 import Util ( nOfThem, isSingleton, equalLength, notNull )
84 import ListSetOps ( removeDups )
85 import SrcLoc ( unLoc )
90 %************************************************************************
92 \subsection{New type variables}
94 %************************************************************************
97 newMetaTyVar :: Name -> Kind -> MetaDetails -> TcM TyVar
98 newMetaTyVar name kind details
99 = do { ref <- newMutVar details ;
100 return (mkTcTyVar name kind (MetaTv ref)) }
102 readMetaTyVar :: TyVar -> TcM MetaDetails
103 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
104 readMutVar (metaTvRef tyvar)
106 writeMetaTyVar :: TyVar -> MetaDetails -> TcM ()
107 writeMetaTyVar tyvar val = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
108 writeMutVar (metaTvRef tyvar) val
110 newFlexiTyVar :: Kind -> TcM TcTyVar
112 = newUnique `thenM` \ uniq ->
113 newMetaTyVar (mkSysTvName uniq FSLIT("t")) kind Flexi
115 newTyFlexiVarTy :: Kind -> TcM TcType
117 = newFlexiTyVar kind `thenM` \ tc_tyvar ->
118 returnM (TyVarTy tc_tyvar)
120 newTyFlexiVarTys :: Int -> Kind -> TcM [TcType]
121 newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind)
123 isRigidType :: TcType -> TcM Bool
124 -- Check that the type is rigid, *taking the type refinement into account*
125 -- In other words if a rigid type variable tv is refined to a wobbly type,
126 -- the answer should be False
127 -- ToDo: can this happen?
129 = do { rigids <- mapM is_rigid (varSetElems (tyVarsOfType ty))
130 ; return (and rigids) }
132 is_rigid tv = do { details <- lookupTcTyVar tv
134 RigidTv -> return True
135 IndirectTv True ty -> isRigidType ty
136 other -> return False
139 newKindVar :: TcM TcKind
140 newKindVar = do { uniq <- newUnique
141 ; ref <- newMutVar Nothing
142 ; return (KindVar (mkKindVar uniq ref)) }
144 newKindVars :: Int -> TcM [TcKind]
145 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
149 %************************************************************************
151 \subsection{Type instantiation}
153 %************************************************************************
155 Instantiating a bunch of type variables
159 Note that we don't change the print-name
160 This won't confuse the type checker but there's a chance
161 that two different tyvars will print the same way
162 in an error message. -dppr-debug will show up the difference
163 Better watch out for this. If worst comes to worst, just
168 -----------------------
169 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
171 = do { tc_tvs <- mappM tcInstTyVar tyvars
172 ; let tys = mkTyVarTys tc_tvs
173 ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
174 -- Since the tyvars are freshly made,
175 -- they cannot possibly be captured by
176 -- any existing for-alls. Hence zipTopTvSubst
179 = do { uniq <- newUnique
180 ; let name = setNameUnique (tyVarName tyvar) uniq
181 -- See Note [TyVarName]
182 ; newMetaTyVar name (tyVarKind tyvar) Flexi }
184 tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
185 -- tcInstType instantiates the outer-level for-alls of a TcType with
186 -- fresh (mutable) type variables, splits off the dictionary part,
187 -- and returns the pieces.
189 = case tcSplitForAllTys ty of
190 ([], rho) -> -- There may be overloading despite no type variables;
191 -- (?x :: Int) => Int -> Int
193 (theta, tau) = tcSplitPhiTy rho
195 returnM ([], theta, tau)
197 (tyvars, rho) -> tcInstTyVars tyvars `thenM` \ (tyvars', _, tenv) ->
199 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
201 returnM (tyvars', theta, tau)
203 ---------------------------------------------
204 -- Similar functions but for skolem constants
206 tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
207 tcSkolTyVars info tyvars = mappM (tcSkolTyVar info) tyvars
209 tcSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
210 tcSkolTyVar info tyvar
211 = do { uniq <- newUnique
212 ; let name = setNameUnique (tyVarName tyvar) uniq
213 -- See Note [TyVarName]
214 ; return (mkTcTyVar name (tyVarKind tyvar)
217 tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
219 = case tcSplitForAllTys ty of
221 (theta, tau) = tcSplitPhiTy rho
223 returnM ([], theta, tau)
225 (tyvars, rho) -> tcSkolTyVars info tyvars `thenM` \ tyvars' ->
227 tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
228 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
230 returnM (tyvars', theta, tau)
234 %************************************************************************
236 \subsection{Putting and getting mutable type variables}
238 %************************************************************************
241 putMetaTyVar :: TcTyVar -> TcType -> TcM ()
243 putMetaTyVar tyvar ty = writeMetaTyVar tyvar (Indirect ty)
245 putMetaTyVar tyvar ty
246 | not (isMetaTyVar tyvar)
247 = pprTrace "putTcTyVar" (ppr tyvar) $
251 = ASSERT( isMetaTyVar tyvar )
252 ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
253 do { ASSERTM( do { details <- readMetaTyVar tyvar; return (isFlexi details) } )
254 ; writeMetaTyVar tyvar (Indirect ty) }
261 But it's more fun to short out indirections on the way: If this
262 version returns a TyVar, then that TyVar is unbound. If it returns
263 any other type, then there might be bound TyVars embedded inside it.
265 We return Nothing iff the original box was unbound.
268 data LookupTyVarResult -- The result of a lookupTcTyVar call
271 | IndirectTv Bool TcType
272 -- True => This is a non-wobbly type refinement,
273 -- gotten from GADT match unification
274 -- False => This is a wobbly type,
275 -- gotten from inference unification
277 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
278 -- This function is the ONLY PLACE that we consult the
279 -- type refinement carried by the monad
281 -- The boolean returned with Indirect
283 = case tcTyVarDetails tyvar of
284 SkolemTv _ -> do { type_reft <- getTypeRefinement
285 ; case lookupVarEnv type_reft tyvar of
286 Just ty -> return (IndirectTv True ty)
287 Nothing -> return RigidTv
289 MetaTv ref -> do { details <- readMutVar ref
291 Indirect ty -> return (IndirectTv False ty)
292 Flexi -> return FlexiTv
295 -- Look up a meta type variable, conditionally consulting
296 -- the current type refinement
297 condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
298 condLookupTcTyVar use_refinement tyvar
299 | use_refinement = lookupTcTyVar tyvar
301 = case tcTyVarDetails tyvar of
302 SkolemTv _ -> return RigidTv
303 MetaTv ref -> do { details <- readMutVar ref
305 Indirect ty -> return (IndirectTv False ty)
306 Flexi -> return FlexiTv
310 -- gaw 2004 We aren't shorting anything out anymore, at least for now
312 | not (isTcTyVar tyvar)
313 = pprTrace "getTcTyVar" (ppr tyvar) $
314 returnM (Just (mkTyVarTy tyvar))
317 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
318 readMetaTyVar tyvar `thenM` \ maybe_ty ->
320 Just ty -> short_out ty `thenM` \ ty' ->
321 writeMetaTyVar tyvar (Just ty') `thenM_`
324 Nothing -> returnM Nothing
326 short_out :: TcType -> TcM TcType
327 short_out ty@(TyVarTy tyvar)
328 | not (isTcTyVar tyvar)
332 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
334 Just ty' -> short_out ty' `thenM` \ ty' ->
335 writeMetaTyVar tyvar (Just ty') `thenM_`
340 short_out other_ty = returnM other_ty
345 %************************************************************************
347 \subsection{Zonking -- the exernal interfaces}
349 %************************************************************************
351 ----------------- Type variables
354 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
355 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
357 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
358 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
359 returnM (tyVarsOfTypes tys)
361 zonkTcTyVar :: TcTyVar -> TcM TcType
362 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) True tyvar
365 ----------------- Types
368 zonkTcType :: TcType -> TcM TcType
369 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) True ty
371 zonkTcTypes :: [TcType] -> TcM [TcType]
372 zonkTcTypes tys = mappM zonkTcType tys
374 zonkTcClassConstraints cts = mappM zonk cts
375 where zonk (clas, tys)
376 = zonkTcTypes tys `thenM` \ new_tys ->
377 returnM (clas, new_tys)
379 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
380 zonkTcThetaType theta = mappM zonkTcPredType theta
382 zonkTcPredType :: TcPredType -> TcM TcPredType
383 zonkTcPredType (ClassP c ts)
384 = zonkTcTypes ts `thenM` \ new_ts ->
385 returnM (ClassP c new_ts)
386 zonkTcPredType (IParam n t)
387 = zonkTcType t `thenM` \ new_t ->
388 returnM (IParam n new_t)
391 ------------------- These ...ToType, ...ToKind versions
392 are used at the end of type checking
395 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
396 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
397 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
398 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
399 -- The meta tyvar is updated to point to the new regular TyVar. Now any
400 -- bound occurences of the original type variable will get zonked to
401 -- the immutable version.
403 -- We leave skolem TyVars alone; they are imutable.
404 zonkQuantifiedTyVar tv
405 | isSkolemTyVar tv = return tv
406 -- It might be a skolem type variable,
407 -- for example from a user type signature
409 | otherwise -- It's a meta-type-variable
410 = do { details <- readMetaTyVar tv
412 -- Create the new, frozen, regular type variable
413 ; let final_kind = defaultKind (tyVarKind tv)
414 final_tv = mkTyVar (tyVarName tv) final_kind
416 -- Bind the meta tyvar to the new tyvar
418 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
420 -- [Sept 04] I don't think this should happen
421 -- See note [Silly Type Synonym]
423 other -> writeMetaTyVar tv (Indirect (mkTyVarTy final_tv))
425 -- Return the new tyvar
429 [Silly Type Synonyms]
432 type C u a = u -- Note 'a' unused
434 foo :: (forall a. C u a -> C u a) -> u
438 bar = foo (\t -> t + t)
440 * From the (\t -> t+t) we get type {Num d} => d -> d
443 * Now unify with type of foo's arg, and we get:
444 {Num (C d a)} => C d a -> C d a
447 * Now abstract over the 'a', but float out the Num (C d a) constraint
448 because it does not 'really' mention a. (see Type.tyVarsOfType)
449 The arg to foo becomes
452 * So we get a dict binding for Num (C d a), which is zonked to give
454 [Note Sept 04: now that we are zonking quantified type variables
455 on construction, the 'a' will be frozen as a regular tyvar on
456 quantification, so the floated dict will still have type (C d a).
457 Which renders this whole note moot; happily!]
459 * Then the /\a abstraction has a zonked 'a' in it.
461 All very silly. I think its harmless to ignore the problem. We'll end up with
462 a /\a in the final result but all the occurrences of a will be zonked to ()
465 %************************************************************************
467 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
469 %* For internal use only! *
471 %************************************************************************
474 -- For unbound, mutable tyvars, zonkType uses the function given to it
475 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
476 -- type variable and zonks the kind too
478 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
479 -- see zonkTcType, and zonkTcTypeToType
480 -> Bool -- Should we consult the current type refinement?
483 zonkType unbound_var_fn rflag ty
486 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
487 returnM (TyConApp tycon tys')
489 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
490 go ty2 `thenM` \ ty2' ->
491 returnM (NoteTy (SynNote ty1') ty2')
493 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
495 go (PredTy p) = go_pred p `thenM` \ p' ->
498 go (FunTy arg res) = go arg `thenM` \ arg' ->
499 go res `thenM` \ res' ->
500 returnM (FunTy arg' res')
502 go (AppTy fun arg) = go fun `thenM` \ fun' ->
503 go arg `thenM` \ arg' ->
504 returnM (mkAppTy fun' arg')
505 -- NB the mkAppTy; we might have instantiated a
506 -- type variable to a type constructor, so we need
507 -- to pull the TyConApp to the top.
509 -- The two interesting cases!
510 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn rflag tyvar
512 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
513 go ty `thenM` \ ty' ->
514 returnM (ForAllTy tyvar ty')
516 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
517 returnM (ClassP c tys')
518 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
519 returnM (IParam n ty')
521 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
522 -> Bool -- Consult the type refinement?
523 -> TcTyVar -> TcM TcType
524 zonkTyVar unbound_var_fn rflag tyvar
525 | not (isTcTyVar tyvar) -- When zonking (forall a. ...a...), the occurrences of
526 -- the quantified variable a are TyVars not TcTyVars
527 = returnM (TyVarTy tyvar)
530 = condLookupTcTyVar rflag tyvar `thenM` \ details ->
532 -- If b is true, the variable was refined, and therefore it is okay
533 -- to continue refining inside. Otherwise it was wobbly and we should
534 -- not refine further inside.
535 IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
536 FlexiTv -> unbound_var_fn tyvar -- Unbound flexi
537 RigidTv -> return (TyVarTy tyvar) -- Rigid, no zonking necessary
542 %************************************************************************
546 %************************************************************************
549 readKindVar :: KindVar -> TcM (Maybe TcKind)
550 writeKindVar :: KindVar -> TcKind -> TcM ()
551 readKindVar (KVar _ ref) = readMutVar ref
552 writeKindVar (KVar _ ref) val = writeMutVar ref (Just val)
555 zonkTcKind :: TcKind -> TcM TcKind
556 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
557 ; k2' <- zonkTcKind k2
558 ; returnM (FunKind k1' k2') }
559 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
562 Just k -> zonkTcKind k }
563 zonkTcKind other_kind = returnM other_kind
566 zonkTcKindToKind :: TcKind -> TcM Kind
567 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
568 ; k2' <- zonkTcKindToKind k2
569 ; returnM (FunKind k1' k2') }
571 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
573 Nothing -> return liftedTypeKind
574 Just k -> zonkTcKindToKind k }
576 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
577 zonkTcKindToKind other_kind = returnM other_kind
580 %************************************************************************
582 \subsection{Checking a user type}
584 %************************************************************************
586 When dealing with a user-written type, we first translate it from an HsType
587 to a Type, performing kind checking, and then check various things that should
588 be true about it. We don't want to perform these checks at the same time
589 as the initial translation because (a) they are unnecessary for interface-file
590 types and (b) when checking a mutually recursive group of type and class decls,
591 we can't "look" at the tycons/classes yet. Also, the checks are are rather
592 diverse, and used to really mess up the other code.
594 One thing we check for is 'rank'.
596 Rank 0: monotypes (no foralls)
597 Rank 1: foralls at the front only, Rank 0 inside
598 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
600 basic ::= tyvar | T basic ... basic
602 r2 ::= forall tvs. cxt => r2a
603 r2a ::= r1 -> r2a | basic
604 r1 ::= forall tvs. cxt => r0
605 r0 ::= r0 -> r0 | basic
607 Another thing is to check that type synonyms are saturated.
608 This might not necessarily show up in kind checking.
610 data T k = MkT (k Int)
616 = FunSigCtxt Name -- Function type signature
617 | ExprSigCtxt -- Expression type signature
618 | ConArgCtxt Name -- Data constructor argument
619 | TySynCtxt Name -- RHS of a type synonym decl
620 | GenPatCtxt -- Pattern in generic decl
621 -- f{| a+b |} (Inl x) = ...
622 | PatSigCtxt -- Type sig in pattern
624 | ResSigCtxt -- Result type sig
626 | ForSigCtxt Name -- Foreign inport or export signature
627 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
628 | DefaultDeclCtxt -- Types in a default declaration
630 -- Notes re TySynCtxt
631 -- We allow type synonyms that aren't types; e.g. type List = []
633 -- If the RHS mentions tyvars that aren't in scope, we'll
634 -- quantify over them:
635 -- e.g. type T = a->a
636 -- will become type T = forall a. a->a
638 -- With gla-exts that's right, but for H98 we should complain.
641 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
642 pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt
644 pprUserTypeCtxt ty (FunSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
645 pprUserTypeCtxt ty ExprSigCtxt = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
646 pprUserTypeCtxt ty (ConArgCtxt c) = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
647 pprUserTypeCtxt ty (TySynCtxt c) = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
648 nest 2 (ptext SLIT(", namely") <+> ppr ty)]
649 pprUserTypeCtxt ty GenPatCtxt = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
650 pprUserTypeCtxt ty PatSigCtxt = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
651 pprUserTypeCtxt ty ResSigCtxt = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
652 pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
653 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
654 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
656 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
660 checkValidType :: UserTypeCtxt -> Type -> TcM ()
661 -- Checks that the type is valid for the given context
662 checkValidType ctxt ty
663 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
664 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
666 rank | gla_exts = Arbitrary
668 = case ctxt of -- Haskell 98
671 DefaultDeclCtxt-> Rank 0
673 TySynCtxt _ -> Rank 0
674 ExprSigCtxt -> Rank 1
675 FunSigCtxt _ -> Rank 1
676 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
677 -- constructor, hence rank 1
678 ForSigCtxt _ -> Rank 1
679 RuleSigCtxt _ -> Rank 1
681 actual_kind = typeKind ty
683 kind_ok = case ctxt of
684 TySynCtxt _ -> True -- Any kind will do
685 ResSigCtxt -> isOpenTypeKind actual_kind
686 ExprSigCtxt -> isOpenTypeKind actual_kind
687 GenPatCtxt -> isLiftedTypeKind actual_kind
688 ForSigCtxt _ -> isLiftedTypeKind actual_kind
689 other -> isArgTypeKind actual_kind
691 ubx_tup | not gla_exts = UT_NotOk
692 | otherwise = case ctxt of
696 -- Unboxed tuples ok in function results,
697 -- but for type synonyms we allow them even at
700 -- Check that the thing has kind Type, and is lifted if necessary
701 checkTc kind_ok (kindErr actual_kind) `thenM_`
703 -- Check the internal validity of the type itself
704 check_poly_type rank ubx_tup ty `thenM_`
706 traceTc (text "checkValidType done" <+> ppr ty)
711 data Rank = Rank Int | Arbitrary
713 decRank :: Rank -> Rank
714 decRank Arbitrary = Arbitrary
715 decRank (Rank n) = Rank (n-1)
717 ----------------------------------------
718 data UbxTupFlag = UT_Ok | UT_NotOk
719 -- The "Ok" version means "ok if -fglasgow-exts is on"
721 ----------------------------------------
722 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
723 check_poly_type (Rank 0) ubx_tup ty
724 = check_tau_type (Rank 0) ubx_tup ty
726 check_poly_type rank ubx_tup ty
728 (tvs, theta, tau) = tcSplitSigmaTy ty
730 check_valid_theta SigmaCtxt theta `thenM_`
731 check_tau_type (decRank rank) ubx_tup tau `thenM_`
732 checkFreeness tvs theta `thenM_`
733 checkAmbiguity tvs theta (tyVarsOfType tau)
735 ----------------------------------------
736 check_arg_type :: Type -> TcM ()
737 -- The sort of type that can instantiate a type variable,
738 -- or be the argument of a type constructor.
739 -- Not an unboxed tuple, not a forall.
740 -- Other unboxed types are very occasionally allowed as type
741 -- arguments depending on the kind of the type constructor
743 -- For example, we want to reject things like:
745 -- instance Ord a => Ord (forall s. T s a)
747 -- g :: T s (forall b.b)
749 -- NB: unboxed tuples can have polymorphic or unboxed args.
750 -- This happens in the workers for functions returning
751 -- product types with polymorphic components.
752 -- But not in user code.
753 -- Anyway, they are dealt with by a special case in check_tau_type
756 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
757 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
759 ----------------------------------------
760 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
761 -- Rank is allowed rank for function args
762 -- No foralls otherwise
764 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
765 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
766 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
768 -- Naked PredTys don't usually show up, but they can as a result of
769 -- {-# SPECIALISE instance Ord Char #-}
770 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
771 -- are handled, but the quick thing is just to permit PredTys here.
772 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
773 check_source_ty dflags TypeCtxt sty
775 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
776 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
777 = check_poly_type rank UT_NotOk arg_ty `thenM_`
778 check_tau_type rank UT_Ok res_ty
780 check_tau_type rank ubx_tup (AppTy ty1 ty2)
781 = check_arg_type ty1 `thenM_` check_arg_type ty2
783 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
784 -- Synonym notes are built only when the synonym is
785 -- saturated (see Type.mkSynTy)
786 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
788 -- If -fglasgow-exts then don't check the 'note' part.
789 -- This allows us to instantiate a synonym defn with a
790 -- for-all type, or with a partially-applied type synonym.
791 -- e.g. type T a b = a
794 -- Here, T is partially applied, so it's illegal in H98.
795 -- But if you expand S first, then T we get just
800 -- For H98, do check the un-expanded part
801 check_tau_type rank ubx_tup syn
804 check_tau_type rank ubx_tup ty
806 check_tau_type rank ubx_tup (NoteTy other_note ty)
807 = check_tau_type rank ubx_tup ty
809 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
811 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
812 -- synonym application, leaving it to checkValidType (i.e. right here)
814 checkTc syn_arity_ok arity_msg `thenM_`
815 mappM_ check_arg_type tys
817 | isUnboxedTupleTyCon tc
818 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
819 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
820 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
821 -- Args are allowed to be unlifted, or
822 -- more unboxed tuples, so can't use check_arg_ty
825 = mappM_ check_arg_type tys
828 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
830 syn_arity_ok = tc_arity <= n_args
831 -- It's OK to have an *over-applied* type synonym
832 -- data Tree a b = ...
833 -- type Foo a = Tree [a]
834 -- f :: Foo a b -> ...
836 tc_arity = tyConArity tc
838 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
839 ubx_tup_msg = ubxArgTyErr ty
841 ----------------------------------------
842 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
843 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
844 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
845 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
850 %************************************************************************
852 \subsection{Checking a theta or source type}
854 %************************************************************************
857 -- Enumerate the contexts in which a "source type", <S>, can occur
861 -- or (N a) where N is a newtype
864 = ClassSCCtxt Name -- Superclasses of clas
865 -- class <S> => C a where ...
866 | SigmaCtxt -- Theta part of a normal for-all type
867 -- f :: <S> => a -> a
868 | DataTyCtxt Name -- Theta part of a data decl
869 -- data <S> => T a = MkT a
870 | TypeCtxt -- Source type in an ordinary type
872 | InstThetaCtxt -- Context of an instance decl
873 -- instance <S> => C [a] where ...
874 | InstHeadCtxt -- Head of an instance decl
875 -- instance ... => Eq a where ...
877 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
878 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
879 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
880 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
881 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
882 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
886 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
887 checkValidTheta ctxt theta
888 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
890 -------------------------
891 check_valid_theta ctxt []
893 check_valid_theta ctxt theta
894 = getDOpts `thenM` \ dflags ->
895 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
896 -- Actually, in instance decls and type signatures,
897 -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
898 -- so this error can only fire for the context of a class or
900 mappM_ (check_source_ty dflags ctxt) theta
902 (_,dups) = removeDups tcCmpPred theta
904 -------------------------
905 check_source_ty dflags ctxt pred@(ClassP cls tys)
906 = -- Class predicates are valid in all contexts
907 checkTc (arity == n_tys) arity_err `thenM_`
909 -- Check the form of the argument types
910 mappM_ check_arg_type tys `thenM_`
911 checkTc (check_class_pred_tys dflags ctxt tys)
912 (predTyVarErr pred $$ how_to_allow)
915 class_name = className cls
916 arity = classArity cls
918 arity_err = arityErr "Class" class_name arity n_tys
920 how_to_allow = case ctxt of
921 InstHeadCtxt -> empty -- Should not happen
922 InstThetaCtxt -> parens undecidableMsg
923 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
925 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
926 -- Implicit parameters only allows in type
927 -- signatures; not in instance decls, superclasses etc
928 -- The reason for not allowing implicit params in instances is a bit subtle
929 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
930 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
931 -- discharge all the potential usas of the ?x in e. For example, a
932 -- constraint Foo [Int] might come out of e,and applying the
933 -- instance decl would show up two uses of ?x.
936 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
938 -------------------------
939 check_class_pred_tys dflags ctxt tys
941 InstHeadCtxt -> True -- We check for instance-head
942 -- formation in checkValidInstHead
943 InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
944 other -> gla_exts || all tyvar_head tys
946 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
947 gla_exts = dopt Opt_GlasgowExts dflags
949 -------------------------
950 tyvar_head ty -- Haskell 98 allows predicates of form
951 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
952 | otherwise -- where a is a type variable
953 = case tcSplitAppTy_maybe ty of
954 Just (ty, _) -> tyvar_head ty
961 is ambiguous if P contains generic variables
962 (i.e. one of the Vs) that are not mentioned in tau
964 However, we need to take account of functional dependencies
965 when we speak of 'mentioned in tau'. Example:
966 class C a b | a -> b where ...
968 forall x y. (C x y) => x
969 is not ambiguous because x is mentioned and x determines y
971 NB; the ambiguity check is only used for *user* types, not for types
972 coming from inteface files. The latter can legitimately have
973 ambiguous types. Example
975 class S a where s :: a -> (Int,Int)
976 instance S Char where s _ = (1,1)
977 f:: S a => [a] -> Int -> (Int,Int)
978 f (_::[a]) x = (a*x,b)
979 where (a,b) = s (undefined::a)
981 Here the worker for f gets the type
982 fw :: forall a. S a => Int -> (# Int, Int #)
984 If the list of tv_names is empty, we have a monotype, and then we
985 don't need to check for ambiguity either, because the test can't fail
989 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
990 checkAmbiguity forall_tyvars theta tau_tyvars
991 = mappM_ complain (filter is_ambig theta)
993 complain pred = addErrTc (ambigErr pred)
994 extended_tau_vars = grow theta tau_tyvars
996 -- Only a *class* predicate can give rise to ambiguity
997 -- An *implicit parameter* cannot. For example:
998 -- foo :: (?x :: [a]) => Int
1000 -- is fine. The call site will suppply a particular 'x'
1001 is_ambig pred = isClassPred pred &&
1002 any ambig_var (varSetElems (tyVarsOfPred pred))
1004 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1005 not (ct_var `elemVarSet` extended_tau_vars)
1008 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1009 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1010 ptext SLIT("must be reachable from the type after the '=>'"))]
1013 In addition, GHC insists that at least one type variable
1014 in each constraint is in V. So we disallow a type like
1015 forall a. Eq b => b -> b
1016 even in a scope where b is in scope.
1019 checkFreeness forall_tyvars theta
1020 = mappM_ complain (filter is_free theta)
1022 is_free pred = not (isIPPred pred)
1023 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1024 bound_var ct_var = ct_var `elem` forall_tyvars
1025 complain pred = addErrTc (freeErr pred)
1028 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1029 ptext SLIT("are already in scope"),
1030 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1035 checkThetaCtxt ctxt theta
1036 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1037 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1039 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1040 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
1041 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1043 arityErr kind name n m
1044 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1045 n_arguments <> comma, text "but has been given", int m]
1047 n_arguments | n == 0 = ptext SLIT("no arguments")
1048 | n == 1 = ptext SLIT("1 argument")
1049 | True = hsep [int n, ptext SLIT("arguments")]
1053 %************************************************************************
1055 \subsection{Checking for a decent instance head type}
1057 %************************************************************************
1059 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1060 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1062 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1063 flag is on, or (2)~the instance is imported (they must have been
1064 compiled elsewhere). In these cases, we let them go through anyway.
1066 We can also have instances for functions: @instance Foo (a -> b) ...@.
1069 checkValidInstHead :: Type -> TcM (Class, [TcType])
1071 checkValidInstHead ty -- Should be a source type
1072 = case tcSplitPredTy_maybe ty of {
1073 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1076 case getClassPredTys_maybe pred of {
1077 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1080 getDOpts `thenM` \ dflags ->
1081 mappM_ check_arg_type tys `thenM_`
1082 check_inst_head dflags clas tys `thenM_`
1086 check_inst_head dflags clas tys
1087 -- If GlasgowExts then check at least one isn't a type variable
1088 | dopt Opt_GlasgowExts dflags
1089 = check_tyvars dflags clas tys
1091 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1093 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1094 not (isSynTyCon tycon), -- ...but not a synonym
1095 all tcIsTyVarTy arg_tys, -- Applied to type variables
1096 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1097 -- This last condition checks that all the type variables are distinct
1101 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1104 (first_ty : _) = tys
1106 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1107 text "where T is not a synonym, and a,b,c are distinct type variables")
1109 check_tyvars dflags clas tys
1110 -- Check that at least one isn't a type variable
1111 -- unless -fallow-undecideable-instances
1112 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1113 | not (all tcIsTyVarTy tys) = returnM ()
1114 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1116 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1119 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1123 instTypeErr pp_ty msg
1124 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,