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(..), -- Friend; can see representation
53 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
54 TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
55 MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef,
56 tcCmpPred, tcEqType, 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, tcView,
65 pprPred, pprTheta, pprClassPred )
66 import Kind ( Kind(..), KindVar, kindVarRef, 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, findDupsEq )
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 _ ty2) = go ty2 -- Discard free-tyvar annotations
532 go (PredTy p) = go_pred p `thenM` \ p' ->
535 go (FunTy arg res) = go arg `thenM` \ arg' ->
536 go res `thenM` \ res' ->
537 returnM (FunTy arg' res')
539 go (AppTy fun arg) = go fun `thenM` \ fun' ->
540 go arg `thenM` \ arg' ->
541 returnM (mkAppTy fun' arg')
542 -- NB the mkAppTy; we might have instantiated a
543 -- type variable to a type constructor, so we need
544 -- to pull the TyConApp to the top.
546 -- The two interesting cases!
547 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn rflag tyvar
549 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
550 go ty `thenM` \ ty' ->
551 returnM (ForAllTy tyvar ty')
553 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
554 returnM (ClassP c tys')
555 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
556 returnM (IParam n ty')
558 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
559 -> Bool -- Consult the type refinement?
560 -> TcTyVar -> TcM TcType
561 zonkTyVar unbound_var_fn rflag tyvar
562 | not (isTcTyVar tyvar) -- When zonking (forall a. ...a...), the occurrences of
563 -- the quantified variable 'a' are TyVars not TcTyVars
564 = returnM (TyVarTy tyvar)
567 = condLookupTcTyVar rflag tyvar `thenM` \ details ->
569 -- If b is true, the variable was refined, and therefore it is okay
570 -- to continue refining inside. Otherwise it was wobbly and we should
571 -- not refine further inside.
572 IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
573 DoneTv (MetaTv _) -> unbound_var_fn tyvar -- Unbound meta type variable
574 DoneTv other -> return (TyVarTy tyvar) -- Rigid, no zonking necessary
579 %************************************************************************
583 %************************************************************************
586 readKindVar :: KindVar -> TcM (Maybe TcKind)
587 writeKindVar :: KindVar -> TcKind -> TcM ()
588 readKindVar kv = readMutVar (kindVarRef kv)
589 writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
592 zonkTcKind :: TcKind -> TcM TcKind
593 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
594 ; k2' <- zonkTcKind k2
595 ; returnM (FunKind k1' k2') }
596 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
599 Just k -> zonkTcKind k }
600 zonkTcKind other_kind = returnM other_kind
603 zonkTcKindToKind :: TcKind -> TcM Kind
604 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
605 ; k2' <- zonkTcKindToKind k2
606 ; returnM (FunKind k1' k2') }
608 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
610 Nothing -> return liftedTypeKind
611 Just k -> zonkTcKindToKind k }
613 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
614 zonkTcKindToKind other_kind = returnM other_kind
617 %************************************************************************
619 \subsection{Checking a user type}
621 %************************************************************************
623 When dealing with a user-written type, we first translate it from an HsType
624 to a Type, performing kind checking, and then check various things that should
625 be true about it. We don't want to perform these checks at the same time
626 as the initial translation because (a) they are unnecessary for interface-file
627 types and (b) when checking a mutually recursive group of type and class decls,
628 we can't "look" at the tycons/classes yet. Also, the checks are are rather
629 diverse, and used to really mess up the other code.
631 One thing we check for is 'rank'.
633 Rank 0: monotypes (no foralls)
634 Rank 1: foralls at the front only, Rank 0 inside
635 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
637 basic ::= tyvar | T basic ... basic
639 r2 ::= forall tvs. cxt => r2a
640 r2a ::= r1 -> r2a | basic
641 r1 ::= forall tvs. cxt => r0
642 r0 ::= r0 -> r0 | basic
644 Another thing is to check that type synonyms are saturated.
645 This might not necessarily show up in kind checking.
647 data T k = MkT (k Int)
653 = FunSigCtxt Name -- Function type signature
654 -- Also used for types in SPECIALISE pragmas
655 | ExprSigCtxt -- Expression type signature
656 | ConArgCtxt Name -- Data constructor argument
657 | TySynCtxt Name -- RHS of a type synonym decl
658 | GenPatCtxt -- Pattern in generic decl
659 -- f{| a+b |} (Inl x) = ...
660 | PatSigCtxt -- Type sig in pattern
662 | ResSigCtxt -- Result type sig
664 | ForSigCtxt Name -- Foreign inport or export signature
665 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
666 | DefaultDeclCtxt -- Types in a default declaration
667 | SpecInstCtxt -- SPECIALISE instance pragma
669 -- Notes re TySynCtxt
670 -- We allow type synonyms that aren't types; e.g. type List = []
672 -- If the RHS mentions tyvars that aren't in scope, we'll
673 -- quantify over them:
674 -- e.g. type T = a->a
675 -- will become type T = forall a. a->a
677 -- With gla-exts that's right, but for H98 we should complain.
680 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
681 pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt
683 pprUserTypeCtxt ty (FunSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
684 pprUserTypeCtxt ty ExprSigCtxt = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
685 pprUserTypeCtxt ty (ConArgCtxt c) = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
686 pprUserTypeCtxt ty (TySynCtxt c) = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
687 nest 2 (ptext SLIT(", namely") <+> ppr ty)]
688 pprUserTypeCtxt ty GenPatCtxt = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
689 pprUserTypeCtxt ty PatSigCtxt = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
690 pprUserTypeCtxt ty ResSigCtxt = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
691 pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
692 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
693 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
694 pprUserTypeCtxt ty SpecInstCtxt = sep [ptext SLIT("In a SPECIALISE instance pragma:"), nest 2 (ppr ty)]
696 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
700 checkValidType :: UserTypeCtxt -> Type -> TcM ()
701 -- Checks that the type is valid for the given context
702 checkValidType ctxt ty
703 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
704 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
706 rank | gla_exts = Arbitrary
708 = case ctxt of -- Haskell 98
711 DefaultDeclCtxt-> Rank 0
713 TySynCtxt _ -> Rank 0
714 ExprSigCtxt -> Rank 1
715 FunSigCtxt _ -> Rank 1
716 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
717 -- constructor, hence rank 1
718 ForSigCtxt _ -> Rank 1
719 RuleSigCtxt _ -> Rank 1
720 SpecInstCtxt -> 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 other_note ty)
825 = check_tau_type rank ubx_tup ty
827 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
829 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
830 -- synonym application, leaving it to checkValidType (i.e. right here)
832 do { -- It's OK to have an *over-applied* type synonym
833 -- data Tree a b = ...
834 -- type Foo a = Tree [a]
835 -- f :: Foo a b -> ...
837 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
838 Nothing -> failWithTc arity_msg
840 ; gla_exts <- doptM Opt_GlasgowExts
842 -- If -fglasgow-exts then don't check the type arguments
843 -- This allows us to instantiate a synonym defn with a
844 -- for-all type, or with a partially-applied type synonym.
845 -- e.g. type T a b = a
848 -- Here, T is partially applied, so it's illegal in H98.
849 -- But if you expand S first, then T we get just
854 -- For H98, do check the type args
855 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 }
872 tc_arity = tyConArity tc
874 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
875 ubx_tup_msg = ubxArgTyErr ty
877 ----------------------------------------
878 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
879 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
880 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
881 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
886 %************************************************************************
888 \subsection{Checking a theta or source type}
890 %************************************************************************
893 -- Enumerate the contexts in which a "source type", <S>, can occur
897 -- or (N a) where N is a newtype
900 = ClassSCCtxt Name -- Superclasses of clas
901 -- class <S> => C a where ...
902 | SigmaCtxt -- Theta part of a normal for-all type
903 -- f :: <S> => a -> a
904 | DataTyCtxt Name -- Theta part of a data decl
905 -- data <S> => T a = MkT a
906 | TypeCtxt -- Source type in an ordinary type
908 | InstThetaCtxt -- Context of an instance decl
909 -- instance <S> => C [a] where ...
910 | InstHeadCtxt -- Head of an instance decl
911 -- instance ... => Eq a where ...
913 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
914 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
915 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
916 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
917 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
918 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
922 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
923 checkValidTheta ctxt theta
924 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
926 -------------------------
927 check_valid_theta ctxt []
929 check_valid_theta ctxt theta
930 = getDOpts `thenM` \ dflags ->
931 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
932 -- Actually, in instance decls and type signatures,
933 -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
934 -- so this error can only fire for the context of a class or
936 mappM_ (check_source_ty dflags ctxt) theta
938 (_,dups) = removeDups tcCmpPred theta
940 -------------------------
941 check_source_ty dflags ctxt pred@(ClassP cls tys)
942 = -- Class predicates are valid in all contexts
943 checkTc (arity == n_tys) arity_err `thenM_`
945 -- Check the form of the argument types
946 mappM_ check_arg_type tys `thenM_`
947 checkTc (check_class_pred_tys dflags ctxt tys)
948 (predTyVarErr pred $$ how_to_allow)
951 class_name = className cls
952 arity = classArity cls
954 arity_err = arityErr "Class" class_name arity n_tys
956 how_to_allow = case ctxt of
957 InstHeadCtxt -> empty -- Should not happen
958 InstThetaCtxt -> parens undecidableMsg
959 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
961 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
962 -- Implicit parameters only allows in type
963 -- signatures; not in instance decls, superclasses etc
964 -- The reason for not allowing implicit params in instances is a bit subtle
965 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
966 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
967 -- discharge all the potential usas of the ?x in e. For example, a
968 -- constraint Foo [Int] might come out of e,and applying the
969 -- instance decl would show up two uses of ?x.
972 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
974 -------------------------
975 check_class_pred_tys dflags ctxt tys
977 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
978 InstHeadCtxt -> True -- We check for instance-head
979 -- formation in checkValidInstHead
980 InstThetaCtxt -> undecidable_ok || distinct_tyvars tys
981 other -> gla_exts || all tyvar_head tys
983 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
984 gla_exts = dopt Opt_GlasgowExts dflags
986 -------------------------
987 distinct_tyvars tys -- Check that the types are all distinct type variables
988 = all tcIsTyVarTy tys && null (findDupsEq tcEqType tys)
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 = sep [ptext SLIT("Non-type variables, or repeated type variables,"),
1082 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1083 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1085 arityErr kind name n m
1086 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1087 n_arguments <> comma, text "but has been given", int m]
1089 n_arguments | n == 0 = ptext SLIT("no arguments")
1090 | n == 1 = ptext SLIT("1 argument")
1091 | True = hsep [int n, ptext SLIT("arguments")]
1095 %************************************************************************
1097 \subsection{Checking for a decent instance head type}
1099 %************************************************************************
1101 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1102 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1104 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1105 flag is on, or (2)~the instance is imported (they must have been
1106 compiled elsewhere). In these cases, we let them go through anyway.
1108 We can also have instances for functions: @instance Foo (a -> b) ...@.
1111 checkValidInstHead :: Type -> TcM (Class, [TcType])
1113 checkValidInstHead ty -- Should be a source type
1114 = case tcSplitPredTy_maybe ty of {
1115 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1118 case getClassPredTys_maybe pred of {
1119 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1122 getDOpts `thenM` \ dflags ->
1123 mappM_ check_arg_type tys `thenM_`
1124 check_inst_head dflags clas tys `thenM_`
1128 check_inst_head dflags clas tys
1129 -- If GlasgowExts then check at least one isn't a type variable
1130 | dopt Opt_GlasgowExts dflags
1131 = check_tyvars dflags clas tys
1133 -- WITH HASKELL 98, MUST HAVE C (T a b c)
1135 tcValidInstHeadTy first_ty
1139 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1142 (first_ty : _) = tys
1144 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1145 text "where T is not a synonym, and a,b,c are distinct type variables")
1147 check_tyvars dflags clas tys
1148 -- Check that at least one isn't a type variable
1149 -- unless -fallow-undecideable-instances
1150 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1151 | not (all tcIsTyVarTy tys) = returnM ()
1152 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1154 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1157 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1161 instTypeErr pp_ty msg
1162 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,