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 newWantedCoVar, writeWantedCoVar, readWantedCoVar,
30 newIP, newDict, newSilentGiven, isSilentEvVar,
32 newWantedEvVar, newWantedEvVars,
33 newTcEvBinds, addTcEvBind,
35 --------------------------------
37 tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
38 tcInstType, instMetaTyVar,
39 tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
40 tcSkolDFunType, tcSuperSkolTyVars,
42 --------------------------------
43 -- Checking type validity
44 Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
45 SourceTyCtxt(..), checkValidTheta,
47 checkValidTypeInst, checkTyFamFreeness,
49 growPredTyVars, growThetaTyVars, validDerivPred,
51 --------------------------------
53 zonkType, mkZonkTcTyVar, zonkTcPredType,
55 skolemiseUnboundMetaTyVar,
56 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
57 zonkQuantifiedTyVar, zonkQuantifiedTyVars,
58 zonkTcType, zonkTcTypes, zonkTcThetaType,
59 zonkTcKindToKind, zonkTcKind,
60 zonkImplication, zonkEvVar, zonkWantedEvVar, zonkFlavoredEvVar,
61 zonkWC, zonkWantedEvVars,
66 readKindVar, writeKindVar
69 #include "HsVersions.h"
81 import HsSyn -- HsType
82 import TcRnMonad -- TcType, amongst others
96 import Unique( Unique )
100 import Data.List ( (\\) )
104 %************************************************************************
108 %************************************************************************
111 newKindVar :: TcM TcKind
112 newKindVar = do { uniq <- newUnique
113 ; ref <- newMutVar Flexi
114 ; return (mkTyVarTy (mkKindVar uniq ref)) }
116 newKindVars :: Int -> TcM [TcKind]
117 newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
121 %************************************************************************
123 Evidence variables; range over constraints we can abstract over
125 %************************************************************************
128 newEvVars :: TcThetaType -> TcM [EvVar]
129 newEvVars theta = mapM newEvVar theta
131 newWantedEvVar :: TcPredType -> TcM EvVar
132 newWantedEvVar (EqPred ty1 ty2) = newWantedCoVar ty1 ty2
133 newWantedEvVar (ClassP cls tys) = newDict cls tys
134 newWantedEvVar (IParam ip ty) = newIP ip ty
136 newWantedEvVars :: TcThetaType -> TcM [EvVar]
137 newWantedEvVars theta = mapM newWantedEvVar theta
139 newWantedCoVar :: TcType -> TcType -> TcM CoVar
140 newWantedCoVar ty1 ty2 = newCoVar ty1 ty2
143 newEvVar :: TcPredType -> TcM EvVar
144 -- Creates new *rigid* variables for predicates
145 newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
146 newEvVar (ClassP cls tys) = newDict cls tys
147 newEvVar (IParam ip ty) = newIP ip ty
149 newCoVar :: TcType -> TcType -> TcM CoVar
151 = do { name <- newName (mkTyVarOccFS (fsLit "co"))
152 ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
154 newIP :: IPName Name -> TcType -> TcM IpId
156 = do { name <- newName (getOccName (ipNameName ip))
157 ; return (mkLocalId name (mkPredTy (IParam ip ty))) }
159 newDict :: Class -> [TcType] -> TcM DictId
161 = do { name <- newName (mkDictOcc (getOccName cls))
162 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
164 newName :: OccName -> TcM Name
166 = do { uniq <- newUnique
168 ; return (mkInternalName uniq occ loc) }
171 newSilentGiven :: PredType -> TcM EvVar
172 -- Make a dictionary for a "silent" given dictionary
173 -- Behaves just like any EvVar except that it responds True to isSilentDict
174 -- This is used only to suppress confusing error reports
175 newSilentGiven (ClassP cls tys)
176 = do { uniq <- newUnique
177 ; let name = mkSystemName uniq (mkDictOcc (getOccName cls))
178 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
179 newSilentGiven (EqPred ty1 ty2)
180 = do { uniq <- newUnique
181 ; let name = mkSystemName uniq (mkTyVarOccFS (fsLit "co"))
182 ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
183 newSilentGiven pred@(IParam {})
184 = pprPanic "newSilentDict" (ppr pred) -- Implicit parameters rejected earlier
186 isSilentEvVar :: EvVar -> Bool
187 isSilentEvVar v = isSystemName (Var.varName v)
188 -- Notice that all *other* evidence variables get Internal Names
192 %************************************************************************
194 SkolemTvs (immutable)
196 %************************************************************************
199 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
200 -> TcType -- Type to instantiate
201 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
202 -- (type vars (excl coercion vars), preds (incl equalities), rho)
203 tcInstType inst_tyvars ty
204 = case tcSplitForAllTys ty of
205 ([], rho) -> let -- There may be overloading despite no type variables;
206 -- (?x :: Int) => Int -> Int
207 (theta, tau) = tcSplitPhiTy rho
209 return ([], theta, tau)
211 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
213 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
214 -- Either the tyvars are freshly made, by inst_tyvars,
215 -- or any nested foralls have different binders.
216 -- Either way, zipTopTvSubst is ok
218 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
219 ; return (tyvars', theta, tau) }
221 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
222 -- Instantiate a type signature with skolem constants, but
223 -- do *not* give them fresh names, because we want the name to
224 -- be in the type environment: it is lexically scoped.
225 tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty
227 tcSuperSkolTyVars :: [TyVar] -> [TcTyVar]
228 -- Make skolem constants, but do *not* give them new names, as above
229 -- Moreover, make them "super skolems"; see comments with superSkolemTv
230 tcSuperSkolTyVars tyvars
231 = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) superSkolemTv
234 tcInstSkolTyVar :: Bool -> TyVar -> TcM TcTyVar
235 -- Instantiate the tyvar, using
236 -- * the occ-name and kind of the supplied tyvar,
237 -- * the unique from the monad,
238 -- * the location either from the tyvar (skol_info = SigSkol)
239 -- or from the monad (otherwise)
240 tcInstSkolTyVar overlappable tyvar
241 = do { uniq <- newUnique
243 ; let new_name = mkInternalName uniq occ loc
244 ; return (mkTcTyVar new_name kind (SkolemTv overlappable)) }
246 old_name = tyVarName tyvar
247 occ = nameOccName old_name
248 kind = tyVarKind tyvar
250 tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar]
251 tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars
253 tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
254 tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars
256 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
257 -- Instantiate a type with fresh skolem constants
258 -- Binding location comes from the monad
259 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
261 tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
262 -- Make meta SigTv type variables for patten-bound scoped type varaibles
263 -- We use SigTvs for them, so that they can't unify with arbitrary types
264 tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
265 -- ToDo: the "function binding site is bogus
269 %************************************************************************
271 MetaTvs (meta type variables; mutable)
273 %************************************************************************
276 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
277 -- Make a new meta tyvar out of thin air
278 newMetaTyVar meta_info kind
279 = do { uniq <- newMetaUnique
280 ; ref <- newMutVar Flexi
281 ; let name = mkTcTyVarName uniq s
282 s = case meta_info of
286 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
288 mkTcTyVarName :: Unique -> FastString -> Name
289 -- Make sure that fresh TcTyVar names finish with a digit
290 -- leaving the un-cluttered names free for user names
291 mkTcTyVarName uniq str = mkSysTvName uniq str
293 instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
294 -- Make a new meta tyvar whose Name and Kind
295 -- come from an existing TyVar
296 instMetaTyVar meta_info tyvar
297 = do { uniq <- newMetaUnique
298 ; ref <- newMutVar Flexi
299 ; let name = mkSystemName uniq (getOccName tyvar)
300 kind = tyVarKind tyvar
301 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
303 readMetaTyVar :: TyVar -> TcM MetaDetails
304 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
305 readMutVar (metaTvRef tyvar)
307 readWantedCoVar :: CoVar -> TcM MetaDetails
308 readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
309 readMutVar (metaTvRef covar)
311 isFilledMetaTyVar :: TyVar -> TcM Bool
312 -- True of a filled-in (Indirect) meta type variable
314 | not (isTcTyVar tv) = return False
315 | MetaTv _ ref <- tcTyVarDetails tv
316 = do { details <- readMutVar ref
317 ; return (isIndirect details) }
318 | otherwise = return False
320 isFlexiMetaTyVar :: TyVar -> TcM Bool
321 -- True of a un-filled-in (Flexi) meta type variable
323 | not (isTcTyVar tv) = return False
324 | MetaTv _ ref <- tcTyVarDetails tv
325 = do { details <- readMutVar ref
326 ; return (isFlexi details) }
327 | otherwise = return False
330 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
331 -- Write into a currently-empty MetaTyVar
333 writeMetaTyVar tyvar ty
335 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
337 -- Everything from here on only happens if DEBUG is on
338 | not (isTcTyVar tyvar)
339 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
342 | MetaTv _ ref <- tcTyVarDetails tyvar
343 = writeMetaTyVarRef tyvar ref ty
346 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
349 writeWantedCoVar :: CoVar -> Coercion -> TcM ()
350 writeWantedCoVar cv co = writeMetaTyVar cv co
353 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
354 -- Here the tyvar is for error checking only;
355 -- the ref cell must be for the same tyvar
356 writeMetaTyVarRef tyvar ref ty
358 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
359 ; writeMutVar ref (Indirect ty) }
361 -- Everything from here on only happens if DEBUG is on
362 | not (isPredTy tv_kind) -- Don't check kinds for updates to coercion variables
363 , not (ty_kind `isSubKind` tv_kind)
364 = WARN( True, hang (text "Ill-kinded update to meta tyvar")
365 2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
369 = do { meta_details <- readMutVar ref;
370 ; WARN( not (isFlexi meta_details),
371 hang (text "Double update of meta tyvar")
372 2 (ppr tyvar $$ ppr meta_details) )
374 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
375 ; writeMutVar ref (Indirect ty) }
377 tv_kind = tyVarKind tyvar
378 ty_kind = typeKind ty
382 %************************************************************************
386 %************************************************************************
389 newFlexiTyVar :: Kind -> TcM TcTyVar
390 newFlexiTyVar kind = newMetaTyVar TauTv kind
392 newFlexiTyVarTy :: Kind -> TcM TcType
393 newFlexiTyVarTy kind = do
394 tc_tyvar <- newFlexiTyVar kind
395 return (TyVarTy tc_tyvar)
397 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
398 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
400 tcInstTyVar :: TyVar -> TcM TcTyVar
401 -- Instantiate with a META type variable
402 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
404 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
405 -- Instantiate with META type variables
407 = do { tc_tvs <- mapM tcInstTyVar tyvars
408 ; let tys = mkTyVarTys tc_tvs
409 ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
410 -- Since the tyvars are freshly made,
411 -- they cannot possibly be captured by
412 -- any existing for-alls. Hence zipTopTvSubst
416 %************************************************************************
420 %************************************************************************
423 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
425 | isSkolemTyVar sig_tv
426 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
428 = ASSERT( isSigTyVar sig_tv )
429 do { ty <- zonkTcTyVar sig_tv
430 ; return (tcGetTyVar "zonkSigTyVar" ty) }
431 -- 'ty' is bound to be a type variable, because SigTvs
432 -- can only be unified with type variables
437 %************************************************************************
439 \subsection{Zonking -- the exernal interfaces}
441 %************************************************************************
443 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
444 To improve subsequent calls to the same function it writes the zonked set back into
448 tcGetGlobalTyVars :: TcM TcTyVarSet
450 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
451 ; gbl_tvs <- readMutVar gtv_var
452 ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
453 ; writeMutVar gtv_var gbl_tvs'
457 ----------------- Type variables
460 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
461 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
463 zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
464 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
466 ----------------- Types
467 zonkTcTypeCarefully :: TcType -> TcM TcType
468 -- Do not zonk type variables free in the environment
469 zonkTcTypeCarefully ty
470 = do { env_tvs <- tcGetGlobalTyVars
471 ; zonkType (zonk_tv env_tvs) ty }
474 | tv `elemVarSet` env_tvs
475 = return (TyVarTy tv)
477 = ASSERT( isTcTyVar tv )
478 case tcTyVarDetails tv of
479 SkolemTv {} -> return (TyVarTy tv)
480 RuntimeUnk {} -> return (TyVarTy tv)
481 FlatSkol ty -> zonkType (zonk_tv env_tvs) ty
482 MetaTv _ ref -> do { cts <- readMutVar ref
484 Flexi -> return (TyVarTy tv)
485 Indirect ty -> zonkType (zonk_tv env_tvs) ty }
487 zonkTcType :: TcType -> TcM TcType
488 -- Simply look through all Flexis
489 zonkTcType ty = zonkType zonkTcTyVar ty
491 zonkTcTyVar :: TcTyVar -> TcM TcType
492 -- Simply look through all Flexis
494 = ASSERT2( isTcTyVar tv, ppr tv )
495 case tcTyVarDetails tv of
496 SkolemTv {} -> return (TyVarTy tv)
497 RuntimeUnk {} -> return (TyVarTy tv)
498 FlatSkol ty -> zonkTcType ty
499 MetaTv _ ref -> do { cts <- readMutVar ref
501 Flexi -> return (TyVarTy tv)
502 Indirect ty -> zonkTcType ty }
504 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
505 -- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
506 zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
509 = case tcTyVarDetails tv of
510 SkolemTv {} -> return (TyVarTy tv)
511 RuntimeUnk {} -> return (TyVarTy tv)
512 FlatSkol ty -> zonkType zonk_tv ty
513 MetaTv _ ref -> do { cts <- readMutVar ref
515 Flexi -> zonk_flexi tv
516 Indirect ty -> zonkType zonk_tv ty }
518 = case lookupTyVar subst tv of
519 Just ty -> zonkType zonk_tv ty
520 Nothing -> return (TyVarTy tv)
522 zonkTcTypes :: [TcType] -> TcM [TcType]
523 zonkTcTypes tys = mapM zonkTcType tys
525 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
526 zonkTcThetaType theta = mapM zonkTcPredType theta
528 zonkTcPredType :: TcPredType -> TcM TcPredType
529 zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts
530 zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t
531 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
534 ------------------- These ...ToType, ...ToKind versions
535 are used at the end of type checking
538 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
539 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
541 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
542 -- The quantified type variables often include meta type variables
543 -- we want to freeze them into ordinary type variables, and
544 -- default their kind (e.g. from OpenTypeKind to TypeKind)
545 -- -- see notes with Kind.defaultKind
546 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
547 -- bound occurences of the original type variable will get zonked to
548 -- the immutable version.
550 -- We leave skolem TyVars alone; they are immutable.
551 zonkQuantifiedTyVar tv
552 = ASSERT2( isTcTyVar tv, ppr tv )
553 case tcTyVarDetails tv of
554 SkolemTv {} -> WARN( True, ppr tv ) -- Dec10: Can this really happen?
555 do { kind <- zonkTcType (tyVarKind tv)
556 ; return $ setTyVarKind tv kind }
557 -- It might be a skolem type variable,
558 -- for example from a user type signature
562 -- [Sept 04] Check for non-empty.
563 -- See note [Silly Type Synonym]
564 (readMutVar _ref >>= \cts ->
567 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
570 skolemiseUnboundMetaTyVar tv vanillaSkolemTv
571 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
573 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
574 -- We have a Meta tyvar with a ref-cell inside it
575 -- Skolemise it, including giving it a new Name, so that
576 -- we are totally out of Meta-tyvar-land
577 -- We create a skolem TyVar, not a regular TyVar
578 -- See Note [Zonking to Skolem]
579 skolemiseUnboundMetaTyVar tv details
580 = ASSERT2( isMetaTyVar tv, ppr tv )
581 do { span <- getSrcSpanM -- Get the location from "here"
582 -- ie where we are generalising
583 ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land
584 ; let final_kind = defaultKind (tyVarKind tv)
585 final_name = mkInternalName uniq (getOccName tv) span
586 final_tv = mkTcTyVar final_name final_kind details
587 ; writeMetaTyVar tv (mkTyVarTy final_tv)
592 zonkImplication :: Implication -> TcM Implication
593 zonkImplication implic@(Implic { ic_given = given
596 = do { -- No need to zonk the skolems
597 ; given' <- mapM zonkEvVar given
598 ; loc' <- zonkGivenLoc loc
599 ; wanted' <- zonkWC wanted
600 ; return (implic { ic_given = given'
601 , ic_wanted = wanted'
604 zonkEvVar :: EvVar -> TcM EvVar
605 zonkEvVar var = do { ty' <- zonkTcType (varType var)
606 ; return (setVarType var ty') }
608 zonkFlavoredEvVar :: FlavoredEvVar -> TcM FlavoredEvVar
609 zonkFlavoredEvVar (EvVarX ev fl)
610 = do { ev' <- zonkEvVar ev
611 ; fl' <- zonkFlavor fl
612 ; return (EvVarX ev' fl') }
614 zonkWC :: WantedConstraints -> TcM WantedConstraints
615 zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
616 = do { flat' <- zonkWantedEvVars flat
617 ; implic' <- mapBagM zonkImplication implic
618 ; insol' <- mapBagM zonkFlavoredEvVar insol
619 ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
621 zonkWantedEvVars :: Bag WantedEvVar -> TcM (Bag WantedEvVar)
622 zonkWantedEvVars = mapBagM zonkWantedEvVar
624 zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
625 zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) }
627 zonkFlavor :: CtFlavor -> TcM CtFlavor
628 zonkFlavor (Given loc) = do { loc' <- zonkGivenLoc loc; return (Given loc') }
629 zonkFlavor fl = return fl
631 zonkGivenLoc :: GivenLoc -> TcM GivenLoc
632 -- GivenLocs may have unification variables inside them!
633 zonkGivenLoc (CtLoc skol_info span ctxt)
634 = do { skol_info' <- zonkSkolemInfo skol_info
635 ; return (CtLoc skol_info' span ctxt) }
637 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
638 zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty
639 ; return (SigSkol cx ty') }
640 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
641 ; return (InferSkol ntys') }
643 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
644 zonkSkolemInfo skol_info = return skol_info
647 Note [Silly Type Synonyms]
648 ~~~~~~~~~~~~~~~~~~~~~~~~~~
650 type C u a = u -- Note 'a' unused
652 foo :: (forall a. C u a -> C u a) -> u
656 bar = foo (\t -> t + t)
658 * From the (\t -> t+t) we get type {Num d} => d -> d
661 * Now unify with type of foo's arg, and we get:
662 {Num (C d a)} => C d a -> C d a
665 * Now abstract over the 'a', but float out the Num (C d a) constraint
666 because it does not 'really' mention a. (see exactTyVarsOfType)
667 The arg to foo becomes
670 * So we get a dict binding for Num (C d a), which is zonked to give
672 [Note Sept 04: now that we are zonking quantified type variables
673 on construction, the 'a' will be frozen as a regular tyvar on
674 quantification, so the floated dict will still have type (C d a).
675 Which renders this whole note moot; happily!]
677 * Then the \/\a abstraction has a zonked 'a' in it.
679 All very silly. I think its harmless to ignore the problem. We'll end up with
680 a \/\a in the final result but all the occurrences of a will be zonked to ()
682 Note [Zonking to Skolem]
683 ~~~~~~~~~~~~~~~~~~~~~~~~
684 We used to zonk quantified type variables to regular TyVars. However, this
685 leads to problems. Consider this program from the regression test suite:
687 eval :: Int -> String -> String -> String
688 eval 0 root actual = evalRHS 0 root actual
691 evalRHS 0 root actual = eval 0 root actual
693 It leads to the deferral of an equality (wrapped in an implication constraint)
695 forall a. (String -> String -> String) ~ a
697 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
698 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
699 This has the *side effect* of also zonking the `a' in the deferred equality
700 (which at this point is being handed around wrapped in an implication
703 Finally, the equality (with the zonked `a') will be handed back to the
704 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
705 If we zonk `a' with a regular type variable, we will have this regular type
706 variable now floating around in the simplifier, which in many places assumes to
707 only see proper TcTyVars.
709 We can avoid this problem by zonking with a skolem. The skolem is rigid
710 (which we require for a quantified variable), but is still a TcTyVar that the
711 simplifier knows how to deal with.
714 %************************************************************************
716 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
718 %* For internal use only! *
720 %************************************************************************
723 -- For unbound, mutable tyvars, zonkType uses the function given to it
724 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
725 -- type variable and zonks the kind too
727 zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars
728 -> TcType -> TcM Type
729 zonkType zonk_tc_tyvar ty
732 go (TyConApp tc tys) = do tys' <- mapM go tys
733 return (TyConApp tc tys')
735 go (PredTy p) = do p' <- go_pred p
738 go (FunTy arg res) = do arg' <- go arg
740 return (FunTy arg' res')
742 go (AppTy fun arg) = do fun' <- go fun
744 return (mkAppTy fun' arg')
745 -- NB the mkAppTy; we might have instantiated a
746 -- type variable to a type constructor, so we need
747 -- to pull the TyConApp to the top.
749 -- The two interesting cases!
750 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
751 | otherwise = liftM TyVarTy $
752 zonkTyVar zonk_tc_tyvar tyvar
753 -- Ordinary (non Tc) tyvars occur inside quantified types
755 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
757 tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
758 return (ForAllTy tyvar' ty')
760 go_pred (ClassP c tys) = do tys' <- mapM go tys
761 return (ClassP c tys')
762 go_pred (IParam n ty) = do ty' <- go ty
763 return (IParam n ty')
764 go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
766 return (EqPred ty1' ty2')
768 mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var
769 -> TcTyVar -> TcM TcType
770 mkZonkTcTyVar unbound_var_fn tyvar
771 = ASSERT( isTcTyVar tyvar )
772 case tcTyVarDetails tyvar of
773 SkolemTv {} -> return (TyVarTy tyvar)
774 RuntimeUnk {} -> return (TyVarTy tyvar)
775 FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
776 MetaTv _ ref -> do { cts <- readMutVar ref
778 Flexi -> unbound_var_fn tyvar
779 Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
781 -- Zonk the kind of a non-TC tyvar in case it is a coercion variable
782 -- (their kind contains types).
783 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for a TcTyVar
784 -> TyVar -> TcM TyVar
785 zonkTyVar zonk_tc_tyvar tv
787 = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
788 ; return $ setTyVarKind tv kind }
789 | otherwise = return tv
794 %************************************************************************
798 %************************************************************************
801 readKindVar :: KindVar -> TcM (MetaDetails)
802 writeKindVar :: KindVar -> TcKind -> TcM ()
803 readKindVar kv = readMutVar (kindVarRef kv)
804 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
807 zonkTcKind :: TcKind -> TcM TcKind
808 zonkTcKind k = zonkTcType k
811 zonkTcKindToKind :: TcKind -> TcM Kind
812 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
813 -- Haskell specifies that * is to be used, so we follow that.
815 = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
818 %************************************************************************
820 \subsection{Checking a user type}
822 %************************************************************************
824 When dealing with a user-written type, we first translate it from an HsType
825 to a Type, performing kind checking, and then check various things that should
826 be true about it. We don't want to perform these checks at the same time
827 as the initial translation because (a) they are unnecessary for interface-file
828 types and (b) when checking a mutually recursive group of type and class decls,
829 we can't "look" at the tycons/classes yet. Also, the checks are are rather
830 diverse, and used to really mess up the other code.
832 One thing we check for is 'rank'.
834 Rank 0: monotypes (no foralls)
835 Rank 1: foralls at the front only, Rank 0 inside
836 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
838 basic ::= tyvar | T basic ... basic
840 r2 ::= forall tvs. cxt => r2a
841 r2a ::= r1 -> r2a | basic
842 r1 ::= forall tvs. cxt => r0
843 r0 ::= r0 -> r0 | basic
845 Another thing is to check that type synonyms are saturated.
846 This might not necessarily show up in kind checking.
848 data T k = MkT (k Int)
853 checkValidType :: UserTypeCtxt -> Type -> TcM ()
854 -- Checks that the type is valid for the given context
855 checkValidType ctxt ty = do
856 traceTc "checkValidType" (ppr ty)
857 unboxed <- xoptM Opt_UnboxedTuples
858 rank2 <- xoptM Opt_Rank2Types
859 rankn <- xoptM Opt_RankNTypes
860 polycomp <- xoptM Opt_PolymorphicComponents
862 gen_rank n | rankn = ArbitraryRank
867 DefaultDeclCtxt-> MustBeMonoType
868 ResSigCtxt -> MustBeMonoType
869 LamPatSigCtxt -> gen_rank 0
870 BindPatSigCtxt -> gen_rank 0
871 TySynCtxt _ -> gen_rank 0
872 GenPatCtxt -> gen_rank 1
873 -- This one is a bit of a hack
874 -- See the forall-wrapping in TcClassDcl.mkGenericInstance
876 ExprSigCtxt -> gen_rank 1
877 FunSigCtxt _ -> gen_rank 1
878 ConArgCtxt _ | polycomp -> gen_rank 2
879 -- We are given the type of the entire
880 -- constructor, hence rank 1
881 | otherwise -> gen_rank 1
883 ForSigCtxt _ -> gen_rank 1
884 SpecInstCtxt -> gen_rank 1
885 ThBrackCtxt -> gen_rank 1
886 GenSigCtxt -> panic "checkValidType"
887 -- Can't happen; GenSigCtxt not used for *user* sigs
889 actual_kind = typeKind ty
891 kind_ok = case ctxt of
892 TySynCtxt _ -> True -- Any kind will do
893 ThBrackCtxt -> True -- Any kind will do
894 ResSigCtxt -> isSubOpenTypeKind actual_kind
895 ExprSigCtxt -> isSubOpenTypeKind actual_kind
896 GenPatCtxt -> isLiftedTypeKind actual_kind
897 ForSigCtxt _ -> isLiftedTypeKind actual_kind
898 _ -> isSubArgTypeKind actual_kind
900 ubx_tup = case ctxt of
901 TySynCtxt _ | unboxed -> UT_Ok
902 ExprSigCtxt | unboxed -> UT_Ok
903 ThBrackCtxt | unboxed -> UT_Ok
906 -- Check the internal validity of the type itself
907 check_type rank ubx_tup ty
909 -- Check that the thing has kind Type, and is lifted if necessary
910 -- Do this second, becuase we can't usefully take the kind of an
911 -- ill-formed type such as (a~Int)
912 checkTc kind_ok (kindErr actual_kind)
914 traceTc "checkValidType done" (ppr ty)
916 checkValidMonoType :: Type -> TcM ()
917 checkValidMonoType ty = check_mono_type MustBeMonoType ty
922 data Rank = ArbitraryRank -- Any rank ok
923 | MustBeMonoType -- Monotype regardless of flags
924 | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes
925 | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms
926 | Rank Int -- Rank n, but could be more with -XRankNTypes
928 decRank :: Rank -> Rank -- Function arguments
929 decRank (Rank 0) = Rank 0
930 decRank (Rank n) = Rank (n-1)
931 decRank other_rank = other_rank
933 nonZeroRank :: Rank -> Bool
934 nonZeroRank ArbitraryRank = True
935 nonZeroRank (Rank n) = n>0
936 nonZeroRank _ = False
938 ----------------------------------------
939 data UbxTupFlag = UT_Ok | UT_NotOk
940 -- The "Ok" version means "ok if UnboxedTuples is on"
942 ----------------------------------------
943 check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere
944 -- No unlifted types of any kind
945 check_mono_type rank ty
946 = do { check_type rank UT_NotOk ty
947 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
949 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
950 -- The args say what the *type context* requires, independent
951 -- of *flag* settings. You test the flag settings at usage sites.
953 -- Rank is allowed rank for function args
954 -- Rank 0 means no for-alls anywhere
956 check_type rank ubx_tup ty
957 | not (null tvs && null theta)
958 = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
959 -- Reject e.g. (Maybe (?x::Int => Int)),
960 -- with a decent error message
961 ; check_valid_theta SigmaCtxt theta
962 ; check_type rank ubx_tup tau -- Allow foralls to right of arrow
963 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
965 (tvs, theta, tau) = tcSplitSigmaTy ty
967 -- Naked PredTys should, I think, have been rejected before now
968 check_type _ _ ty@(PredTy {})
969 = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type")
971 check_type _ _ (TyVarTy _) = return ()
973 check_type rank _ (FunTy arg_ty res_ty)
974 = do { check_type (decRank rank) UT_NotOk arg_ty
975 ; check_type rank UT_Ok res_ty }
977 check_type rank _ (AppTy ty1 ty2)
978 = do { check_arg_type rank ty1
979 ; check_arg_type rank ty2 }
981 check_type rank ubx_tup ty@(TyConApp tc tys)
983 = do { -- Check that the synonym has enough args
984 -- This applies equally to open and closed synonyms
985 -- It's OK to have an *over-applied* type synonym
986 -- data Tree a b = ...
987 -- type Foo a = Tree [a]
988 -- f :: Foo a b -> ...
989 checkTc (tyConArity tc <= length tys) arity_msg
991 -- See Note [Liberal type synonyms]
992 ; liberal <- xoptM Opt_LiberalTypeSynonyms
993 ; if not liberal || isSynFamilyTyCon tc then
994 -- For H98 and synonym families, do check the type args
995 mapM_ (check_mono_type SynArgMonoType) tys
997 else -- In the liberal case (only for closed syns), expand then check
999 Just ty' -> check_type rank ubx_tup ty'
1000 Nothing -> pprPanic "check_tau_type" (ppr ty)
1003 | isUnboxedTupleTyCon tc
1004 = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
1005 ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
1007 ; impred <- xoptM Opt_ImpredicativeTypes
1008 ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
1009 -- c.f. check_arg_type
1010 -- However, args are allowed to be unlifted, or
1011 -- more unboxed tuples, so can't use check_arg_ty
1012 ; mapM_ (check_type rank' UT_Ok) tys }
1015 = mapM_ (check_arg_type rank) tys
1018 ubx_tup_ok ub_tuples_allowed = case ubx_tup of
1019 UT_Ok -> ub_tuples_allowed
1023 tc_arity = tyConArity tc
1025 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1026 ubx_tup_msg = ubxArgTyErr ty
1028 check_type _ _ ty = pprPanic "check_type" (ppr ty)
1030 ----------------------------------------
1031 check_arg_type :: Rank -> Type -> TcM ()
1032 -- The sort of type that can instantiate a type variable,
1033 -- or be the argument of a type constructor.
1034 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
1035 -- Other unboxed types are very occasionally allowed as type
1036 -- arguments depending on the kind of the type constructor
1038 -- For example, we want to reject things like:
1040 -- instance Ord a => Ord (forall s. T s a)
1042 -- g :: T s (forall b.b)
1044 -- NB: unboxed tuples can have polymorphic or unboxed args.
1045 -- This happens in the workers for functions returning
1046 -- product types with polymorphic components.
1047 -- But not in user code.
1048 -- Anyway, they are dealt with by a special case in check_tau_type
1050 check_arg_type rank ty
1051 = do { impred <- xoptM Opt_ImpredicativeTypes
1052 ; let rank' = case rank of -- Predictive => must be monotype
1053 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
1054 _other | impred -> ArbitraryRank
1055 | otherwise -> TyConArgMonoType
1056 -- Make sure that MustBeMonoType is propagated,
1057 -- so that we don't suggest -XImpredicativeTypes in
1058 -- (Ord (forall a.a)) => a -> a
1059 -- and so that if it Must be a monotype, we check that it is!
1061 ; check_type rank' UT_NotOk ty
1062 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1064 ----------------------------------------
1065 forAllTyErr :: Rank -> Type -> SDoc
1067 = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
1070 suggestion = case rank of
1071 Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
1072 TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
1073 SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
1074 _ -> empty -- Polytype is always illegal
1076 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
1077 unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1078 ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1080 kindErr :: Kind -> SDoc
1081 kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1084 Note [Liberal type synonyms]
1085 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1086 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1087 doing validity checking. This allows us to instantiate a synonym defn
1088 with a for-all type, or with a partially-applied type synonym.
1092 Here, T is partially applied, so it's illegal in H98. But if you
1093 expand S first, then T we get just
1097 IMPORTANT: suppose T is a type synonym. Then we must do validity
1098 checking on an appliation (T ty1 ty2)
1100 *either* before expansion (i.e. check ty1, ty2)
1101 *or* after expansion (i.e. expand T ty1 ty2, and then check)
1104 If we do both, we get exponential behaviour!!
1106 data TIACons1 i r c = c i ::: r c
1107 type TIACons2 t x = TIACons1 t (TIACons1 t x)
1108 type TIACons3 t x = TIACons2 t (TIACons1 t x)
1109 type TIACons4 t x = TIACons2 t (TIACons2 t x)
1110 type TIACons7 t x = TIACons4 t (TIACons3 t x)
1113 %************************************************************************
1115 \subsection{Checking a theta or source type}
1117 %************************************************************************
1120 -- Enumerate the contexts in which a "source type", <S>, can occur
1124 -- or (N a) where N is a newtype
1127 = ClassSCCtxt Name -- Superclasses of clas
1128 -- class <S> => C a where ...
1129 | SigmaCtxt -- Theta part of a normal for-all type
1130 -- f :: <S> => a -> a
1131 | DataTyCtxt Name -- Theta part of a data decl
1132 -- data <S> => T a = MkT a
1133 | TypeCtxt -- Source type in an ordinary type
1135 | InstThetaCtxt -- Context of an instance decl
1136 -- instance <S> => C [a] where ...
1138 pprSourceTyCtxt :: SourceTyCtxt -> SDoc
1139 pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
1140 pprSourceTyCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type")
1141 pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
1142 pprSourceTyCtxt InstThetaCtxt = ptext (sLit "the context of an instance declaration")
1143 pprSourceTyCtxt TypeCtxt = ptext (sLit "the context of a type")
1147 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1148 checkValidTheta ctxt theta
1149 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1151 -------------------------
1152 check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
1153 check_valid_theta _ []
1155 check_valid_theta ctxt theta = do
1157 warnTc (notNull dups) (dupPredWarn dups)
1158 mapM_ (check_pred_ty dflags ctxt) theta
1160 (_,dups) = removeDups tcCmpPred theta
1162 -------------------------
1163 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1164 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1165 = do { -- Class predicates are valid in all contexts
1166 ; checkTc (arity == n_tys) arity_err
1168 -- Check the form of the argument types
1169 ; mapM_ checkValidMonoType tys
1170 ; checkTc (check_class_pred_tys dflags ctxt tys)
1171 (predTyVarErr pred $$ how_to_allow)
1174 class_name = className cls
1175 arity = classArity cls
1177 arity_err = arityErr "Class" class_name arity n_tys
1178 how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
1181 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
1182 = do { -- Equational constraints are valid in all contexts if type
1183 -- families are permitted
1184 ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1185 ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
1186 (eqSuperClassErr pred)
1188 -- Check the form of the argument types
1189 ; checkValidMonoType ty1
1190 ; checkValidMonoType ty2
1193 check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
1194 -- Implicit parameters only allowed in type
1195 -- signatures; not in instance decls, superclasses etc
1196 -- The reason for not allowing implicit params in instances is a bit
1198 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
1199 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
1200 -- discharge all the potential usas of the ?x in e. For example, a
1201 -- constraint Foo [Int] might come out of e,and applying the
1202 -- instance decl would show up two uses of ?x.
1205 check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
1207 -------------------------
1208 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1209 check_class_pred_tys dflags ctxt tys
1211 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1212 InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1213 -- Further checks on head and theta in
1214 -- checkInstTermination
1215 _ -> flexible_contexts || all tyvar_head tys
1217 flexible_contexts = xopt Opt_FlexibleContexts dflags
1218 undecidable_ok = xopt Opt_UndecidableInstances dflags
1220 -------------------------
1221 tyvar_head :: Type -> Bool
1222 tyvar_head ty -- Haskell 98 allows predicates of form
1223 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1224 | otherwise -- where a is a type variable
1225 = case tcSplitAppTy_maybe ty of
1226 Just (ty, _) -> tyvar_head ty
1233 is ambiguous if P contains generic variables
1234 (i.e. one of the Vs) that are not mentioned in tau
1236 However, we need to take account of functional dependencies
1237 when we speak of 'mentioned in tau'. Example:
1238 class C a b | a -> b where ...
1240 forall x y. (C x y) => x
1241 is not ambiguous because x is mentioned and x determines y
1243 NB; the ambiguity check is only used for *user* types, not for types
1244 coming from inteface files. The latter can legitimately have
1245 ambiguous types. Example
1247 class S a where s :: a -> (Int,Int)
1248 instance S Char where s _ = (1,1)
1249 f:: S a => [a] -> Int -> (Int,Int)
1250 f (_::[a]) x = (a*x,b)
1251 where (a,b) = s (undefined::a)
1253 Here the worker for f gets the type
1254 fw :: forall a. S a => Int -> (# Int, Int #)
1256 If the list of tv_names is empty, we have a monotype, and then we
1257 don't need to check for ambiguity either, because the test can't fail
1260 In addition, GHC insists that at least one type variable
1261 in each constraint is in V. So we disallow a type like
1262 forall a. Eq b => b -> b
1263 even in a scope where b is in scope.
1266 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1267 checkAmbiguity forall_tyvars theta tau_tyvars
1268 = mapM_ complain (filter is_ambig theta)
1270 complain pred = addErrTc (ambigErr pred)
1271 extended_tau_vars = growThetaTyVars theta tau_tyvars
1273 -- See Note [Implicit parameters and ambiguity] in TcSimplify
1274 is_ambig pred = isClassPred pred &&
1275 any ambig_var (varSetElems (tyVarsOfPred pred))
1277 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1278 not (ct_var `elemVarSet` extended_tau_vars)
1280 ambigErr :: PredType -> SDoc
1282 = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
1283 nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1284 ptext (sLit "must be reachable from the type after the '=>'"))]
1287 Note [Growing the tau-tvs using constraints]
1288 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1289 (growInstsTyVars insts tvs) is the result of extending the set
1290 of tyvars tvs using all conceivable links from pred
1292 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1293 Then grow precs tvs = {a,b,c}
1296 growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
1297 -- See Note [Growing the tau-tvs using constraints]
1298 growThetaTyVars theta tvs
1300 | otherwise = fixVarSet mk_next tvs
1302 mk_next tvs = foldr grow_one tvs theta
1303 grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
1305 growPredTyVars :: TcPredType
1306 -> TyVarSet -- The set to extend
1307 -> TyVarSet -- TyVars of the predicate if it intersects
1308 -- the set, or is implicit parameter
1309 growPredTyVars pred tvs
1310 | IParam {} <- pred = pred_tvs -- See Note [Implicit parameters and ambiguity]
1311 | pred_tvs `intersectsVarSet` tvs = pred_tvs
1312 | otherwise = emptyVarSet
1314 pred_tvs = tyVarsOfPred pred
1317 Note [Implicit parameters and ambiguity]
1318 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1319 Only a *class* predicate can give rise to ambiguity
1320 An *implicit parameter* cannot. For example:
1321 foo :: (?x :: [a]) => Int
1323 is fine. The call site will suppply a particular 'x'
1325 Furthermore, the type variables fixed by an implicit parameter
1326 propagate to the others. E.g.
1327 foo :: (Show a, ?x::[a]) => Int
1329 The type of foo looks ambiguous. But it isn't, because at a call site
1331 let ?x = 5::Int in foo
1332 and all is well. In effect, implicit parameters are, well, parameters,
1333 so we can take their type variables into account as part of the
1334 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
1338 checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
1339 checkThetaCtxt ctxt theta
1340 = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1341 ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
1343 eqSuperClassErr :: PredType -> SDoc
1344 eqSuperClassErr pred
1345 = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:"))
1348 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
1349 badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPred pred
1350 eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPred pred
1352 parens (ptext (sLit "Use -XTypeFamilies to permit this"))
1353 predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
1354 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1355 dupPredWarn :: [[PredType]] -> SDoc
1356 dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1358 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
1359 arityErr kind name n m
1360 = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1361 n_arguments <> comma, text "but has been given",
1362 if m==0 then text "none" else int m]
1364 n_arguments | n == 0 = ptext (sLit "no arguments")
1365 | n == 1 = ptext (sLit "1 argument")
1366 | True = hsep [int n, ptext (sLit "arguments")]
1369 %************************************************************************
1371 \subsection{Checking for a decent instance head type}
1373 %************************************************************************
1375 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1376 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1378 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1379 flag is on, or (2)~the instance is imported (they must have been
1380 compiled elsewhere). In these cases, we let them go through anyway.
1382 We can also have instances for functions: @instance Foo (a -> b) ...@.
1385 checkValidInstHead :: Class -> [Type] -> TcM ()
1386 checkValidInstHead clas tys
1387 = do { dflags <- getDOpts
1389 -- If GlasgowExts then check at least one isn't a type variable
1390 ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
1391 all tcInstHeadTyNotSynonym tys)
1392 (instTypeErr pp_pred head_type_synonym_msg)
1393 ; checkTc (xopt Opt_FlexibleInstances dflags ||
1394 all tcInstHeadTyAppAllTyVars tys)
1395 (instTypeErr pp_pred head_type_args_tyvars_msg)
1396 ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
1398 (instTypeErr pp_pred head_one_type_msg)
1399 -- May not contain type family applications
1400 ; mapM_ checkTyFamFreeness tys
1402 ; mapM_ checkValidMonoType tys
1403 -- For now, I only allow tau-types (not polytypes) in
1404 -- the head of an instance decl.
1405 -- E.g. instance C (forall a. a->a) is rejected
1406 -- One could imagine generalising that, but I'm not sure
1407 -- what all the consequences might be
1411 pp_pred = pprClassPred clas tys
1412 head_type_synonym_msg = parens (
1413 text "All instance types must be of the form (T t1 ... tn)" $$
1414 text "where T is not a synonym." $$
1415 text "Use -XTypeSynonymInstances if you want to disable this.")
1417 head_type_args_tyvars_msg = parens (vcat [
1418 text "All instance types must be of the form (T a1 ... an)",
1419 text "where a1 ... an are *distinct type variables*,",
1420 text "and each type variable appears at most once in the instance head.",
1421 text "Use -XFlexibleInstances if you want to disable this."])
1423 head_one_type_msg = parens (
1424 text "Only one type can be given in an instance head." $$
1425 text "Use -XMultiParamTypeClasses if you want to allow more.")
1427 instTypeErr :: SDoc -> SDoc -> SDoc
1428 instTypeErr pp_ty msg
1429 = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty,
1434 %************************************************************************
1436 \subsection{Checking instance for termination}
1438 %************************************************************************
1441 checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType
1442 -> Class -> [TcType] -> TcM ()
1443 checkValidInstance hs_type tyvars theta clas inst_tys
1444 = setSrcSpan (getLoc hs_type) $
1445 do { setSrcSpan head_loc (checkValidInstHead clas inst_tys)
1446 ; checkValidTheta InstThetaCtxt theta
1447 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1449 -- Check that instance inference will terminate (if we care)
1450 -- For Haskell 98 this will already have been done by checkValidTheta,
1451 -- but as we may be using other extensions we need to check.
1452 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1453 ; unless undecidable_ok $
1454 mapM_ addErrTc (checkInstTermination inst_tys theta)
1456 -- The Coverage Condition
1457 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1458 (instTypeErr (pprClassPred clas inst_tys) msg)
1461 msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1464 -- The location of the "head" of the instance
1465 head_loc = case hs_type of
1466 L _ (HsForAllTy _ _ _ (L loc _)) -> loc
1470 Termination test: the so-called "Paterson conditions" (see Section 5 of
1471 "Understanding functionsl dependencies via Constraint Handling Rules,
1474 We check that each assertion in the context satisfies:
1475 (1) no variable has more occurrences in the assertion than in the head, and
1476 (2) the assertion has fewer constructors and variables (taken together
1477 and counting repetitions) than the head.
1478 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1479 (which have already been checked) guarantee termination.
1481 The underlying idea is that
1483 for any ground substitution, each assertion in the
1484 context has fewer type constructors than the head.
1488 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1489 checkInstTermination tys theta
1490 = mapCatMaybes check theta
1493 size = sizeTypes tys
1495 | not (null (fvPred pred \\ fvs))
1496 = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1497 | sizePred pred >= size
1498 = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1502 predUndecErr :: PredType -> SDoc -> SDoc
1503 predUndecErr pred msg = sep [msg,
1504 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1506 nomoreMsg, smallerMsg, undecidableMsg :: SDoc
1507 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1508 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1509 undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
1512 validDeivPred checks for OK 'deriving' context. See Note [Exotic
1513 derived instance contexts] in TcSimplify. However the predicate is
1514 here because it uses sizeTypes, fvTypes.
1517 validDerivPred :: PredType -> Bool
1518 validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
1519 where fvs = fvTypes tys
1520 validDerivPred _ = False
1524 %************************************************************************
1526 Checking type instance well-formedness and termination
1528 %************************************************************************
1531 -- Check that a "type instance" is well-formed (which includes decidability
1532 -- unless -XUndecidableInstances is given).
1534 checkValidTypeInst :: [Type] -> Type -> TcM ()
1535 checkValidTypeInst typats rhs
1536 = do { -- left-hand side contains no type family applications
1537 -- (vanilla synonyms are fine, though)
1538 ; mapM_ checkTyFamFreeness typats
1540 -- the right-hand side is a tau type
1541 ; checkValidMonoType rhs
1543 -- we have a decidable instance unless otherwise permitted
1544 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1545 ; unless undecidable_ok $
1546 mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1549 -- Make sure that each type family instance is
1550 -- (1) strictly smaller than the lhs,
1551 -- (2) mentions no type variable more often than the lhs, and
1552 -- (3) does not contain any further type family instances.
1554 checkFamInst :: [Type] -- lhs
1555 -> [(TyCon, [Type])] -- type family instances
1557 checkFamInst lhsTys famInsts
1558 = mapCatMaybes check famInsts
1560 size = sizeTypes lhsTys
1561 fvs = fvTypes lhsTys
1563 | not (all isTyFamFree tys)
1564 = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1565 | not (null (fvTypes tys \\ fvs))
1566 = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1567 | size <= sizeTypes tys
1568 = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1572 famInst = TyConApp tc tys
1574 -- Ensure that no type family instances occur in a type.
1576 checkTyFamFreeness :: Type -> TcM ()
1577 checkTyFamFreeness ty
1578 = checkTc (isTyFamFree ty) $
1579 tyFamInstIllegalErr ty
1581 -- Check that a type does not contain any type family applications.
1583 isTyFamFree :: Type -> Bool
1584 isTyFamFree = null . tyFamInsts
1588 tyFamInstIllegalErr :: Type -> SDoc
1589 tyFamInstIllegalErr ty
1590 = hang (ptext (sLit "Illegal type synonym family application in instance") <>
1594 famInstUndecErr :: Type -> SDoc -> SDoc
1595 famInstUndecErr ty msg
1597 nest 2 (ptext (sLit "in the type family application:") <+>
1600 nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
1601 nestedMsg = ptext (sLit "Nested type family application")
1602 nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head")
1603 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1607 %************************************************************************
1609 \subsection{Auxiliary functions}
1611 %************************************************************************
1614 -- Free variables of a type, retaining repetitions, and expanding synonyms
1615 fvType :: Type -> [TyVar]
1616 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1617 fvType (TyVarTy tv) = [tv]
1618 fvType (TyConApp _ tys) = fvTypes tys
1619 fvType (PredTy pred) = fvPred pred
1620 fvType (FunTy arg res) = fvType arg ++ fvType res
1621 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1622 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1624 fvTypes :: [Type] -> [TyVar]
1625 fvTypes tys = concat (map fvType tys)
1627 fvPred :: PredType -> [TyVar]
1628 fvPred (ClassP _ tys') = fvTypes tys'
1629 fvPred (IParam _ ty) = fvType ty
1630 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1632 -- Size of a type: the number of variables and constructors
1633 sizeType :: Type -> Int
1634 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1635 sizeType (TyVarTy _) = 1
1636 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1637 sizeType (PredTy pred) = sizePred pred
1638 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1639 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1640 sizeType (ForAllTy _ ty) = sizeType ty
1642 sizeTypes :: [Type] -> Int
1643 sizeTypes xs = sum (map sizeType xs)
1645 -- Size of a predicate
1647 -- We are considering whether *class* constraints terminate
1648 -- Once we get into an implicit parameter or equality we
1649 -- can't get back to a class constraint, so it's safe
1650 -- to say "size 0". See Trac #4200.
1651 sizePred :: PredType -> Int
1652 sizePred (ClassP _ tys') = sizeTypes tys'
1653 sizePred (IParam {}) = 0
1654 sizePred (EqPred {}) = 0