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 writeWantedCoVar, readWantedCoVar,
30 newIP, newDict, newSilentGiven, isSilentEvVar,
32 newWantedEvVar, newWantedEvVars,
33 newTcEvBinds, addTcEvBind,
35 --------------------------------
37 tcInstTyVars, tcInstSigTyVars,
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) = newCoVar 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
140 newEvVar :: TcPredType -> TcM EvVar
141 -- Creates new *rigid* variables for predicates
142 newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
143 newEvVar (ClassP cls tys) = newDict cls tys
144 newEvVar (IParam ip ty) = newIP ip ty
146 newCoVar :: TcType -> TcType -> TcM CoVar
148 = do { name <- newName (mkTyVarOccFS (fsLit "co"))
149 ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
151 newIP :: IPName Name -> TcType -> TcM IpId
153 = do { name <- newName (getOccName (ipNameName ip))
154 ; return (mkLocalId name (mkPredTy (IParam ip ty))) }
156 newDict :: Class -> [TcType] -> TcM DictId
158 = do { name <- newName (mkDictOcc (getOccName cls))
159 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
161 newName :: OccName -> TcM Name
163 = do { uniq <- newUnique
165 ; return (mkInternalName uniq occ loc) }
168 newSilentGiven :: PredType -> TcM EvVar
169 -- Make a dictionary for a "silent" given dictionary
170 -- Behaves just like any EvVar except that it responds True to isSilentDict
171 -- This is used only to suppress confusing error reports
172 newSilentGiven (ClassP cls tys)
173 = do { uniq <- newUnique
174 ; let name = mkSystemName uniq (mkDictOcc (getOccName cls))
175 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
176 newSilentGiven (EqPred ty1 ty2)
177 = do { uniq <- newUnique
178 ; let name = mkSystemName uniq (mkTyVarOccFS (fsLit "co"))
179 ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
180 newSilentGiven pred@(IParam {})
181 = pprPanic "newSilentDict" (ppr pred) -- Implicit parameters rejected earlier
183 isSilentEvVar :: EvVar -> Bool
184 isSilentEvVar v = isSystemName (Var.varName v)
185 -- Notice that all *other* evidence variables get Internal Names
189 %************************************************************************
191 SkolemTvs (immutable)
193 %************************************************************************
196 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
197 -> TcType -- Type to instantiate
198 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
199 -- (type vars (excl coercion vars), preds (incl equalities), rho)
200 tcInstType inst_tyvars ty
201 = case tcSplitForAllTys ty of
202 ([], rho) -> let -- There may be overloading despite no type variables;
203 -- (?x :: Int) => Int -> Int
204 (theta, tau) = tcSplitPhiTy rho
206 return ([], theta, tau)
208 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
210 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
211 -- Either the tyvars are freshly made, by inst_tyvars,
212 -- or any nested foralls have different binders.
213 -- Either way, zipTopTvSubst is ok
215 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
216 ; return (tyvars', theta, tau) }
218 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
219 -- Instantiate a type signature with skolem constants, but
220 -- do *not* give them fresh names, because we want the name to
221 -- be in the type environment: it is lexically scoped.
222 tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty
224 tcSuperSkolTyVars :: [TyVar] -> [TcTyVar]
225 -- Make skolem constants, but do *not* give them new names, as above
226 -- Moreover, make them "super skolems"; see comments with superSkolemTv
227 tcSuperSkolTyVars tyvars
228 = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) superSkolemTv
231 tcInstSkolTyVar :: Bool -> TyVar -> TcM TcTyVar
232 -- Instantiate the tyvar, using
233 -- * the occ-name and kind of the supplied tyvar,
234 -- * the unique from the monad,
235 -- * the location either from the tyvar (skol_info = SigSkol)
236 -- or from the monad (otherwise)
237 tcInstSkolTyVar overlappable tyvar
238 = do { uniq <- newUnique
240 ; let new_name = mkInternalName uniq occ loc
241 ; return (mkTcTyVar new_name kind (SkolemTv overlappable)) }
243 old_name = tyVarName tyvar
244 occ = nameOccName old_name
245 kind = tyVarKind tyvar
247 tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar]
248 tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars
250 tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
251 tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars
253 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
254 -- Instantiate a type with fresh skolem constants
255 -- Binding location comes from the monad
256 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
258 tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
259 -- Make meta SigTv type variables for patten-bound scoped type varaibles
260 -- We use SigTvs for them, so that they can't unify with arbitrary types
261 tcInstSigTyVars = mapM tcInstSigTyVar
263 tcInstSigTyVar :: TyVar -> TcM TcTyVar
265 = do { uniq <- newMetaUnique
266 ; ref <- newMutVar Flexi
267 ; let name = setNameUnique (tyVarName tyvar) uniq
268 -- Use the same OccName so that the tidy-er
269 -- doesn't rename 'a' to 'a0' etc
270 kind = tyVarKind tyvar
271 ; return (mkTcTyVar name kind (MetaTv SigTv ref)) }
275 %************************************************************************
277 MetaTvs (meta type variables; mutable)
279 %************************************************************************
282 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
283 -- Make a new meta tyvar out of thin air
284 newMetaTyVar meta_info kind
285 = do { uniq <- newMetaUnique
286 ; ref <- newMutVar Flexi
287 ; let name = mkTcTyVarName uniq s
288 s = case meta_info of
292 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
294 mkTcTyVarName :: Unique -> FastString -> Name
295 -- Make sure that fresh TcTyVar names finish with a digit
296 -- leaving the un-cluttered names free for user names
297 mkTcTyVarName uniq str = mkSysTvName uniq str
299 readMetaTyVar :: TyVar -> TcM MetaDetails
300 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
301 readMutVar (metaTvRef tyvar)
303 readWantedCoVar :: CoVar -> TcM MetaDetails
304 readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
305 readMutVar (metaTvRef covar)
307 isFilledMetaTyVar :: TyVar -> TcM Bool
308 -- True of a filled-in (Indirect) meta type variable
310 | not (isTcTyVar tv) = return False
311 | MetaTv _ ref <- tcTyVarDetails tv
312 = do { details <- readMutVar ref
313 ; return (isIndirect details) }
314 | otherwise = return False
316 isFlexiMetaTyVar :: TyVar -> TcM Bool
317 -- True of a un-filled-in (Flexi) meta type variable
319 | not (isTcTyVar tv) = return False
320 | MetaTv _ ref <- tcTyVarDetails tv
321 = do { details <- readMutVar ref
322 ; return (isFlexi details) }
323 | otherwise = return False
326 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
327 -- Write into a currently-empty MetaTyVar
329 writeMetaTyVar tyvar ty
331 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
333 -- Everything from here on only happens if DEBUG is on
334 | not (isTcTyVar tyvar)
335 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
338 | MetaTv _ ref <- tcTyVarDetails tyvar
339 = writeMetaTyVarRef tyvar ref ty
342 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
345 writeWantedCoVar :: CoVar -> Coercion -> TcM ()
346 writeWantedCoVar cv co = writeMetaTyVar cv co
349 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
350 -- Here the tyvar is for error checking only;
351 -- the ref cell must be for the same tyvar
352 writeMetaTyVarRef tyvar ref ty
354 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
355 ; writeMutVar ref (Indirect ty) }
357 -- Everything from here on only happens if DEBUG is on
358 | not (isPredTy tv_kind) -- Don't check kinds for updates to coercion variables
359 , not (ty_kind `isSubKind` tv_kind)
360 = WARN( True, hang (text "Ill-kinded update to meta tyvar")
361 2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
365 = do { meta_details <- readMutVar ref;
366 ; ASSERT2( isFlexi meta_details,
367 hang (text "Double update of meta tyvar")
368 2 (ppr tyvar $$ ppr meta_details) )
370 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
371 ; writeMutVar ref (Indirect ty) }
373 tv_kind = tyVarKind tyvar
374 ty_kind = typeKind ty
378 %************************************************************************
382 %************************************************************************
385 newFlexiTyVar :: Kind -> TcM TcTyVar
386 newFlexiTyVar kind = newMetaTyVar TauTv kind
388 newFlexiTyVarTy :: Kind -> TcM TcType
389 newFlexiTyVarTy kind = do
390 tc_tyvar <- newFlexiTyVar kind
391 return (TyVarTy tc_tyvar)
393 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
394 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
396 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
397 -- Instantiate with META type variables
399 = do { tc_tvs <- mapM tcInstTyVar tyvars
400 ; let tys = mkTyVarTys tc_tvs
401 ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
402 -- Since the tyvars are freshly made,
403 -- they cannot possibly be captured by
404 -- any existing for-alls. Hence zipTopTvSubst
406 tcInstTyVar :: TyVar -> TcM TcTyVar
407 -- Make a new unification variable tyvar whose Name and Kind
408 -- come from an existing TyVar
410 = do { uniq <- newMetaUnique
411 ; ref <- newMutVar Flexi
412 ; let name = mkSystemName uniq (getOccName tyvar)
413 kind = tyVarKind tyvar
414 ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }
418 %************************************************************************
422 %************************************************************************
425 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
427 | isSkolemTyVar sig_tv
428 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
430 = ASSERT( isSigTyVar sig_tv )
431 do { ty <- zonkTcTyVar sig_tv
432 ; return (tcGetTyVar "zonkSigTyVar" ty) }
433 -- 'ty' is bound to be a type variable, because SigTvs
434 -- can only be unified with type variables
439 %************************************************************************
441 \subsection{Zonking -- the exernal interfaces}
443 %************************************************************************
445 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
446 To improve subsequent calls to the same function it writes the zonked set back into
450 tcGetGlobalTyVars :: TcM TcTyVarSet
452 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
453 ; gbl_tvs <- readMutVar gtv_var
454 ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
455 ; writeMutVar gtv_var gbl_tvs'
459 ----------------- Type variables
462 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
463 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
465 zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
466 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
468 ----------------- Types
469 zonkTcTypeCarefully :: TcType -> TcM TcType
470 -- Do not zonk type variables free in the environment
471 zonkTcTypeCarefully ty
472 = do { env_tvs <- tcGetGlobalTyVars
473 ; zonkType (zonk_tv env_tvs) ty }
476 | tv `elemVarSet` env_tvs
477 = return (TyVarTy tv)
479 = ASSERT( isTcTyVar tv )
480 case tcTyVarDetails tv of
481 SkolemTv {} -> return (TyVarTy tv)
482 RuntimeUnk {} -> return (TyVarTy tv)
483 FlatSkol ty -> zonkType (zonk_tv env_tvs) ty
484 MetaTv _ ref -> do { cts <- readMutVar ref
486 Flexi -> return (TyVarTy tv)
487 Indirect ty -> zonkType (zonk_tv env_tvs) ty }
489 zonkTcType :: TcType -> TcM TcType
490 -- Simply look through all Flexis
491 zonkTcType ty = zonkType zonkTcTyVar ty
493 zonkTcTyVar :: TcTyVar -> TcM TcType
494 -- Simply look through all Flexis
496 = ASSERT2( isTcTyVar tv, ppr tv )
497 case tcTyVarDetails tv of
498 SkolemTv {} -> return (TyVarTy tv)
499 RuntimeUnk {} -> return (TyVarTy tv)
500 FlatSkol ty -> zonkTcType ty
501 MetaTv _ ref -> do { cts <- readMutVar ref
503 Flexi -> return (TyVarTy tv)
504 Indirect ty -> zonkTcType ty }
506 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
507 -- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
508 zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
511 = case tcTyVarDetails tv of
512 SkolemTv {} -> return (TyVarTy tv)
513 RuntimeUnk {} -> return (TyVarTy tv)
514 FlatSkol ty -> zonkType zonk_tv ty
515 MetaTv _ ref -> do { cts <- readMutVar ref
517 Flexi -> zonk_flexi tv
518 Indirect ty -> zonkType zonk_tv ty }
520 = case lookupTyVar subst tv of
521 Just ty -> zonkType zonk_tv ty
522 Nothing -> return (TyVarTy tv)
524 zonkTcTypes :: [TcType] -> TcM [TcType]
525 zonkTcTypes tys = mapM zonkTcType tys
527 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
528 zonkTcThetaType theta = mapM zonkTcPredType theta
530 zonkTcPredType :: TcPredType -> TcM TcPredType
531 zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts
532 zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t
533 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
536 ------------------- These ...ToType, ...ToKind versions
537 are used at the end of type checking
540 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
541 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
543 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
544 -- The quantified type variables often include meta type variables
545 -- we want to freeze them into ordinary type variables, and
546 -- default their kind (e.g. from OpenTypeKind to TypeKind)
547 -- -- see notes with Kind.defaultKind
548 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
549 -- bound occurences of the original type variable will get zonked to
550 -- the immutable version.
552 -- We leave skolem TyVars alone; they are immutable.
553 zonkQuantifiedTyVar tv
554 = ASSERT2( isTcTyVar tv, ppr tv )
555 case tcTyVarDetails tv of
556 SkolemTv {} -> WARN( True, ppr tv ) -- Dec10: Can this really happen?
557 do { kind <- zonkTcType (tyVarKind tv)
558 ; return $ setTyVarKind tv kind }
559 -- It might be a skolem type variable,
560 -- for example from a user type signature
564 -- [Sept 04] Check for non-empty.
565 -- See note [Silly Type Synonym]
566 (readMutVar _ref >>= \cts ->
569 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
572 skolemiseUnboundMetaTyVar tv vanillaSkolemTv
573 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
575 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
576 -- We have a Meta tyvar with a ref-cell inside it
577 -- Skolemise it, including giving it a new Name, so that
578 -- we are totally out of Meta-tyvar-land
579 -- We create a skolem TyVar, not a regular TyVar
580 -- See Note [Zonking to Skolem]
581 skolemiseUnboundMetaTyVar tv details
582 = ASSERT2( isMetaTyVar tv, ppr tv )
583 do { span <- getSrcSpanM -- Get the location from "here"
584 -- ie where we are generalising
585 ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land
586 ; let final_kind = defaultKind (tyVarKind tv)
587 final_name = mkInternalName uniq (getOccName tv) span
588 final_tv = mkTcTyVar final_name final_kind details
589 ; writeMetaTyVar tv (mkTyVarTy final_tv)
594 zonkImplication :: Implication -> TcM Implication
595 zonkImplication implic@(Implic { ic_given = given
598 = do { -- No need to zonk the skolems
599 ; given' <- mapM zonkEvVar given
600 ; loc' <- zonkGivenLoc loc
601 ; wanted' <- zonkWC wanted
602 ; return (implic { ic_given = given'
603 , ic_wanted = wanted'
606 zonkEvVar :: EvVar -> TcM EvVar
607 zonkEvVar var = do { ty' <- zonkTcType (varType var)
608 ; return (setVarType var ty') }
610 zonkFlavoredEvVar :: FlavoredEvVar -> TcM FlavoredEvVar
611 zonkFlavoredEvVar (EvVarX ev fl)
612 = do { ev' <- zonkEvVar ev
613 ; fl' <- zonkFlavor fl
614 ; return (EvVarX ev' fl') }
616 zonkWC :: WantedConstraints -> TcM WantedConstraints
617 zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
618 = do { flat' <- zonkWantedEvVars flat
619 ; implic' <- mapBagM zonkImplication implic
620 ; insol' <- mapBagM zonkFlavoredEvVar insol
621 ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
623 zonkWantedEvVars :: Bag WantedEvVar -> TcM (Bag WantedEvVar)
624 zonkWantedEvVars = mapBagM zonkWantedEvVar
626 zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
627 zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) }
629 zonkFlavor :: CtFlavor -> TcM CtFlavor
630 zonkFlavor (Given loc) = do { loc' <- zonkGivenLoc loc; return (Given loc') }
631 zonkFlavor fl = return fl
633 zonkGivenLoc :: GivenLoc -> TcM GivenLoc
634 -- GivenLocs may have unification variables inside them!
635 zonkGivenLoc (CtLoc skol_info span ctxt)
636 = do { skol_info' <- zonkSkolemInfo skol_info
637 ; return (CtLoc skol_info' span ctxt) }
639 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
640 zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty
641 ; return (SigSkol cx ty') }
642 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
643 ; return (InferSkol ntys') }
645 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
646 zonkSkolemInfo skol_info = return skol_info
649 Note [Silly Type Synonyms]
650 ~~~~~~~~~~~~~~~~~~~~~~~~~~
652 type C u a = u -- Note 'a' unused
654 foo :: (forall a. C u a -> C u a) -> u
658 bar = foo (\t -> t + t)
660 * From the (\t -> t+t) we get type {Num d} => d -> d
663 * Now unify with type of foo's arg, and we get:
664 {Num (C d a)} => C d a -> C d a
667 * Now abstract over the 'a', but float out the Num (C d a) constraint
668 because it does not 'really' mention a. (see exactTyVarsOfType)
669 The arg to foo becomes
672 * So we get a dict binding for Num (C d a), which is zonked to give
674 [Note Sept 04: now that we are zonking quantified type variables
675 on construction, the 'a' will be frozen as a regular tyvar on
676 quantification, so the floated dict will still have type (C d a).
677 Which renders this whole note moot; happily!]
679 * Then the \/\a abstraction has a zonked 'a' in it.
681 All very silly. I think its harmless to ignore the problem. We'll end up with
682 a \/\a in the final result but all the occurrences of a will be zonked to ()
684 Note [Zonking to Skolem]
685 ~~~~~~~~~~~~~~~~~~~~~~~~
686 We used to zonk quantified type variables to regular TyVars. However, this
687 leads to problems. Consider this program from the regression test suite:
689 eval :: Int -> String -> String -> String
690 eval 0 root actual = evalRHS 0 root actual
693 evalRHS 0 root actual = eval 0 root actual
695 It leads to the deferral of an equality (wrapped in an implication constraint)
697 forall a. (String -> String -> String) ~ a
699 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
700 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
701 This has the *side effect* of also zonking the `a' in the deferred equality
702 (which at this point is being handed around wrapped in an implication
705 Finally, the equality (with the zonked `a') will be handed back to the
706 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
707 If we zonk `a' with a regular type variable, we will have this regular type
708 variable now floating around in the simplifier, which in many places assumes to
709 only see proper TcTyVars.
711 We can avoid this problem by zonking with a skolem. The skolem is rigid
712 (which we require for a quantified variable), but is still a TcTyVar that the
713 simplifier knows how to deal with.
716 %************************************************************************
718 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
720 %* For internal use only! *
722 %************************************************************************
725 -- For unbound, mutable tyvars, zonkType uses the function given to it
726 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
727 -- type variable and zonks the kind too
729 zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars
730 -> TcType -> TcM Type
731 zonkType zonk_tc_tyvar ty
734 go (TyConApp tc tys) = do tys' <- mapM go tys
735 return (TyConApp tc tys')
737 go (PredTy p) = do p' <- go_pred p
740 go (FunTy arg res) = do arg' <- go arg
742 return (FunTy arg' res')
744 go (AppTy fun arg) = do fun' <- go fun
746 return (mkAppTy fun' arg')
747 -- NB the mkAppTy; we might have instantiated a
748 -- type variable to a type constructor, so we need
749 -- to pull the TyConApp to the top.
751 -- The two interesting cases!
752 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
753 | otherwise = liftM TyVarTy $
754 zonkTyVar zonk_tc_tyvar tyvar
755 -- Ordinary (non Tc) tyvars occur inside quantified types
757 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
759 tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
760 return (ForAllTy tyvar' ty')
762 go_pred (ClassP c tys) = do tys' <- mapM go tys
763 return (ClassP c tys')
764 go_pred (IParam n ty) = do ty' <- go ty
765 return (IParam n ty')
766 go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
768 return (EqPred ty1' ty2')
770 mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var
771 -> TcTyVar -> TcM TcType
772 mkZonkTcTyVar unbound_var_fn tyvar
773 = ASSERT( isTcTyVar tyvar )
774 case tcTyVarDetails tyvar of
775 SkolemTv {} -> return (TyVarTy tyvar)
776 RuntimeUnk {} -> return (TyVarTy tyvar)
777 FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
778 MetaTv _ ref -> do { cts <- readMutVar ref
780 Flexi -> unbound_var_fn tyvar
781 Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
783 -- Zonk the kind of a non-TC tyvar in case it is a coercion variable
784 -- (their kind contains types).
785 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for a TcTyVar
786 -> TyVar -> TcM TyVar
787 zonkTyVar zonk_tc_tyvar tv
789 = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
790 ; return $ setTyVarKind tv kind }
791 | otherwise = return tv
796 %************************************************************************
800 %************************************************************************
803 readKindVar :: KindVar -> TcM (MetaDetails)
804 writeKindVar :: KindVar -> TcKind -> TcM ()
805 readKindVar kv = readMutVar (kindVarRef kv)
806 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
809 zonkTcKind :: TcKind -> TcM TcKind
810 zonkTcKind k = zonkTcType k
813 zonkTcKindToKind :: TcKind -> TcM Kind
814 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
815 -- Haskell specifies that * is to be used, so we follow that.
817 = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
820 %************************************************************************
822 \subsection{Checking a user type}
824 %************************************************************************
826 When dealing with a user-written type, we first translate it from an HsType
827 to a Type, performing kind checking, and then check various things that should
828 be true about it. We don't want to perform these checks at the same time
829 as the initial translation because (a) they are unnecessary for interface-file
830 types and (b) when checking a mutually recursive group of type and class decls,
831 we can't "look" at the tycons/classes yet. Also, the checks are are rather
832 diverse, and used to really mess up the other code.
834 One thing we check for is 'rank'.
836 Rank 0: monotypes (no foralls)
837 Rank 1: foralls at the front only, Rank 0 inside
838 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
840 basic ::= tyvar | T basic ... basic
842 r2 ::= forall tvs. cxt => r2a
843 r2a ::= r1 -> r2a | basic
844 r1 ::= forall tvs. cxt => r0
845 r0 ::= r0 -> r0 | basic
847 Another thing is to check that type synonyms are saturated.
848 This might not necessarily show up in kind checking.
850 data T k = MkT (k Int)
855 checkValidType :: UserTypeCtxt -> Type -> TcM ()
856 -- Checks that the type is valid for the given context
857 checkValidType ctxt ty = do
858 traceTc "checkValidType" (ppr ty)
859 unboxed <- xoptM Opt_UnboxedTuples
860 rank2 <- xoptM Opt_Rank2Types
861 rankn <- xoptM Opt_RankNTypes
862 polycomp <- xoptM Opt_PolymorphicComponents
864 gen_rank n | rankn = ArbitraryRank
869 DefaultDeclCtxt-> MustBeMonoType
870 ResSigCtxt -> MustBeMonoType
871 LamPatSigCtxt -> gen_rank 0
872 BindPatSigCtxt -> gen_rank 0
873 TySynCtxt _ -> gen_rank 0
874 GenPatCtxt -> gen_rank 1
875 -- This one is a bit of a hack
876 -- See the forall-wrapping in TcClassDcl.mkGenericInstance
878 ExprSigCtxt -> gen_rank 1
879 FunSigCtxt _ -> gen_rank 1
880 ConArgCtxt _ | polycomp -> gen_rank 2
881 -- We are given the type of the entire
882 -- constructor, hence rank 1
883 | otherwise -> gen_rank 1
885 ForSigCtxt _ -> gen_rank 1
886 SpecInstCtxt -> gen_rank 1
887 ThBrackCtxt -> gen_rank 1
888 GenSigCtxt -> panic "checkValidType"
889 -- Can't happen; GenSigCtxt not used for *user* sigs
891 actual_kind = typeKind ty
893 kind_ok = case ctxt of
894 TySynCtxt _ -> True -- Any kind will do
895 ThBrackCtxt -> True -- Any kind will do
896 ResSigCtxt -> isSubOpenTypeKind actual_kind
897 ExprSigCtxt -> isSubOpenTypeKind actual_kind
898 GenPatCtxt -> isLiftedTypeKind actual_kind
899 ForSigCtxt _ -> isLiftedTypeKind actual_kind
900 _ -> isSubArgTypeKind actual_kind
902 ubx_tup = case ctxt of
903 TySynCtxt _ | unboxed -> UT_Ok
904 ExprSigCtxt | unboxed -> UT_Ok
905 ThBrackCtxt | unboxed -> UT_Ok
908 -- Check the internal validity of the type itself
909 check_type rank ubx_tup ty
911 -- Check that the thing has kind Type, and is lifted if necessary
912 -- Do this second, becuase we can't usefully take the kind of an
913 -- ill-formed type such as (a~Int)
914 checkTc kind_ok (kindErr actual_kind)
916 traceTc "checkValidType done" (ppr ty)
918 checkValidMonoType :: Type -> TcM ()
919 checkValidMonoType ty = check_mono_type MustBeMonoType ty
924 data Rank = ArbitraryRank -- Any rank ok
925 | MustBeMonoType -- Monotype regardless of flags
926 | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes
927 | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms
928 | Rank Int -- Rank n, but could be more with -XRankNTypes
930 decRank :: Rank -> Rank -- Function arguments
931 decRank (Rank 0) = Rank 0
932 decRank (Rank n) = Rank (n-1)
933 decRank other_rank = other_rank
935 nonZeroRank :: Rank -> Bool
936 nonZeroRank ArbitraryRank = True
937 nonZeroRank (Rank n) = n>0
938 nonZeroRank _ = False
940 ----------------------------------------
941 data UbxTupFlag = UT_Ok | UT_NotOk
942 -- The "Ok" version means "ok if UnboxedTuples is on"
944 ----------------------------------------
945 check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere
946 -- No unlifted types of any kind
947 check_mono_type rank ty
948 = do { check_type rank UT_NotOk ty
949 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
951 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
952 -- The args say what the *type context* requires, independent
953 -- of *flag* settings. You test the flag settings at usage sites.
955 -- Rank is allowed rank for function args
956 -- Rank 0 means no for-alls anywhere
958 check_type rank ubx_tup ty
959 | not (null tvs && null theta)
960 = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
961 -- Reject e.g. (Maybe (?x::Int => Int)),
962 -- with a decent error message
963 ; check_valid_theta SigmaCtxt theta
964 ; check_type rank ubx_tup tau -- Allow foralls to right of arrow
965 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
967 (tvs, theta, tau) = tcSplitSigmaTy ty
969 -- Naked PredTys should, I think, have been rejected before now
970 check_type _ _ ty@(PredTy {})
971 = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type")
973 check_type _ _ (TyVarTy _) = return ()
975 check_type rank _ (FunTy arg_ty res_ty)
976 = do { check_type (decRank rank) UT_NotOk arg_ty
977 ; check_type rank UT_Ok res_ty }
979 check_type rank _ (AppTy ty1 ty2)
980 = do { check_arg_type rank ty1
981 ; check_arg_type rank ty2 }
983 check_type rank ubx_tup ty@(TyConApp tc tys)
985 = do { -- Check that the synonym has enough args
986 -- This applies equally to open and closed synonyms
987 -- It's OK to have an *over-applied* type synonym
988 -- data Tree a b = ...
989 -- type Foo a = Tree [a]
990 -- f :: Foo a b -> ...
991 checkTc (tyConArity tc <= length tys) arity_msg
993 -- See Note [Liberal type synonyms]
994 ; liberal <- xoptM Opt_LiberalTypeSynonyms
995 ; if not liberal || isSynFamilyTyCon tc then
996 -- For H98 and synonym families, do check the type args
997 mapM_ (check_mono_type SynArgMonoType) tys
999 else -- In the liberal case (only for closed syns), expand then check
1001 Just ty' -> check_type rank ubx_tup ty'
1002 Nothing -> pprPanic "check_tau_type" (ppr ty)
1005 | isUnboxedTupleTyCon tc
1006 = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
1007 ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
1009 ; impred <- xoptM Opt_ImpredicativeTypes
1010 ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
1011 -- c.f. check_arg_type
1012 -- However, args are allowed to be unlifted, or
1013 -- more unboxed tuples, so can't use check_arg_ty
1014 ; mapM_ (check_type rank' UT_Ok) tys }
1017 = mapM_ (check_arg_type rank) tys
1020 ubx_tup_ok ub_tuples_allowed = case ubx_tup of
1021 UT_Ok -> ub_tuples_allowed
1025 tc_arity = tyConArity tc
1027 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1028 ubx_tup_msg = ubxArgTyErr ty
1030 check_type _ _ ty = pprPanic "check_type" (ppr ty)
1032 ----------------------------------------
1033 check_arg_type :: Rank -> Type -> TcM ()
1034 -- The sort of type that can instantiate a type variable,
1035 -- or be the argument of a type constructor.
1036 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
1037 -- Other unboxed types are very occasionally allowed as type
1038 -- arguments depending on the kind of the type constructor
1040 -- For example, we want to reject things like:
1042 -- instance Ord a => Ord (forall s. T s a)
1044 -- g :: T s (forall b.b)
1046 -- NB: unboxed tuples can have polymorphic or unboxed args.
1047 -- This happens in the workers for functions returning
1048 -- product types with polymorphic components.
1049 -- But not in user code.
1050 -- Anyway, they are dealt with by a special case in check_tau_type
1052 check_arg_type rank ty
1053 = do { impred <- xoptM Opt_ImpredicativeTypes
1054 ; let rank' = case rank of -- Predictive => must be monotype
1055 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
1056 _other | impred -> ArbitraryRank
1057 | otherwise -> TyConArgMonoType
1058 -- Make sure that MustBeMonoType is propagated,
1059 -- so that we don't suggest -XImpredicativeTypes in
1060 -- (Ord (forall a.a)) => a -> a
1061 -- and so that if it Must be a monotype, we check that it is!
1063 ; check_type rank' UT_NotOk ty
1064 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1066 ----------------------------------------
1067 forAllTyErr :: Rank -> Type -> SDoc
1069 = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
1072 suggestion = case rank of
1073 Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
1074 TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
1075 SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
1076 _ -> empty -- Polytype is always illegal
1078 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
1079 unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1080 ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1082 kindErr :: Kind -> SDoc
1083 kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1086 Note [Liberal type synonyms]
1087 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1088 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1089 doing validity checking. This allows us to instantiate a synonym defn
1090 with a for-all type, or with a partially-applied type synonym.
1094 Here, T is partially applied, so it's illegal in H98. But if you
1095 expand S first, then T we get just
1099 IMPORTANT: suppose T is a type synonym. Then we must do validity
1100 checking on an appliation (T ty1 ty2)
1102 *either* before expansion (i.e. check ty1, ty2)
1103 *or* after expansion (i.e. expand T ty1 ty2, and then check)
1106 If we do both, we get exponential behaviour!!
1108 data TIACons1 i r c = c i ::: r c
1109 type TIACons2 t x = TIACons1 t (TIACons1 t x)
1110 type TIACons3 t x = TIACons2 t (TIACons1 t x)
1111 type TIACons4 t x = TIACons2 t (TIACons2 t x)
1112 type TIACons7 t x = TIACons4 t (TIACons3 t x)
1115 %************************************************************************
1117 \subsection{Checking a theta or source type}
1119 %************************************************************************
1122 -- Enumerate the contexts in which a "source type", <S>, can occur
1126 -- or (N a) where N is a newtype
1129 = ClassSCCtxt Name -- Superclasses of clas
1130 -- class <S> => C a where ...
1131 | SigmaCtxt -- Theta part of a normal for-all type
1132 -- f :: <S> => a -> a
1133 | DataTyCtxt Name -- Theta part of a data decl
1134 -- data <S> => T a = MkT a
1135 | TypeCtxt -- Source type in an ordinary type
1137 | InstThetaCtxt -- Context of an instance decl
1138 -- instance <S> => C [a] where ...
1140 pprSourceTyCtxt :: SourceTyCtxt -> SDoc
1141 pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
1142 pprSourceTyCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type")
1143 pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
1144 pprSourceTyCtxt InstThetaCtxt = ptext (sLit "the context of an instance declaration")
1145 pprSourceTyCtxt TypeCtxt = ptext (sLit "the context of a type")
1149 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1150 checkValidTheta ctxt theta
1151 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1153 -------------------------
1154 check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
1155 check_valid_theta _ []
1157 check_valid_theta ctxt theta = do
1159 warnTc (notNull dups) (dupPredWarn dups)
1160 mapM_ (check_pred_ty dflags ctxt) theta
1162 (_,dups) = removeDups tcCmpPred theta
1164 -------------------------
1165 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1166 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1167 = do { -- Class predicates are valid in all contexts
1168 ; checkTc (arity == n_tys) arity_err
1170 -- Check the form of the argument types
1171 ; mapM_ checkValidMonoType tys
1172 ; checkTc (check_class_pred_tys dflags ctxt tys)
1173 (predTyVarErr pred $$ how_to_allow)
1176 class_name = className cls
1177 arity = classArity cls
1179 arity_err = arityErr "Class" class_name arity n_tys
1180 how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
1183 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
1184 = do { -- Equational constraints are valid in all contexts if type
1185 -- families are permitted
1186 ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1187 ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
1188 (eqSuperClassErr pred)
1190 -- Check the form of the argument types
1191 ; checkValidMonoType ty1
1192 ; checkValidMonoType ty2
1195 check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
1196 -- Implicit parameters only allowed in type
1197 -- signatures; not in instance decls, superclasses etc
1198 -- The reason for not allowing implicit params in instances is a bit
1200 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
1201 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
1202 -- discharge all the potential usas of the ?x in e. For example, a
1203 -- constraint Foo [Int] might come out of e,and applying the
1204 -- instance decl would show up two uses of ?x.
1207 check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
1209 -------------------------
1210 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1211 check_class_pred_tys dflags ctxt tys
1213 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1214 InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1215 -- Further checks on head and theta in
1216 -- checkInstTermination
1217 _ -> flexible_contexts || all tyvar_head tys
1219 flexible_contexts = xopt Opt_FlexibleContexts dflags
1220 undecidable_ok = xopt Opt_UndecidableInstances dflags
1222 -------------------------
1223 tyvar_head :: Type -> Bool
1224 tyvar_head ty -- Haskell 98 allows predicates of form
1225 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1226 | otherwise -- where a is a type variable
1227 = case tcSplitAppTy_maybe ty of
1228 Just (ty, _) -> tyvar_head ty
1235 is ambiguous if P contains generic variables
1236 (i.e. one of the Vs) that are not mentioned in tau
1238 However, we need to take account of functional dependencies
1239 when we speak of 'mentioned in tau'. Example:
1240 class C a b | a -> b where ...
1242 forall x y. (C x y) => x
1243 is not ambiguous because x is mentioned and x determines y
1245 NB; the ambiguity check is only used for *user* types, not for types
1246 coming from inteface files. The latter can legitimately have
1247 ambiguous types. Example
1249 class S a where s :: a -> (Int,Int)
1250 instance S Char where s _ = (1,1)
1251 f:: S a => [a] -> Int -> (Int,Int)
1252 f (_::[a]) x = (a*x,b)
1253 where (a,b) = s (undefined::a)
1255 Here the worker for f gets the type
1256 fw :: forall a. S a => Int -> (# Int, Int #)
1258 If the list of tv_names is empty, we have a monotype, and then we
1259 don't need to check for ambiguity either, because the test can't fail
1262 In addition, GHC insists that at least one type variable
1263 in each constraint is in V. So we disallow a type like
1264 forall a. Eq b => b -> b
1265 even in a scope where b is in scope.
1268 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1269 checkAmbiguity forall_tyvars theta tau_tyvars
1270 = mapM_ complain (filter is_ambig theta)
1272 complain pred = addErrTc (ambigErr pred)
1273 extended_tau_vars = growThetaTyVars theta tau_tyvars
1275 -- See Note [Implicit parameters and ambiguity] in TcSimplify
1276 is_ambig pred = isClassPred pred &&
1277 any ambig_var (varSetElems (tyVarsOfPred pred))
1279 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1280 not (ct_var `elemVarSet` extended_tau_vars)
1282 ambigErr :: PredType -> SDoc
1284 = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
1285 nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1286 ptext (sLit "must be reachable from the type after the '=>'"))]
1289 Note [Growing the tau-tvs using constraints]
1290 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1291 (growInstsTyVars insts tvs) is the result of extending the set
1292 of tyvars tvs using all conceivable links from pred
1294 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1295 Then grow precs tvs = {a,b,c}
1298 growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
1299 -- See Note [Growing the tau-tvs using constraints]
1300 growThetaTyVars theta tvs
1302 | otherwise = fixVarSet mk_next tvs
1304 mk_next tvs = foldr grow_one tvs theta
1305 grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
1307 growPredTyVars :: TcPredType
1308 -> TyVarSet -- The set to extend
1309 -> TyVarSet -- TyVars of the predicate if it intersects
1310 -- the set, or is implicit parameter
1311 growPredTyVars pred tvs
1312 | IParam {} <- pred = pred_tvs -- See Note [Implicit parameters and ambiguity]
1313 | pred_tvs `intersectsVarSet` tvs = pred_tvs
1314 | otherwise = emptyVarSet
1316 pred_tvs = tyVarsOfPred pred
1319 Note [Implicit parameters and ambiguity]
1320 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1321 Only a *class* predicate can give rise to ambiguity
1322 An *implicit parameter* cannot. For example:
1323 foo :: (?x :: [a]) => Int
1325 is fine. The call site will suppply a particular 'x'
1327 Furthermore, the type variables fixed by an implicit parameter
1328 propagate to the others. E.g.
1329 foo :: (Show a, ?x::[a]) => Int
1331 The type of foo looks ambiguous. But it isn't, because at a call site
1333 let ?x = 5::Int in foo
1334 and all is well. In effect, implicit parameters are, well, parameters,
1335 so we can take their type variables into account as part of the
1336 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
1340 checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
1341 checkThetaCtxt ctxt theta
1342 = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1343 ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
1345 eqSuperClassErr :: PredType -> SDoc
1346 eqSuperClassErr pred
1347 = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:"))
1350 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
1351 badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPred pred
1352 eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPred pred
1354 parens (ptext (sLit "Use -XTypeFamilies to permit this"))
1355 predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
1356 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1357 dupPredWarn :: [[PredType]] -> SDoc
1358 dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1360 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
1361 arityErr kind name n m
1362 = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1363 n_arguments <> comma, text "but has been given",
1364 if m==0 then text "none" else int m]
1366 n_arguments | n == 0 = ptext (sLit "no arguments")
1367 | n == 1 = ptext (sLit "1 argument")
1368 | True = hsep [int n, ptext (sLit "arguments")]
1371 %************************************************************************
1373 \subsection{Checking for a decent instance head type}
1375 %************************************************************************
1377 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1378 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1380 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1381 flag is on, or (2)~the instance is imported (they must have been
1382 compiled elsewhere). In these cases, we let them go through anyway.
1384 We can also have instances for functions: @instance Foo (a -> b) ...@.
1387 checkValidInstHead :: Class -> [Type] -> TcM ()
1388 checkValidInstHead clas tys
1389 = do { dflags <- getDOpts
1391 -- If GlasgowExts then check at least one isn't a type variable
1392 ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
1393 all tcInstHeadTyNotSynonym tys)
1394 (instTypeErr pp_pred head_type_synonym_msg)
1395 ; checkTc (xopt Opt_FlexibleInstances dflags ||
1396 all tcInstHeadTyAppAllTyVars tys)
1397 (instTypeErr pp_pred head_type_args_tyvars_msg)
1398 ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
1400 (instTypeErr pp_pred head_one_type_msg)
1401 -- May not contain type family applications
1402 ; mapM_ checkTyFamFreeness tys
1404 ; mapM_ checkValidMonoType tys
1405 -- For now, I only allow tau-types (not polytypes) in
1406 -- the head of an instance decl.
1407 -- E.g. instance C (forall a. a->a) is rejected
1408 -- One could imagine generalising that, but I'm not sure
1409 -- what all the consequences might be
1413 pp_pred = pprClassPred clas tys
1414 head_type_synonym_msg = parens (
1415 text "All instance types must be of the form (T t1 ... tn)" $$
1416 text "where T is not a synonym." $$
1417 text "Use -XTypeSynonymInstances if you want to disable this.")
1419 head_type_args_tyvars_msg = parens (vcat [
1420 text "All instance types must be of the form (T a1 ... an)",
1421 text "where a1 ... an are *distinct type variables*,",
1422 text "and each type variable appears at most once in the instance head.",
1423 text "Use -XFlexibleInstances if you want to disable this."])
1425 head_one_type_msg = parens (
1426 text "Only one type can be given in an instance head." $$
1427 text "Use -XMultiParamTypeClasses if you want to allow more.")
1429 instTypeErr :: SDoc -> SDoc -> SDoc
1430 instTypeErr pp_ty msg
1431 = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty,
1436 %************************************************************************
1438 \subsection{Checking instance for termination}
1440 %************************************************************************
1443 checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType
1444 -> Class -> [TcType] -> TcM ()
1445 checkValidInstance hs_type tyvars theta clas inst_tys
1446 = setSrcSpan (getLoc hs_type) $
1447 do { setSrcSpan head_loc (checkValidInstHead clas inst_tys)
1448 ; checkValidTheta InstThetaCtxt theta
1449 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1451 -- Check that instance inference will terminate (if we care)
1452 -- For Haskell 98 this will already have been done by checkValidTheta,
1453 -- but as we may be using other extensions we need to check.
1454 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1455 ; unless undecidable_ok $
1456 mapM_ addErrTc (checkInstTermination inst_tys theta)
1458 -- The Coverage Condition
1459 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1460 (instTypeErr (pprClassPred clas inst_tys) msg)
1463 msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1466 -- The location of the "head" of the instance
1467 head_loc = case hs_type of
1468 L _ (HsForAllTy _ _ _ (L loc _)) -> loc
1472 Termination test: the so-called "Paterson conditions" (see Section 5 of
1473 "Understanding functionsl dependencies via Constraint Handling Rules,
1476 We check that each assertion in the context satisfies:
1477 (1) no variable has more occurrences in the assertion than in the head, and
1478 (2) the assertion has fewer constructors and variables (taken together
1479 and counting repetitions) than the head.
1480 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1481 (which have already been checked) guarantee termination.
1483 The underlying idea is that
1485 for any ground substitution, each assertion in the
1486 context has fewer type constructors than the head.
1490 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1491 checkInstTermination tys theta
1492 = mapCatMaybes check theta
1495 size = sizeTypes tys
1497 | not (null (fvPred pred \\ fvs))
1498 = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1499 | sizePred pred >= size
1500 = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1504 predUndecErr :: PredType -> SDoc -> SDoc
1505 predUndecErr pred msg = sep [msg,
1506 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1508 nomoreMsg, smallerMsg, undecidableMsg :: SDoc
1509 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1510 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1511 undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
1514 validDeivPred checks for OK 'deriving' context. See Note [Exotic
1515 derived instance contexts] in TcSimplify. However the predicate is
1516 here because it uses sizeTypes, fvTypes.
1519 validDerivPred :: PredType -> Bool
1520 validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
1521 where fvs = fvTypes tys
1522 validDerivPred _ = False
1526 %************************************************************************
1528 Checking type instance well-formedness and termination
1530 %************************************************************************
1533 -- Check that a "type instance" is well-formed (which includes decidability
1534 -- unless -XUndecidableInstances is given).
1536 checkValidTypeInst :: [Type] -> Type -> TcM ()
1537 checkValidTypeInst typats rhs
1538 = do { -- left-hand side contains no type family applications
1539 -- (vanilla synonyms are fine, though)
1540 ; mapM_ checkTyFamFreeness typats
1542 -- the right-hand side is a tau type
1543 ; checkValidMonoType rhs
1545 -- we have a decidable instance unless otherwise permitted
1546 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1547 ; unless undecidable_ok $
1548 mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1551 -- Make sure that each type family instance is
1552 -- (1) strictly smaller than the lhs,
1553 -- (2) mentions no type variable more often than the lhs, and
1554 -- (3) does not contain any further type family instances.
1556 checkFamInst :: [Type] -- lhs
1557 -> [(TyCon, [Type])] -- type family instances
1559 checkFamInst lhsTys famInsts
1560 = mapCatMaybes check famInsts
1562 size = sizeTypes lhsTys
1563 fvs = fvTypes lhsTys
1565 | not (all isTyFamFree tys)
1566 = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1567 | not (null (fvTypes tys \\ fvs))
1568 = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1569 | size <= sizeTypes tys
1570 = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1574 famInst = TyConApp tc tys
1576 -- Ensure that no type family instances occur in a type.
1578 checkTyFamFreeness :: Type -> TcM ()
1579 checkTyFamFreeness ty
1580 = checkTc (isTyFamFree ty) $
1581 tyFamInstIllegalErr ty
1583 -- Check that a type does not contain any type family applications.
1585 isTyFamFree :: Type -> Bool
1586 isTyFamFree = null . tyFamInsts
1590 tyFamInstIllegalErr :: Type -> SDoc
1591 tyFamInstIllegalErr ty
1592 = hang (ptext (sLit "Illegal type synonym family application in instance") <>
1596 famInstUndecErr :: Type -> SDoc -> SDoc
1597 famInstUndecErr ty msg
1599 nest 2 (ptext (sLit "in the type family application:") <+>
1602 nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
1603 nestedMsg = ptext (sLit "Nested type family application")
1604 nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head")
1605 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1609 %************************************************************************
1611 \subsection{Auxiliary functions}
1613 %************************************************************************
1616 -- Free variables of a type, retaining repetitions, and expanding synonyms
1617 fvType :: Type -> [TyVar]
1618 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1619 fvType (TyVarTy tv) = [tv]
1620 fvType (TyConApp _ tys) = fvTypes tys
1621 fvType (PredTy pred) = fvPred pred
1622 fvType (FunTy arg res) = fvType arg ++ fvType res
1623 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1624 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1626 fvTypes :: [Type] -> [TyVar]
1627 fvTypes tys = concat (map fvType tys)
1629 fvPred :: PredType -> [TyVar]
1630 fvPred (ClassP _ tys') = fvTypes tys'
1631 fvPred (IParam _ ty) = fvType ty
1632 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1634 -- Size of a type: the number of variables and constructors
1635 sizeType :: Type -> Int
1636 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1637 sizeType (TyVarTy _) = 1
1638 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1639 sizeType (PredTy pred) = sizePred pred
1640 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1641 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1642 sizeType (ForAllTy _ ty) = sizeType ty
1644 sizeTypes :: [Type] -> Int
1645 sizeTypes xs = sum (map sizeType xs)
1647 -- Size of a predicate
1649 -- We are considering whether *class* constraints terminate
1650 -- Once we get into an implicit parameter or equality we
1651 -- can't get back to a class constraint, so it's safe
1652 -- to say "size 0". See Trac #4200.
1653 sizePred :: PredType -> Int
1654 sizePred (ClassP _ tys') = sizeTypes tys'
1655 sizePred (IParam {}) = 0
1656 sizePred (EqPred {}) = 0