2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
6 Monadic type operations
8 This module contains monadic operations over types that contain
13 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
15 --------------------------------
16 -- Creating new mutable type variables
18 newFlexiTyVarTy, -- Kind -> TcM TcType
19 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
20 newKindVar, newKindVars,
23 newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
24 isFilledMetaTyVar, isFlexiMetaTyVar,
26 --------------------------------
27 -- Creating new evidence variables
28 newEvVar, newCoVar, newEvVars,
29 newIP, newDict, newSilentGiven, isSilentEvVar,
31 newWantedEvVar, newWantedEvVars,
32 newTcEvBinds, addTcEvBind,
34 --------------------------------
36 tcInstTyVars, tcInstSigTyVars,
38 tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
39 tcSkolDFunType, tcSuperSkolTyVars,
41 --------------------------------
42 -- Checking type validity
43 Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
44 SourceTyCtxt(..), checkValidTheta,
45 checkValidInstHead, checkValidInstance,
46 checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
48 growPredTyVars, growThetaTyVars, validDerivPred,
50 --------------------------------
52 zonkType, mkZonkTcTyVar, zonkTcPredType,
53 zonkTcTypeCarefully, skolemiseUnboundMetaTyVar,
54 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
55 zonkQuantifiedTyVar, zonkQuantifiedTyVars,
56 zonkTcType, zonkTcTypes, zonkTcThetaType,
57 zonkTcKindToKind, zonkTcKind,
58 zonkImplication, zonkEvVar, zonkWantedEvVar, zonkFlavoredEvVar,
59 zonkWC, zonkWantedEvVars,
64 readKindVar, writeKindVar
67 #include "HsVersions.h"
78 import HsSyn -- HsType
79 import TcRnMonad -- TcType, amongst others
93 import Unique( Unique )
97 import Data.List ( (\\) )
101 %************************************************************************
105 %************************************************************************
108 newKindVar :: TcM TcKind
109 newKindVar = do { uniq <- newUnique
110 ; ref <- newMutVar Flexi
111 ; return (mkTyVarTy (mkKindVar uniq ref)) }
113 newKindVars :: Int -> TcM [TcKind]
114 newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
118 %************************************************************************
120 Evidence variables; range over constraints we can abstract over
122 %************************************************************************
125 newEvVars :: TcThetaType -> TcM [EvVar]
126 newEvVars theta = mapM newEvVar theta
128 newWantedEvVar :: TcPredType -> TcM EvVar
129 newWantedEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
130 newWantedEvVar (ClassP cls tys) = newDict cls tys
131 newWantedEvVar (IParam ip ty) = newIP ip ty
133 newWantedEvVars :: TcThetaType -> TcM [EvVar]
134 newWantedEvVars theta = mapM newWantedEvVar theta
137 newEvVar :: TcPredType -> TcM EvVar
138 -- Creates new *rigid* variables for predicates
139 newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
140 newEvVar (ClassP cls tys) = newDict cls tys
141 newEvVar (IParam ip ty) = newIP ip ty
143 newCoVar :: TcType -> TcType -> TcM CoVar
145 = do { name <- newName (mkVarOccFS (fsLit "co"))
146 ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
148 newIP :: IPName Name -> TcType -> TcM IpId
150 = do { name <- newName (getOccName (ipNameName ip))
151 ; return (mkLocalId name (mkPredTy (IParam ip ty))) }
153 newDict :: Class -> [TcType] -> TcM DictId
155 = do { name <- newName (mkDictOcc (getOccName cls))
156 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
158 newName :: OccName -> TcM Name
160 = do { uniq <- newUnique
162 ; return (mkInternalName uniq occ loc) }
165 newSilentGiven :: PredType -> TcM EvVar
166 -- Make a dictionary for a "silent" given dictionary
167 -- Behaves just like any EvVar except that it responds True to isSilentDict
168 -- This is used only to suppress confusing error reports
169 newSilentGiven (ClassP cls tys)
170 = do { uniq <- newUnique
171 ; let name = mkSystemName uniq (mkDictOcc (getOccName cls))
172 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
173 newSilentGiven (EqPred ty1 ty2)
174 = do { uniq <- newUnique
175 ; let name = mkSystemName uniq (mkTyVarOccFS (fsLit "co"))
176 ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
177 newSilentGiven pred@(IParam {})
178 = pprPanic "newSilentDict" (ppr pred) -- Implicit parameters rejected earlier
180 isSilentEvVar :: EvVar -> Bool
181 isSilentEvVar v = isSystemName (Var.varName v)
182 -- Notice that all *other* evidence variables get Internal Names
186 %************************************************************************
188 SkolemTvs (immutable)
190 %************************************************************************
193 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
194 -> TcType -- Type to instantiate
195 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
196 -- (type vars (excl coercion vars), preds (incl equalities), rho)
197 tcInstType inst_tyvars ty
198 = case tcSplitForAllTys ty of
199 ([], rho) -> let -- There may be overloading despite no type variables;
200 -- (?x :: Int) => Int -> Int
201 (theta, tau) = tcSplitPhiTy rho
203 return ([], theta, tau)
205 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
207 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
208 -- Either the tyvars are freshly made, by inst_tyvars,
209 -- or any nested foralls have different binders.
210 -- Either way, zipTopTvSubst is ok
212 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
213 ; return (tyvars', theta, tau) }
215 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
216 -- Instantiate a type signature with skolem constants, but
217 -- do *not* give them fresh names, because we want the name to
218 -- be in the type environment: it is lexically scoped.
219 tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty
221 tcSuperSkolTyVars :: [TyVar] -> [TcTyVar]
222 -- Make skolem constants, but do *not* give them new names, as above
223 -- Moreover, make them "super skolems"; see comments with superSkolemTv
224 tcSuperSkolTyVars tyvars
225 = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) superSkolemTv
228 tcInstSkolTyVar :: Bool -> TyVar -> TcM TcTyVar
229 -- Instantiate the tyvar, using
230 -- * the occ-name and kind of the supplied tyvar,
231 -- * the unique from the monad,
232 -- * the location either from the tyvar (skol_info = SigSkol)
233 -- or from the monad (otherwise)
234 tcInstSkolTyVar overlappable tyvar
235 = do { uniq <- newUnique
237 ; let new_name = mkInternalName uniq occ loc
238 ; return (mkTcTyVar new_name kind (SkolemTv overlappable)) }
240 old_name = tyVarName tyvar
241 occ = nameOccName old_name
242 kind = tyVarKind tyvar
244 tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar]
245 tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars
247 tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
248 tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars
250 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
251 -- Instantiate a type with fresh skolem constants
252 -- Binding location comes from the monad
253 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
255 tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
256 -- Make meta SigTv type variables for patten-bound scoped type varaibles
257 -- We use SigTvs for them, so that they can't unify with arbitrary types
258 tcInstSigTyVars = mapM tcInstSigTyVar
260 tcInstSigTyVar :: TyVar -> TcM TcTyVar
262 = do { uniq <- newMetaUnique
263 ; ref <- newMutVar Flexi
264 ; let name = setNameUnique (tyVarName tyvar) uniq
265 -- Use the same OccName so that the tidy-er
266 -- doesn't rename 'a' to 'a0' etc
267 kind = tyVarKind tyvar
268 ; return (mkTcTyVar name kind (MetaTv SigTv ref)) }
272 %************************************************************************
274 MetaTvs (meta type variables; mutable)
276 %************************************************************************
279 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
280 -- Make a new meta tyvar out of thin air
281 newMetaTyVar meta_info kind
282 = do { uniq <- newMetaUnique
283 ; ref <- newMutVar Flexi
284 ; let name = mkTcTyVarName uniq s
285 s = case meta_info of
289 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
291 mkTcTyVarName :: Unique -> FastString -> Name
292 -- Make sure that fresh TcTyVar names finish with a digit
293 -- leaving the un-cluttered names free for user names
294 mkTcTyVarName uniq str = mkSysTvName uniq str
296 readMetaTyVar :: TyVar -> TcM MetaDetails
297 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
298 readMutVar (metaTvRef tyvar)
300 isFilledMetaTyVar :: TyVar -> TcM Bool
301 -- True of a filled-in (Indirect) meta type variable
303 | not (isTcTyVar tv) = return False
304 | MetaTv _ ref <- tcTyVarDetails tv
305 = do { details <- readMutVar ref
306 ; return (isIndirect details) }
307 | otherwise = return False
309 isFlexiMetaTyVar :: TyVar -> TcM Bool
310 -- True of a un-filled-in (Flexi) meta type variable
312 | not (isTcTyVar tv) = return False
313 | MetaTv _ ref <- tcTyVarDetails tv
314 = do { details <- readMutVar ref
315 ; return (isFlexi details) }
316 | otherwise = return False
319 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
320 -- Write into a currently-empty MetaTyVar
322 writeMetaTyVar tyvar ty
324 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
326 -- Everything from here on only happens if DEBUG is on
327 | not (isTcTyVar tyvar)
328 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
331 | MetaTv _ ref <- tcTyVarDetails tyvar
332 = writeMetaTyVarRef tyvar ref ty
335 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
339 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
340 -- Here the tyvar is for error checking only;
341 -- the ref cell must be for the same tyvar
342 writeMetaTyVarRef tyvar ref ty
344 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
345 ; writeMutVar ref (Indirect ty) }
347 -- Everything from here on only happens if DEBUG is on
348 | not (isPredTy tv_kind) -- Don't check kinds for updates to coercion variables
349 , not (ty_kind `isSubKind` tv_kind)
350 = WARN( True, hang (text "Ill-kinded update to meta tyvar")
351 2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
355 = do { meta_details <- readMutVar ref;
356 ; ASSERT2( isFlexi meta_details,
357 hang (text "Double update of meta tyvar")
358 2 (ppr tyvar $$ ppr meta_details) )
360 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
361 ; writeMutVar ref (Indirect ty) }
363 tv_kind = tyVarKind tyvar
364 ty_kind = typeKind ty
368 %************************************************************************
372 %************************************************************************
375 newFlexiTyVar :: Kind -> TcM TcTyVar
376 newFlexiTyVar kind = newMetaTyVar TauTv kind
378 newFlexiTyVarTy :: Kind -> TcM TcType
379 newFlexiTyVarTy kind = do
380 tc_tyvar <- newFlexiTyVar kind
381 return (TyVarTy tc_tyvar)
383 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
384 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
386 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
387 -- Instantiate with META type variables
389 = do { tc_tvs <- mapM tcInstTyVar tyvars
390 ; let tys = mkTyVarTys tc_tvs
391 ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
392 -- Since the tyvars are freshly made,
393 -- they cannot possibly be captured by
394 -- any existing for-alls. Hence zipTopTvSubst
396 tcInstTyVar :: TyVar -> TcM TcTyVar
397 -- Make a new unification variable tyvar whose Name and Kind
398 -- come from an existing TyVar
400 = do { uniq <- newMetaUnique
401 ; ref <- newMutVar Flexi
402 ; let name = mkSystemName uniq (getOccName tyvar)
403 kind = tyVarKind tyvar
404 ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }
408 %************************************************************************
412 %************************************************************************
415 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
417 | isSkolemTyVar sig_tv
418 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
420 = ASSERT( isSigTyVar sig_tv )
421 do { ty <- zonkTcTyVar sig_tv
422 ; return (tcGetTyVar "zonkSigTyVar" ty) }
423 -- 'ty' is bound to be a type variable, because SigTvs
424 -- can only be unified with type variables
429 %************************************************************************
431 \subsection{Zonking -- the exernal interfaces}
433 %************************************************************************
435 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
436 To improve subsequent calls to the same function it writes the zonked set back into
440 tcGetGlobalTyVars :: TcM TcTyVarSet
442 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
443 ; gbl_tvs <- readMutVar gtv_var
444 ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
445 ; writeMutVar gtv_var gbl_tvs'
449 ----------------- Type variables
452 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
453 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
455 zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
456 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
458 ----------------- Types
459 zonkTcTypeCarefully :: TcType -> TcM TcType
460 -- Do not zonk type variables free in the environment
461 zonkTcTypeCarefully ty
462 = do { env_tvs <- tcGetGlobalTyVars
463 ; zonkType (zonk_tv env_tvs) ty }
466 | tv `elemVarSet` env_tvs
467 = return (TyVarTy tv)
469 = ASSERT( isTcTyVar tv )
470 case tcTyVarDetails tv of
471 SkolemTv {} -> return (TyVarTy tv)
472 RuntimeUnk {} -> return (TyVarTy tv)
473 FlatSkol ty -> zonkType (zonk_tv env_tvs) ty
474 MetaTv _ ref -> do { cts <- readMutVar ref
476 Flexi -> return (TyVarTy tv)
477 Indirect ty -> zonkType (zonk_tv env_tvs) ty }
479 zonkTcType :: TcType -> TcM TcType
480 -- Simply look through all Flexis
481 zonkTcType ty = zonkType zonkTcTyVar ty
483 zonkTcTyVar :: TcTyVar -> TcM TcType
484 -- Simply look through all Flexis
486 = ASSERT2( isTcTyVar tv, ppr tv )
487 case tcTyVarDetails tv of
488 SkolemTv {} -> return (TyVarTy tv)
489 RuntimeUnk {} -> return (TyVarTy tv)
490 FlatSkol ty -> zonkTcType ty
491 MetaTv _ ref -> do { cts <- readMutVar ref
493 Flexi -> return (TyVarTy tv)
494 Indirect ty -> zonkTcType ty }
496 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
497 -- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
498 zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
501 = case tcTyVarDetails tv of
502 SkolemTv {} -> return (TyVarTy tv)
503 RuntimeUnk {} -> return (TyVarTy tv)
504 FlatSkol ty -> zonkType zonk_tv ty
505 MetaTv _ ref -> do { cts <- readMutVar ref
507 Flexi -> zonk_flexi tv
508 Indirect ty -> zonkType zonk_tv ty }
510 = case lookupTyVar subst tv of
511 Just ty -> zonkType zonk_tv ty
512 Nothing -> return (TyVarTy tv)
514 zonkTcTypes :: [TcType] -> TcM [TcType]
515 zonkTcTypes tys = mapM zonkTcType tys
517 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
518 zonkTcThetaType theta = mapM zonkTcPredType theta
520 zonkTcPredType :: TcPredType -> TcM TcPredType
521 zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts
522 zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t
523 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
526 ------------------- These ...ToType, ...ToKind versions
527 are used at the end of type checking
530 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
531 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
533 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
534 -- The quantified type variables often include meta type variables
535 -- we want to freeze them into ordinary type variables, and
536 -- default their kind (e.g. from OpenTypeKind to TypeKind)
537 -- -- see notes with Kind.defaultKind
538 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
539 -- bound occurences of the original type variable will get zonked to
540 -- the immutable version.
542 -- We leave skolem TyVars alone; they are immutable.
543 zonkQuantifiedTyVar tv
544 = ASSERT2( isTcTyVar tv, ppr tv )
545 case tcTyVarDetails tv of
546 SkolemTv {} -> WARN( True, ppr tv ) -- Dec10: Can this really happen?
547 do { kind <- zonkTcType (tyVarKind tv)
548 ; return $ setTyVarKind tv kind }
549 -- It might be a skolem type variable,
550 -- for example from a user type signature
554 -- [Sept 04] Check for non-empty.
555 -- See note [Silly Type Synonym]
556 (readMutVar _ref >>= \cts ->
559 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
562 skolemiseUnboundMetaTyVar tv vanillaSkolemTv
563 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
565 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
566 -- We have a Meta tyvar with a ref-cell inside it
567 -- Skolemise it, including giving it a new Name, so that
568 -- we are totally out of Meta-tyvar-land
569 -- We create a skolem TyVar, not a regular TyVar
570 -- See Note [Zonking to Skolem]
571 skolemiseUnboundMetaTyVar tv details
572 = ASSERT2( isMetaTyVar tv, ppr tv )
573 do { span <- getSrcSpanM -- Get the location from "here"
574 -- ie where we are generalising
575 ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land
576 ; let final_kind = defaultKind (tyVarKind tv)
577 final_name = mkInternalName uniq (getOccName tv) span
578 final_tv = mkTcTyVar final_name final_kind details
579 ; writeMetaTyVar tv (mkTyVarTy final_tv)
584 zonkImplication :: Implication -> TcM Implication
585 zonkImplication implic@(Implic { ic_given = given
588 = do { -- No need to zonk the skolems
589 ; given' <- mapM zonkEvVar given
590 ; loc' <- zonkGivenLoc loc
591 ; wanted' <- zonkWC wanted
592 ; return (implic { ic_given = given'
593 , ic_wanted = wanted'
596 zonkEvVar :: EvVar -> TcM EvVar
597 zonkEvVar var = do { ty' <- zonkTcType (varType var)
598 ; return (setVarType var ty') }
600 zonkFlavoredEvVar :: FlavoredEvVar -> TcM FlavoredEvVar
601 zonkFlavoredEvVar (EvVarX ev fl)
602 = do { ev' <- zonkEvVar ev
603 ; fl' <- zonkFlavor fl
604 ; return (EvVarX ev' fl') }
606 zonkWC :: WantedConstraints -> TcM WantedConstraints
607 zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
608 = do { flat' <- zonkWantedEvVars flat
609 ; implic' <- mapBagM zonkImplication implic
610 ; insol' <- mapBagM zonkFlavoredEvVar insol
611 ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
613 zonkWantedEvVars :: Bag WantedEvVar -> TcM (Bag WantedEvVar)
614 zonkWantedEvVars = mapBagM zonkWantedEvVar
616 zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
617 zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) }
619 zonkFlavor :: CtFlavor -> TcM CtFlavor
620 zonkFlavor (Given loc gk) = do { loc' <- zonkGivenLoc loc; return (Given loc' gk) }
621 zonkFlavor fl = return fl
623 zonkGivenLoc :: GivenLoc -> TcM GivenLoc
624 -- GivenLocs may have unification variables inside them!
625 zonkGivenLoc (CtLoc skol_info span ctxt)
626 = do { skol_info' <- zonkSkolemInfo skol_info
627 ; return (CtLoc skol_info' span ctxt) }
629 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
630 zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty
631 ; return (SigSkol cx ty') }
632 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
633 ; return (InferSkol ntys') }
635 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
636 zonkSkolemInfo skol_info = return skol_info
639 Note [Silly Type Synonyms]
640 ~~~~~~~~~~~~~~~~~~~~~~~~~~
642 type C u a = u -- Note 'a' unused
644 foo :: (forall a. C u a -> C u a) -> u
648 bar = foo (\t -> t + t)
650 * From the (\t -> t+t) we get type {Num d} => d -> d
653 * Now unify with type of foo's arg, and we get:
654 {Num (C d a)} => C d a -> C d a
657 * Now abstract over the 'a', but float out the Num (C d a) constraint
658 because it does not 'really' mention a. (see exactTyVarsOfType)
659 The arg to foo becomes
662 * So we get a dict binding for Num (C d a), which is zonked to give
664 [Note Sept 04: now that we are zonking quantified type variables
665 on construction, the 'a' will be frozen as a regular tyvar on
666 quantification, so the floated dict will still have type (C d a).
667 Which renders this whole note moot; happily!]
669 * Then the \/\a abstraction has a zonked 'a' in it.
671 All very silly. I think its harmless to ignore the problem. We'll end up with
672 a \/\a in the final result but all the occurrences of a will be zonked to ()
674 Note [Zonking to Skolem]
675 ~~~~~~~~~~~~~~~~~~~~~~~~
676 We used to zonk quantified type variables to regular TyVars. However, this
677 leads to problems. Consider this program from the regression test suite:
679 eval :: Int -> String -> String -> String
680 eval 0 root actual = evalRHS 0 root actual
683 evalRHS 0 root actual = eval 0 root actual
685 It leads to the deferral of an equality (wrapped in an implication constraint)
687 forall a. (String -> String -> String) ~ a
689 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
690 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
691 This has the *side effect* of also zonking the `a' in the deferred equality
692 (which at this point is being handed around wrapped in an implication
695 Finally, the equality (with the zonked `a') will be handed back to the
696 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
697 If we zonk `a' with a regular type variable, we will have this regular type
698 variable now floating around in the simplifier, which in many places assumes to
699 only see proper TcTyVars.
701 We can avoid this problem by zonking with a skolem. The skolem is rigid
702 (which we require for a quantified variable), but is still a TcTyVar that the
703 simplifier knows how to deal with.
706 %************************************************************************
708 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
710 %* For internal use only! *
712 %************************************************************************
715 -- For unbound, mutable tyvars, zonkType uses the function given to it
716 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
717 -- type variable and zonks the kind too
719 zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars
720 -> TcType -> TcM Type
721 zonkType zonk_tc_tyvar ty
724 go (TyConApp tc tys) = do tys' <- mapM go tys
725 return (TyConApp tc tys')
727 go (PredTy p) = do p' <- go_pred p
730 go (FunTy arg res) = do arg' <- go arg
732 return (FunTy arg' res')
734 go (AppTy fun arg) = do fun' <- go fun
736 return (mkAppTy fun' arg')
737 -- NB the mkAppTy; we might have instantiated a
738 -- type variable to a type constructor, so we need
739 -- to pull the TyConApp to the top.
741 -- The two interesting cases!
742 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
743 | otherwise = return (TyVarTy tyvar)
744 -- Ordinary (non Tc) tyvars occur inside quantified types
746 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
748 tyvar' <- return tyvar
749 return (ForAllTy tyvar' ty')
751 go_pred (ClassP c tys) = do tys' <- mapM go tys
752 return (ClassP c tys')
753 go_pred (IParam n ty) = do ty' <- go ty
754 return (IParam n ty')
755 go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
757 return (EqPred ty1' ty2')
759 mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var
760 -> TcTyVar -> TcM TcType
761 mkZonkTcTyVar unbound_var_fn tyvar
762 = ASSERT( isTcTyVar tyvar )
763 case tcTyVarDetails tyvar of
764 SkolemTv {} -> return (TyVarTy tyvar)
765 RuntimeUnk {} -> return (TyVarTy tyvar)
766 FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
767 MetaTv _ ref -> do { cts <- readMutVar ref
769 Flexi -> unbound_var_fn tyvar
770 Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
775 %************************************************************************
779 %************************************************************************
782 readKindVar :: KindVar -> TcM (MetaDetails)
783 writeKindVar :: KindVar -> TcKind -> TcM ()
784 readKindVar kv = readMutVar (kindVarRef kv)
785 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
788 zonkTcKind :: TcKind -> TcM TcKind
789 zonkTcKind k = zonkTcType k
792 zonkTcKindToKind :: TcKind -> TcM Kind
793 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
794 -- Haskell specifies that * is to be used, so we follow that.
796 = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
799 %************************************************************************
801 \subsection{Checking a user type}
803 %************************************************************************
805 When dealing with a user-written type, we first translate it from an HsType
806 to a Type, performing kind checking, and then check various things that should
807 be true about it. We don't want to perform these checks at the same time
808 as the initial translation because (a) they are unnecessary for interface-file
809 types and (b) when checking a mutually recursive group of type and class decls,
810 we can't "look" at the tycons/classes yet. Also, the checks are are rather
811 diverse, and used to really mess up the other code.
813 One thing we check for is 'rank'.
815 Rank 0: monotypes (no foralls)
816 Rank 1: foralls at the front only, Rank 0 inside
817 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
819 basic ::= tyvar | T basic ... basic
821 r2 ::= forall tvs. cxt => r2a
822 r2a ::= r1 -> r2a | basic
823 r1 ::= forall tvs. cxt => r0
824 r0 ::= r0 -> r0 | basic
826 Another thing is to check that type synonyms are saturated.
827 This might not necessarily show up in kind checking.
829 data T k = MkT (k Int)
834 checkValidType :: UserTypeCtxt -> Type -> TcM ()
835 -- Checks that the type is valid for the given context
836 checkValidType ctxt ty = do
837 traceTc "checkValidType" (ppr ty)
838 unboxed <- xoptM Opt_UnboxedTuples
839 rank2 <- xoptM Opt_Rank2Types
840 rankn <- xoptM Opt_RankNTypes
841 polycomp <- xoptM Opt_PolymorphicComponents
843 gen_rank n | rankn = ArbitraryRank
848 DefaultDeclCtxt-> MustBeMonoType
849 ResSigCtxt -> MustBeMonoType
850 LamPatSigCtxt -> gen_rank 0
851 BindPatSigCtxt -> gen_rank 0
852 TySynCtxt _ -> gen_rank 0
853 GenPatCtxt -> gen_rank 1
854 -- This one is a bit of a hack
855 -- See the forall-wrapping in TcClassDcl.mkGenericInstance
857 ExprSigCtxt -> gen_rank 1
858 FunSigCtxt _ -> gen_rank 1
859 ConArgCtxt _ | polycomp -> gen_rank 2
860 -- We are given the type of the entire
861 -- constructor, hence rank 1
862 | otherwise -> gen_rank 1
864 ForSigCtxt _ -> gen_rank 1
865 SpecInstCtxt -> gen_rank 1
866 ThBrackCtxt -> gen_rank 1
867 GenSigCtxt -> panic "checkValidType"
868 -- Can't happen; GenSigCtxt not used for *user* sigs
870 actual_kind = typeKind ty
872 kind_ok = case ctxt of
873 TySynCtxt _ -> True -- Any kind will do
874 ThBrackCtxt -> True -- Any kind will do
875 ResSigCtxt -> isSubOpenTypeKind actual_kind
876 ExprSigCtxt -> isSubOpenTypeKind actual_kind
877 GenPatCtxt -> isLiftedTypeKind actual_kind
878 ForSigCtxt _ -> isLiftedTypeKind actual_kind
879 _ -> isSubArgTypeKind actual_kind
881 ubx_tup = case ctxt of
882 TySynCtxt _ | unboxed -> UT_Ok
883 ExprSigCtxt | unboxed -> UT_Ok
884 ThBrackCtxt | unboxed -> UT_Ok
887 -- Check the internal validity of the type itself
888 check_type rank ubx_tup ty
890 -- Check that the thing has kind Type, and is lifted if necessary
891 -- Do this second, becuase we can't usefully take the kind of an
892 -- ill-formed type such as (a~Int)
893 checkTc kind_ok (kindErr actual_kind)
895 traceTc "checkValidType done" (ppr ty)
897 checkValidMonoType :: Type -> TcM ()
898 checkValidMonoType ty = check_mono_type MustBeMonoType ty
903 data Rank = ArbitraryRank -- Any rank ok
904 | MustBeMonoType -- Monotype regardless of flags
905 | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes
906 | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms
907 | Rank Int -- Rank n, but could be more with -XRankNTypes
909 decRank :: Rank -> Rank -- Function arguments
910 decRank (Rank 0) = Rank 0
911 decRank (Rank n) = Rank (n-1)
912 decRank other_rank = other_rank
914 nonZeroRank :: Rank -> Bool
915 nonZeroRank ArbitraryRank = True
916 nonZeroRank (Rank n) = n>0
917 nonZeroRank _ = False
919 ----------------------------------------
920 data UbxTupFlag = UT_Ok | UT_NotOk
921 -- The "Ok" version means "ok if UnboxedTuples is on"
923 ----------------------------------------
924 check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere
925 -- No unlifted types of any kind
926 check_mono_type rank ty
927 = do { check_type rank UT_NotOk ty
928 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
930 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
931 -- The args say what the *type context* requires, independent
932 -- of *flag* settings. You test the flag settings at usage sites.
934 -- Rank is allowed rank for function args
935 -- Rank 0 means no for-alls anywhere
937 check_type rank ubx_tup ty
938 | not (null tvs && null theta)
939 = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
940 -- Reject e.g. (Maybe (?x::Int => Int)),
941 -- with a decent error message
942 ; check_valid_theta SigmaCtxt theta
943 ; check_type rank ubx_tup tau -- Allow foralls to right of arrow
944 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
946 (tvs, theta, tau) = tcSplitSigmaTy ty
948 -- Naked PredTys should, I think, have been rejected before now
949 check_type _ _ ty@(PredTy {})
950 = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type")
952 check_type _ _ (TyVarTy _) = return ()
954 check_type rank _ (FunTy arg_ty res_ty)
955 = do { check_type (decRank rank) UT_NotOk arg_ty
956 ; check_type rank UT_Ok res_ty }
958 check_type rank _ (AppTy ty1 ty2)
959 = do { check_arg_type rank ty1
960 ; check_arg_type rank ty2 }
962 check_type rank ubx_tup ty@(TyConApp tc tys)
964 = do { -- Check that the synonym has enough args
965 -- This applies equally to open and closed synonyms
966 -- It's OK to have an *over-applied* type synonym
967 -- data Tree a b = ...
968 -- type Foo a = Tree [a]
969 -- f :: Foo a b -> ...
970 checkTc (tyConArity tc <= length tys) arity_msg
972 -- See Note [Liberal type synonyms]
973 ; liberal <- xoptM Opt_LiberalTypeSynonyms
974 ; if not liberal || isSynFamilyTyCon tc then
975 -- For H98 and synonym families, do check the type args
976 mapM_ (check_mono_type SynArgMonoType) tys
978 else -- In the liberal case (only for closed syns), expand then check
980 Just ty' -> check_type rank ubx_tup ty'
981 Nothing -> pprPanic "check_tau_type" (ppr ty)
984 | isUnboxedTupleTyCon tc
985 = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
986 ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
988 ; impred <- xoptM Opt_ImpredicativeTypes
989 ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
990 -- c.f. check_arg_type
991 -- However, args are allowed to be unlifted, or
992 -- more unboxed tuples, so can't use check_arg_ty
993 ; mapM_ (check_type rank' UT_Ok) tys }
996 = mapM_ (check_arg_type rank) tys
999 ubx_tup_ok ub_tuples_allowed = case ubx_tup of
1000 UT_Ok -> ub_tuples_allowed
1004 tc_arity = tyConArity tc
1006 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1007 ubx_tup_msg = ubxArgTyErr ty
1009 check_type _ _ ty = pprPanic "check_type" (ppr ty)
1011 ----------------------------------------
1012 check_arg_type :: Rank -> Type -> TcM ()
1013 -- The sort of type that can instantiate a type variable,
1014 -- or be the argument of a type constructor.
1015 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
1016 -- Other unboxed types are very occasionally allowed as type
1017 -- arguments depending on the kind of the type constructor
1019 -- For example, we want to reject things like:
1021 -- instance Ord a => Ord (forall s. T s a)
1023 -- g :: T s (forall b.b)
1025 -- NB: unboxed tuples can have polymorphic or unboxed args.
1026 -- This happens in the workers for functions returning
1027 -- product types with polymorphic components.
1028 -- But not in user code.
1029 -- Anyway, they are dealt with by a special case in check_tau_type
1031 check_arg_type rank ty
1032 = do { impred <- xoptM Opt_ImpredicativeTypes
1033 ; let rank' = case rank of -- Predictive => must be monotype
1034 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
1035 _other | impred -> ArbitraryRank
1036 | otherwise -> TyConArgMonoType
1037 -- Make sure that MustBeMonoType is propagated,
1038 -- so that we don't suggest -XImpredicativeTypes in
1039 -- (Ord (forall a.a)) => a -> a
1040 -- and so that if it Must be a monotype, we check that it is!
1042 ; check_type rank' UT_NotOk ty
1043 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1045 ----------------------------------------
1046 forAllTyErr :: Rank -> Type -> SDoc
1048 = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
1051 suggestion = case rank of
1052 Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
1053 TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
1054 SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
1055 _ -> empty -- Polytype is always illegal
1057 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
1058 unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1059 ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1061 kindErr :: Kind -> SDoc
1062 kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1065 Note [Liberal type synonyms]
1066 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1067 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1068 doing validity checking. This allows us to instantiate a synonym defn
1069 with a for-all type, or with a partially-applied type synonym.
1073 Here, T is partially applied, so it's illegal in H98. But if you
1074 expand S first, then T we get just
1078 IMPORTANT: suppose T is a type synonym. Then we must do validity
1079 checking on an appliation (T ty1 ty2)
1081 *either* before expansion (i.e. check ty1, ty2)
1082 *or* after expansion (i.e. expand T ty1 ty2, and then check)
1085 If we do both, we get exponential behaviour!!
1087 data TIACons1 i r c = c i ::: r c
1088 type TIACons2 t x = TIACons1 t (TIACons1 t x)
1089 type TIACons3 t x = TIACons2 t (TIACons1 t x)
1090 type TIACons4 t x = TIACons2 t (TIACons2 t x)
1091 type TIACons7 t x = TIACons4 t (TIACons3 t x)
1094 %************************************************************************
1096 \subsection{Checking a theta or source type}
1098 %************************************************************************
1101 -- Enumerate the contexts in which a "source type", <S>, can occur
1105 -- or (N a) where N is a newtype
1108 = ClassSCCtxt Name -- Superclasses of clas
1109 -- class <S> => C a where ...
1110 | SigmaCtxt -- Theta part of a normal for-all type
1111 -- f :: <S> => a -> a
1112 | DataTyCtxt Name -- Theta part of a data decl
1113 -- data <S> => T a = MkT a
1114 | TypeCtxt -- Source type in an ordinary type
1116 | InstThetaCtxt -- Context of an instance decl
1117 -- instance <S> => C [a] where ...
1119 pprSourceTyCtxt :: SourceTyCtxt -> SDoc
1120 pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
1121 pprSourceTyCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type")
1122 pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
1123 pprSourceTyCtxt InstThetaCtxt = ptext (sLit "the context of an instance declaration")
1124 pprSourceTyCtxt TypeCtxt = ptext (sLit "the context of a type")
1128 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1129 checkValidTheta ctxt theta
1130 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1132 -------------------------
1133 check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
1134 check_valid_theta _ []
1136 check_valid_theta ctxt theta = do
1138 warnTc (notNull dups) (dupPredWarn dups)
1139 mapM_ (check_pred_ty dflags ctxt) theta
1141 (_,dups) = removeDups cmpPred theta
1143 -------------------------
1144 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1145 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1146 = do { -- Class predicates are valid in all contexts
1147 ; checkTc (arity == n_tys) arity_err
1149 -- Check the form of the argument types
1150 ; mapM_ checkValidMonoType tys
1151 ; checkTc (check_class_pred_tys dflags ctxt tys)
1152 (predTyVarErr pred $$ how_to_allow)
1155 class_name = className cls
1156 arity = classArity cls
1158 arity_err = arityErr "Class" class_name arity n_tys
1159 how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
1162 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
1163 = do { -- Equational constraints are valid in all contexts if type
1164 -- families are permitted
1165 ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1166 ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
1167 (eqSuperClassErr pred)
1169 -- Check the form of the argument types
1170 ; checkValidMonoType ty1
1171 ; checkValidMonoType ty2
1174 check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
1175 -- Implicit parameters only allowed in type
1176 -- signatures; not in instance decls, superclasses etc
1177 -- The reason for not allowing implicit params in instances is a bit
1179 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
1180 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
1181 -- discharge all the potential usas of the ?x in e. For example, a
1182 -- constraint Foo [Int] might come out of e,and applying the
1183 -- instance decl would show up two uses of ?x.
1186 check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
1188 -------------------------
1189 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1190 check_class_pred_tys dflags ctxt tys
1192 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1193 InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1194 -- Further checks on head and theta in
1195 -- checkInstTermination
1196 _ -> flexible_contexts || all tyvar_head tys
1198 flexible_contexts = xopt Opt_FlexibleContexts dflags
1199 undecidable_ok = xopt Opt_UndecidableInstances dflags
1201 -------------------------
1202 tyvar_head :: Type -> Bool
1203 tyvar_head ty -- Haskell 98 allows predicates of form
1204 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1205 | otherwise -- where a is a type variable
1206 = case tcSplitAppTy_maybe ty of
1207 Just (ty, _) -> tyvar_head ty
1214 is ambiguous if P contains generic variables
1215 (i.e. one of the Vs) that are not mentioned in tau
1217 However, we need to take account of functional dependencies
1218 when we speak of 'mentioned in tau'. Example:
1219 class C a b | a -> b where ...
1221 forall x y. (C x y) => x
1222 is not ambiguous because x is mentioned and x determines y
1224 NB; the ambiguity check is only used for *user* types, not for types
1225 coming from inteface files. The latter can legitimately have
1226 ambiguous types. Example
1228 class S a where s :: a -> (Int,Int)
1229 instance S Char where s _ = (1,1)
1230 f:: S a => [a] -> Int -> (Int,Int)
1231 f (_::[a]) x = (a*x,b)
1232 where (a,b) = s (undefined::a)
1234 Here the worker for f gets the type
1235 fw :: forall a. S a => Int -> (# Int, Int #)
1237 If the list of tv_names is empty, we have a monotype, and then we
1238 don't need to check for ambiguity either, because the test can't fail
1241 In addition, GHC insists that at least one type variable
1242 in each constraint is in V. So we disallow a type like
1243 forall a. Eq b => b -> b
1244 even in a scope where b is in scope.
1247 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1248 checkAmbiguity forall_tyvars theta tau_tyvars
1249 = mapM_ complain (filter is_ambig theta)
1251 complain pred = addErrTc (ambigErr pred)
1252 extended_tau_vars = growThetaTyVars theta tau_tyvars
1254 -- See Note [Implicit parameters and ambiguity] in TcSimplify
1255 is_ambig pred = isClassPred pred &&
1256 any ambig_var (varSetElems (tyVarsOfPred pred))
1258 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1259 not (ct_var `elemVarSet` extended_tau_vars)
1261 ambigErr :: PredType -> SDoc
1263 = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPredTy pred),
1264 nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1265 ptext (sLit "must be reachable from the type after the '=>'"))]
1268 Note [Growing the tau-tvs using constraints]
1269 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1270 (growInstsTyVars insts tvs) is the result of extending the set
1271 of tyvars tvs using all conceivable links from pred
1273 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1274 Then grow precs tvs = {a,b,c}
1277 growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
1278 -- See Note [Growing the tau-tvs using constraints]
1279 growThetaTyVars theta tvs
1281 | otherwise = fixVarSet mk_next tvs
1283 mk_next tvs = foldr grow_one tvs theta
1284 grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
1286 growPredTyVars :: TcPredType
1287 -> TyVarSet -- The set to extend
1288 -> TyVarSet -- TyVars of the predicate if it intersects
1289 -- the set, or is implicit parameter
1290 growPredTyVars pred tvs
1291 | IParam {} <- pred = pred_tvs -- See Note [Implicit parameters and ambiguity]
1292 | pred_tvs `intersectsVarSet` tvs = pred_tvs
1293 | otherwise = emptyVarSet
1295 pred_tvs = tyVarsOfPred pred
1298 Note [Implicit parameters and ambiguity]
1299 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1300 Only a *class* predicate can give rise to ambiguity
1301 An *implicit parameter* cannot. For example:
1302 foo :: (?x :: [a]) => Int
1304 is fine. The call site will suppply a particular 'x'
1306 Furthermore, the type variables fixed by an implicit parameter
1307 propagate to the others. E.g.
1308 foo :: (Show a, ?x::[a]) => Int
1310 The type of foo looks ambiguous. But it isn't, because at a call site
1312 let ?x = 5::Int in foo
1313 and all is well. In effect, implicit parameters are, well, parameters,
1314 so we can take their type variables into account as part of the
1315 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
1319 checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
1320 checkThetaCtxt ctxt theta
1321 = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1322 ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
1324 eqSuperClassErr :: PredType -> SDoc
1325 eqSuperClassErr pred
1326 = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:"))
1329 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
1330 badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPredTy pred
1331 eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPredTy pred
1333 parens (ptext (sLit "Use -XTypeFamilies to permit this"))
1334 predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
1335 nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)]
1336 dupPredWarn :: [[PredType]] -> SDoc
1337 dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPredTy (map head dups)
1339 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
1340 arityErr kind name n m
1341 = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1342 n_arguments <> comma, text "but has been given",
1343 if m==0 then text "none" else int m]
1345 n_arguments | n == 0 = ptext (sLit "no arguments")
1346 | n == 1 = ptext (sLit "1 argument")
1347 | True = hsep [int n, ptext (sLit "arguments")]
1350 %************************************************************************
1352 \subsection{Checking for a decent instance head type}
1354 %************************************************************************
1356 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1357 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1359 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1360 flag is on, or (2)~the instance is imported (they must have been
1361 compiled elsewhere). In these cases, we let them go through anyway.
1363 We can also have instances for functions: @instance Foo (a -> b) ...@.
1366 checkValidInstHead :: Class -> [Type] -> TcM ()
1367 checkValidInstHead clas tys
1368 = do { dflags <- getDOpts
1370 -- If GlasgowExts then check at least one isn't a type variable
1371 ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
1372 all tcInstHeadTyNotSynonym tys)
1373 (instTypeErr pp_pred head_type_synonym_msg)
1374 ; checkTc (xopt Opt_FlexibleInstances dflags ||
1375 all tcInstHeadTyAppAllTyVars tys)
1376 (instTypeErr pp_pred head_type_args_tyvars_msg)
1377 ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
1379 (instTypeErr pp_pred head_one_type_msg)
1380 -- May not contain type family applications
1381 ; mapM_ checkTyFamFreeness tys
1383 ; mapM_ checkValidMonoType tys
1384 -- For now, I only allow tau-types (not polytypes) in
1385 -- the head of an instance decl.
1386 -- E.g. instance C (forall a. a->a) is rejected
1387 -- One could imagine generalising that, but I'm not sure
1388 -- what all the consequences might be
1392 pp_pred = pprClassPred clas tys
1393 head_type_synonym_msg = parens (
1394 text "All instance types must be of the form (T t1 ... tn)" $$
1395 text "where T is not a synonym." $$
1396 text "Use -XTypeSynonymInstances if you want to disable this.")
1398 head_type_args_tyvars_msg = parens (vcat [
1399 text "All instance types must be of the form (T a1 ... an)",
1400 text "where a1 ... an are *distinct type variables*,",
1401 text "and each type variable appears at most once in the instance head.",
1402 text "Use -XFlexibleInstances if you want to disable this."])
1404 head_one_type_msg = parens (
1405 text "Only one type can be given in an instance head." $$
1406 text "Use -XMultiParamTypeClasses if you want to allow more.")
1408 instTypeErr :: SDoc -> SDoc -> SDoc
1409 instTypeErr pp_ty msg
1410 = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty,
1415 %************************************************************************
1417 \subsection{Checking instance for termination}
1419 %************************************************************************
1422 checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType
1423 -> Class -> [TcType] -> TcM ()
1424 checkValidInstance hs_type tyvars theta clas inst_tys
1425 = setSrcSpan (getLoc hs_type) $
1426 do { setSrcSpan head_loc (checkValidInstHead clas inst_tys)
1427 ; checkValidTheta InstThetaCtxt theta
1428 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1430 -- Check that instance inference will terminate (if we care)
1431 -- For Haskell 98 this will already have been done by checkValidTheta,
1432 -- but as we may be using other extensions we need to check.
1433 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1434 ; unless undecidable_ok $
1435 mapM_ addErrTc (checkInstTermination inst_tys theta)
1437 -- The Coverage Condition
1438 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1439 (instTypeErr (pprClassPred clas inst_tys) msg)
1442 msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1445 -- The location of the "head" of the instance
1446 head_loc = case hs_type of
1447 L _ (HsForAllTy _ _ _ (L loc _)) -> loc
1451 Termination test: the so-called "Paterson conditions" (see Section 5 of
1452 "Understanding functionsl dependencies via Constraint Handling Rules,
1455 We check that each assertion in the context satisfies:
1456 (1) no variable has more occurrences in the assertion than in the head, and
1457 (2) the assertion has fewer constructors and variables (taken together
1458 and counting repetitions) than the head.
1459 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1460 (which have already been checked) guarantee termination.
1462 The underlying idea is that
1464 for any ground substitution, each assertion in the
1465 context has fewer type constructors than the head.
1469 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1470 checkInstTermination tys theta
1471 = mapCatMaybes check theta
1474 size = sizeTypes tys
1476 | not (null (fvPred pred \\ fvs))
1477 = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1478 | sizePred pred >= size
1479 = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1483 predUndecErr :: PredType -> SDoc -> SDoc
1484 predUndecErr pred msg = sep [msg,
1485 nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)]
1487 nomoreMsg, smallerMsg, undecidableMsg :: SDoc
1488 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1489 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1490 undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
1493 validDeivPred checks for OK 'deriving' context. See Note [Exotic
1494 derived instance contexts] in TcSimplify. However the predicate is
1495 here because it uses sizeTypes, fvTypes.
1498 validDerivPred :: PredType -> Bool
1499 validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
1500 where fvs = fvTypes tys
1501 validDerivPred _ = False
1505 %************************************************************************
1507 Checking type instance well-formedness and termination
1509 %************************************************************************
1512 -- Check that a "type instance" is well-formed (which includes decidability
1513 -- unless -XUndecidableInstances is given).
1515 checkValidTypeInst :: [Type] -> Type -> TcM ()
1516 checkValidTypeInst typats rhs
1517 = do { -- left-hand side contains no type family applications
1518 -- (vanilla synonyms are fine, though)
1519 ; mapM_ checkTyFamFreeness typats
1521 -- the right-hand side is a tau type
1522 ; checkValidMonoType rhs
1524 -- we have a decidable instance unless otherwise permitted
1525 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1526 ; unless undecidable_ok $
1527 mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1530 -- Make sure that each type family instance is
1531 -- (1) strictly smaller than the lhs,
1532 -- (2) mentions no type variable more often than the lhs, and
1533 -- (3) does not contain any further type family instances.
1535 checkFamInst :: [Type] -- lhs
1536 -> [(TyCon, [Type])] -- type family instances
1538 checkFamInst lhsTys famInsts
1539 = mapCatMaybes check famInsts
1541 size = sizeTypes lhsTys
1542 fvs = fvTypes lhsTys
1544 | not (all isTyFamFree tys)
1545 = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1546 | not (null (fvTypes tys \\ fvs))
1547 = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1548 | size <= sizeTypes tys
1549 = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1553 famInst = TyConApp tc tys
1555 -- Ensure that no type family instances occur in a type.
1557 checkTyFamFreeness :: Type -> TcM ()
1558 checkTyFamFreeness ty
1559 = checkTc (isTyFamFree ty) $
1560 tyFamInstIllegalErr ty
1562 -- Check that a type does not contain any type family applications.
1564 isTyFamFree :: Type -> Bool
1565 isTyFamFree = null . tyFamInsts
1569 tyFamInstIllegalErr :: Type -> SDoc
1570 tyFamInstIllegalErr ty
1571 = hang (ptext (sLit "Illegal type synonym family application in instance") <>
1575 famInstUndecErr :: Type -> SDoc -> SDoc
1576 famInstUndecErr ty msg
1578 nest 2 (ptext (sLit "in the type family application:") <+>
1581 nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
1582 nestedMsg = ptext (sLit "Nested type family application")
1583 nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head")
1584 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1588 %************************************************************************
1590 \subsection{Auxiliary functions}
1592 %************************************************************************
1595 -- Free variables of a type, retaining repetitions, and expanding synonyms
1596 fvType :: Type -> [TyVar]
1597 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1598 fvType (TyVarTy tv) = [tv]
1599 fvType (TyConApp _ tys) = fvTypes tys
1600 fvType (PredTy pred) = fvPred pred
1601 fvType (FunTy arg res) = fvType arg ++ fvType res
1602 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1603 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1605 fvTypes :: [Type] -> [TyVar]
1606 fvTypes tys = concat (map fvType tys)
1608 fvPred :: PredType -> [TyVar]
1609 fvPred (ClassP _ tys') = fvTypes tys'
1610 fvPred (IParam _ ty) = fvType ty
1611 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1613 -- Size of a type: the number of variables and constructors
1614 sizeType :: Type -> Int
1615 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1616 sizeType (TyVarTy _) = 1
1617 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1618 sizeType (PredTy pred) = sizePred pred
1619 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1620 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1621 sizeType (ForAllTy _ ty) = sizeType ty
1623 sizeTypes :: [Type] -> Int
1624 sizeTypes xs = sum (map sizeType xs)
1626 -- Size of a predicate
1628 -- We are considering whether *class* constraints terminate
1629 -- Once we get into an implicit parameter or equality we
1630 -- can't get back to a class constraint, so it's safe
1631 -- to say "size 0". See Trac #4200.
1632 sizePred :: PredType -> Int
1633 sizePred (ClassP _ tys') = sizeTypes tys'
1634 sizePred (IParam {}) = 0
1635 sizePred (EqPred {}) = 0