2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
6 Monadic type operations
8 This module contains monadic operations over types that contain
13 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
15 --------------------------------
16 -- Creating new mutable type variables
18 newFlexiTyVarTy, -- Kind -> TcM TcType
19 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
20 newKindVar, newKindVars,
23 newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
24 isFilledMetaTyVar, isFlexiMetaTyVar,
26 --------------------------------
27 -- Creating new evidence variables
28 newEvVar, newCoVar, newEvVars,
29 newIP, newDict, newSilentGiven, isSilentEvVar,
31 newWantedEvVar, newWantedEvVars,
32 newTcEvBinds, addTcEvBind,
34 --------------------------------
36 tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
37 tcInstType, instMetaTyVar,
38 tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
39 tcSkolDFunType, tcSuperSkolTyVars,
41 --------------------------------
42 -- Checking type validity
43 Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
44 SourceTyCtxt(..), checkValidTheta,
45 checkValidInstHead, checkValidInstance,
46 checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
48 growPredTyVars, growThetaTyVars, validDerivPred,
50 --------------------------------
52 zonkType, mkZonkTcTyVar, zonkTcPredType,
53 zonkTcTypeCarefully, skolemiseUnboundMetaTyVar,
54 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
55 zonkQuantifiedTyVar, zonkQuantifiedTyVars,
56 zonkTcType, zonkTcTypes, zonkTcThetaType,
57 zonkTcKindToKind, zonkTcKind,
58 zonkImplication, zonkEvVar, zonkWantedEvVar, zonkFlavoredEvVar,
59 zonkWC, zonkWantedEvVars,
64 readKindVar, writeKindVar
67 #include "HsVersions.h"
78 import HsSyn -- HsType
79 import TcRnMonad -- TcType, amongst others
93 import Unique( Unique )
97 import Data.List ( (\\) )
101 %************************************************************************
105 %************************************************************************
108 newKindVar :: TcM TcKind
109 newKindVar = do { uniq <- newUnique
110 ; ref <- newMutVar Flexi
111 ; return (mkTyVarTy (mkKindVar uniq ref)) }
113 newKindVars :: Int -> TcM [TcKind]
114 newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
118 %************************************************************************
120 Evidence variables; range over constraints we can abstract over
122 %************************************************************************
125 newEvVars :: TcThetaType -> TcM [EvVar]
126 newEvVars theta = mapM newEvVar theta
128 newWantedEvVar :: TcPredType -> TcM EvVar
129 newWantedEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
130 newWantedEvVar (ClassP cls tys) = newDict cls tys
131 newWantedEvVar (IParam ip ty) = newIP ip ty
133 newWantedEvVars :: TcThetaType -> TcM [EvVar]
134 newWantedEvVars theta = mapM newWantedEvVar theta
137 newEvVar :: TcPredType -> TcM EvVar
138 -- Creates new *rigid* variables for predicates
139 newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
140 newEvVar (ClassP cls tys) = newDict cls tys
141 newEvVar (IParam ip ty) = newIP ip ty
143 newCoVar :: TcType -> TcType -> TcM CoVar
145 = do { name <- newName (mkVarOccFS (fsLit "co"))
146 ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
148 newIP :: IPName Name -> TcType -> TcM IpId
150 = do { name <- newName (getOccName (ipNameName ip))
151 ; return (mkLocalId name (mkPredTy (IParam ip ty))) }
153 newDict :: Class -> [TcType] -> TcM DictId
155 = do { name <- newName (mkDictOcc (getOccName cls))
156 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
158 newName :: OccName -> TcM Name
160 = do { uniq <- newUnique
162 ; return (mkInternalName uniq occ loc) }
165 newSilentGiven :: PredType -> TcM EvVar
166 -- Make a dictionary for a "silent" given dictionary
167 -- Behaves just like any EvVar except that it responds True to isSilentDict
168 -- This is used only to suppress confusing error reports
169 newSilentGiven (ClassP cls tys)
170 = do { uniq <- newUnique
171 ; let name = mkSystemName uniq (mkDictOcc (getOccName cls))
172 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
173 newSilentGiven (EqPred ty1 ty2)
174 = do { uniq <- newUnique
175 ; let name = mkSystemName uniq (mkTyVarOccFS (fsLit "co"))
176 ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
177 newSilentGiven pred@(IParam {})
178 = pprPanic "newSilentDict" (ppr pred) -- Implicit parameters rejected earlier
180 isSilentEvVar :: EvVar -> Bool
181 isSilentEvVar v = isSystemName (Var.varName v)
182 -- Notice that all *other* evidence variables get Internal Names
186 %************************************************************************
188 SkolemTvs (immutable)
190 %************************************************************************
193 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
194 -> TcType -- Type to instantiate
195 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
196 -- (type vars (excl coercion vars), preds (incl equalities), rho)
197 tcInstType inst_tyvars ty
198 = case tcSplitForAllTys ty of
199 ([], rho) -> let -- There may be overloading despite no type variables;
200 -- (?x :: Int) => Int -> Int
201 (theta, tau) = tcSplitPhiTy rho
203 return ([], theta, tau)
205 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
207 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
208 -- Either the tyvars are freshly made, by inst_tyvars,
209 -- or any nested foralls have different binders.
210 -- Either way, zipTopTvSubst is ok
212 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
213 ; return (tyvars', theta, tau) }
215 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
216 -- Instantiate a type signature with skolem constants, but
217 -- do *not* give them fresh names, because we want the name to
218 -- be in the type environment: it is lexically scoped.
219 tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty
221 tcSuperSkolTyVars :: [TyVar] -> [TcTyVar]
222 -- Make skolem constants, but do *not* give them new names, as above
223 -- Moreover, make them "super skolems"; see comments with superSkolemTv
224 tcSuperSkolTyVars tyvars
225 = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) superSkolemTv
228 tcInstSkolTyVar :: Bool -> TyVar -> TcM TcTyVar
229 -- Instantiate the tyvar, using
230 -- * the occ-name and kind of the supplied tyvar,
231 -- * the unique from the monad,
232 -- * the location either from the tyvar (skol_info = SigSkol)
233 -- or from the monad (otherwise)
234 tcInstSkolTyVar overlappable tyvar
235 = do { uniq <- newUnique
237 ; let new_name = mkInternalName uniq occ loc
238 ; return (mkTcTyVar new_name kind (SkolemTv overlappable)) }
240 old_name = tyVarName tyvar
241 occ = nameOccName old_name
242 kind = tyVarKind tyvar
244 tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar]
245 tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars
247 tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
248 tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars
250 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
251 -- Instantiate a type with fresh skolem constants
252 -- Binding location comes from the monad
253 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
255 tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
256 -- Make meta SigTv type variables for patten-bound scoped type varaibles
257 -- We use SigTvs for them, so that they can't unify with arbitrary types
258 tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
259 -- ToDo: the "function binding site is bogus
263 %************************************************************************
265 MetaTvs (meta type variables; mutable)
267 %************************************************************************
270 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
271 -- Make a new meta tyvar out of thin air
272 newMetaTyVar meta_info kind
273 = do { uniq <- newMetaUnique
274 ; ref <- newMutVar Flexi
275 ; let name = mkTcTyVarName uniq s
276 s = case meta_info of
280 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
282 mkTcTyVarName :: Unique -> FastString -> Name
283 -- Make sure that fresh TcTyVar names finish with a digit
284 -- leaving the un-cluttered names free for user names
285 mkTcTyVarName uniq str = mkSysTvName uniq str
287 instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
288 -- Make a new meta tyvar whose Name and Kind
289 -- come from an existing TyVar
290 instMetaTyVar meta_info tyvar
291 = do { uniq <- newMetaUnique
292 ; ref <- newMutVar Flexi
293 ; let name = mkSystemName uniq (getOccName tyvar)
294 kind = tyVarKind tyvar
295 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
297 readMetaTyVar :: TyVar -> TcM MetaDetails
298 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
299 readMutVar (metaTvRef tyvar)
301 isFilledMetaTyVar :: TyVar -> TcM Bool
302 -- True of a filled-in (Indirect) meta type variable
304 | not (isTcTyVar tv) = return False
305 | MetaTv _ ref <- tcTyVarDetails tv
306 = do { details <- readMutVar ref
307 ; return (isIndirect details) }
308 | otherwise = return False
310 isFlexiMetaTyVar :: TyVar -> TcM Bool
311 -- True of a un-filled-in (Flexi) meta type variable
313 | not (isTcTyVar tv) = return False
314 | MetaTv _ ref <- tcTyVarDetails tv
315 = do { details <- readMutVar ref
316 ; return (isFlexi details) }
317 | otherwise = return False
320 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
321 -- Write into a currently-empty MetaTyVar
323 writeMetaTyVar tyvar ty
325 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
327 -- Everything from here on only happens if DEBUG is on
328 | not (isTcTyVar tyvar)
329 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
332 | MetaTv _ ref <- tcTyVarDetails tyvar
333 = writeMetaTyVarRef tyvar ref ty
336 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
340 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
341 -- Here the tyvar is for error checking only;
342 -- the ref cell must be for the same tyvar
343 writeMetaTyVarRef tyvar ref ty
345 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
346 ; writeMutVar ref (Indirect ty) }
348 -- Everything from here on only happens if DEBUG is on
349 | not (isPredTy tv_kind) -- Don't check kinds for updates to coercion variables
350 , not (ty_kind `isSubKind` tv_kind)
351 = WARN( True, hang (text "Ill-kinded update to meta tyvar")
352 2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
356 = do { meta_details <- readMutVar ref;
357 ; ASSERT2( isFlexi meta_details,
358 hang (text "Double update of meta tyvar")
359 2 (ppr tyvar $$ ppr meta_details) )
361 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
362 ; writeMutVar ref (Indirect ty) }
364 tv_kind = tyVarKind tyvar
365 ty_kind = typeKind ty
369 %************************************************************************
373 %************************************************************************
376 newFlexiTyVar :: Kind -> TcM TcTyVar
377 newFlexiTyVar kind = newMetaTyVar TauTv kind
379 newFlexiTyVarTy :: Kind -> TcM TcType
380 newFlexiTyVarTy kind = do
381 tc_tyvar <- newFlexiTyVar kind
382 return (TyVarTy tc_tyvar)
384 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
385 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
387 tcInstTyVar :: TyVar -> TcM TcTyVar
388 -- Instantiate with a META type variable
389 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
391 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
392 -- Instantiate with META type variables
394 = do { tc_tvs <- mapM tcInstTyVar tyvars
395 ; let tys = mkTyVarTys tc_tvs
396 ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
397 -- Since the tyvars are freshly made,
398 -- they cannot possibly be captured by
399 -- any existing for-alls. Hence zipTopTvSubst
403 %************************************************************************
407 %************************************************************************
410 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
412 | isSkolemTyVar sig_tv
413 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
415 = ASSERT( isSigTyVar sig_tv )
416 do { ty <- zonkTcTyVar sig_tv
417 ; return (tcGetTyVar "zonkSigTyVar" ty) }
418 -- 'ty' is bound to be a type variable, because SigTvs
419 -- can only be unified with type variables
424 %************************************************************************
426 \subsection{Zonking -- the exernal interfaces}
428 %************************************************************************
430 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
431 To improve subsequent calls to the same function it writes the zonked set back into
435 tcGetGlobalTyVars :: TcM TcTyVarSet
437 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
438 ; gbl_tvs <- readMutVar gtv_var
439 ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
440 ; writeMutVar gtv_var gbl_tvs'
444 ----------------- Type variables
447 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
448 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
450 zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
451 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
453 ----------------- Types
454 zonkTcTypeCarefully :: TcType -> TcM TcType
455 -- Do not zonk type variables free in the environment
456 zonkTcTypeCarefully ty
457 = do { env_tvs <- tcGetGlobalTyVars
458 ; zonkType (zonk_tv env_tvs) ty }
461 | tv `elemVarSet` env_tvs
462 = return (TyVarTy tv)
464 = ASSERT( isTcTyVar tv )
465 case tcTyVarDetails tv of
466 SkolemTv {} -> return (TyVarTy tv)
467 RuntimeUnk {} -> return (TyVarTy tv)
468 FlatSkol ty -> zonkType (zonk_tv env_tvs) ty
469 MetaTv _ ref -> do { cts <- readMutVar ref
471 Flexi -> return (TyVarTy tv)
472 Indirect ty -> zonkType (zonk_tv env_tvs) ty }
474 zonkTcType :: TcType -> TcM TcType
475 -- Simply look through all Flexis
476 zonkTcType ty = zonkType zonkTcTyVar ty
478 zonkTcTyVar :: TcTyVar -> TcM TcType
479 -- Simply look through all Flexis
481 = ASSERT2( isTcTyVar tv, ppr tv )
482 case tcTyVarDetails tv of
483 SkolemTv {} -> return (TyVarTy tv)
484 RuntimeUnk {} -> return (TyVarTy tv)
485 FlatSkol ty -> zonkTcType ty
486 MetaTv _ ref -> do { cts <- readMutVar ref
488 Flexi -> return (TyVarTy tv)
489 Indirect ty -> zonkTcType ty }
491 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
492 -- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
493 zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
496 = case tcTyVarDetails tv of
497 SkolemTv {} -> return (TyVarTy tv)
498 RuntimeUnk {} -> return (TyVarTy tv)
499 FlatSkol ty -> zonkType zonk_tv ty
500 MetaTv _ ref -> do { cts <- readMutVar ref
502 Flexi -> zonk_flexi tv
503 Indirect ty -> zonkType zonk_tv ty }
505 = case lookupTyVar subst tv of
506 Just ty -> zonkType zonk_tv ty
507 Nothing -> return (TyVarTy tv)
509 zonkTcTypes :: [TcType] -> TcM [TcType]
510 zonkTcTypes tys = mapM zonkTcType tys
512 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
513 zonkTcThetaType theta = mapM zonkTcPredType theta
515 zonkTcPredType :: TcPredType -> TcM TcPredType
516 zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts
517 zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t
518 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
521 ------------------- These ...ToType, ...ToKind versions
522 are used at the end of type checking
525 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
526 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
528 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
529 -- The quantified type variables often include meta type variables
530 -- we want to freeze them into ordinary type variables, and
531 -- default their kind (e.g. from OpenTypeKind to TypeKind)
532 -- -- see notes with Kind.defaultKind
533 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
534 -- bound occurences of the original type variable will get zonked to
535 -- the immutable version.
537 -- We leave skolem TyVars alone; they are immutable.
538 zonkQuantifiedTyVar tv
539 = ASSERT2( isTcTyVar tv, ppr tv )
540 case tcTyVarDetails tv of
541 SkolemTv {} -> WARN( True, ppr tv ) -- Dec10: Can this really happen?
542 do { kind <- zonkTcType (tyVarKind tv)
543 ; return $ setTyVarKind tv kind }
544 -- It might be a skolem type variable,
545 -- for example from a user type signature
549 -- [Sept 04] Check for non-empty.
550 -- See note [Silly Type Synonym]
551 (readMutVar _ref >>= \cts ->
554 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
557 skolemiseUnboundMetaTyVar tv vanillaSkolemTv
558 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
560 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
561 -- We have a Meta tyvar with a ref-cell inside it
562 -- Skolemise it, including giving it a new Name, so that
563 -- we are totally out of Meta-tyvar-land
564 -- We create a skolem TyVar, not a regular TyVar
565 -- See Note [Zonking to Skolem]
566 skolemiseUnboundMetaTyVar tv details
567 = ASSERT2( isMetaTyVar tv, ppr tv )
568 do { span <- getSrcSpanM -- Get the location from "here"
569 -- ie where we are generalising
570 ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land
571 ; let final_kind = defaultKind (tyVarKind tv)
572 final_name = mkInternalName uniq (getOccName tv) span
573 final_tv = mkTcTyVar final_name final_kind details
574 ; writeMetaTyVar tv (mkTyVarTy final_tv)
579 zonkImplication :: Implication -> TcM Implication
580 zonkImplication implic@(Implic { ic_given = given
583 = do { -- No need to zonk the skolems
584 ; given' <- mapM zonkEvVar given
585 ; loc' <- zonkGivenLoc loc
586 ; wanted' <- zonkWC wanted
587 ; return (implic { ic_given = given'
588 , ic_wanted = wanted'
591 zonkEvVar :: EvVar -> TcM EvVar
592 zonkEvVar var = do { ty' <- zonkTcType (varType var)
593 ; return (setVarType var ty') }
595 zonkFlavoredEvVar :: FlavoredEvVar -> TcM FlavoredEvVar
596 zonkFlavoredEvVar (EvVarX ev fl)
597 = do { ev' <- zonkEvVar ev
598 ; fl' <- zonkFlavor fl
599 ; return (EvVarX ev' fl') }
601 zonkWC :: WantedConstraints -> TcM WantedConstraints
602 zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
603 = do { flat' <- zonkWantedEvVars flat
604 ; implic' <- mapBagM zonkImplication implic
605 ; insol' <- mapBagM zonkFlavoredEvVar insol
606 ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
608 zonkWantedEvVars :: Bag WantedEvVar -> TcM (Bag WantedEvVar)
609 zonkWantedEvVars = mapBagM zonkWantedEvVar
611 zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
612 zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) }
614 zonkFlavor :: CtFlavor -> TcM CtFlavor
615 zonkFlavor (Given loc) = do { loc' <- zonkGivenLoc loc; return (Given loc') }
616 zonkFlavor fl = return fl
618 zonkGivenLoc :: GivenLoc -> TcM GivenLoc
619 -- GivenLocs may have unification variables inside them!
620 zonkGivenLoc (CtLoc skol_info span ctxt)
621 = do { skol_info' <- zonkSkolemInfo skol_info
622 ; return (CtLoc skol_info' span ctxt) }
624 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
625 zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty
626 ; return (SigSkol cx ty') }
627 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
628 ; return (InferSkol ntys') }
630 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
631 zonkSkolemInfo skol_info = return skol_info
634 Note [Silly Type Synonyms]
635 ~~~~~~~~~~~~~~~~~~~~~~~~~~
637 type C u a = u -- Note 'a' unused
639 foo :: (forall a. C u a -> C u a) -> u
643 bar = foo (\t -> t + t)
645 * From the (\t -> t+t) we get type {Num d} => d -> d
648 * Now unify with type of foo's arg, and we get:
649 {Num (C d a)} => C d a -> C d a
652 * Now abstract over the 'a', but float out the Num (C d a) constraint
653 because it does not 'really' mention a. (see exactTyVarsOfType)
654 The arg to foo becomes
657 * So we get a dict binding for Num (C d a), which is zonked to give
659 [Note Sept 04: now that we are zonking quantified type variables
660 on construction, the 'a' will be frozen as a regular tyvar on
661 quantification, so the floated dict will still have type (C d a).
662 Which renders this whole note moot; happily!]
664 * Then the \/\a abstraction has a zonked 'a' in it.
666 All very silly. I think its harmless to ignore the problem. We'll end up with
667 a \/\a in the final result but all the occurrences of a will be zonked to ()
669 Note [Zonking to Skolem]
670 ~~~~~~~~~~~~~~~~~~~~~~~~
671 We used to zonk quantified type variables to regular TyVars. However, this
672 leads to problems. Consider this program from the regression test suite:
674 eval :: Int -> String -> String -> String
675 eval 0 root actual = evalRHS 0 root actual
678 evalRHS 0 root actual = eval 0 root actual
680 It leads to the deferral of an equality (wrapped in an implication constraint)
682 forall a. (String -> String -> String) ~ a
684 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
685 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
686 This has the *side effect* of also zonking the `a' in the deferred equality
687 (which at this point is being handed around wrapped in an implication
690 Finally, the equality (with the zonked `a') will be handed back to the
691 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
692 If we zonk `a' with a regular type variable, we will have this regular type
693 variable now floating around in the simplifier, which in many places assumes to
694 only see proper TcTyVars.
696 We can avoid this problem by zonking with a skolem. The skolem is rigid
697 (which we require for a quantified variable), but is still a TcTyVar that the
698 simplifier knows how to deal with.
701 %************************************************************************
703 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
705 %* For internal use only! *
707 %************************************************************************
710 -- For unbound, mutable tyvars, zonkType uses the function given to it
711 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
712 -- type variable and zonks the kind too
714 zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars
715 -> TcType -> TcM Type
716 zonkType zonk_tc_tyvar ty
719 go (TyConApp tc tys) = do tys' <- mapM go tys
720 return (TyConApp tc tys')
722 go (PredTy p) = do p' <- go_pred p
725 go (FunTy arg res) = do arg' <- go arg
727 return (FunTy arg' res')
729 go (AppTy fun arg) = do fun' <- go fun
731 return (mkAppTy fun' arg')
732 -- NB the mkAppTy; we might have instantiated a
733 -- type variable to a type constructor, so we need
734 -- to pull the TyConApp to the top.
736 -- The two interesting cases!
737 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
738 | otherwise = return (TyVarTy tyvar)
739 -- Ordinary (non Tc) tyvars occur inside quantified types
741 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
743 tyvar' <- return tyvar
744 return (ForAllTy tyvar' ty')
746 go_pred (ClassP c tys) = do tys' <- mapM go tys
747 return (ClassP c tys')
748 go_pred (IParam n ty) = do ty' <- go ty
749 return (IParam n ty')
750 go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
752 return (EqPred ty1' ty2')
754 mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var
755 -> TcTyVar -> TcM TcType
756 mkZonkTcTyVar unbound_var_fn tyvar
757 = ASSERT( isTcTyVar tyvar )
758 case tcTyVarDetails tyvar of
759 SkolemTv {} -> return (TyVarTy tyvar)
760 RuntimeUnk {} -> return (TyVarTy tyvar)
761 FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
762 MetaTv _ ref -> do { cts <- readMutVar ref
764 Flexi -> unbound_var_fn tyvar
765 Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
770 %************************************************************************
774 %************************************************************************
777 readKindVar :: KindVar -> TcM (MetaDetails)
778 writeKindVar :: KindVar -> TcKind -> TcM ()
779 readKindVar kv = readMutVar (kindVarRef kv)
780 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
783 zonkTcKind :: TcKind -> TcM TcKind
784 zonkTcKind k = zonkTcType k
787 zonkTcKindToKind :: TcKind -> TcM Kind
788 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
789 -- Haskell specifies that * is to be used, so we follow that.
791 = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
794 %************************************************************************
796 \subsection{Checking a user type}
798 %************************************************************************
800 When dealing with a user-written type, we first translate it from an HsType
801 to a Type, performing kind checking, and then check various things that should
802 be true about it. We don't want to perform these checks at the same time
803 as the initial translation because (a) they are unnecessary for interface-file
804 types and (b) when checking a mutually recursive group of type and class decls,
805 we can't "look" at the tycons/classes yet. Also, the checks are are rather
806 diverse, and used to really mess up the other code.
808 One thing we check for is 'rank'.
810 Rank 0: monotypes (no foralls)
811 Rank 1: foralls at the front only, Rank 0 inside
812 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
814 basic ::= tyvar | T basic ... basic
816 r2 ::= forall tvs. cxt => r2a
817 r2a ::= r1 -> r2a | basic
818 r1 ::= forall tvs. cxt => r0
819 r0 ::= r0 -> r0 | basic
821 Another thing is to check that type synonyms are saturated.
822 This might not necessarily show up in kind checking.
824 data T k = MkT (k Int)
829 checkValidType :: UserTypeCtxt -> Type -> TcM ()
830 -- Checks that the type is valid for the given context
831 checkValidType ctxt ty = do
832 traceTc "checkValidType" (ppr ty)
833 unboxed <- xoptM Opt_UnboxedTuples
834 rank2 <- xoptM Opt_Rank2Types
835 rankn <- xoptM Opt_RankNTypes
836 polycomp <- xoptM Opt_PolymorphicComponents
838 gen_rank n | rankn = ArbitraryRank
843 DefaultDeclCtxt-> MustBeMonoType
844 ResSigCtxt -> MustBeMonoType
845 LamPatSigCtxt -> gen_rank 0
846 BindPatSigCtxt -> gen_rank 0
847 TySynCtxt _ -> gen_rank 0
848 GenPatCtxt -> gen_rank 1
849 -- This one is a bit of a hack
850 -- See the forall-wrapping in TcClassDcl.mkGenericInstance
852 ExprSigCtxt -> gen_rank 1
853 FunSigCtxt _ -> gen_rank 1
854 ConArgCtxt _ | polycomp -> gen_rank 2
855 -- We are given the type of the entire
856 -- constructor, hence rank 1
857 | otherwise -> gen_rank 1
859 ForSigCtxt _ -> gen_rank 1
860 SpecInstCtxt -> gen_rank 1
861 ThBrackCtxt -> gen_rank 1
862 GenSigCtxt -> panic "checkValidType"
863 -- Can't happen; GenSigCtxt not used for *user* sigs
865 actual_kind = typeKind ty
867 kind_ok = case ctxt of
868 TySynCtxt _ -> True -- Any kind will do
869 ThBrackCtxt -> True -- Any kind will do
870 ResSigCtxt -> isSubOpenTypeKind actual_kind
871 ExprSigCtxt -> isSubOpenTypeKind actual_kind
872 GenPatCtxt -> isLiftedTypeKind actual_kind
873 ForSigCtxt _ -> isLiftedTypeKind actual_kind
874 _ -> isSubArgTypeKind actual_kind
876 ubx_tup = case ctxt of
877 TySynCtxt _ | unboxed -> UT_Ok
878 ExprSigCtxt | unboxed -> UT_Ok
879 ThBrackCtxt | unboxed -> UT_Ok
882 -- Check the internal validity of the type itself
883 check_type rank ubx_tup ty
885 -- Check that the thing has kind Type, and is lifted if necessary
886 -- Do this second, becuase we can't usefully take the kind of an
887 -- ill-formed type such as (a~Int)
888 checkTc kind_ok (kindErr actual_kind)
890 traceTc "checkValidType done" (ppr ty)
892 checkValidMonoType :: Type -> TcM ()
893 checkValidMonoType ty = check_mono_type MustBeMonoType ty
898 data Rank = ArbitraryRank -- Any rank ok
899 | MustBeMonoType -- Monotype regardless of flags
900 | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes
901 | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms
902 | Rank Int -- Rank n, but could be more with -XRankNTypes
904 decRank :: Rank -> Rank -- Function arguments
905 decRank (Rank 0) = Rank 0
906 decRank (Rank n) = Rank (n-1)
907 decRank other_rank = other_rank
909 nonZeroRank :: Rank -> Bool
910 nonZeroRank ArbitraryRank = True
911 nonZeroRank (Rank n) = n>0
912 nonZeroRank _ = False
914 ----------------------------------------
915 data UbxTupFlag = UT_Ok | UT_NotOk
916 -- The "Ok" version means "ok if UnboxedTuples is on"
918 ----------------------------------------
919 check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere
920 -- No unlifted types of any kind
921 check_mono_type rank ty
922 = do { check_type rank UT_NotOk ty
923 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
925 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
926 -- The args say what the *type context* requires, independent
927 -- of *flag* settings. You test the flag settings at usage sites.
929 -- Rank is allowed rank for function args
930 -- Rank 0 means no for-alls anywhere
932 check_type rank ubx_tup ty
933 | not (null tvs && null theta)
934 = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
935 -- Reject e.g. (Maybe (?x::Int => Int)),
936 -- with a decent error message
937 ; check_valid_theta SigmaCtxt theta
938 ; check_type rank ubx_tup tau -- Allow foralls to right of arrow
939 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
941 (tvs, theta, tau) = tcSplitSigmaTy ty
943 -- Naked PredTys should, I think, have been rejected before now
944 check_type _ _ ty@(PredTy {})
945 = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type")
947 check_type _ _ (TyVarTy _) = return ()
949 check_type rank _ (FunTy arg_ty res_ty)
950 = do { check_type (decRank rank) UT_NotOk arg_ty
951 ; check_type rank UT_Ok res_ty }
953 check_type rank _ (AppTy ty1 ty2)
954 = do { check_arg_type rank ty1
955 ; check_arg_type rank ty2 }
957 check_type rank ubx_tup ty@(TyConApp tc tys)
959 = do { -- Check that the synonym has enough args
960 -- This applies equally to open and closed synonyms
961 -- It's OK to have an *over-applied* type synonym
962 -- data Tree a b = ...
963 -- type Foo a = Tree [a]
964 -- f :: Foo a b -> ...
965 checkTc (tyConArity tc <= length tys) arity_msg
967 -- See Note [Liberal type synonyms]
968 ; liberal <- xoptM Opt_LiberalTypeSynonyms
969 ; if not liberal || isSynFamilyTyCon tc then
970 -- For H98 and synonym families, do check the type args
971 mapM_ (check_mono_type SynArgMonoType) tys
973 else -- In the liberal case (only for closed syns), expand then check
975 Just ty' -> check_type rank ubx_tup ty'
976 Nothing -> pprPanic "check_tau_type" (ppr ty)
979 | isUnboxedTupleTyCon tc
980 = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
981 ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
983 ; impred <- xoptM Opt_ImpredicativeTypes
984 ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
985 -- c.f. check_arg_type
986 -- However, args are allowed to be unlifted, or
987 -- more unboxed tuples, so can't use check_arg_ty
988 ; mapM_ (check_type rank' UT_Ok) tys }
991 = mapM_ (check_arg_type rank) tys
994 ubx_tup_ok ub_tuples_allowed = case ubx_tup of
995 UT_Ok -> ub_tuples_allowed
999 tc_arity = tyConArity tc
1001 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1002 ubx_tup_msg = ubxArgTyErr ty
1004 check_type _ _ ty = pprPanic "check_type" (ppr ty)
1006 ----------------------------------------
1007 check_arg_type :: Rank -> Type -> TcM ()
1008 -- The sort of type that can instantiate a type variable,
1009 -- or be the argument of a type constructor.
1010 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
1011 -- Other unboxed types are very occasionally allowed as type
1012 -- arguments depending on the kind of the type constructor
1014 -- For example, we want to reject things like:
1016 -- instance Ord a => Ord (forall s. T s a)
1018 -- g :: T s (forall b.b)
1020 -- NB: unboxed tuples can have polymorphic or unboxed args.
1021 -- This happens in the workers for functions returning
1022 -- product types with polymorphic components.
1023 -- But not in user code.
1024 -- Anyway, they are dealt with by a special case in check_tau_type
1026 check_arg_type rank ty
1027 = do { impred <- xoptM Opt_ImpredicativeTypes
1028 ; let rank' = case rank of -- Predictive => must be monotype
1029 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
1030 _other | impred -> ArbitraryRank
1031 | otherwise -> TyConArgMonoType
1032 -- Make sure that MustBeMonoType is propagated,
1033 -- so that we don't suggest -XImpredicativeTypes in
1034 -- (Ord (forall a.a)) => a -> a
1035 -- and so that if it Must be a monotype, we check that it is!
1037 ; check_type rank' UT_NotOk ty
1038 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1040 ----------------------------------------
1041 forAllTyErr :: Rank -> Type -> SDoc
1043 = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
1046 suggestion = case rank of
1047 Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
1048 TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
1049 SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
1050 _ -> empty -- Polytype is always illegal
1052 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
1053 unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1054 ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1056 kindErr :: Kind -> SDoc
1057 kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1060 Note [Liberal type synonyms]
1061 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1062 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1063 doing validity checking. This allows us to instantiate a synonym defn
1064 with a for-all type, or with a partially-applied type synonym.
1068 Here, T is partially applied, so it's illegal in H98. But if you
1069 expand S first, then T we get just
1073 IMPORTANT: suppose T is a type synonym. Then we must do validity
1074 checking on an appliation (T ty1 ty2)
1076 *either* before expansion (i.e. check ty1, ty2)
1077 *or* after expansion (i.e. expand T ty1 ty2, and then check)
1080 If we do both, we get exponential behaviour!!
1082 data TIACons1 i r c = c i ::: r c
1083 type TIACons2 t x = TIACons1 t (TIACons1 t x)
1084 type TIACons3 t x = TIACons2 t (TIACons1 t x)
1085 type TIACons4 t x = TIACons2 t (TIACons2 t x)
1086 type TIACons7 t x = TIACons4 t (TIACons3 t x)
1089 %************************************************************************
1091 \subsection{Checking a theta or source type}
1093 %************************************************************************
1096 -- Enumerate the contexts in which a "source type", <S>, can occur
1100 -- or (N a) where N is a newtype
1103 = ClassSCCtxt Name -- Superclasses of clas
1104 -- class <S> => C a where ...
1105 | SigmaCtxt -- Theta part of a normal for-all type
1106 -- f :: <S> => a -> a
1107 | DataTyCtxt Name -- Theta part of a data decl
1108 -- data <S> => T a = MkT a
1109 | TypeCtxt -- Source type in an ordinary type
1111 | InstThetaCtxt -- Context of an instance decl
1112 -- instance <S> => C [a] where ...
1114 pprSourceTyCtxt :: SourceTyCtxt -> SDoc
1115 pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
1116 pprSourceTyCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type")
1117 pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
1118 pprSourceTyCtxt InstThetaCtxt = ptext (sLit "the context of an instance declaration")
1119 pprSourceTyCtxt TypeCtxt = ptext (sLit "the context of a type")
1123 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1124 checkValidTheta ctxt theta
1125 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1127 -------------------------
1128 check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
1129 check_valid_theta _ []
1131 check_valid_theta ctxt theta = do
1133 warnTc (notNull dups) (dupPredWarn dups)
1134 mapM_ (check_pred_ty dflags ctxt) theta
1136 (_,dups) = removeDups cmpPred theta
1138 -------------------------
1139 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1140 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1141 = do { -- Class predicates are valid in all contexts
1142 ; checkTc (arity == n_tys) arity_err
1144 -- Check the form of the argument types
1145 ; mapM_ checkValidMonoType tys
1146 ; checkTc (check_class_pred_tys dflags ctxt tys)
1147 (predTyVarErr pred $$ how_to_allow)
1150 class_name = className cls
1151 arity = classArity cls
1153 arity_err = arityErr "Class" class_name arity n_tys
1154 how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
1157 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
1158 = do { -- Equational constraints are valid in all contexts if type
1159 -- families are permitted
1160 ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1161 ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
1162 (eqSuperClassErr pred)
1164 -- Check the form of the argument types
1165 ; checkValidMonoType ty1
1166 ; checkValidMonoType ty2
1169 check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
1170 -- Implicit parameters only allowed in type
1171 -- signatures; not in instance decls, superclasses etc
1172 -- The reason for not allowing implicit params in instances is a bit
1174 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
1175 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
1176 -- discharge all the potential usas of the ?x in e. For example, a
1177 -- constraint Foo [Int] might come out of e,and applying the
1178 -- instance decl would show up two uses of ?x.
1181 check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
1183 -------------------------
1184 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1185 check_class_pred_tys dflags ctxt tys
1187 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1188 InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1189 -- Further checks on head and theta in
1190 -- checkInstTermination
1191 _ -> flexible_contexts || all tyvar_head tys
1193 flexible_contexts = xopt Opt_FlexibleContexts dflags
1194 undecidable_ok = xopt Opt_UndecidableInstances dflags
1196 -------------------------
1197 tyvar_head :: Type -> Bool
1198 tyvar_head ty -- Haskell 98 allows predicates of form
1199 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1200 | otherwise -- where a is a type variable
1201 = case tcSplitAppTy_maybe ty of
1202 Just (ty, _) -> tyvar_head ty
1209 is ambiguous if P contains generic variables
1210 (i.e. one of the Vs) that are not mentioned in tau
1212 However, we need to take account of functional dependencies
1213 when we speak of 'mentioned in tau'. Example:
1214 class C a b | a -> b where ...
1216 forall x y. (C x y) => x
1217 is not ambiguous because x is mentioned and x determines y
1219 NB; the ambiguity check is only used for *user* types, not for types
1220 coming from inteface files. The latter can legitimately have
1221 ambiguous types. Example
1223 class S a where s :: a -> (Int,Int)
1224 instance S Char where s _ = (1,1)
1225 f:: S a => [a] -> Int -> (Int,Int)
1226 f (_::[a]) x = (a*x,b)
1227 where (a,b) = s (undefined::a)
1229 Here the worker for f gets the type
1230 fw :: forall a. S a => Int -> (# Int, Int #)
1232 If the list of tv_names is empty, we have a monotype, and then we
1233 don't need to check for ambiguity either, because the test can't fail
1236 In addition, GHC insists that at least one type variable
1237 in each constraint is in V. So we disallow a type like
1238 forall a. Eq b => b -> b
1239 even in a scope where b is in scope.
1242 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1243 checkAmbiguity forall_tyvars theta tau_tyvars
1244 = mapM_ complain (filter is_ambig theta)
1246 complain pred = addErrTc (ambigErr pred)
1247 extended_tau_vars = growThetaTyVars theta tau_tyvars
1249 -- See Note [Implicit parameters and ambiguity] in TcSimplify
1250 is_ambig pred = isClassPred pred &&
1251 any ambig_var (varSetElems (tyVarsOfPred pred))
1253 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1254 not (ct_var `elemVarSet` extended_tau_vars)
1256 ambigErr :: PredType -> SDoc
1258 = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPredTy pred),
1259 nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1260 ptext (sLit "must be reachable from the type after the '=>'"))]
1263 Note [Growing the tau-tvs using constraints]
1264 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1265 (growInstsTyVars insts tvs) is the result of extending the set
1266 of tyvars tvs using all conceivable links from pred
1268 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1269 Then grow precs tvs = {a,b,c}
1272 growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
1273 -- See Note [Growing the tau-tvs using constraints]
1274 growThetaTyVars theta tvs
1276 | otherwise = fixVarSet mk_next tvs
1278 mk_next tvs = foldr grow_one tvs theta
1279 grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
1281 growPredTyVars :: TcPredType
1282 -> TyVarSet -- The set to extend
1283 -> TyVarSet -- TyVars of the predicate if it intersects
1284 -- the set, or is implicit parameter
1285 growPredTyVars pred tvs
1286 | IParam {} <- pred = pred_tvs -- See Note [Implicit parameters and ambiguity]
1287 | pred_tvs `intersectsVarSet` tvs = pred_tvs
1288 | otherwise = emptyVarSet
1290 pred_tvs = tyVarsOfPred pred
1293 Note [Implicit parameters and ambiguity]
1294 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1295 Only a *class* predicate can give rise to ambiguity
1296 An *implicit parameter* cannot. For example:
1297 foo :: (?x :: [a]) => Int
1299 is fine. The call site will suppply a particular 'x'
1301 Furthermore, the type variables fixed by an implicit parameter
1302 propagate to the others. E.g.
1303 foo :: (Show a, ?x::[a]) => Int
1305 The type of foo looks ambiguous. But it isn't, because at a call site
1307 let ?x = 5::Int in foo
1308 and all is well. In effect, implicit parameters are, well, parameters,
1309 so we can take their type variables into account as part of the
1310 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
1314 checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
1315 checkThetaCtxt ctxt theta
1316 = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1317 ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
1319 eqSuperClassErr :: PredType -> SDoc
1320 eqSuperClassErr pred
1321 = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:"))
1324 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
1325 badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPredTy pred
1326 eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPredTy pred
1328 parens (ptext (sLit "Use -XTypeFamilies to permit this"))
1329 predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
1330 nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)]
1331 dupPredWarn :: [[PredType]] -> SDoc
1332 dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPredTy (map head dups)
1334 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
1335 arityErr kind name n m
1336 = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1337 n_arguments <> comma, text "but has been given",
1338 if m==0 then text "none" else int m]
1340 n_arguments | n == 0 = ptext (sLit "no arguments")
1341 | n == 1 = ptext (sLit "1 argument")
1342 | True = hsep [int n, ptext (sLit "arguments")]
1345 %************************************************************************
1347 \subsection{Checking for a decent instance head type}
1349 %************************************************************************
1351 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1352 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1354 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1355 flag is on, or (2)~the instance is imported (they must have been
1356 compiled elsewhere). In these cases, we let them go through anyway.
1358 We can also have instances for functions: @instance Foo (a -> b) ...@.
1361 checkValidInstHead :: Class -> [Type] -> TcM ()
1362 checkValidInstHead clas tys
1363 = do { dflags <- getDOpts
1365 -- If GlasgowExts then check at least one isn't a type variable
1366 ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
1367 all tcInstHeadTyNotSynonym tys)
1368 (instTypeErr pp_pred head_type_synonym_msg)
1369 ; checkTc (xopt Opt_FlexibleInstances dflags ||
1370 all tcInstHeadTyAppAllTyVars tys)
1371 (instTypeErr pp_pred head_type_args_tyvars_msg)
1372 ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
1374 (instTypeErr pp_pred head_one_type_msg)
1375 -- May not contain type family applications
1376 ; mapM_ checkTyFamFreeness tys
1378 ; mapM_ checkValidMonoType tys
1379 -- For now, I only allow tau-types (not polytypes) in
1380 -- the head of an instance decl.
1381 -- E.g. instance C (forall a. a->a) is rejected
1382 -- One could imagine generalising that, but I'm not sure
1383 -- what all the consequences might be
1387 pp_pred = pprClassPred clas tys
1388 head_type_synonym_msg = parens (
1389 text "All instance types must be of the form (T t1 ... tn)" $$
1390 text "where T is not a synonym." $$
1391 text "Use -XTypeSynonymInstances if you want to disable this.")
1393 head_type_args_tyvars_msg = parens (vcat [
1394 text "All instance types must be of the form (T a1 ... an)",
1395 text "where a1 ... an are *distinct type variables*,",
1396 text "and each type variable appears at most once in the instance head.",
1397 text "Use -XFlexibleInstances if you want to disable this."])
1399 head_one_type_msg = parens (
1400 text "Only one type can be given in an instance head." $$
1401 text "Use -XMultiParamTypeClasses if you want to allow more.")
1403 instTypeErr :: SDoc -> SDoc -> SDoc
1404 instTypeErr pp_ty msg
1405 = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty,
1410 %************************************************************************
1412 \subsection{Checking instance for termination}
1414 %************************************************************************
1417 checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType
1418 -> Class -> [TcType] -> TcM ()
1419 checkValidInstance hs_type tyvars theta clas inst_tys
1420 = setSrcSpan (getLoc hs_type) $
1421 do { setSrcSpan head_loc (checkValidInstHead clas inst_tys)
1422 ; checkValidTheta InstThetaCtxt theta
1423 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1425 -- Check that instance inference will terminate (if we care)
1426 -- For Haskell 98 this will already have been done by checkValidTheta,
1427 -- but as we may be using other extensions we need to check.
1428 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1429 ; unless undecidable_ok $
1430 mapM_ addErrTc (checkInstTermination inst_tys theta)
1432 -- The Coverage Condition
1433 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1434 (instTypeErr (pprClassPred clas inst_tys) msg)
1437 msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1440 -- The location of the "head" of the instance
1441 head_loc = case hs_type of
1442 L _ (HsForAllTy _ _ _ (L loc _)) -> loc
1446 Termination test: the so-called "Paterson conditions" (see Section 5 of
1447 "Understanding functionsl dependencies via Constraint Handling Rules,
1450 We check that each assertion in the context satisfies:
1451 (1) no variable has more occurrences in the assertion than in the head, and
1452 (2) the assertion has fewer constructors and variables (taken together
1453 and counting repetitions) than the head.
1454 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1455 (which have already been checked) guarantee termination.
1457 The underlying idea is that
1459 for any ground substitution, each assertion in the
1460 context has fewer type constructors than the head.
1464 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1465 checkInstTermination tys theta
1466 = mapCatMaybes check theta
1469 size = sizeTypes tys
1471 | not (null (fvPred pred \\ fvs))
1472 = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1473 | sizePred pred >= size
1474 = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1478 predUndecErr :: PredType -> SDoc -> SDoc
1479 predUndecErr pred msg = sep [msg,
1480 nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)]
1482 nomoreMsg, smallerMsg, undecidableMsg :: SDoc
1483 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1484 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1485 undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
1488 validDeivPred checks for OK 'deriving' context. See Note [Exotic
1489 derived instance contexts] in TcSimplify. However the predicate is
1490 here because it uses sizeTypes, fvTypes.
1493 validDerivPred :: PredType -> Bool
1494 validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
1495 where fvs = fvTypes tys
1496 validDerivPred _ = False
1500 %************************************************************************
1502 Checking type instance well-formedness and termination
1504 %************************************************************************
1507 -- Check that a "type instance" is well-formed (which includes decidability
1508 -- unless -XUndecidableInstances is given).
1510 checkValidTypeInst :: [Type] -> Type -> TcM ()
1511 checkValidTypeInst typats rhs
1512 = do { -- left-hand side contains no type family applications
1513 -- (vanilla synonyms are fine, though)
1514 ; mapM_ checkTyFamFreeness typats
1516 -- the right-hand side is a tau type
1517 ; checkValidMonoType rhs
1519 -- we have a decidable instance unless otherwise permitted
1520 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1521 ; unless undecidable_ok $
1522 mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1525 -- Make sure that each type family instance is
1526 -- (1) strictly smaller than the lhs,
1527 -- (2) mentions no type variable more often than the lhs, and
1528 -- (3) does not contain any further type family instances.
1530 checkFamInst :: [Type] -- lhs
1531 -> [(TyCon, [Type])] -- type family instances
1533 checkFamInst lhsTys famInsts
1534 = mapCatMaybes check famInsts
1536 size = sizeTypes lhsTys
1537 fvs = fvTypes lhsTys
1539 | not (all isTyFamFree tys)
1540 = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1541 | not (null (fvTypes tys \\ fvs))
1542 = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1543 | size <= sizeTypes tys
1544 = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1548 famInst = TyConApp tc tys
1550 -- Ensure that no type family instances occur in a type.
1552 checkTyFamFreeness :: Type -> TcM ()
1553 checkTyFamFreeness ty
1554 = checkTc (isTyFamFree ty) $
1555 tyFamInstIllegalErr ty
1557 -- Check that a type does not contain any type family applications.
1559 isTyFamFree :: Type -> Bool
1560 isTyFamFree = null . tyFamInsts
1564 tyFamInstIllegalErr :: Type -> SDoc
1565 tyFamInstIllegalErr ty
1566 = hang (ptext (sLit "Illegal type synonym family application in instance") <>
1570 famInstUndecErr :: Type -> SDoc -> SDoc
1571 famInstUndecErr ty msg
1573 nest 2 (ptext (sLit "in the type family application:") <+>
1576 nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
1577 nestedMsg = ptext (sLit "Nested type family application")
1578 nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head")
1579 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1583 %************************************************************************
1585 \subsection{Auxiliary functions}
1587 %************************************************************************
1590 -- Free variables of a type, retaining repetitions, and expanding synonyms
1591 fvType :: Type -> [TyVar]
1592 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1593 fvType (TyVarTy tv) = [tv]
1594 fvType (TyConApp _ tys) = fvTypes tys
1595 fvType (PredTy pred) = fvPred pred
1596 fvType (FunTy arg res) = fvType arg ++ fvType res
1597 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1598 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1600 fvTypes :: [Type] -> [TyVar]
1601 fvTypes tys = concat (map fvType tys)
1603 fvPred :: PredType -> [TyVar]
1604 fvPred (ClassP _ tys') = fvTypes tys'
1605 fvPred (IParam _ ty) = fvType ty
1606 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1608 -- Size of a type: the number of variables and constructors
1609 sizeType :: Type -> Int
1610 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1611 sizeType (TyVarTy _) = 1
1612 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1613 sizeType (PredTy pred) = sizePred pred
1614 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1615 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1616 sizeType (ForAllTy _ ty) = sizeType ty
1618 sizeTypes :: [Type] -> Int
1619 sizeTypes xs = sum (map sizeType xs)
1621 -- Size of a predicate
1623 -- We are considering whether *class* constraints terminate
1624 -- Once we get into an implicit parameter or equality we
1625 -- can't get back to a class constraint, so it's safe
1626 -- to say "size 0". See Trac #4200.
1627 sizePred :: PredType -> Int
1628 sizePred (ClassP _ tys') = sizeTypes tys'
1629 sizePred (IParam {}) = 0
1630 sizePred (EqPred {}) = 0