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 tcValidInstHeadTy, 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, 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 -- Unrefined SkolemTv or virgin MetaTv/SigSkolTv
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 -- Also used for types in SPECIALISE pragmas
659 | ExprSigCtxt -- Expression type signature
660 | ConArgCtxt Name -- Data constructor argument
661 | TySynCtxt Name -- RHS of a type synonym decl
662 | GenPatCtxt -- Pattern in generic decl
663 -- f{| a+b |} (Inl x) = ...
664 | PatSigCtxt -- Type sig in pattern
666 | ResSigCtxt -- Result type sig
668 | ForSigCtxt Name -- Foreign inport or export signature
669 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
670 | DefaultDeclCtxt -- Types in a default declaration
671 | SpecInstCtxt -- SPECIALISE instance pragma
673 -- Notes re TySynCtxt
674 -- We allow type synonyms that aren't types; e.g. type List = []
676 -- If the RHS mentions tyvars that aren't in scope, we'll
677 -- quantify over them:
678 -- e.g. type T = a->a
679 -- will become type T = forall a. a->a
681 -- With gla-exts that's right, but for H98 we should complain.
684 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
685 pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt
687 pprUserTypeCtxt ty (FunSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
688 pprUserTypeCtxt ty ExprSigCtxt = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
689 pprUserTypeCtxt ty (ConArgCtxt c) = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
690 pprUserTypeCtxt ty (TySynCtxt c) = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
691 nest 2 (ptext SLIT(", namely") <+> ppr ty)]
692 pprUserTypeCtxt ty GenPatCtxt = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
693 pprUserTypeCtxt ty PatSigCtxt = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
694 pprUserTypeCtxt ty ResSigCtxt = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
695 pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
696 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
697 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
698 pprUserTypeCtxt ty SpecInstCtxt = sep [ptext SLIT("In a SPECIALISE instance pragma:"), nest 2 (ppr ty)]
700 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
704 checkValidType :: UserTypeCtxt -> Type -> TcM ()
705 -- Checks that the type is valid for the given context
706 checkValidType ctxt ty
707 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
708 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
710 rank | gla_exts = Arbitrary
712 = case ctxt of -- Haskell 98
715 DefaultDeclCtxt-> Rank 0
717 TySynCtxt _ -> Rank 0
718 ExprSigCtxt -> Rank 1
719 FunSigCtxt _ -> Rank 1
720 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
721 -- constructor, hence rank 1
722 ForSigCtxt _ -> Rank 1
723 RuleSigCtxt _ -> Rank 1
724 SpecInstCtxt -> Rank 1
726 actual_kind = typeKind ty
728 kind_ok = case ctxt of
729 TySynCtxt _ -> True -- Any kind will do
730 ResSigCtxt -> isOpenTypeKind actual_kind
731 ExprSigCtxt -> isOpenTypeKind actual_kind
732 GenPatCtxt -> isLiftedTypeKind actual_kind
733 ForSigCtxt _ -> isLiftedTypeKind actual_kind
734 other -> isArgTypeKind actual_kind
736 ubx_tup | not gla_exts = UT_NotOk
737 | otherwise = case ctxt of
741 -- Unboxed tuples ok in function results,
742 -- but for type synonyms we allow them even at
745 -- Check that the thing has kind Type, and is lifted if necessary
746 checkTc kind_ok (kindErr actual_kind) `thenM_`
748 -- Check the internal validity of the type itself
749 check_poly_type rank ubx_tup ty `thenM_`
751 traceTc (text "checkValidType done" <+> ppr ty)
756 data Rank = Rank Int | Arbitrary
758 decRank :: Rank -> Rank
759 decRank Arbitrary = Arbitrary
760 decRank (Rank n) = Rank (n-1)
762 ----------------------------------------
763 data UbxTupFlag = UT_Ok | UT_NotOk
764 -- The "Ok" version means "ok if -fglasgow-exts is on"
766 ----------------------------------------
767 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
768 check_poly_type (Rank 0) ubx_tup ty
769 = check_tau_type (Rank 0) ubx_tup ty
771 check_poly_type rank ubx_tup ty
773 (tvs, theta, tau) = tcSplitSigmaTy ty
775 check_valid_theta SigmaCtxt theta `thenM_`
776 check_tau_type (decRank rank) ubx_tup tau `thenM_`
777 checkFreeness tvs theta `thenM_`
778 checkAmbiguity tvs theta (tyVarsOfType tau)
780 ----------------------------------------
781 check_arg_type :: Type -> TcM ()
782 -- The sort of type that can instantiate a type variable,
783 -- or be the argument of a type constructor.
784 -- Not an unboxed tuple, not a forall.
785 -- Other unboxed types are very occasionally allowed as type
786 -- arguments depending on the kind of the type constructor
788 -- For example, we want to reject things like:
790 -- instance Ord a => Ord (forall s. T s a)
792 -- g :: T s (forall b.b)
794 -- NB: unboxed tuples can have polymorphic or unboxed args.
795 -- This happens in the workers for functions returning
796 -- product types with polymorphic components.
797 -- But not in user code.
798 -- Anyway, they are dealt with by a special case in check_tau_type
801 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
802 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
804 ----------------------------------------
805 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
806 -- Rank is allowed rank for function args
807 -- No foralls otherwise
809 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
810 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
811 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
813 -- Naked PredTys don't usually show up, but they can as a result of
814 -- {-# SPECIALISE instance Ord Char #-}
815 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
816 -- are handled, but the quick thing is just to permit PredTys here.
817 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
818 check_source_ty dflags TypeCtxt sty
820 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
821 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
822 = check_poly_type rank UT_NotOk arg_ty `thenM_`
823 check_tau_type rank UT_Ok res_ty
825 check_tau_type rank ubx_tup (AppTy ty1 ty2)
826 = check_arg_type ty1 `thenM_` check_arg_type ty2
828 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
829 -- Synonym notes are built only when the synonym is
830 -- saturated (see Type.mkSynTy)
831 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
833 -- If -fglasgow-exts then don't check the 'note' part.
834 -- This allows us to instantiate a synonym defn with a
835 -- for-all type, or with a partially-applied type synonym.
836 -- e.g. type T a b = a
839 -- Here, T is partially applied, so it's illegal in H98.
840 -- But if you expand S first, then T we get just
845 -- For H98, do check the un-expanded part
846 check_tau_type rank ubx_tup syn
849 check_tau_type rank ubx_tup ty
851 check_tau_type rank ubx_tup (NoteTy other_note ty)
852 = check_tau_type rank ubx_tup ty
854 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
856 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
857 -- synonym application, leaving it to checkValidType (i.e. right here)
859 checkTc syn_arity_ok arity_msg `thenM_`
860 mappM_ check_arg_type tys
862 | isUnboxedTupleTyCon tc
863 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
864 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
865 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
866 -- Args are allowed to be unlifted, or
867 -- more unboxed tuples, so can't use check_arg_ty
870 = mappM_ check_arg_type tys
873 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
875 syn_arity_ok = tc_arity <= n_args
876 -- It's OK to have an *over-applied* type synonym
877 -- data Tree a b = ...
878 -- type Foo a = Tree [a]
879 -- f :: Foo a b -> ...
881 tc_arity = tyConArity tc
883 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
884 ubx_tup_msg = ubxArgTyErr ty
886 ----------------------------------------
887 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
888 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
889 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
890 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
895 %************************************************************************
897 \subsection{Checking a theta or source type}
899 %************************************************************************
902 -- Enumerate the contexts in which a "source type", <S>, can occur
906 -- or (N a) where N is a newtype
909 = ClassSCCtxt Name -- Superclasses of clas
910 -- class <S> => C a where ...
911 | SigmaCtxt -- Theta part of a normal for-all type
912 -- f :: <S> => a -> a
913 | DataTyCtxt Name -- Theta part of a data decl
914 -- data <S> => T a = MkT a
915 | TypeCtxt -- Source type in an ordinary type
917 | InstThetaCtxt -- Context of an instance decl
918 -- instance <S> => C [a] where ...
919 | InstHeadCtxt -- Head of an instance decl
920 -- instance ... => Eq a where ...
922 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
923 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
924 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
925 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
926 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
927 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
931 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
932 checkValidTheta ctxt theta
933 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
935 -------------------------
936 check_valid_theta ctxt []
938 check_valid_theta ctxt theta
939 = getDOpts `thenM` \ dflags ->
940 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
941 -- Actually, in instance decls and type signatures,
942 -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
943 -- so this error can only fire for the context of a class or
945 mappM_ (check_source_ty dflags ctxt) theta
947 (_,dups) = removeDups tcCmpPred theta
949 -------------------------
950 check_source_ty dflags ctxt pred@(ClassP cls tys)
951 = -- Class predicates are valid in all contexts
952 checkTc (arity == n_tys) arity_err `thenM_`
954 -- Check the form of the argument types
955 mappM_ check_arg_type tys `thenM_`
956 checkTc (check_class_pred_tys dflags ctxt tys)
957 (predTyVarErr pred $$ how_to_allow)
960 class_name = className cls
961 arity = classArity cls
963 arity_err = arityErr "Class" class_name arity n_tys
965 how_to_allow = case ctxt of
966 InstHeadCtxt -> empty -- Should not happen
967 InstThetaCtxt -> parens undecidableMsg
968 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
970 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
971 -- Implicit parameters only allows in type
972 -- signatures; not in instance decls, superclasses etc
973 -- The reason for not allowing implicit params in instances is a bit subtle
974 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
975 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
976 -- discharge all the potential usas of the ?x in e. For example, a
977 -- constraint Foo [Int] might come out of e,and applying the
978 -- instance decl would show up two uses of ?x.
981 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
983 -------------------------
984 check_class_pred_tys dflags ctxt tys
986 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
987 InstHeadCtxt -> True -- We check for instance-head
988 -- formation in checkValidInstHead
989 InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
990 other -> gla_exts || all tyvar_head tys
992 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
993 gla_exts = dopt Opt_GlasgowExts dflags
995 -------------------------
996 tyvar_head ty -- Haskell 98 allows predicates of form
997 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
998 | otherwise -- where a is a type variable
999 = case tcSplitAppTy_maybe ty of
1000 Just (ty, _) -> tyvar_head ty
1007 is ambiguous if P contains generic variables
1008 (i.e. one of the Vs) that are not mentioned in tau
1010 However, we need to take account of functional dependencies
1011 when we speak of 'mentioned in tau'. Example:
1012 class C a b | a -> b where ...
1014 forall x y. (C x y) => x
1015 is not ambiguous because x is mentioned and x determines y
1017 NB; the ambiguity check is only used for *user* types, not for types
1018 coming from inteface files. The latter can legitimately have
1019 ambiguous types. Example
1021 class S a where s :: a -> (Int,Int)
1022 instance S Char where s _ = (1,1)
1023 f:: S a => [a] -> Int -> (Int,Int)
1024 f (_::[a]) x = (a*x,b)
1025 where (a,b) = s (undefined::a)
1027 Here the worker for f gets the type
1028 fw :: forall a. S a => Int -> (# Int, Int #)
1030 If the list of tv_names is empty, we have a monotype, and then we
1031 don't need to check for ambiguity either, because the test can't fail
1035 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1036 checkAmbiguity forall_tyvars theta tau_tyvars
1037 = mappM_ complain (filter is_ambig theta)
1039 complain pred = addErrTc (ambigErr pred)
1040 extended_tau_vars = grow theta tau_tyvars
1042 -- Only a *class* predicate can give rise to ambiguity
1043 -- An *implicit parameter* cannot. For example:
1044 -- foo :: (?x :: [a]) => Int
1046 -- is fine. The call site will suppply a particular 'x'
1047 is_ambig pred = isClassPred pred &&
1048 any ambig_var (varSetElems (tyVarsOfPred pred))
1050 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1051 not (ct_var `elemVarSet` extended_tau_vars)
1054 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1055 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1056 ptext SLIT("must be reachable from the type after the '=>'"))]
1059 In addition, GHC insists that at least one type variable
1060 in each constraint is in V. So we disallow a type like
1061 forall a. Eq b => b -> b
1062 even in a scope where b is in scope.
1065 checkFreeness forall_tyvars theta
1066 = mappM_ complain (filter is_free theta)
1068 is_free pred = not (isIPPred pred)
1069 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1070 bound_var ct_var = ct_var `elem` forall_tyvars
1071 complain pred = addErrTc (freeErr pred)
1074 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1075 ptext SLIT("are already in scope"),
1076 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1081 checkThetaCtxt ctxt theta
1082 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1083 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1085 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1086 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
1087 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1089 arityErr kind name n m
1090 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1091 n_arguments <> comma, text "but has been given", int m]
1093 n_arguments | n == 0 = ptext SLIT("no arguments")
1094 | n == 1 = ptext SLIT("1 argument")
1095 | True = hsep [int n, ptext SLIT("arguments")]
1099 %************************************************************************
1101 \subsection{Checking for a decent instance head type}
1103 %************************************************************************
1105 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1106 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1108 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1109 flag is on, or (2)~the instance is imported (they must have been
1110 compiled elsewhere). In these cases, we let them go through anyway.
1112 We can also have instances for functions: @instance Foo (a -> b) ...@.
1115 checkValidInstHead :: Type -> TcM (Class, [TcType])
1117 checkValidInstHead ty -- Should be a source type
1118 = case tcSplitPredTy_maybe ty of {
1119 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1122 case getClassPredTys_maybe pred of {
1123 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1126 getDOpts `thenM` \ dflags ->
1127 mappM_ check_arg_type tys `thenM_`
1128 check_inst_head dflags clas tys `thenM_`
1132 check_inst_head dflags clas tys
1133 -- If GlasgowExts then check at least one isn't a type variable
1134 | dopt Opt_GlasgowExts dflags
1135 = check_tyvars dflags clas tys
1137 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1139 tcValidInstHeadTy first_ty
1143 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1146 (first_ty : _) = tys
1148 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1149 text "where T is not a synonym, and a,b,c are distinct type variables")
1151 check_tyvars dflags clas tys
1152 -- Check that at least one isn't a type variable
1153 -- unless -fallow-undecideable-instances
1154 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1155 | not (all tcIsTyVarTy tys) = returnM ()
1156 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1158 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1161 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1165 instTypeErr pp_ty msg
1166 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,