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,
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,
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 DynFlags ( 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 newKindVar :: TcM TcKind
126 newKindVar = do { uniq <- newUnique
127 ; ref <- newMutVar Nothing
128 ; return (KindVar (mkKindVar uniq ref)) }
130 newKindVars :: Int -> TcM [TcKind]
131 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
135 %************************************************************************
137 \subsection{Type instantiation}
139 %************************************************************************
141 Instantiating a bunch of type variables
145 Note that we don't change the print-name
146 This won't confuse the type checker but there's a chance
147 that two different tyvars will print the same way
148 in an error message. -dppr-debug will show up the difference
149 Better watch out for this. If worst comes to worst, just
154 -----------------------
155 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
157 = do { tc_tvs <- mappM tcInstTyVar tyvars
158 ; let tys = mkTyVarTys tc_tvs
159 ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
160 -- Since the tyvars are freshly made,
161 -- they cannot possibly be captured by
162 -- any existing for-alls. Hence zipTopTvSubst
164 tcInstTyVar tyvar -- Freshen the Name of the tyvar
165 = do { uniq <- newUnique
166 ; newMetaTyVar (setNameUnique (tyVarName tyvar) uniq)
167 (tyVarKind tyvar) Flexi }
169 tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
170 -- tcInstType instantiates the outer-level for-alls of a TcType with
171 -- fresh (mutable) type variables, splits off the dictionary part,
172 -- and returns the pieces.
173 tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty
176 ---------------------------------------------
177 tcInstSigType :: Name -> [Name] -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
178 -- Instantiate a type with fresh SigSkol variables
179 -- See Note [Signature skolems] in TcType.
181 -- Tne new type variables have the sane Name as the original *iff* they are scoped.
182 -- For scoped tyvars, we don't need a fresh unique, because the renamer has made them
183 -- unique, and it's better not to do so because we extend the envt
184 -- with them as scoped type variables, and we'd like to avoid spurious
185 -- 's = s' bindings in error messages
187 -- For non-scoped ones, we *must* instantiate fresh ones:
189 -- type T = forall a. [a] -> [a]
191 -- f = g where { g :: T; g = <rhs> }
193 -- We must not use the same 'a' from the defn of T at both places!!
195 tcInstSigType id_name scoped_names ty = tc_inst_type (tcInstSigTyVars id_name scoped_names) ty
197 tcInstSigTyVars :: Name -> [Name] -> [TyVar] -> TcM [TcTyVar]
198 tcInstSigTyVars id_name scoped_names tyvars
202 = do { let name = tyVarName tv
203 ; ref <- newMutVar Flexi
204 ; name' <- if name `elem` scoped_names
206 else do { uniq <- newUnique; return (setNameUnique name uniq) }
207 ; return (mkTcTyVar name' (tyVarKind tv)
208 (SigSkolTv id_name ref)) }
211 ---------------------------------------------
212 tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
213 -- Instantiate a type with fresh skolem constants
214 tcSkolType info ty = tc_inst_type (tcSkolTyVars info) ty
216 tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
217 tcSkolTyVars info tyvars
218 = do { us <- newUniqueSupply
219 ; return (zipWith skol_tv tyvars (uniqsFromSupply us)) }
221 skol_tv tv uniq = mkTcTyVar (setNameUnique (tyVarName tv) uniq)
222 (tyVarKind tv) (SkolemTv info)
223 -- See Note [TyVarName]
226 ---------------------------------------------
227 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
228 -- Instantiate a type signature with skolem constants, but
229 -- do *not* give them fresh names, because we want the name to
230 -- be in the type environment -- it is lexically scoped.
231 tcSkolSigType info ty
232 = tc_inst_type (\tvs -> return (tcSkolSigTyVars info tvs)) ty
234 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
235 tcSkolSigTyVars info tyvars = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info)
238 -----------------------
239 tc_inst_type :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
240 -> TcType -- Type to instantiate
241 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
242 tc_inst_type inst_tyvars ty
243 = case tcSplitForAllTys ty of
244 ([], rho) -> let -- There may be overloading despite no type variables;
245 -- (?x :: Int) => Int -> Int
246 (theta, tau) = tcSplitPhiTy rho
248 return ([], theta, tau)
250 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
252 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
253 -- Either the tyvars are freshly made, by inst_tyvars,
254 -- or (in the call from tcSkolSigType) any nested foralls
255 -- have different binders. Either way, zipTopTvSubst is ok
257 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
258 ; return (tyvars', theta, tau) }
262 %************************************************************************
264 \subsection{Putting and getting mutable type variables}
266 %************************************************************************
269 putMetaTyVar :: TcTyVar -> TcType -> TcM ()
271 putMetaTyVar tyvar ty = writeMetaTyVar tyvar (Indirect ty)
273 putMetaTyVar tyvar ty
274 | not (isMetaTyVar tyvar)
275 = pprTrace "putTcTyVar" (ppr tyvar) $
279 = ASSERT( isMetaTyVar tyvar )
280 ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
281 do { ASSERTM( do { details <- readMetaTyVar tyvar; return (isFlexi details) } )
282 ; writeMetaTyVar tyvar (Indirect ty) }
289 But it's more fun to short out indirections on the way: If this
290 version returns a TyVar, then that TyVar is unbound. If it returns
291 any other type, then there might be bound TyVars embedded inside it.
293 We return Nothing iff the original box was unbound.
296 data LookupTyVarResult -- The result of a lookupTcTyVar call
297 = DoneTv TcTyVarDetails
298 | IndirectTv Bool TcType
299 -- True => This is a non-wobbly type refinement,
300 -- gotten from GADT match unification
301 -- False => This is a wobbly type,
302 -- gotten from inference unification
304 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
305 -- This function is the ONLY PLACE that we consult the
306 -- type refinement carried by the monad
309 details = tcTyVarDetails tyvar
312 MetaTv ref -> lookup_wobbly details ref
314 SkolemTv _ -> do { type_reft <- getTypeRefinement
315 ; case lookupVarEnv type_reft tyvar of
316 Just ty -> return (IndirectTv True ty)
317 Nothing -> return (DoneTv details)
320 -- For SigSkolTvs try the refinement, and, failing that
321 -- see if it's been unified to anything. It's a combination
322 -- of SkolemTv and MetaTv
323 SigSkolTv _ ref -> do { type_reft <- getTypeRefinement
324 ; case lookupVarEnv type_reft tyvar of
325 Just ty -> return (IndirectTv True ty)
326 Nothing -> lookup_wobbly details ref
329 -- Look up a meta type variable, conditionally consulting
330 -- the current type refinement
331 condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
332 condLookupTcTyVar use_refinement tyvar
333 | use_refinement = lookupTcTyVar tyvar
336 MetaTv ref -> lookup_wobbly details ref
337 SkolemTv _ -> return (DoneTv details)
338 SigSkolTv _ ref -> lookup_wobbly details ref
340 details = tcTyVarDetails tyvar
342 lookup_wobbly :: TcTyVarDetails -> IORef MetaDetails -> TcM LookupTyVarResult
343 lookup_wobbly details ref
344 = do { meta_details <- readMutVar ref
345 ; case meta_details of
346 Indirect ty -> return (IndirectTv False ty)
347 Flexi -> return (DoneTv details)
351 -- gaw 2004 We aren't shorting anything out anymore, at least for now
353 | not (isTcTyVar tyvar)
354 = pprTrace "getTcTyVar" (ppr tyvar) $
355 returnM (Just (mkTyVarTy tyvar))
358 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
359 readMetaTyVar tyvar `thenM` \ maybe_ty ->
361 Just ty -> short_out ty `thenM` \ ty' ->
362 writeMetaTyVar tyvar (Just ty') `thenM_`
365 Nothing -> returnM Nothing
367 short_out :: TcType -> TcM TcType
368 short_out ty@(TyVarTy tyvar)
369 | not (isTcTyVar tyvar)
373 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
375 Just ty' -> short_out ty' `thenM` \ ty' ->
376 writeMetaTyVar tyvar (Just ty') `thenM_`
381 short_out other_ty = returnM other_ty
386 %************************************************************************
388 \subsection{Zonking -- the exernal interfaces}
390 %************************************************************************
392 ----------------- Type variables
395 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
396 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
398 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
399 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
400 returnM (tyVarsOfTypes tys)
402 zonkTcTyVar :: TcTyVar -> TcM TcType
403 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) True tyvar
406 ----------------- Types
409 zonkTcType :: TcType -> TcM TcType
410 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) True ty
412 zonkTcTypes :: [TcType] -> TcM [TcType]
413 zonkTcTypes tys = mappM zonkTcType tys
415 zonkTcClassConstraints cts = mappM zonk cts
416 where zonk (clas, tys)
417 = zonkTcTypes tys `thenM` \ new_tys ->
418 returnM (clas, new_tys)
420 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
421 zonkTcThetaType theta = mappM zonkTcPredType theta
423 zonkTcPredType :: TcPredType -> TcM TcPredType
424 zonkTcPredType (ClassP c ts)
425 = zonkTcTypes ts `thenM` \ new_ts ->
426 returnM (ClassP c new_ts)
427 zonkTcPredType (IParam n t)
428 = zonkTcType t `thenM` \ new_t ->
429 returnM (IParam n new_t)
432 ------------------- These ...ToType, ...ToKind versions
433 are used at the end of type checking
436 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
437 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
438 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
439 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
440 -- The meta tyvar is updated to point to the new regular TyVar. Now any
441 -- bound occurences of the original type variable will get zonked to
442 -- the immutable version.
444 -- We leave skolem TyVars alone; they are immutable.
445 zonkQuantifiedTyVar tv
446 | isSkolemTyVar tv = return tv
447 -- It might be a skolem type variable,
448 -- for example from a user type signature
450 | otherwise -- It's a meta-type-variable
451 = do { details <- readMetaTyVar tv
453 -- Create the new, frozen, regular type variable
454 ; let final_kind = defaultKind (tyVarKind tv)
455 final_tv = mkTyVar (tyVarName tv) final_kind
457 -- Bind the meta tyvar to the new tyvar
459 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
461 -- [Sept 04] I don't think this should happen
462 -- See note [Silly Type Synonym]
464 other -> writeMetaTyVar tv (Indirect (mkTyVarTy final_tv))
466 -- Return the new tyvar
470 [Silly Type Synonyms]
473 type C u a = u -- Note 'a' unused
475 foo :: (forall a. C u a -> C u a) -> u
479 bar = foo (\t -> t + t)
481 * From the (\t -> t+t) we get type {Num d} => d -> d
484 * Now unify with type of foo's arg, and we get:
485 {Num (C d a)} => C d a -> C d a
488 * Now abstract over the 'a', but float out the Num (C d a) constraint
489 because it does not 'really' mention a. (see Type.tyVarsOfType)
490 The arg to foo becomes
493 * So we get a dict binding for Num (C d a), which is zonked to give
495 [Note Sept 04: now that we are zonking quantified type variables
496 on construction, the 'a' will be frozen as a regular tyvar on
497 quantification, so the floated dict will still have type (C d a).
498 Which renders this whole note moot; happily!]
500 * Then the /\a abstraction has a zonked 'a' in it.
502 All very silly. I think its harmless to ignore the problem. We'll end up with
503 a /\a in the final result but all the occurrences of a will be zonked to ()
506 %************************************************************************
508 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
510 %* For internal use only! *
512 %************************************************************************
515 -- For unbound, mutable tyvars, zonkType uses the function given to it
516 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
517 -- type variable and zonks the kind too
519 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
520 -- see zonkTcType, and zonkTcTypeToType
521 -> Bool -- Should we consult the current type refinement?
524 zonkType unbound_var_fn rflag ty
527 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
528 returnM (TyConApp tycon tys')
530 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
531 go ty2 `thenM` \ ty2' ->
532 returnM (NoteTy (SynNote ty1') ty2')
534 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
536 go (PredTy p) = go_pred p `thenM` \ p' ->
539 go (FunTy arg res) = go arg `thenM` \ arg' ->
540 go res `thenM` \ res' ->
541 returnM (FunTy arg' res')
543 go (AppTy fun arg) = go fun `thenM` \ fun' ->
544 go arg `thenM` \ arg' ->
545 returnM (mkAppTy fun' arg')
546 -- NB the mkAppTy; we might have instantiated a
547 -- type variable to a type constructor, so we need
548 -- to pull the TyConApp to the top.
550 -- The two interesting cases!
551 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn rflag tyvar
553 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
554 go ty `thenM` \ ty' ->
555 returnM (ForAllTy tyvar ty')
557 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
558 returnM (ClassP c tys')
559 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
560 returnM (IParam n ty')
562 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
563 -> Bool -- Consult the type refinement?
564 -> TcTyVar -> TcM TcType
565 zonkTyVar unbound_var_fn rflag tyvar
566 | not (isTcTyVar tyvar) -- When zonking (forall a. ...a...), the occurrences of
567 -- the quantified variable 'a' are TyVars not TcTyVars
568 = returnM (TyVarTy tyvar)
571 = condLookupTcTyVar rflag tyvar `thenM` \ details ->
573 -- If b is true, the variable was refined, and therefore it is okay
574 -- to continue refining inside. Otherwise it was wobbly and we should
575 -- not refine further inside.
576 IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
577 DoneTv (MetaTv _) -> unbound_var_fn tyvar -- Unbound meta type variable
578 DoneTv other -> return (TyVarTy tyvar) -- Rigid, no zonking necessary
583 %************************************************************************
587 %************************************************************************
590 readKindVar :: KindVar -> TcM (Maybe TcKind)
591 writeKindVar :: KindVar -> TcKind -> TcM ()
592 readKindVar (KVar _ ref) = readMutVar ref
593 writeKindVar (KVar _ ref) val = writeMutVar ref (Just val)
596 zonkTcKind :: TcKind -> TcM TcKind
597 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
598 ; k2' <- zonkTcKind k2
599 ; returnM (FunKind k1' k2') }
600 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
603 Just k -> zonkTcKind k }
604 zonkTcKind other_kind = returnM other_kind
607 zonkTcKindToKind :: TcKind -> TcM Kind
608 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
609 ; k2' <- zonkTcKindToKind k2
610 ; returnM (FunKind k1' k2') }
612 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
614 Nothing -> return liftedTypeKind
615 Just k -> zonkTcKindToKind k }
617 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
618 zonkTcKindToKind other_kind = returnM other_kind
621 %************************************************************************
623 \subsection{Checking a user type}
625 %************************************************************************
627 When dealing with a user-written type, we first translate it from an HsType
628 to a Type, performing kind checking, and then check various things that should
629 be true about it. We don't want to perform these checks at the same time
630 as the initial translation because (a) they are unnecessary for interface-file
631 types and (b) when checking a mutually recursive group of type and class decls,
632 we can't "look" at the tycons/classes yet. Also, the checks are are rather
633 diverse, and used to really mess up the other code.
635 One thing we check for is 'rank'.
637 Rank 0: monotypes (no foralls)
638 Rank 1: foralls at the front only, Rank 0 inside
639 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
641 basic ::= tyvar | T basic ... basic
643 r2 ::= forall tvs. cxt => r2a
644 r2a ::= r1 -> r2a | basic
645 r1 ::= forall tvs. cxt => r0
646 r0 ::= r0 -> r0 | basic
648 Another thing is to check that type synonyms are saturated.
649 This might not necessarily show up in kind checking.
651 data T k = MkT (k Int)
657 = FunSigCtxt Name -- Function type signature
658 | ExprSigCtxt -- Expression type signature
659 | ConArgCtxt Name -- Data constructor argument
660 | TySynCtxt Name -- RHS of a type synonym decl
661 | GenPatCtxt -- Pattern in generic decl
662 -- f{| a+b |} (Inl x) = ...
663 | PatSigCtxt -- Type sig in pattern
665 | ResSigCtxt -- Result type sig
667 | ForSigCtxt Name -- Foreign inport or export signature
668 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
669 | DefaultDeclCtxt -- Types in a default declaration
671 -- Notes re TySynCtxt
672 -- We allow type synonyms that aren't types; e.g. type List = []
674 -- If the RHS mentions tyvars that aren't in scope, we'll
675 -- quantify over them:
676 -- e.g. type T = a->a
677 -- will become type T = forall a. a->a
679 -- With gla-exts that's right, but for H98 we should complain.
682 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
683 pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt
685 pprUserTypeCtxt ty (FunSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
686 pprUserTypeCtxt ty ExprSigCtxt = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
687 pprUserTypeCtxt ty (ConArgCtxt c) = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
688 pprUserTypeCtxt ty (TySynCtxt c) = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
689 nest 2 (ptext SLIT(", namely") <+> ppr ty)]
690 pprUserTypeCtxt ty GenPatCtxt = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
691 pprUserTypeCtxt ty PatSigCtxt = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
692 pprUserTypeCtxt ty ResSigCtxt = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
693 pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
694 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
695 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
697 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
701 checkValidType :: UserTypeCtxt -> Type -> TcM ()
702 -- Checks that the type is valid for the given context
703 checkValidType ctxt ty
704 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
705 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
707 rank | gla_exts = Arbitrary
709 = case ctxt of -- Haskell 98
712 DefaultDeclCtxt-> Rank 0
714 TySynCtxt _ -> Rank 0
715 ExprSigCtxt -> Rank 1
716 FunSigCtxt _ -> Rank 1
717 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
718 -- constructor, hence rank 1
719 ForSigCtxt _ -> Rank 1
720 RuleSigCtxt _ -> Rank 1
722 actual_kind = typeKind ty
724 kind_ok = case ctxt of
725 TySynCtxt _ -> True -- Any kind will do
726 ResSigCtxt -> isOpenTypeKind actual_kind
727 ExprSigCtxt -> isOpenTypeKind actual_kind
728 GenPatCtxt -> isLiftedTypeKind actual_kind
729 ForSigCtxt _ -> isLiftedTypeKind actual_kind
730 other -> isArgTypeKind actual_kind
732 ubx_tup | not gla_exts = UT_NotOk
733 | otherwise = case ctxt of
737 -- Unboxed tuples ok in function results,
738 -- but for type synonyms we allow them even at
741 -- Check that the thing has kind Type, and is lifted if necessary
742 checkTc kind_ok (kindErr actual_kind) `thenM_`
744 -- Check the internal validity of the type itself
745 check_poly_type rank ubx_tup ty `thenM_`
747 traceTc (text "checkValidType done" <+> ppr ty)
752 data Rank = Rank Int | Arbitrary
754 decRank :: Rank -> Rank
755 decRank Arbitrary = Arbitrary
756 decRank (Rank n) = Rank (n-1)
758 ----------------------------------------
759 data UbxTupFlag = UT_Ok | UT_NotOk
760 -- The "Ok" version means "ok if -fglasgow-exts is on"
762 ----------------------------------------
763 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
764 check_poly_type (Rank 0) ubx_tup ty
765 = check_tau_type (Rank 0) ubx_tup ty
767 check_poly_type rank ubx_tup ty
769 (tvs, theta, tau) = tcSplitSigmaTy ty
771 check_valid_theta SigmaCtxt theta `thenM_`
772 check_tau_type (decRank rank) ubx_tup tau `thenM_`
773 checkFreeness tvs theta `thenM_`
774 checkAmbiguity tvs theta (tyVarsOfType tau)
776 ----------------------------------------
777 check_arg_type :: Type -> TcM ()
778 -- The sort of type that can instantiate a type variable,
779 -- or be the argument of a type constructor.
780 -- Not an unboxed tuple, not a forall.
781 -- Other unboxed types are very occasionally allowed as type
782 -- arguments depending on the kind of the type constructor
784 -- For example, we want to reject things like:
786 -- instance Ord a => Ord (forall s. T s a)
788 -- g :: T s (forall b.b)
790 -- NB: unboxed tuples can have polymorphic or unboxed args.
791 -- This happens in the workers for functions returning
792 -- product types with polymorphic components.
793 -- But not in user code.
794 -- Anyway, they are dealt with by a special case in check_tau_type
797 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
798 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
800 ----------------------------------------
801 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
802 -- Rank is allowed rank for function args
803 -- No foralls otherwise
805 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
806 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
807 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
809 -- Naked PredTys don't usually show up, but they can as a result of
810 -- {-# SPECIALISE instance Ord Char #-}
811 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
812 -- are handled, but the quick thing is just to permit PredTys here.
813 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
814 check_source_ty dflags TypeCtxt sty
816 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
817 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
818 = check_poly_type rank UT_NotOk arg_ty `thenM_`
819 check_tau_type rank UT_Ok res_ty
821 check_tau_type rank ubx_tup (AppTy ty1 ty2)
822 = check_arg_type ty1 `thenM_` check_arg_type ty2
824 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
825 -- Synonym notes are built only when the synonym is
826 -- saturated (see Type.mkSynTy)
827 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
829 -- If -fglasgow-exts then don't check the 'note' part.
830 -- This allows us to instantiate a synonym defn with a
831 -- for-all type, or with a partially-applied type synonym.
832 -- e.g. type T a b = a
835 -- Here, T is partially applied, so it's illegal in H98.
836 -- But if you expand S first, then T we get just
841 -- For H98, do check the un-expanded part
842 check_tau_type rank ubx_tup syn
845 check_tau_type rank ubx_tup ty
847 check_tau_type rank ubx_tup (NoteTy other_note ty)
848 = check_tau_type rank ubx_tup ty
850 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
852 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
853 -- synonym application, leaving it to checkValidType (i.e. right here)
855 checkTc syn_arity_ok arity_msg `thenM_`
856 mappM_ check_arg_type tys
858 | isUnboxedTupleTyCon tc
859 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
860 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
861 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
862 -- Args are allowed to be unlifted, or
863 -- more unboxed tuples, so can't use check_arg_ty
866 = mappM_ check_arg_type tys
869 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
871 syn_arity_ok = tc_arity <= n_args
872 -- It's OK to have an *over-applied* type synonym
873 -- data Tree a b = ...
874 -- type Foo a = Tree [a]
875 -- f :: Foo a b -> ...
877 tc_arity = tyConArity tc
879 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
880 ubx_tup_msg = ubxArgTyErr ty
882 ----------------------------------------
883 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
884 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
885 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
886 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
891 %************************************************************************
893 \subsection{Checking a theta or source type}
895 %************************************************************************
898 -- Enumerate the contexts in which a "source type", <S>, can occur
902 -- or (N a) where N is a newtype
905 = ClassSCCtxt Name -- Superclasses of clas
906 -- class <S> => C a where ...
907 | SigmaCtxt -- Theta part of a normal for-all type
908 -- f :: <S> => a -> a
909 | DataTyCtxt Name -- Theta part of a data decl
910 -- data <S> => T a = MkT a
911 | TypeCtxt -- Source type in an ordinary type
913 | InstThetaCtxt -- Context of an instance decl
914 -- instance <S> => C [a] where ...
915 | InstHeadCtxt -- Head of an instance decl
916 -- instance ... => Eq a where ...
918 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
919 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
920 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
921 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
922 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
923 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
927 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
928 checkValidTheta ctxt theta
929 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
931 -------------------------
932 check_valid_theta ctxt []
934 check_valid_theta ctxt theta
935 = getDOpts `thenM` \ dflags ->
936 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
937 -- Actually, in instance decls and type signatures,
938 -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
939 -- so this error can only fire for the context of a class or
941 mappM_ (check_source_ty dflags ctxt) theta
943 (_,dups) = removeDups tcCmpPred theta
945 -------------------------
946 check_source_ty dflags ctxt pred@(ClassP cls tys)
947 = -- Class predicates are valid in all contexts
948 checkTc (arity == n_tys) arity_err `thenM_`
950 -- Check the form of the argument types
951 mappM_ check_arg_type tys `thenM_`
952 checkTc (check_class_pred_tys dflags ctxt tys)
953 (predTyVarErr pred $$ how_to_allow)
956 class_name = className cls
957 arity = classArity cls
959 arity_err = arityErr "Class" class_name arity n_tys
961 how_to_allow = case ctxt of
962 InstHeadCtxt -> empty -- Should not happen
963 InstThetaCtxt -> parens undecidableMsg
964 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
966 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
967 -- Implicit parameters only allows in type
968 -- signatures; not in instance decls, superclasses etc
969 -- The reason for not allowing implicit params in instances is a bit subtle
970 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
971 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
972 -- discharge all the potential usas of the ?x in e. For example, a
973 -- constraint Foo [Int] might come out of e,and applying the
974 -- instance decl would show up two uses of ?x.
977 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
979 -------------------------
980 check_class_pred_tys dflags ctxt tys
982 InstHeadCtxt -> True -- We check for instance-head
983 -- formation in checkValidInstHead
984 InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
985 other -> gla_exts || all tyvar_head tys
987 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
988 gla_exts = dopt Opt_GlasgowExts dflags
990 -------------------------
991 tyvar_head ty -- Haskell 98 allows predicates of form
992 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
993 | otherwise -- where a is a type variable
994 = case tcSplitAppTy_maybe ty of
995 Just (ty, _) -> tyvar_head ty
1002 is ambiguous if P contains generic variables
1003 (i.e. one of the Vs) that are not mentioned in tau
1005 However, we need to take account of functional dependencies
1006 when we speak of 'mentioned in tau'. Example:
1007 class C a b | a -> b where ...
1009 forall x y. (C x y) => x
1010 is not ambiguous because x is mentioned and x determines y
1012 NB; the ambiguity check is only used for *user* types, not for types
1013 coming from inteface files. The latter can legitimately have
1014 ambiguous types. Example
1016 class S a where s :: a -> (Int,Int)
1017 instance S Char where s _ = (1,1)
1018 f:: S a => [a] -> Int -> (Int,Int)
1019 f (_::[a]) x = (a*x,b)
1020 where (a,b) = s (undefined::a)
1022 Here the worker for f gets the type
1023 fw :: forall a. S a => Int -> (# Int, Int #)
1025 If the list of tv_names is empty, we have a monotype, and then we
1026 don't need to check for ambiguity either, because the test can't fail
1030 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1031 checkAmbiguity forall_tyvars theta tau_tyvars
1032 = mappM_ complain (filter is_ambig theta)
1034 complain pred = addErrTc (ambigErr pred)
1035 extended_tau_vars = grow theta tau_tyvars
1037 -- Only a *class* predicate can give rise to ambiguity
1038 -- An *implicit parameter* cannot. For example:
1039 -- foo :: (?x :: [a]) => Int
1041 -- is fine. The call site will suppply a particular 'x'
1042 is_ambig pred = isClassPred pred &&
1043 any ambig_var (varSetElems (tyVarsOfPred pred))
1045 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1046 not (ct_var `elemVarSet` extended_tau_vars)
1049 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1050 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1051 ptext SLIT("must be reachable from the type after the '=>'"))]
1054 In addition, GHC insists that at least one type variable
1055 in each constraint is in V. So we disallow a type like
1056 forall a. Eq b => b -> b
1057 even in a scope where b is in scope.
1060 checkFreeness forall_tyvars theta
1061 = mappM_ complain (filter is_free theta)
1063 is_free pred = not (isIPPred pred)
1064 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1065 bound_var ct_var = ct_var `elem` forall_tyvars
1066 complain pred = addErrTc (freeErr pred)
1069 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1070 ptext SLIT("are already in scope"),
1071 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1076 checkThetaCtxt ctxt theta
1077 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1078 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1080 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1081 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
1082 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1084 arityErr kind name n m
1085 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1086 n_arguments <> comma, text "but has been given", int m]
1088 n_arguments | n == 0 = ptext SLIT("no arguments")
1089 | n == 1 = ptext SLIT("1 argument")
1090 | True = hsep [int n, ptext SLIT("arguments")]
1094 %************************************************************************
1096 \subsection{Checking for a decent instance head type}
1098 %************************************************************************
1100 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1101 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1103 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1104 flag is on, or (2)~the instance is imported (they must have been
1105 compiled elsewhere). In these cases, we let them go through anyway.
1107 We can also have instances for functions: @instance Foo (a -> b) ...@.
1110 checkValidInstHead :: Type -> TcM (Class, [TcType])
1112 checkValidInstHead ty -- Should be a source type
1113 = case tcSplitPredTy_maybe ty of {
1114 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1117 case getClassPredTys_maybe pred of {
1118 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1121 getDOpts `thenM` \ dflags ->
1122 mappM_ check_arg_type tys `thenM_`
1123 check_inst_head dflags clas tys `thenM_`
1127 check_inst_head dflags clas tys
1128 -- If GlasgowExts then check at least one isn't a type variable
1129 | dopt Opt_GlasgowExts dflags
1130 = check_tyvars dflags clas tys
1132 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1134 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1135 not (isSynTyCon tycon), -- ...but not a synonym
1136 all tcIsTyVarTy arg_tys, -- Applied to type variables
1137 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1138 -- This last condition checks that all the type variables are distinct
1142 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1145 (first_ty : _) = tys
1147 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1148 text "where T is not a synonym, and a,b,c are distinct type variables")
1150 check_tyvars dflags clas tys
1151 -- Check that at least one isn't a type variable
1152 -- unless -fallow-undecideable-instances
1153 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1154 | not (all tcIsTyVarTy tys) = returnM ()
1155 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1157 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1160 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1164 instTypeErr pp_ty msg
1165 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,